Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dimkerim Structured version   Visualization version   GIF version

Theorem dimkerim 33157
Description: Given a linear map 𝐹 between vector spaces 𝑉 and 𝑈, the dimension of the vector space 𝑉 is the sum of the dimension of 𝐹 's kernel and the dimension of 𝐹's image. Second part of theorem 5.3 in [Lang] p. 141 This can also be described as the Rank-nullity theorem, (dim‘𝐼) being the rank of 𝐹 (the dimension of its image), and (dim‘𝐾) its nullity (the dimension of its kernel). (Contributed by Thierry Arnoux, 17-May-2023.)
Hypotheses
Ref Expression
dimkerim.0 0 = (0g𝑈)
dimkerim.k 𝐾 = (𝑉s (𝐹 “ { 0 }))
dimkerim.i 𝐼 = (𝑈s ran 𝐹)
Assertion
Ref Expression
dimkerim ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼)))

Proof of Theorem dimkerim
Dummy variables 𝑏 𝑢 𝑣 𝑤 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dimkerim.0 . . . . 5 0 = (0g𝑈)
2 dimkerim.k . . . . 5 𝐾 = (𝑉s (𝐹 “ { 0 }))
31, 2kerlmhm 33150 . . . 4 ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝐾 ∈ LVec)
4 eqid 2724 . . . . 5 (LBasis‘𝐾) = (LBasis‘𝐾)
54lbsex 21005 . . . 4 (𝐾 ∈ LVec → (LBasis‘𝐾) ≠ ∅)
63, 5syl 17 . . 3 ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → (LBasis‘𝐾) ≠ ∅)
7 n0 4338 . . 3 ((LBasis‘𝐾) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ (LBasis‘𝐾))
86, 7sylib 217 . 2 ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → ∃𝑤 𝑤 ∈ (LBasis‘𝐾))
9 simpllr 773 . . . . 5 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑤 ∈ (LBasis‘𝐾))
10 vex 3470 . . . . . . 7 𝑏 ∈ V
1110difexi 5318 . . . . . 6 (𝑏𝑤) ∈ V
1211a1i 11 . . . . 5 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ∈ V)
13 disjdif 4463 . . . . . 6 (𝑤 ∩ (𝑏𝑤)) = ∅
1413a1i 11 . . . . 5 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑤 ∩ (𝑏𝑤)) = ∅)
15 hashunx 14342 . . . . 5 ((𝑤 ∈ (LBasis‘𝐾) ∧ (𝑏𝑤) ∈ V ∧ (𝑤 ∩ (𝑏𝑤)) = ∅) → (♯‘(𝑤 ∪ (𝑏𝑤))) = ((♯‘𝑤) +𝑒 (♯‘(𝑏𝑤))))
169, 12, 14, 15syl3anc 1368 . . . 4 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (♯‘(𝑤 ∪ (𝑏𝑤))) = ((♯‘𝑤) +𝑒 (♯‘(𝑏𝑤))))
17 simp-4l 780 . . . . 5 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑉 ∈ LVec)
18 simpr 484 . . . . . . 7 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑤𝑏)
19 undif 4473 . . . . . . 7 (𝑤𝑏 ↔ (𝑤 ∪ (𝑏𝑤)) = 𝑏)
2018, 19sylib 217 . . . . . 6 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑤 ∪ (𝑏𝑤)) = 𝑏)
21 simplr 766 . . . . . 6 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑏 ∈ (LBasis‘𝑉))
2220, 21eqeltrd 2825 . . . . 5 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑤 ∪ (𝑏𝑤)) ∈ (LBasis‘𝑉))
23 eqid 2724 . . . . . 6 (LBasis‘𝑉) = (LBasis‘𝑉)
2423dimval 33130 . . . . 5 ((𝑉 ∈ LVec ∧ (𝑤 ∪ (𝑏𝑤)) ∈ (LBasis‘𝑉)) → (dim‘𝑉) = (♯‘(𝑤 ∪ (𝑏𝑤))))
2517, 22, 24syl2anc 583 . . . 4 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (dim‘𝑉) = (♯‘(𝑤 ∪ (𝑏𝑤))))
263ad3antrrr 727 . . . . . 6 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝐾 ∈ LVec)
274dimval 33130 . . . . . 6 ((𝐾 ∈ LVec ∧ 𝑤 ∈ (LBasis‘𝐾)) → (dim‘𝐾) = (♯‘𝑤))
2826, 9, 27syl2anc 583 . . . . 5 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (dim‘𝐾) = (♯‘𝑤))
29 dimkerim.i . . . . . . . . 9 𝐼 = (𝑈s ran 𝐹)
3029imlmhm 33151 . . . . . . . 8 ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝐼 ∈ LVec)
3130ad3antrrr 727 . . . . . . 7 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝐼 ∈ LVec)
32 simp-4r 781 . . . . . . . . . . 11 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝐹 ∈ (𝑉 LMHom 𝑈))
33 lmhmlmod2 20869 . . . . . . . . . . 11 (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝑈 ∈ LMod)
3432, 33syl 17 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑈 ∈ LMod)
35 lmhmrnlss 20887 . . . . . . . . . . 11 (𝐹 ∈ (𝑉 LMHom 𝑈) → ran 𝐹 ∈ (LSubSp‘𝑈))
3632, 35syl 17 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ran 𝐹 ∈ (LSubSp‘𝑈))
37 df-ima 5679 . . . . . . . . . . 11 (𝐹 “ ((LSpan‘𝑉)‘(𝑏𝑤))) = ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))
38 imassrn 6060 . . . . . . . . . . . 12 (𝐹 “ ((LSpan‘𝑉)‘(𝑏𝑤))) ⊆ ran 𝐹
3938a1i 11 . . . . . . . . . . 11 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 “ ((LSpan‘𝑉)‘(𝑏𝑤))) ⊆ ran 𝐹)
4037, 39eqsstrrid 4023 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ⊆ ran 𝐹)
41 lveclmod 20943 . . . . . . . . . . . . 13 (𝑉 ∈ LVec → 𝑉 ∈ LMod)
4241ad4antr 729 . . . . . . . . . . . 12 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑉 ∈ LMod)
4323lbslinds 21695 . . . . . . . . . . . . . . 15 (LBasis‘𝑉) ⊆ (LIndS‘𝑉)
4443, 21sselid 3972 . . . . . . . . . . . . . 14 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑏 ∈ (LIndS‘𝑉))
45 difssd 4124 . . . . . . . . . . . . . 14 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ⊆ 𝑏)
46 lindsss 21686 . . . . . . . . . . . . . 14 ((𝑉 ∈ LMod ∧ 𝑏 ∈ (LIndS‘𝑉) ∧ (𝑏𝑤) ⊆ 𝑏) → (𝑏𝑤) ∈ (LIndS‘𝑉))
4742, 44, 45, 46syl3anc 1368 . . . . . . . . . . . . 13 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ∈ (LIndS‘𝑉))
48 eqid 2724 . . . . . . . . . . . . . 14 (Base‘𝑉) = (Base‘𝑉)
4948linds1 21672 . . . . . . . . . . . . 13 ((𝑏𝑤) ∈ (LIndS‘𝑉) → (𝑏𝑤) ⊆ (Base‘𝑉))
5047, 49syl 17 . . . . . . . . . . . 12 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ⊆ (Base‘𝑉))
51 eqid 2724 . . . . . . . . . . . . 13 (LSubSp‘𝑉) = (LSubSp‘𝑉)
52 eqid 2724 . . . . . . . . . . . . 13 (LSpan‘𝑉) = (LSpan‘𝑉)
5348, 51, 52lspcl 20812 . . . . . . . . . . . 12 ((𝑉 ∈ LMod ∧ (𝑏𝑤) ⊆ (Base‘𝑉)) → ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉))
5442, 50, 53syl2anc 583 . . . . . . . . . . 11 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉))
55 eqid 2724 . . . . . . . . . . . 12 (𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) = (𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))
5651, 55reslmhm 20889 . . . . . . . . . . 11 ((𝐹 ∈ (𝑉 LMHom 𝑈) ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉)) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMHom 𝑈))
5732, 54, 56syl2anc 583 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMHom 𝑈))
58 eqid 2724 . . . . . . . . . . . 12 (LSubSp‘𝑈) = (LSubSp‘𝑈)
5929, 58reslmhm2b 20891 . . . . . . . . . . 11 ((𝑈 ∈ LMod ∧ ran 𝐹 ∈ (LSubSp‘𝑈) ∧ ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ⊆ ran 𝐹) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMHom 𝑈) ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMHom 𝐼)))
6059biimpa 476 . . . . . . . . . 10 (((𝑈 ∈ LMod ∧ ran 𝐹 ∈ (LSubSp‘𝑈) ∧ ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ⊆ ran 𝐹) ∧ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMHom 𝑈)) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMHom 𝐼))
6134, 36, 40, 57, 60syl31anc 1370 . . . . . . . . 9 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMHom 𝐼))
62 lmghm 20868 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝐹 ∈ (𝑉 GrpHom 𝑈))
6362ad4antlr 730 . . . . . . . . . . . . . . . 16 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝐹 ∈ (𝑉 GrpHom 𝑈))
6448, 23lbsss 20914 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ (LBasis‘𝑉) → 𝑏 ⊆ (Base‘𝑉))
6521, 64syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑏 ⊆ (Base‘𝑉))
6645, 65sstrd 3984 . . . . . . . . . . . . . . . . . 18 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ⊆ (Base‘𝑉))
6742, 66, 53syl2anc 583 . . . . . . . . . . . . . . . . 17 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉))
6851lsssubg 20793 . . . . . . . . . . . . . . . . 17 ((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉)) → ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (SubGrp‘𝑉))
6942, 67, 68syl2anc 583 . . . . . . . . . . . . . . . 16 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (SubGrp‘𝑉))
7055resghm 19146 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ (𝑉 GrpHom 𝑈) ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (SubGrp‘𝑉)) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) GrpHom 𝑈))
7163, 69, 70syl2anc 583 . . . . . . . . . . . . . . 15 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) GrpHom 𝑈))
72 eqid 2724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Base‘𝑈) = (Base‘𝑈)
7348, 72lmhmf 20871 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈))
7473ad4antlr 730 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈))
7574ffnd 6708 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝐹 Fn (Base‘𝑉))
7648, 52lspssv 20819 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑉 ∈ LMod ∧ (𝑏𝑤) ⊆ (Base‘𝑉)) → ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉))
7742, 66, 76syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉))
7875, 77fnssresd 6664 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) Fn ((LSpan‘𝑉)‘(𝑏𝑤)))
79 fniniseg 7051 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) Fn ((LSpan‘𝑉)‘(𝑏𝑤)) → (𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }) ↔ (𝑥 ∈ ((LSpan‘𝑉)‘(𝑏𝑤)) ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘𝑥) = 0 )))
8079biimpa 476 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) Fn ((LSpan‘𝑉)‘(𝑏𝑤)) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → (𝑥 ∈ ((LSpan‘𝑉)‘(𝑏𝑤)) ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘𝑥) = 0 ))
8178, 80sylan 579 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → (𝑥 ∈ ((LSpan‘𝑉)‘(𝑏𝑤)) ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘𝑥) = 0 ))
8281simpld 494 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → 𝑥 ∈ ((LSpan‘𝑉)‘(𝑏𝑤)))
8375adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → 𝐹 Fn (Base‘𝑉))
8477adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉))
8584, 82sseldd 3975 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → 𝑥 ∈ (Base‘𝑉))
8682fvresd 6901 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘𝑥) = (𝐹𝑥))
8781simprd 495 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘𝑥) = 0 )
8886, 87eqtr3d 2766 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → (𝐹𝑥) = 0 )
89 fniniseg 7051 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 Fn (Base‘𝑉) → (𝑥 ∈ (𝐹 “ { 0 }) ↔ (𝑥 ∈ (Base‘𝑉) ∧ (𝐹𝑥) = 0 )))
9089biimpar 477 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 Fn (Base‘𝑉) ∧ (𝑥 ∈ (Base‘𝑉) ∧ (𝐹𝑥) = 0 )) → 𝑥 ∈ (𝐹 “ { 0 }))
9183, 85, 88, 90syl12anc 834 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → 𝑥 ∈ (𝐹 “ { 0 }))
9282, 91elind 4186 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → 𝑥 ∈ (((LSpan‘𝑉)‘(𝑏𝑤)) ∩ (𝐹 “ { 0 })))
93 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LBasis‘𝐾))
94 eqid 2724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Base‘𝐾) = (Base‘𝐾)
95 eqid 2724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (LSpan‘𝐾) = (LSpan‘𝐾)
9694, 4, 95lbssp 20916 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ∈ (LBasis‘𝐾) → ((LSpan‘𝐾)‘𝑤) = (Base‘𝐾))
9793, 96syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝐾)‘𝑤) = (Base‘𝐾))
9841ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑉 ∈ LMod)
99 eqid 2724 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐹 “ { 0 }) = (𝐹 “ { 0 })
10099, 1, 51lmhmkerlss 20888 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹 ∈ (𝑉 LMHom 𝑈) → (𝐹 “ { 0 }) ∈ (LSubSp‘𝑉))
101100ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (𝐹 “ { 0 }) ∈ (LSubSp‘𝑉))
10294, 4lbsss 20914 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 ∈ (LBasis‘𝐾) → 𝑤 ⊆ (Base‘𝐾))
10393, 102syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ⊆ (Base‘𝐾))
104 cnvimass 6070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐹 “ { 0 }) ⊆ dom 𝐹
105104, 73fssdm 6727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐹 ∈ (𝑉 LMHom 𝑈) → (𝐹 “ { 0 }) ⊆ (Base‘𝑉))
1062, 48ressbas2 17180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹 “ { 0 }) ⊆ (Base‘𝑉) → (𝐹 “ { 0 }) = (Base‘𝐾))
107105, 106syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐹 ∈ (𝑉 LMHom 𝑈) → (𝐹 “ { 0 }) = (Base‘𝐾))
108107ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (𝐹 “ { 0 }) = (Base‘𝐾))
109103, 108sseqtrrd 4015 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ⊆ (𝐹 “ { 0 }))
1102, 52, 95, 51lsslsp 20851 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑉 ∈ LMod ∧ (𝐹 “ { 0 }) ∈ (LSubSp‘𝑉) ∧ 𝑤 ⊆ (𝐹 “ { 0 })) → ((LSpan‘𝐾)‘𝑤) = ((LSpan‘𝑉)‘𝑤))
111110eqcomd 2730 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑉 ∈ LMod ∧ (𝐹 “ { 0 }) ∈ (LSubSp‘𝑉) ∧ 𝑤 ⊆ (𝐹 “ { 0 })) → ((LSpan‘𝑉)‘𝑤) = ((LSpan‘𝐾)‘𝑤))
11298, 101, 109, 111syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝑉)‘𝑤) = ((LSpan‘𝐾)‘𝑤))
11397, 112, 1083eqtr4d 2774 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝑉)‘𝑤) = (𝐹 “ { 0 }))
114113ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘𝑤) = (𝐹 “ { 0 }))
115114ineq2d 4204 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (((LSpan‘𝑉)‘(𝑏𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = (((LSpan‘𝑉)‘(𝑏𝑤)) ∩ (𝐹 “ { 0 })))
116 eqid 2724 . . . . . . . . . . . . . . . . . . . . . . . 24 (0g𝑉) = (0g𝑉)
11723, 52, 116lbsdiflsp0 33156 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑉 ∈ LVec ∧ 𝑏 ∈ (LBasis‘𝑉) ∧ 𝑤𝑏) → (((LSpan‘𝑉)‘(𝑏𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = {(0g𝑉)})
118117ad5ant145 1366 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (((LSpan‘𝑉)‘(𝑏𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = {(0g𝑉)})
119115, 118eqtr3d 2766 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (((LSpan‘𝑉)‘(𝑏𝑤)) ∩ (𝐹 “ { 0 })) = {(0g𝑉)})
120119adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → (((LSpan‘𝑉)‘(𝑏𝑤)) ∩ (𝐹 “ { 0 })) = {(0g𝑉)})
12192, 120eleqtrd 2827 . . . . . . . . . . . . . . . . . . 19 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → 𝑥 ∈ {(0g𝑉)})
122121ex 412 . . . . . . . . . . . . . . . . . 18 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }) → 𝑥 ∈ {(0g𝑉)}))
123122ssrdv 3980 . . . . . . . . . . . . . . . . 17 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }) ⊆ {(0g𝑉)})
124116, 48, 520ellsp 32917 . . . . . . . . . . . . . . . . . . . 20 ((𝑉 ∈ LMod ∧ (𝑏𝑤) ⊆ (Base‘𝑉)) → (0g𝑉) ∈ ((LSpan‘𝑉)‘(𝑏𝑤)))
12542, 66, 124syl2anc 583 . . . . . . . . . . . . . . . . . . 19 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (0g𝑉) ∈ ((LSpan‘𝑉)‘(𝑏𝑤)))
126 fvexd 6896 . . . . . . . . . . . . . . . . . . . 20 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) ∈ V)
127125fvresd 6901 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) = (𝐹‘(0g𝑉)))
128116, 1ghmid 19136 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 ∈ (𝑉 GrpHom 𝑈) → (𝐹‘(0g𝑉)) = 0 )
12962, 128syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹 ∈ (𝑉 LMHom 𝑈) → (𝐹‘(0g𝑉)) = 0 )
130129ad4antlr 730 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹‘(0g𝑉)) = 0 )
131127, 130eqtrd 2764 . . . . . . . . . . . . . . . . . . . 20 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) = 0 )
132 elsng 4634 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) ∈ V → (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) ∈ { 0 } ↔ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) = 0 ))
133132biimpar 477 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) ∈ V ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) = 0 ) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) ∈ { 0 })
134126, 131, 133syl2anc 583 . . . . . . . . . . . . . . . . . . 19 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) ∈ { 0 })
13578, 125, 134elpreimad 7050 . . . . . . . . . . . . . . . . . 18 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (0g𝑉) ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }))
136135snssd 4804 . . . . . . . . . . . . . . . . 17 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → {(0g𝑉)} ⊆ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }))
137123, 136eqssd 3991 . . . . . . . . . . . . . . . 16 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }) = {(0g𝑉)})
138 lmodgrp 20702 . . . . . . . . . . . . . . . . . . 19 (𝑉 ∈ LMod → 𝑉 ∈ Grp)
139 grpmnd 18859 . . . . . . . . . . . . . . . . . . 19 (𝑉 ∈ Grp → 𝑉 ∈ Mnd)
14042, 138, 1393syl 18 . . . . . . . . . . . . . . . . . 18 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑉 ∈ Mnd)
14155, 48, 116ress0g 18684 . . . . . . . . . . . . . . . . . 18 ((𝑉 ∈ Mnd ∧ (0g𝑉) ∈ ((LSpan‘𝑉)‘(𝑏𝑤)) ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉)) → (0g𝑉) = (0g‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
142140, 125, 77, 141syl3anc 1368 . . . . . . . . . . . . . . . . 17 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (0g𝑉) = (0g‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
143142sneqd 4632 . . . . . . . . . . . . . . . 16 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → {(0g𝑉)} = {(0g‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))})
144137, 143eqtrd 2764 . . . . . . . . . . . . . . 15 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }) = {(0g‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))})
145 eqid 2724 . . . . . . . . . . . . . . . . 17 (Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))) = (Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))
146 eqid 2724 . . . . . . . . . . . . . . . . 17 (0g‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))) = (0g‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))
147145, 72, 146, 1kerf1ghm 19161 . . . . . . . . . . . . . . . 16 ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) GrpHom 𝑈) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):(Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))–1-1→(Base‘𝑈) ↔ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }) = {(0g‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))}))
148147biimpar 477 . . . . . . . . . . . . . . 15 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) GrpHom 𝑈) ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }) = {(0g‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))}) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):(Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))–1-1→(Base‘𝑈))
14971, 144, 148syl2anc 583 . . . . . . . . . . . . . 14 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):(Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))–1-1→(Base‘𝑈))
150 eqidd 2725 . . . . . . . . . . . . . . 15 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) = (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))))
15155, 48ressbas2 17180 . . . . . . . . . . . . . . . 16 (((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉) → ((LSpan‘𝑉)‘(𝑏𝑤)) = (Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
15277, 151syl 17 . . . . . . . . . . . . . . 15 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) = (Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
153 eqidd 2725 . . . . . . . . . . . . . . 15 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (Base‘𝑈) = (Base‘𝑈))
154150, 152, 153f1eq123d 6815 . . . . . . . . . . . . . 14 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1→(Base‘𝑈) ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):(Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))–1-1→(Base‘𝑈)))
155149, 154mpbird 257 . . . . . . . . . . . . 13 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1→(Base‘𝑈))
156 f1ssr 6784 . . . . . . . . . . . . 13 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1→(Base‘𝑈) ∧ ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ⊆ ran 𝐹) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1→ran 𝐹)
157155, 40, 156syl2anc 583 . . . . . . . . . . . 12 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1→ran 𝐹)
158 f1f1orn 6834 . . . . . . . . . . . 12 ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1→ran 𝐹 → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1-onto→ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))))
159157, 158syl 17 . . . . . . . . . . 11 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1-onto→ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))))
160 simp-4r 781 . . . . . . . . . . . . . . . . . 18 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → (𝐹𝑥) = 𝑦)
16175ad6antr 733 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝐹 Fn (Base‘𝑉))
162 simpllr 773 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝑢 ∈ ((LSpan‘𝑉)‘𝑤))
163113ad8antr 737 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → ((LSpan‘𝑉)‘𝑤) = (𝐹 “ { 0 }))
164162, 163eleqtrd 2827 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝑢 ∈ (𝐹 “ { 0 }))
165 fniniseg 7051 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹 Fn (Base‘𝑉) → (𝑢 ∈ (𝐹 “ { 0 }) ↔ (𝑢 ∈ (Base‘𝑉) ∧ (𝐹𝑢) = 0 )))
166165simplbda 499 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 Fn (Base‘𝑉) ∧ 𝑢 ∈ (𝐹 “ { 0 })) → (𝐹𝑢) = 0 )
167161, 164, 166syl2anc 583 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → (𝐹𝑢) = 0 )
168167oveq1d 7416 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → ((𝐹𝑢)(+g𝑈)(𝐹𝑣)) = ( 0 (+g𝑈)(𝐹𝑣)))
169 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝑥 = (𝑢(+g𝑉)𝑣))
170169fveq2d 6885 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → (𝐹𝑥) = (𝐹‘(𝑢(+g𝑉)𝑣)))
17163ad6antr 733 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝐹 ∈ (𝑉 GrpHom 𝑈))
17248, 52lspss 20820 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑉 ∈ LMod ∧ 𝑏 ⊆ (Base‘𝑉) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ ((LSpan‘𝑉)‘𝑏))
17342, 65, 18, 172syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ ((LSpan‘𝑉)‘𝑏))
17448, 23, 52lbssp 20916 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 ∈ (LBasis‘𝑉) → ((LSpan‘𝑉)‘𝑏) = (Base‘𝑉))
17521, 174syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘𝑏) = (Base‘𝑉))
176173, 175sseqtrd 4014 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉))
177176ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) → ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉))
178177ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉))
179178, 162sseldd 3975 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝑢 ∈ (Base‘𝑉))
18077ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) → ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉))
181180ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉))
182 simplr 766 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤)))
183181, 182sseldd 3975 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝑣 ∈ (Base‘𝑉))
184 eqid 2724 . . . . . . . . . . . . . . . . . . . . . 22 (+g𝑉) = (+g𝑉)
185 eqid 2724 . . . . . . . . . . . . . . . . . . . . . 22 (+g𝑈) = (+g𝑈)
18648, 184, 185ghmlin 19135 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (𝑉 GrpHom 𝑈) ∧ 𝑢 ∈ (Base‘𝑉) ∧ 𝑣 ∈ (Base‘𝑉)) → (𝐹‘(𝑢(+g𝑉)𝑣)) = ((𝐹𝑢)(+g𝑈)(𝐹𝑣)))
187171, 179, 183, 186syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → (𝐹‘(𝑢(+g𝑉)𝑣)) = ((𝐹𝑢)(+g𝑈)(𝐹𝑣)))
188170, 187eqtr2d 2765 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → ((𝐹𝑢)(+g𝑈)(𝐹𝑣)) = (𝐹𝑥))
189 lmhmlvec2 33149 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝑈 ∈ LVec)
190189lvecgrpd 20945 . . . . . . . . . . . . . . . . . . . . 21 ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝑈 ∈ Grp)
191190ad9antr 739 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝑈 ∈ Grp)
19274ad6antr 733 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈))
193192, 183ffvelcdmd 7077 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → (𝐹𝑣) ∈ (Base‘𝑈))
19472, 185, 1, 191, 193grplidd 18888 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → ( 0 (+g𝑈)(𝐹𝑣)) = (𝐹𝑣))
195168, 188, 1943eqtr3d 2772 . . . . . . . . . . . . . . . . . 18 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → (𝐹𝑥) = (𝐹𝑣))
196160, 195eqtr3d 2766 . . . . . . . . . . . . . . . . 17 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝑦 = (𝐹𝑣))
197161, 183, 182fnfvimad 7227 . . . . . . . . . . . . . . . . 17 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → (𝐹𝑣) ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏𝑤))))
198196, 197eqeltrd 2825 . . . . . . . . . . . . . . . 16 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏𝑤))))
199 simp-7l 786 . . . . . . . . . . . . . . . . 17 ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) → 𝑉 ∈ LVec)
200 simplr 766 . . . . . . . . . . . . . . . . . 18 ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) → 𝑥 ∈ (Base‘𝑉))
201109ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑤 ⊆ (𝐹 “ { 0 }))
202105ad4antlr 730 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 “ { 0 }) ⊆ (Base‘𝑉))
203201, 202sstrd 3984 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑤 ⊆ (Base‘𝑉))
204 eqid 2724 . . . . . . . . . . . . . . . . . . . . . 22 (LSSum‘𝑉) = (LSSum‘𝑉)
20548, 52, 204lsmsp2 20924 . . . . . . . . . . . . . . . . . . . . 21 ((𝑉 ∈ LMod ∧ 𝑤 ⊆ (Base‘𝑉) ∧ (𝑏𝑤) ⊆ (Base‘𝑉)) → (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏𝑤))) = ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏𝑤))))
20642, 203, 66, 205syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏𝑤))) = ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏𝑤))))
20720fveq2d 6885 . . . . . . . . . . . . . . . . . . . 20 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏𝑤))) = ((LSpan‘𝑉)‘𝑏))
208206, 207, 1753eqtrrd 2769 . . . . . . . . . . . . . . . . . . 19 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (Base‘𝑉) = (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏𝑤))))
209208ad3antrrr 727 . . . . . . . . . . . . . . . . . 18 ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) → (Base‘𝑉) = (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏𝑤))))
210200, 209eleqtrd 2827 . . . . . . . . . . . . . . . . 17 ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) → 𝑥 ∈ (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏𝑤))))
21148, 184, 204lsmelvalx 19549 . . . . . . . . . . . . . . . . . 18 ((𝑉 ∈ LVec ∧ ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉) ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉)) → (𝑥 ∈ (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏𝑤))) ↔ ∃𝑢 ∈ ((LSpan‘𝑉)‘𝑤)∃𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))𝑥 = (𝑢(+g𝑉)𝑣)))
212211biimpa 476 . . . . . . . . . . . . . . . . 17 (((𝑉 ∈ LVec ∧ ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉) ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉)) ∧ 𝑥 ∈ (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏𝑤)))) → ∃𝑢 ∈ ((LSpan‘𝑉)‘𝑤)∃𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))𝑥 = (𝑢(+g𝑉)𝑣))
213199, 177, 180, 210, 212syl31anc 1370 . . . . . . . . . . . . . . . 16 ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) → ∃𝑢 ∈ ((LSpan‘𝑉)‘𝑤)∃𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))𝑥 = (𝑢(+g𝑉)𝑣))
214198, 213r19.29vva 3205 . . . . . . . . . . . . . . 15 ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏𝑤))))
215 fvelrnb 6942 . . . . . . . . . . . . . . . . 17 (𝐹 Fn (Base‘𝑉) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ (Base‘𝑉)(𝐹𝑥) = 𝑦))
216215biimpa 476 . . . . . . . . . . . . . . . 16 ((𝐹 Fn (Base‘𝑉) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑥 ∈ (Base‘𝑉)(𝐹𝑥) = 𝑦)
21775, 216sylan 579 . . . . . . . . . . . . . . 15 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑥 ∈ (Base‘𝑉)(𝐹𝑥) = 𝑦)
218214, 217r19.29a 3154 . . . . . . . . . . . . . 14 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏𝑤))))
21939, 218eqelssd 3995 . . . . . . . . . . . . 13 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 “ ((LSpan‘𝑉)‘(𝑏𝑤))) = ran 𝐹)
22037, 219eqtr3id 2778 . . . . . . . . . . . 12 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) = ran 𝐹)
221220f1oeq3d 6820 . . . . . . . . . . 11 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1-onto→ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1-onto→ran 𝐹))
222159, 221mpbid 231 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1-onto→ran 𝐹)
22342, 50, 76syl2anc 583 . . . . . . . . . . . 12 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉))
224223, 151syl 17 . . . . . . . . . . 11 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) = (Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
225 frn 6714 . . . . . . . . . . . . 13 (𝐹:(Base‘𝑉)⟶(Base‘𝑈) → ran 𝐹 ⊆ (Base‘𝑈))
22629, 72ressbas2 17180 . . . . . . . . . . . . 13 (ran 𝐹 ⊆ (Base‘𝑈) → ran 𝐹 = (Base‘𝐼))
22773, 225, 2263syl 18 . . . . . . . . . . . 12 (𝐹 ∈ (𝑉 LMHom 𝑈) → ran 𝐹 = (Base‘𝐼))
22832, 227syl 17 . . . . . . . . . . 11 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ran 𝐹 = (Base‘𝐼))
229150, 224, 228f1oeq123d 6817 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1-onto→ran 𝐹 ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):(Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))–1-1-onto→(Base‘𝐼)))
230222, 229mpbid 231 . . . . . . . . 9 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):(Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))–1-1-onto→(Base‘𝐼))
231 eqid 2724 . . . . . . . . . 10 (Base‘𝐼) = (Base‘𝐼)
232145, 231islmim 20899 . . . . . . . . 9 ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMIso 𝐼) ↔ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMHom 𝐼) ∧ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):(Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))–1-1-onto→(Base‘𝐼)))
23361, 230, 232sylanbrc 582 . . . . . . . 8 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMIso 𝐼))
23448, 52lspssid 20821 . . . . . . . . . . 11 ((𝑉 ∈ LMod ∧ (𝑏𝑤) ⊆ (Base‘𝑉)) → (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤)))
23542, 50, 234syl2anc 583 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤)))
23651, 55lsslinds 21693 . . . . . . . . . . 11 ((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤))) → ((𝑏𝑤) ∈ (LIndS‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))) ↔ (𝑏𝑤) ∈ (LIndS‘𝑉)))
237236biimpar 477 . . . . . . . . . 10 (((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ (𝑏𝑤) ∈ (LIndS‘𝑉)) → (𝑏𝑤) ∈ (LIndS‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
23842, 67, 235, 47, 237syl31anc 1370 . . . . . . . . 9 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ∈ (LIndS‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
239 eqid 2724 . . . . . . . . . . . . 13 (LSpan‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))) = (LSpan‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))
24055, 52, 239, 51lsslsp 20851 . . . . . . . . . . . 12 ((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤))) → ((LSpan‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))‘(𝑏𝑤)) = ((LSpan‘𝑉)‘(𝑏𝑤)))
241240eqcomd 2730 . . . . . . . . . . 11 ((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤))) → ((LSpan‘𝑉)‘(𝑏𝑤)) = ((LSpan‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))‘(𝑏𝑤)))
24242, 54, 235, 241syl3anc 1368 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) = ((LSpan‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))‘(𝑏𝑤)))
243242, 224eqtr3d 2766 . . . . . . . . 9 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))‘(𝑏𝑤)) = (Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
244 eqid 2724 . . . . . . . . . 10 (LBasis‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))) = (LBasis‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))
245145, 244, 239islbs4 21694 . . . . . . . . 9 ((𝑏𝑤) ∈ (LBasis‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))) ↔ ((𝑏𝑤) ∈ (LIndS‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))) ∧ ((LSpan‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))‘(𝑏𝑤)) = (Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))))
246238, 243, 245sylanbrc 582 . . . . . . . 8 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ∈ (LBasis‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
247 eqid 2724 . . . . . . . . 9 (LBasis‘𝐼) = (LBasis‘𝐼)
248244, 247lmimlbs 21698 . . . . . . . 8 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMIso 𝐼) ∧ (𝑏𝑤) ∈ (LBasis‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤)) ∈ (LBasis‘𝐼))
249233, 246, 248syl2anc 583 . . . . . . 7 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤)) ∈ (LBasis‘𝐼))
250247dimval 33130 . . . . . . 7 ((𝐼 ∈ LVec ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤)) ∈ (LBasis‘𝐼)) → (dim‘𝐼) = (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤))))
25131, 249, 250syl2anc 583 . . . . . 6 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (dim‘𝐼) = (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤))))
252 f1imaeng 9005 . . . . . . . 8 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1→ran 𝐹 ∧ (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤)) ∧ (𝑏𝑤) ∈ (LIndS‘𝑉)) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤)) ≈ (𝑏𝑤))
253 hasheni 14304 . . . . . . . 8 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤)) ≈ (𝑏𝑤) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤))) = (♯‘(𝑏𝑤)))
254252, 253syl 17 . . . . . . 7 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1→ran 𝐹 ∧ (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤)) ∧ (𝑏𝑤) ∈ (LIndS‘𝑉)) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤))) = (♯‘(𝑏𝑤)))
255157, 235, 47, 254syl3anc 1368 . . . . . 6 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤))) = (♯‘(𝑏𝑤)))
256251, 255eqtrd 2764 . . . . 5 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (dim‘𝐼) = (♯‘(𝑏𝑤)))
25728, 256oveq12d 7419 . . . 4 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((dim‘𝐾) +𝑒 (dim‘𝐼)) = ((♯‘𝑤) +𝑒 (♯‘(𝑏𝑤))))
25816, 25, 2573eqtr4d 2774 . . 3 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼)))
2594lbslinds 21695 . . . . . 6 (LBasis‘𝐾) ⊆ (LIndS‘𝐾)
260259, 93sselid 3972 . . . . 5 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LIndS‘𝐾))
26151, 2lsslinds 21693 . . . . . 6 ((𝑉 ∈ LMod ∧ (𝐹 “ { 0 }) ∈ (LSubSp‘𝑉) ∧ 𝑤 ⊆ (𝐹 “ { 0 })) → (𝑤 ∈ (LIndS‘𝐾) ↔ 𝑤 ∈ (LIndS‘𝑉)))
262261biimpa 476 . . . . 5 (((𝑉 ∈ LMod ∧ (𝐹 “ { 0 }) ∈ (LSubSp‘𝑉) ∧ 𝑤 ⊆ (𝐹 “ { 0 })) ∧ 𝑤 ∈ (LIndS‘𝐾)) → 𝑤 ∈ (LIndS‘𝑉))
26398, 101, 109, 260, 262syl31anc 1370 . . . 4 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LIndS‘𝑉))
26423islinds4 21697 . . . . 5 (𝑉 ∈ LVec → (𝑤 ∈ (LIndS‘𝑉) ↔ ∃𝑏 ∈ (LBasis‘𝑉)𝑤𝑏))
265264ad2antrr 723 . . . 4 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (𝑤 ∈ (LIndS‘𝑉) ↔ ∃𝑏 ∈ (LBasis‘𝑉)𝑤𝑏))
266263, 265mpbid 231 . . 3 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ∃𝑏 ∈ (LBasis‘𝑉)𝑤𝑏)
267258, 266r19.29a 3154 . 2 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼)))
2688, 267exlimddv 1930 1 ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1084   = wceq 1533  wex 1773  wcel 2098  wne 2932  wrex 3062  Vcvv 3466  cdif 3937  cun 3938  cin 3939  wss 3940  c0 4314  {csn 4620   class class class wbr 5138  ccnv 5665  ran crn 5667  cres 5668  cima 5669   Fn wfn 6528  wf 6529  1-1wf1 6530  1-1-ontowf1o 6532  cfv 6533  (class class class)co 7401  cen 8931   +𝑒 cxad 13086  chash 14286  Basecbs 17142  s cress 17171  +gcplusg 17195  0gc0g 17383  Mndcmnd 18656  Grpcgrp 18852  SubGrpcsubg 19036   GrpHom cghm 19127  LSSumclsm 19543  LModclmod 20695  LSubSpclss 20767  LSpanclspn 20807   LMHom clmhm 20856   LMIso clmim 20857  LBasisclbs 20911  LVecclvec 20939  LIndSclinds 21667  dimcldim 33128
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-reg 9582  ax-inf2 9631  ax-ac2 10453  ax-cnex 11161  ax-resscn 11162  ax-1cn 11163  ax-icn 11164  ax-addcl 11165  ax-addrcl 11166  ax-mulcl 11167  ax-mulrcl 11168  ax-mulcom 11169  ax-addass 11170  ax-mulass 11171  ax-distr 11172  ax-i2m1 11173  ax-1ne0 11174  ax-1rid 11175  ax-rnegex 11176  ax-rrecex 11177  ax-cnre 11178  ax-pre-lttri 11179  ax-pre-lttrn 11180  ax-pre-ltadd 11181  ax-pre-mulgt0 11182
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-rpss 7706  df-om 7849  df-1st 7968  df-2nd 7969  df-supp 8141  df-tpos 8206  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-oadd 8465  df-er 8698  df-map 8817  df-ixp 8887  df-en 8935  df-dom 8936  df-sdom 8937  df-fin 8938  df-fsupp 9357  df-sup 9432  df-oi 9500  df-r1 9754  df-rank 9755  df-dju 9891  df-card 9929  df-acn 9932  df-ac 10106  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-xnn0 12541  df-z 12555  df-dec 12674  df-uz 12819  df-xadd 13089  df-fz 13481  df-fzo 13624  df-seq 13963  df-hash 14287  df-struct 17078  df-sets 17095  df-slot 17113  df-ndx 17125  df-base 17143  df-ress 17172  df-plusg 17208  df-mulr 17209  df-sca 17211  df-vsca 17212  df-ip 17213  df-tset 17214  df-ple 17215  df-ocomp 17216  df-ds 17217  df-hom 17219  df-cco 17220  df-0g 17385  df-gsum 17386  df-prds 17391  df-pws 17393  df-mre 17528  df-mrc 17529  df-mri 17530  df-acs 17531  df-proset 18249  df-drs 18250  df-poset 18267  df-ipo 18482  df-mgm 18562  df-sgrp 18641  df-mnd 18657  df-mhm 18702  df-submnd 18703  df-grp 18855  df-minusg 18856  df-sbg 18857  df-mulg 18985  df-subg 19039  df-ghm 19128  df-cntz 19222  df-lsm 19545  df-cmn 19691  df-abl 19692  df-mgp 20029  df-rng 20047  df-ur 20076  df-ring 20129  df-oppr 20225  df-dvdsr 20248  df-unit 20249  df-invr 20279  df-nzr 20404  df-subrg 20460  df-drng 20578  df-lmod 20697  df-lss 20768  df-lsp 20808  df-lmhm 20859  df-lmim 20860  df-lbs 20912  df-lvec 20940  df-sra 21010  df-rgmod 21011  df-dsmm 21594  df-frlm 21609  df-uvc 21645  df-lindf 21668  df-linds 21669  df-dim 33129
This theorem is referenced by:  qusdimsum  33158
  Copyright terms: Public domain W3C validator