[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : DecidableEq ι
⊢ toMatrix b ↑b = 1
[PROOFSTEP]
ext i j
[GOAL]
case a.h
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
inst✝ : DecidableEq ι
i j : ι
⊢ toMatrix b (↑b) i j = OfNat.ofNat 1 i j
[PROOFSTEP]
rw [toMatrix_apply, coord_apply, Matrix.one_eq_pi_single, Pi.single_apply]
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : Ring k
inst✝² : Module k V
b : AffineBasis ι k P
ι'✝ : Type u_1
inst✝¹ : Fintype ι'✝
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
ι' : Type u_2
q : ι' → P
i : ι'
⊢ ∑ j : ι, toMatrix b q i j = 1
[PROOFSTEP]
simp
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁶ : AddCommGroup V
inst✝⁵ : AffineSpace V P
inst✝⁴ : Ring k
inst✝³ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : toMatrix b p * A = 1
⊢ AffineIndependent k p
[PROOFSTEP]
rw [affineIndependent_iff_eq_of_fintype_affineCombination_eq]
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁶ : AddCommGroup V
inst✝⁵ : AffineSpace V P
inst✝⁴ : Ring k
inst✝³ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : toMatrix b p * A = 1
⊢ ∀ (w1 w2 : ι' → k),
    ∑ i : ι', w1 i = 1 →
      ∑ i : ι', w2 i = 1 →
        ↑(Finset.affineCombination k Finset.univ p) w1 = ↑(Finset.affineCombination k Finset.univ p) w2 → w1 = w2
[PROOFSTEP]
intro w₁ w₂ hw₁ hw₂ hweq
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁶ : AddCommGroup V
inst✝⁵ : AffineSpace V P
inst✝⁴ : Ring k
inst✝³ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : toMatrix b p * A = 1
w₁ w₂ : ι' → k
hw₁ : ∑ i : ι', w₁ i = 1
hw₂ : ∑ i : ι', w₂ i = 1
hweq : ↑(Finset.affineCombination k Finset.univ p) w₁ = ↑(Finset.affineCombination k Finset.univ p) w₂
⊢ w₁ = w₂
[PROOFSTEP]
have hweq' : (b.toMatrix p).vecMul w₁ = (b.toMatrix p).vecMul w₂ :=
  by
  ext j
  change
    (∑ i, w₁ i • b.coord j (p i)) =
      ∑ i,
        w₂ i •
          b.coord j
            (p i)
              -- Porting note: Added `u` because `∘` was causing trouble
  have u : (fun i => b.coord j (p i)) = b.coord j ∘ p := by simp only [(· ∘ ·)]
  rw [← Finset.univ.affineCombination_eq_linear_combination _ _ hw₁, ←
    Finset.univ.affineCombination_eq_linear_combination _ _ hw₂, u, ← Finset.univ.map_affineCombination p w₁ hw₁, ←
    Finset.univ.map_affineCombination p w₂ hw₂, hweq]
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁶ : AddCommGroup V
inst✝⁵ : AffineSpace V P
inst✝⁴ : Ring k
inst✝³ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : toMatrix b p * A = 1
w₁ w₂ : ι' → k
hw₁ : ∑ i : ι', w₁ i = 1
hw₂ : ∑ i : ι', w₂ i = 1
hweq : ↑(Finset.affineCombination k Finset.univ p) w₁ = ↑(Finset.affineCombination k Finset.univ p) w₂
⊢ vecMul w₁ (toMatrix b p) = vecMul w₂ (toMatrix b p)
[PROOFSTEP]
ext j
[GOAL]
case h
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁶ : AddCommGroup V
inst✝⁵ : AffineSpace V P
inst✝⁴ : Ring k
inst✝³ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : toMatrix b p * A = 1
w₁ w₂ : ι' → k
hw₁ : ∑ i : ι', w₁ i = 1
hw₂ : ∑ i : ι', w₂ i = 1
hweq : ↑(Finset.affineCombination k Finset.univ p) w₁ = ↑(Finset.affineCombination k Finset.univ p) w₂
j : ι
⊢ vecMul w₁ (toMatrix b p) j = vecMul w₂ (toMatrix b p) j
[PROOFSTEP]
change
  (∑ i, w₁ i • b.coord j (p i)) =
    ∑ i,
      w₂ i •
        b.coord j
          (p i)
            -- Porting note: Added `u` because `∘` was causing trouble
[GOAL]
case h
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁶ : AddCommGroup V
inst✝⁵ : AffineSpace V P
inst✝⁴ : Ring k
inst✝³ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : toMatrix b p * A = 1
w₁ w₂ : ι' → k
hw₁ : ∑ i : ι', w₁ i = 1
hw₂ : ∑ i : ι', w₂ i = 1
hweq : ↑(Finset.affineCombination k Finset.univ p) w₁ = ↑(Finset.affineCombination k Finset.univ p) w₂
j : ι
⊢ ∑ i : ι', w₁ i • ↑(coord b j) (p i) = ∑ i : ι', w₂ i • ↑(coord b j) (p i)
[PROOFSTEP]
have u : (fun i => b.coord j (p i)) = b.coord j ∘ p := by simp only [(· ∘ ·)]
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁶ : AddCommGroup V
inst✝⁵ : AffineSpace V P
inst✝⁴ : Ring k
inst✝³ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : toMatrix b p * A = 1
w₁ w₂ : ι' → k
hw₁ : ∑ i : ι', w₁ i = 1
hw₂ : ∑ i : ι', w₂ i = 1
hweq : ↑(Finset.affineCombination k Finset.univ p) w₁ = ↑(Finset.affineCombination k Finset.univ p) w₂
j : ι
⊢ (fun i => ↑(coord b j) (p i)) = ↑(coord b j) ∘ p
[PROOFSTEP]
simp only [(· ∘ ·)]
[GOAL]
case h
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁶ : AddCommGroup V
inst✝⁵ : AffineSpace V P
inst✝⁴ : Ring k
inst✝³ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : toMatrix b p * A = 1
w₁ w₂ : ι' → k
hw₁ : ∑ i : ι', w₁ i = 1
hw₂ : ∑ i : ι', w₂ i = 1
hweq : ↑(Finset.affineCombination k Finset.univ p) w₁ = ↑(Finset.affineCombination k Finset.univ p) w₂
j : ι
u : (fun i => ↑(coord b j) (p i)) = ↑(coord b j) ∘ p
⊢ ∑ i : ι', w₁ i • ↑(coord b j) (p i) = ∑ i : ι', w₂ i • ↑(coord b j) (p i)
[PROOFSTEP]
rw [← Finset.univ.affineCombination_eq_linear_combination _ _ hw₁, ←
  Finset.univ.affineCombination_eq_linear_combination _ _ hw₂, u, ← Finset.univ.map_affineCombination p w₁ hw₁, ←
  Finset.univ.map_affineCombination p w₂ hw₂, hweq]
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁶ : AddCommGroup V
inst✝⁵ : AffineSpace V P
inst✝⁴ : Ring k
inst✝³ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : toMatrix b p * A = 1
w₁ w₂ : ι' → k
hw₁ : ∑ i : ι', w₁ i = 1
hw₂ : ∑ i : ι', w₂ i = 1
hweq : ↑(Finset.affineCombination k Finset.univ p) w₁ = ↑(Finset.affineCombination k Finset.univ p) w₂
hweq' : vecMul w₁ (toMatrix b p) = vecMul w₂ (toMatrix b p)
⊢ w₁ = w₂
[PROOFSTEP]
replace hweq' := congr_arg (fun w => A.vecMul w) hweq'
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁶ : AddCommGroup V
inst✝⁵ : AffineSpace V P
inst✝⁴ : Ring k
inst✝³ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι'
p : ι' → P
A : Matrix ι ι' k
hA : toMatrix b p * A = 1
w₁ w₂ : ι' → k
hw₁ : ∑ i : ι', w₁ i = 1
hw₂ : ∑ i : ι', w₂ i = 1
hweq : ↑(Finset.affineCombination k Finset.univ p) w₁ = ↑(Finset.affineCombination k Finset.univ p) w₂
hweq' : (fun w => vecMul w A) (vecMul w₁ (toMatrix b p)) = (fun w => vecMul w A) (vecMul w₂ (toMatrix b p))
⊢ w₁ = w₂
[PROOFSTEP]
simpa only [Matrix.vecMul_vecMul, hA, Matrix.vecMul_one] using hweq'
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * toMatrix b p = 1
⊢ affineSpan k (range p) = ⊤
[PROOFSTEP]
suffices ∀ i, b i ∈ affineSpan k (range p)
  by
  rw [eq_top_iff, ← b.tot, affineSpan_le]
  rintro q ⟨i, rfl⟩
  exact this i
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * toMatrix b p = 1
this : ∀ (i : ι), ↑b i ∈ affineSpan k (range p)
⊢ affineSpan k (range p) = ⊤
[PROOFSTEP]
rw [eq_top_iff, ← b.tot, affineSpan_le]
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * toMatrix b p = 1
this : ∀ (i : ι), ↑b i ∈ affineSpan k (range p)
⊢ range ↑b ⊆ ↑(affineSpan k (range p))
[PROOFSTEP]
rintro q ⟨i, rfl⟩
[GOAL]
case intro
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * toMatrix b p = 1
this : ∀ (i : ι), ↑b i ∈ affineSpan k (range p)
i : ι
⊢ ↑b i ∈ ↑(affineSpan k (range p))
[PROOFSTEP]
exact this i
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * toMatrix b p = 1
⊢ ∀ (i : ι), ↑b i ∈ affineSpan k (range p)
[PROOFSTEP]
intro i
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * toMatrix b p = 1
i : ι
⊢ ↑b i ∈ affineSpan k (range p)
[PROOFSTEP]
have hAi : ∑ j, A i j = 1 := by
  calc
    ∑ j, A i j = ∑ j, A i j * ∑ l, b.toMatrix p j l := by simp
    _ = ∑ j, ∑ l, A i j * b.toMatrix p j l := by simp_rw [Finset.mul_sum]
    _ = ∑ l, ∑ j, A i j * b.toMatrix p j l := by rw [Finset.sum_comm]
    _ = ∑ l, (A * b.toMatrix p) i l := rfl
    _ = 1 := by simp [hA, Matrix.one_apply, Finset.filter_eq]
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * toMatrix b p = 1
i : ι
⊢ ∑ j : ι', A i j = 1
[PROOFSTEP]
calc
  ∑ j, A i j = ∑ j, A i j * ∑ l, b.toMatrix p j l := by simp
  _ = ∑ j, ∑ l, A i j * b.toMatrix p j l := by simp_rw [Finset.mul_sum]
  _ = ∑ l, ∑ j, A i j * b.toMatrix p j l := by rw [Finset.sum_comm]
  _ = ∑ l, (A * b.toMatrix p) i l := rfl
  _ = 1 := by simp [hA, Matrix.one_apply, Finset.filter_eq]
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * toMatrix b p = 1
i : ι
⊢ ∑ j : ι', A i j = ∑ j : ι', A i j * ∑ l : ι, toMatrix b p j l
[PROOFSTEP]
simp
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * toMatrix b p = 1
i : ι
⊢ ∑ j : ι', A i j * ∑ l : ι, toMatrix b p j l = ∑ j : ι', ∑ l : ι, A i j * toMatrix b p j l
[PROOFSTEP]
simp_rw [Finset.mul_sum]
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * toMatrix b p = 1
i : ι
⊢ ∑ j : ι', ∑ l : ι, A i j * toMatrix b p j l = ∑ l : ι, ∑ j : ι', A i j * toMatrix b p j l
[PROOFSTEP]
rw [Finset.sum_comm]
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * toMatrix b p = 1
i : ι
⊢ ∑ l : ι, (A * toMatrix b p) i l = 1
[PROOFSTEP]
simp [hA, Matrix.one_apply, Finset.filter_eq]
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * toMatrix b p = 1
i : ι
hAi : ∑ j : ι', A i j = 1
⊢ ↑b i ∈ affineSpan k (range p)
[PROOFSTEP]
have hbi : b i = Finset.univ.affineCombination k p (A i) :=
  by
  apply b.ext_elem
  intro j
  rw [b.coord_apply, Finset.univ.map_affineCombination _ _ hAi,
    Finset.univ.affineCombination_eq_linear_combination _ _ hAi]
  change _ = (A * b.toMatrix p) i j
  simp_rw [hA, Matrix.one_apply, @eq_comm _ i j]
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * toMatrix b p = 1
i : ι
hAi : ∑ j : ι', A i j = 1
⊢ ↑b i = ↑(Finset.affineCombination k Finset.univ p) (A i)
[PROOFSTEP]
apply b.ext_elem
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * toMatrix b p = 1
i : ι
hAi : ∑ j : ι', A i j = 1
⊢ ∀ (i_1 : ι), ↑(coord b i_1) (↑b i) = ↑(coord b i_1) (↑(Finset.affineCombination k Finset.univ p) (A i))
[PROOFSTEP]
intro j
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * toMatrix b p = 1
i : ι
hAi : ∑ j : ι', A i j = 1
j : ι
⊢ ↑(coord b j) (↑b i) = ↑(coord b j) (↑(Finset.affineCombination k Finset.univ p) (A i))
[PROOFSTEP]
rw [b.coord_apply, Finset.univ.map_affineCombination _ _ hAi,
  Finset.univ.affineCombination_eq_linear_combination _ _ hAi]
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * toMatrix b p = 1
i : ι
hAi : ∑ j : ι', A i j = 1
j : ι
⊢ (if j = i then 1 else 0) = ∑ i_1 : ι', A i i_1 • (↑(coord b j) ∘ p) i_1
[PROOFSTEP]
change _ = (A * b.toMatrix p) i j
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * toMatrix b p = 1
i : ι
hAi : ∑ j : ι', A i j = 1
j : ι
⊢ (if j = i then 1 else 0) = (A * toMatrix b p) i j
[PROOFSTEP]
simp_rw [hA, Matrix.one_apply, @eq_comm _ i j]
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * toMatrix b p = 1
i : ι
hAi : ∑ j : ι', A i j = 1
hbi : ↑b i = ↑(Finset.affineCombination k Finset.univ p) (A i)
⊢ ↑b i ∈ affineSpan k (range p)
[PROOFSTEP]
rw [hbi]
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * toMatrix b p = 1
i : ι
hAi : ∑ j : ι', A i j = 1
hbi : ↑b i = ↑(Finset.affineCombination k Finset.univ p) (A i)
⊢ ↑(Finset.affineCombination k Finset.univ p) (A i) ∈ affineSpan k (range p)
[PROOFSTEP]
exact affineCombination_mem_affineSpan hAi p
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : Ring k
inst✝² : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝¹ : Fintype ι'
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
⊢ vecMul (↑(coords b₂) x) (toMatrix b ↑b₂) = ↑(coords b) x
[PROOFSTEP]
ext j
[GOAL]
case h
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : Ring k
inst✝² : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝¹ : Fintype ι'
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ vecMul (↑(coords b₂) x) (toMatrix b ↑b₂) j = ↑(coords b) x j
[PROOFSTEP]
change _ = b.coord j x
[GOAL]
case h
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : Ring k
inst✝² : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝¹ : Fintype ι'
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ vecMul (↑(coords b₂) x) (toMatrix b ↑b₂) j = ↑(coord b j) x
[PROOFSTEP]
conv_rhs => rw [← b₂.affineCombination_coord_eq_self x]
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : Ring k
inst✝² : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝¹ : Fintype ι'
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
| ↑(coord b j) x
[PROOFSTEP]
rw [← b₂.affineCombination_coord_eq_self x]
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : Ring k
inst✝² : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝¹ : Fintype ι'
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
| ↑(coord b j) x
[PROOFSTEP]
rw [← b₂.affineCombination_coord_eq_self x]
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : Ring k
inst✝² : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝¹ : Fintype ι'
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
| ↑(coord b j) x
[PROOFSTEP]
rw [← b₂.affineCombination_coord_eq_self x]
[GOAL]
case h
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : Ring k
inst✝² : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝¹ : Fintype ι'
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ vecMul (↑(coords b₂) x) (toMatrix b ↑b₂) j =
    ↑(coord b j) (↑(Finset.affineCombination k Finset.univ ↑b₂) fun i => ↑(coord b₂ i) x)
[PROOFSTEP]
rw [Finset.map_affineCombination _ _ _ (b₂.sum_coord_apply_eq_one x)]
[GOAL]
case h
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : Ring k
inst✝² : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝¹ : Fintype ι'
inst✝ : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ vecMul (↑(coords b₂) x) (toMatrix b ↑b₂) j =
    ↑(Finset.affineCombination ((fun a => k) x) Finset.univ (↑(coord b j) ∘ ↑b₂)) fun i => ↑(coord b₂ i) x
[PROOFSTEP]
simp [Matrix.vecMul, Matrix.dotProduct, toMatrix_apply, coords]
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁶ : AddCommGroup V
inst✝⁵ : AffineSpace V P
inst✝⁴ : Ring k
inst✝³ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι
⊢ toMatrix b ↑b₂ * toMatrix b₂ ↑b = 1
[PROOFSTEP]
ext l m
[GOAL]
case a.h
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁶ : AddCommGroup V
inst✝⁵ : AffineSpace V P
inst✝⁴ : Ring k
inst✝³ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι
l m : ι
⊢ (toMatrix b ↑b₂ * toMatrix b₂ ↑b) l m = OfNat.ofNat 1 l m
[PROOFSTEP]
change (b₂.toMatrix b).vecMul (b.coords (b₂ l)) m = _
[GOAL]
case a.h
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁶ : AddCommGroup V
inst✝⁵ : AffineSpace V P
inst✝⁴ : Ring k
inst✝³ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι
l m : ι
⊢ vecMul (↑(coords b) (↑b₂ l)) (toMatrix b₂ ↑b) m = OfNat.ofNat 1 l m
[PROOFSTEP]
rw [toMatrix_vecMul_coords, coords_apply, ← toMatrix_apply, toMatrix_self]
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι → P
⊢ IsUnit (toMatrix b p) ↔ AffineIndependent k p ∧ affineSpan k (range p) = ⊤
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι → P
⊢ IsUnit (toMatrix b p) → AffineIndependent k p ∧ affineSpan k (range p) = ⊤
[PROOFSTEP]
rintro ⟨⟨B, A, hA, hA'⟩, rfl : B = b.toMatrix p⟩
[GOAL]
case mp.intro.mk
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι → P
A : Matrix ι ι k
hA : toMatrix b p * A = 1
hA' : A * toMatrix b p = 1
⊢ AffineIndependent k p ∧ affineSpan k (range p) = ⊤
[PROOFSTEP]
exact ⟨b.affineIndependent_of_toMatrix_right_inv p hA, b.affineSpan_eq_top_of_toMatrix_left_inv p hA'⟩
[GOAL]
case mpr
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι → P
⊢ AffineIndependent k p ∧ affineSpan k (range p) = ⊤ → IsUnit (toMatrix b p)
[PROOFSTEP]
rintro ⟨h_tot, h_ind⟩
[GOAL]
case mpr.intro
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι → P
h_tot : AffineIndependent k p
h_ind : affineSpan k (range p) = ⊤
⊢ IsUnit (toMatrix b p)
[PROOFSTEP]
let b' : AffineBasis ι k P := ⟨p, h_tot, h_ind⟩
[GOAL]
case mpr.intro
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι → P
h_tot : AffineIndependent k p
h_ind : affineSpan k (range p) = ⊤
b' : AffineBasis ι k P := { toFun := p, ind' := h_tot, tot' := h_ind }
⊢ IsUnit (toMatrix b p)
[PROOFSTEP]
change IsUnit (b.toMatrix b')
[GOAL]
case mpr.intro
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁷ : AddCommGroup V
inst✝⁶ : AffineSpace V P
inst✝⁵ : Ring k
inst✝⁴ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝³ : Fintype ι'
inst✝² : Fintype ι
b₂ : AffineBasis ι k P
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial k
p : ι → P
h_tot : AffineIndependent k p
h_ind : affineSpan k (range p) = ⊤
b' : AffineBasis ι k P := { toFun := p, ind' := h_tot, tot' := h_ind }
⊢ IsUnit (toMatrix b ↑b')
[PROOFSTEP]
exact b.isUnit_toMatrix b'
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
⊢ vecMul (↑(coords b) x) (toMatrix b ↑b₂)⁻¹ = ↑(coords b₂) x
[PROOFSTEP]
have hu := b.isUnit_toMatrix b₂
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (toMatrix b ↑b₂)
⊢ vecMul (↑(coords b) x) (toMatrix b ↑b₂)⁻¹ = ↑(coords b₂) x
[PROOFSTEP]
rw [Matrix.isUnit_iff_isUnit_det] at hu
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (det (toMatrix b ↑b₂))
⊢ vecMul (↑(coords b) x) (toMatrix b ↑b₂)⁻¹ = ↑(coords b₂) x
[PROOFSTEP]
rw [← b.toMatrix_vecMul_coords b₂, Matrix.vecMul_vecMul, Matrix.mul_nonsing_inv _ hu, Matrix.vecMul_one]
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
⊢ det (toMatrix b ↑b₂) • ↑(coords b₂) x = ↑(cramer (toMatrix b ↑b₂)ᵀ) (↑(coords b) x)
[PROOFSTEP]
have hu := b.isUnit_toMatrix b₂
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (toMatrix b ↑b₂)
⊢ det (toMatrix b ↑b₂) • ↑(coords b₂) x = ↑(cramer (toMatrix b ↑b₂)ᵀ) (↑(coords b) x)
[PROOFSTEP]
rw [Matrix.isUnit_iff_isUnit_det] at hu
[GOAL]
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : CommRing k
inst✝² : Module k V
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (det (toMatrix b ↑b₂))
⊢ det (toMatrix b ↑b₂) • ↑(coords b₂) x = ↑(cramer (toMatrix b ↑b₂)ᵀ) (↑(coords b) x)
[PROOFSTEP]
rw [← b.toMatrix_inv_vecMul_toMatrix, Matrix.det_smul_inv_vecMul_eq_cramer_transpose _ _ hu]