k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.468482
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₂p₃ : p₂ ≠ p₃
hp₁ : ¬p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
⊢ AffineIndependent k (![p₁, p₂, p₃] ∘ ↑(Equiv.swap 0 2))
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.468482
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₂p₃ : p₂ ≠ p₃
hp₁ : ¬p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
⊢ AffineIndependent k ![p₁, p₂, p₃]
rw [← affineIndependent_equiv (Equiv.swap (0 : Fin 3) 2)]
case h.e'_9
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.468482
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₂p₃ : p₂ ≠ p₃
hp₁ : ¬p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
⊢ ![p₁, p₂, p₃] ∘ ↑(Equiv.swap 0 2) = ![p₃, p₂, p₁]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.468482
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₂p₃ : p₂ ≠ p₃
hp₁ : ¬p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
⊢ AffineIndependent k (![p₁, p₂, p₃] ∘ ↑(Equiv.swap 0 2))
convert affineIndependent_of_ne_of_mem_of_mem_of_not_mem hp₂p₃.symm hp₃ hp₂ hp₁ using 1
case h.e'_9.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.468482
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₂p₃ : p₂ ≠ p₃
hp₁ : ¬p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
x : Fin 3
⊢ (![p₁, p₂, p₃] ∘ ↑(Equiv.swap 0 2)) x = Matrix.vecCons p₃ ![p₂, p₁] x
case h.e'_9
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.468482
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₂p₃ : p₂ ≠ p₃
hp₁ : ¬p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
⊢ ![p₁, p₂, p₃] ∘ ↑(Equiv.swap 0 2) = ![p₃, p₂, p₁]
ext x
no goals
case h.e'_9.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.468482
s : AffineSubspace k P
p₁ p₂ p₃ : P
hp₂p₃ : p₂ ≠ p₃
hp₁ : ¬p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
x : Fin 3
⊢ (![p₁, p₂, p₃] ∘ ↑(Equiv.swap 0 2)) x = Matrix.vecCons p₃ ![p₂, p₁] x
fin_cases x <;> rfl