R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
⊢ LinearIndependent R fun ji => ↑(stdBasis R Ms ji.fst) (v ji.fst ji.snd)
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
⊢ LinearIndependent R fun ji => ↑(stdBasis R Ms ji.fst) (v ji.fst ji.snd)
have hs' : ∀ j : η, LinearIndependent R fun i : ιs j => stdBasis R Ms j (v j i) := by
  intro j
  exact (hs j).map' _ (ker_stdBasis _ _ _)
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
⊢ ∀ (i : η) (t : Set η),
    Set.Finite t →
      ¬i ∈ t →
        Disjoint (span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
          (⨆ (i : η) (_ : i ∈ t), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
⊢ LinearIndependent R fun ji => ↑(stdBasis R Ms ji.fst) (v ji.fst ji.snd)
apply linearIndependent_iUnion_finite hs'
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
j : η
⊢ LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
⊢ ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
intro j
no goals
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
j : η
⊢ LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
exact (hs j).map' _ (ker_stdBasis _ _ _)
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
⊢ ∀ (i : η) (t : Set η),
    Set.Finite t →
      ¬i ∈ t →
        Disjoint (span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
          (⨆ (i : η) (_ : i ∈ t), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
intro j J _ hiJ
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
simp only
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
have h₀ :
  ∀ j, span R (range fun i : ιs j => stdBasis R Ms j (v j i)) ≤
    LinearMap.range (stdBasis R Ms j) := by
  intro j
  rw [span_le, LinearMap.range_coe]
  apply range_comp_subset_range
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
h₁ : span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ ⨆ (i : η) (_ : i ∈ {j}), LinearMap.range (stdBasis R Ms i)
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
have h₁ :
  span R (range fun i : ιs j => stdBasis R Ms j (v j i)) ≤
    ⨆ i ∈ ({j} : Set _), LinearMap.range (stdBasis R Ms i) := by
  rw [@iSup_singleton _ _ _ fun i => LinearMap.range (stdBasis R (Ms) i)]
  apply h₀
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
h₁ : span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ ⨆ (i : η) (_ : i ∈ {j}), LinearMap.range (stdBasis R Ms i)
h₂ :
  (⨆ (j : η) (_ : j ∈ J), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i))) ≤
    ⨆ (j : η) (_ : j ∈ J), LinearMap.range (stdBasis R (fun j => Ms j) j)
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
h₁ : span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ ⨆ (i : η) (_ : i ∈ {j}), LinearMap.range (stdBasis R Ms i)
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
have h₂ :
  (⨆ j ∈ J, span R (range fun i : ιs j => stdBasis R Ms j (v j i))) ≤
    ⨆ j ∈ J, LinearMap.range (stdBasis R (fun j : η => Ms j) j) :=
  iSup₂_mono fun i _ => h₀ i
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
h₁ : span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ ⨆ (i : η) (_ : i ∈ {j}), LinearMap.range (stdBasis R Ms i)
h₂ :
  (⨆ (j : η) (_ : j ∈ J), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i))) ≤
    ⨆ (j : η) (_ : j ∈ J), LinearMap.range (stdBasis R (fun j => Ms j) j)
h₃ : Disjoint (fun i => i ∈ {j}) J
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
h₁ : span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ ⨆ (i : η) (_ : i ∈ {j}), LinearMap.range (stdBasis R Ms i)
h₂ :
  (⨆ (j : η) (_ : j ∈ J), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i))) ≤
    ⨆ (j : η) (_ : j ∈ J), LinearMap.range (stdBasis R (fun j => Ms j) j)
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
have h₃ : Disjoint (fun i : η => i ∈ ({j} : Set _)) J := by
  convert Set.disjoint_singleton_left.2 hiJ using 0
no goals
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
h₁ : span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ ⨆ (i : η) (_ : i ∈ {j}), LinearMap.range (stdBasis R Ms i)
h₂ :
  (⨆ (j : η) (_ : j ∈ J), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i))) ≤
    ⨆ (j : η) (_ : j ∈ J), LinearMap.range (stdBasis R (fun j => Ms j) j)
h₃ : Disjoint (fun i => i ∈ {j}) J
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
exact (disjoint_stdBasis_stdBasis _ _ _ _ h₃).mono h₁ h₂
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j✝ : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j✝ ∈ J
j : η
⊢ span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
⊢ ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
intro j
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j✝ : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j✝ ∈ J
j : η
⊢ (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ⊆ Set.range ↑(stdBasis R Ms j)
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j✝ : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j✝ ∈ J
j : η
⊢ span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
rw [span_le, LinearMap.range_coe]
no goals
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j✝ : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j✝ ∈ J
j : η
⊢ (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ⊆ Set.range ↑(stdBasis R Ms j)
apply range_comp_subset_range
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
⊢ span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
⊢ span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ ⨆ (i : η) (_ : i ∈ {j}), LinearMap.range (stdBasis R Ms i)
rw [@iSup_singleton _ _ _ fun i => LinearMap.range (stdBasis R (Ms) i)]
no goals
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
⊢ span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
apply h₀
no goals
R : Type u_1
η : Type u_3
ιs : η → Type u_4
Ms : η → Type u_2
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
h₁ : span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ ⨆ (i : η) (_ : i ∈ {j}), LinearMap.range (stdBasis R Ms i)
h₂ :
  (⨆ (j : η) (_ : j ∈ J), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i))) ≤
    ⨆ (j : η) (_ : j ∈ J), LinearMap.range (stdBasis R (fun j => Ms j) j)
⊢ Disjoint (fun i => i ∈ {j}) J
convert Set.disjoint_singleton_left.2 hiJ using 0