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 33453
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 33446 . . . 4 ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝐾 ∈ LVec)
4 eqid 2725 . . . . 5 (LBasis‘𝐾) = (LBasis‘𝐾)
54lbsex 21065 . . . 4 (𝐾 ∈ LVec → (LBasis‘𝐾) ≠ ∅)
63, 5syl 17 . . 3 ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → (LBasis‘𝐾) ≠ ∅)
7 n0 4346 . . 3 ((LBasis‘𝐾) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ (LBasis‘𝐾))
86, 7sylib 217 . 2 ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → ∃𝑤 𝑤 ∈ (LBasis‘𝐾))
9 simpllr 774 . . . . 5 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑤 ∈ (LBasis‘𝐾))
10 vex 3465 . . . . . . 7 𝑏 ∈ V
1110difexi 5331 . . . . . 6 (𝑏𝑤) ∈ V
1211a1i 11 . . . . 5 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ∈ V)
13 disjdif 4473 . . . . . 6 (𝑤 ∩ (𝑏𝑤)) = ∅
1413a1i 11 . . . . 5 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑤 ∩ (𝑏𝑤)) = ∅)
15 hashunx 14381 . . . . 5 ((𝑤 ∈ (LBasis‘𝐾) ∧ (𝑏𝑤) ∈ V ∧ (𝑤 ∩ (𝑏𝑤)) = ∅) → (♯‘(𝑤 ∪ (𝑏𝑤))) = ((♯‘𝑤) +𝑒 (♯‘(𝑏𝑤))))
169, 12, 14, 15syl3anc 1368 . . . 4 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (♯‘(𝑤 ∪ (𝑏𝑤))) = ((♯‘𝑤) +𝑒 (♯‘(𝑏𝑤))))
17 simp-4l 781 . . . . 5 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑉 ∈ LVec)
18 simpr 483 . . . . . . 7 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑤𝑏)
19 undif 4483 . . . . . . 7 (𝑤𝑏 ↔ (𝑤 ∪ (𝑏𝑤)) = 𝑏)
2018, 19sylib 217 . . . . . 6 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑤 ∪ (𝑏𝑤)) = 𝑏)
21 simplr 767 . . . . . 6 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑏 ∈ (LBasis‘𝑉))
2220, 21eqeltrd 2825 . . . . 5 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑤 ∪ (𝑏𝑤)) ∈ (LBasis‘𝑉))
23 eqid 2725 . . . . . 6 (LBasis‘𝑉) = (LBasis‘𝑉)
2423dimval 33426 . . . . 5 ((𝑉 ∈ LVec ∧ (𝑤 ∪ (𝑏𝑤)) ∈ (LBasis‘𝑉)) → (dim‘𝑉) = (♯‘(𝑤 ∪ (𝑏𝑤))))
2517, 22, 24syl2anc 582 . . . 4 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (dim‘𝑉) = (♯‘(𝑤 ∪ (𝑏𝑤))))
263ad3antrrr 728 . . . . . 6 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝐾 ∈ LVec)
274dimval 33426 . . . . . 6 ((𝐾 ∈ LVec ∧ 𝑤 ∈ (LBasis‘𝐾)) → (dim‘𝐾) = (♯‘𝑤))
2826, 9, 27syl2anc 582 . . . . 5 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (dim‘𝐾) = (♯‘𝑤))
29 dimkerim.i . . . . . . . . 9 𝐼 = (𝑈s ran 𝐹)
3029imlmhm 33447 . . . . . . . 8 ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝐼 ∈ LVec)
3130ad3antrrr 728 . . . . . . 7 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝐼 ∈ LVec)
32 simp-4r 782 . . . . . . . . . . 11 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝐹 ∈ (𝑉 LMHom 𝑈))
33 lmhmlmod2 20929 . . . . . . . . . . 11 (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝑈 ∈ LMod)
3432, 33syl 17 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑈 ∈ LMod)
35 lmhmrnlss 20947 . . . . . . . . . . 11 (𝐹 ∈ (𝑉 LMHom 𝑈) → ran 𝐹 ∈ (LSubSp‘𝑈))
3632, 35syl 17 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ran 𝐹 ∈ (LSubSp‘𝑈))
37 df-ima 5691 . . . . . . . . . . 11 (𝐹 “ ((LSpan‘𝑉)‘(𝑏𝑤))) = ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))
38 imassrn 6075 . . . . . . . . . . . 12 (𝐹 “ ((LSpan‘𝑉)‘(𝑏𝑤))) ⊆ ran 𝐹
3938a1i 11 . . . . . . . . . . 11 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 “ ((LSpan‘𝑉)‘(𝑏𝑤))) ⊆ ran 𝐹)
4037, 39eqsstrrid 4026 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ⊆ ran 𝐹)
41 lveclmod 21003 . . . . . . . . . . . . 13 (𝑉 ∈ LVec → 𝑉 ∈ LMod)
4241ad4antr 730 . . . . . . . . . . . 12 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑉 ∈ LMod)
4323lbslinds 21784 . . . . . . . . . . . . . . 15 (LBasis‘𝑉) ⊆ (LIndS‘𝑉)
4443, 21sselid 3974 . . . . . . . . . . . . . 14 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑏 ∈ (LIndS‘𝑉))
45 difssd 4129 . . . . . . . . . . . . . 14 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ⊆ 𝑏)
46 lindsss 21775 . . . . . . . . . . . . . 14 ((𝑉 ∈ LMod ∧ 𝑏 ∈ (LIndS‘𝑉) ∧ (𝑏𝑤) ⊆ 𝑏) → (𝑏𝑤) ∈ (LIndS‘𝑉))
4742, 44, 45, 46syl3anc 1368 . . . . . . . . . . . . 13 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ∈ (LIndS‘𝑉))
48 eqid 2725 . . . . . . . . . . . . . 14 (Base‘𝑉) = (Base‘𝑉)
4948linds1 21761 . . . . . . . . . . . . 13 ((𝑏𝑤) ∈ (LIndS‘𝑉) → (𝑏𝑤) ⊆ (Base‘𝑉))
5047, 49syl 17 . . . . . . . . . . . 12 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ⊆ (Base‘𝑉))
51 eqid 2725 . . . . . . . . . . . . 13 (LSubSp‘𝑉) = (LSubSp‘𝑉)
52 eqid 2725 . . . . . . . . . . . . 13 (LSpan‘𝑉) = (LSpan‘𝑉)
5348, 51, 52lspcl 20872 . . . . . . . . . . . 12 ((𝑉 ∈ LMod ∧ (𝑏𝑤) ⊆ (Base‘𝑉)) → ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉))
5442, 50, 53syl2anc 582 . . . . . . . . . . 11 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉))
55 eqid 2725 . . . . . . . . . . . 12 (𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) = (𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))
5651, 55reslmhm 20949 . . . . . . . . . . 11 ((𝐹 ∈ (𝑉 LMHom 𝑈) ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉)) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMHom 𝑈))
5732, 54, 56syl2anc 582 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMHom 𝑈))
58 eqid 2725 . . . . . . . . . . . 12 (LSubSp‘𝑈) = (LSubSp‘𝑈)
5929, 58reslmhm2b 20951 . . . . . . . . . . 11 ((𝑈 ∈ LMod ∧ ran 𝐹 ∈ (LSubSp‘𝑈) ∧ ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ⊆ ran 𝐹) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMHom 𝑈) ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMHom 𝐼)))
6059biimpa 475 . . . . . . . . . 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 20928 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝐹 ∈ (𝑉 GrpHom 𝑈))
6362ad4antlr 731 . . . . . . . . . . . . . . . 16 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝐹 ∈ (𝑉 GrpHom 𝑈))
6448, 23lbsss 20974 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ (LBasis‘𝑉) → 𝑏 ⊆ (Base‘𝑉))
6521, 64syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑏 ⊆ (Base‘𝑉))
6645, 65sstrd 3987 . . . . . . . . . . . . . . . . . 18 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ⊆ (Base‘𝑉))
6742, 66, 53syl2anc 582 . . . . . . . . . . . . . . . . 17 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉))
6851lsssubg 20853 . . . . . . . . . . . . . . . . 17 ((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉)) → ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (SubGrp‘𝑉))
6942, 67, 68syl2anc 582 . . . . . . . . . . . . . . . 16 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (SubGrp‘𝑉))
7055resghm 19195 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ (𝑉 GrpHom 𝑈) ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (SubGrp‘𝑉)) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) GrpHom 𝑈))
7163, 69, 70syl2anc 582 . . . . . . . . . . . . . . 15 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) GrpHom 𝑈))
72 eqid 2725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Base‘𝑈) = (Base‘𝑈)
7348, 72lmhmf 20931 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈))
7473ad4antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈))
7574ffnd 6724 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝐹 Fn (Base‘𝑉))
7648, 52lspssv 20879 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑉 ∈ LMod ∧ (𝑏𝑤) ⊆ (Base‘𝑉)) → ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉))
7742, 66, 76syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉))
7875, 77fnssresd 6680 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) Fn ((LSpan‘𝑉)‘(𝑏𝑤)))
79 fniniseg 7068 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) Fn ((LSpan‘𝑉)‘(𝑏𝑤)) → (𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }) ↔ (𝑥 ∈ ((LSpan‘𝑉)‘(𝑏𝑤)) ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘𝑥) = 0 )))
8079biimpa 475 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) Fn ((LSpan‘𝑉)‘(𝑏𝑤)) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → (𝑥 ∈ ((LSpan‘𝑉)‘(𝑏𝑤)) ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘𝑥) = 0 ))
8178, 80sylan 578 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → (𝑥 ∈ ((LSpan‘𝑉)‘(𝑏𝑤)) ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘𝑥) = 0 ))
8281simpld 493 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → 𝑥 ∈ ((LSpan‘𝑉)‘(𝑏𝑤)))
8375adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → 𝐹 Fn (Base‘𝑉))
8477adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉))
8584, 82sseldd 3977 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → 𝑥 ∈ (Base‘𝑉))
8682fvresd 6916 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘𝑥) = (𝐹𝑥))
8781simprd 494 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘𝑥) = 0 )
8886, 87eqtr3d 2767 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → (𝐹𝑥) = 0 )
89 fniniseg 7068 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 Fn (Base‘𝑉) → (𝑥 ∈ (𝐹 “ { 0 }) ↔ (𝑥 ∈ (Base‘𝑉) ∧ (𝐹𝑥) = 0 )))
9089biimpar 476 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 Fn (Base‘𝑉) ∧ (𝑥 ∈ (Base‘𝑉) ∧ (𝐹𝑥) = 0 )) → 𝑥 ∈ (𝐹 “ { 0 }))
9183, 85, 88, 90syl12anc 835 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → 𝑥 ∈ (𝐹 “ { 0 }))
9282, 91elind 4192 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → 𝑥 ∈ (((LSpan‘𝑉)‘(𝑏𝑤)) ∩ (𝐹 “ { 0 })))
93 simpr 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LBasis‘𝐾))
94 eqid 2725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Base‘𝐾) = (Base‘𝐾)
95 eqid 2725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (LSpan‘𝐾) = (LSpan‘𝐾)
9694, 4, 95lbssp 20976 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ∈ (LBasis‘𝐾) → ((LSpan‘𝐾)‘𝑤) = (Base‘𝐾))
9793, 96syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝐾)‘𝑤) = (Base‘𝐾))
9841ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑉 ∈ LMod)
99 eqid 2725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐹 “ { 0 }) = (𝐹 “ { 0 })
10099, 1, 51lmhmkerlss 20948 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹 ∈ (𝑉 LMHom 𝑈) → (𝐹 “ { 0 }) ∈ (LSubSp‘𝑉))
101100ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (𝐹 “ { 0 }) ∈ (LSubSp‘𝑉))
10294, 4lbsss 20974 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 ∈ (LBasis‘𝐾) → 𝑤 ⊆ (Base‘𝐾))
10393, 102syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ⊆ (Base‘𝐾))
104 cnvimass 6086 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐹 “ { 0 }) ⊆ dom 𝐹
105104, 73fssdm 6742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐹 ∈ (𝑉 LMHom 𝑈) → (𝐹 “ { 0 }) ⊆ (Base‘𝑉))
1062, 48ressbas2 17221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹 “ { 0 }) ⊆ (Base‘𝑉) → (𝐹 “ { 0 }) = (Base‘𝐾))
107105, 106syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐹 ∈ (𝑉 LMHom 𝑈) → (𝐹 “ { 0 }) = (Base‘𝐾))
108107ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (𝐹 “ { 0 }) = (Base‘𝐾))
109103, 108sseqtrrd 4018 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ⊆ (𝐹 “ { 0 }))
1102, 52, 95, 51lsslsp 20911 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑉 ∈ LMod ∧ (𝐹 “ { 0 }) ∈ (LSubSp‘𝑉) ∧ 𝑤 ⊆ (𝐹 “ { 0 })) → ((LSpan‘𝐾)‘𝑤) = ((LSpan‘𝑉)‘𝑤))
111110eqcomd 2731 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑉 ∈ LMod ∧ (𝐹 “ { 0 }) ∈ (LSubSp‘𝑉) ∧ 𝑤 ⊆ (𝐹 “ { 0 })) → ((LSpan‘𝑉)‘𝑤) = ((LSpan‘𝐾)‘𝑤))
11298, 101, 109, 111syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝑉)‘𝑤) = ((LSpan‘𝐾)‘𝑤))
11397, 112, 1083eqtr4d 2775 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝑉)‘𝑤) = (𝐹 “ { 0 }))
114113ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘𝑤) = (𝐹 “ { 0 }))
115114ineq2d 4210 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (((LSpan‘𝑉)‘(𝑏𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = (((LSpan‘𝑉)‘(𝑏𝑤)) ∩ (𝐹 “ { 0 })))
116 eqid 2725 . . . . . . . . . . . . . . . . . . . . . . . 24 (0g𝑉) = (0g𝑉)
11723, 52, 116lbsdiflsp0 33452 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑉 ∈ LVec ∧ 𝑏 ∈ (LBasis‘𝑉) ∧ 𝑤𝑏) → (((LSpan‘𝑉)‘(𝑏𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = {(0g𝑉)})
118117ad5ant145 1366 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (((LSpan‘𝑉)‘(𝑏𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = {(0g𝑉)})
119115, 118eqtr3d 2767 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (((LSpan‘𝑉)‘(𝑏𝑤)) ∩ (𝐹 “ { 0 })) = {(0g𝑉)})
120119adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → (((LSpan‘𝑉)‘(𝑏𝑤)) ∩ (𝐹 “ { 0 })) = {(0g𝑉)})
12192, 120eleqtrd 2827 . . . . . . . . . . . . . . . . . . 19 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → 𝑥 ∈ {(0g𝑉)})
122121ex 411 . . . . . . . . . . . . . . . . . 18 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }) → 𝑥 ∈ {(0g𝑉)}))
123122ssrdv 3982 . . . . . . . . . . . . . . . . 17 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }) ⊆ {(0g𝑉)})
124116, 48, 520ellsp 33180 . . . . . . . . . . . . . . . . . . . 20 ((𝑉 ∈ LMod ∧ (𝑏𝑤) ⊆ (Base‘𝑉)) → (0g𝑉) ∈ ((LSpan‘𝑉)‘(𝑏𝑤)))
12542, 66, 124syl2anc 582 . . . . . . . . . . . . . . . . . . 19 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (0g𝑉) ∈ ((LSpan‘𝑉)‘(𝑏𝑤)))
126 fvexd 6911 . . . . . . . . . . . . . . . . . . . 20 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) ∈ V)
127125fvresd 6916 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) = (𝐹‘(0g𝑉)))
128116, 1ghmid 19185 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 ∈ (𝑉 GrpHom 𝑈) → (𝐹‘(0g𝑉)) = 0 )
12962, 128syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹 ∈ (𝑉 LMHom 𝑈) → (𝐹‘(0g𝑉)) = 0 )
130129ad4antlr 731 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹‘(0g𝑉)) = 0 )
131127, 130eqtrd 2765 . . . . . . . . . . . . . . . . . . . 20 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) = 0 )
132 elsng 4644 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) ∈ V → (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) ∈ { 0 } ↔ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) = 0 ))
133132biimpar 476 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) ∈ V ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) = 0 ) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) ∈ { 0 })
134126, 131, 133syl2anc 582 . . . . . . . . . . . . . . . . . . 19 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) ∈ { 0 })
13578, 125, 134elpreimad 7067 . . . . . . . . . . . . . . . . . 18 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (0g𝑉) ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }))
136135snssd 4814 . . . . . . . . . . . . . . . . 17 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → {(0g𝑉)} ⊆ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }))
137123, 136eqssd 3994 . . . . . . . . . . . . . . . 16 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }) = {(0g𝑉)})
138 lmodgrp 20762 . . . . . . . . . . . . . . . . . . 19 (𝑉 ∈ LMod → 𝑉 ∈ Grp)
139 grpmnd 18905 . . . . . . . . . . . . . . . . . . 19 (𝑉 ∈ Grp → 𝑉 ∈ Mnd)
14042, 138, 1393syl 18 . . . . . . . . . . . . . . . . . 18 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑉 ∈ Mnd)
14155, 48, 116ress0g 18725 . . . . . . . . . . . . . . . . . 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 4642 . . . . . . . . . . . . . . . 16 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → {(0g𝑉)} = {(0g‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))})
144137, 143eqtrd 2765 . . . . . . . . . . . . . . 15 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }) = {(0g‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))})
145 eqid 2725 . . . . . . . . . . . . . . . . 17 (Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))) = (Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))
146 eqid 2725 . . . . . . . . . . . . . . . . 17 (0g‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))) = (0g‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))
147145, 72, 146, 1kerf1ghm 19210 . . . . . . . . . . . . . . . 16 ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) GrpHom 𝑈) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):(Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))–1-1→(Base‘𝑈) ↔ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }) = {(0g‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))}))
148147biimpar 476 . . . . . . . . . . . . . . 15 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) GrpHom 𝑈) ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }) = {(0g‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))}) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):(Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))–1-1→(Base‘𝑈))
14971, 144, 148syl2anc 582 . . . . . . . . . . . . . 14 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):(Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))–1-1→(Base‘𝑈))
150 eqidd 2726 . . . . . . . . . . . . . . 15 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) = (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))))
15155, 48ressbas2 17221 . . . . . . . . . . . . . . . 16 (((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉) → ((LSpan‘𝑉)‘(𝑏𝑤)) = (Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
15277, 151syl 17 . . . . . . . . . . . . . . 15 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) = (Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
153 eqidd 2726 . . . . . . . . . . . . . . 15 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (Base‘𝑈) = (Base‘𝑈))
154150, 152, 153f1eq123d 6830 . . . . . . . . . . . . . 14 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1→(Base‘𝑈) ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):(Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))–1-1→(Base‘𝑈)))
155149, 154mpbird 256 . . . . . . . . . . . . 13 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1→(Base‘𝑈))
156 f1ssr 6799 . . . . . . . . . . . . 13 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1→(Base‘𝑈) ∧ ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ⊆ ran 𝐹) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1→ran 𝐹)
157155, 40, 156syl2anc 582 . . . . . . . . . . . 12 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1→ran 𝐹)
158 f1f1orn 6849 . . . . . . . . . . . 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 782 . . . . . . . . . . . . . . . . . 18 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → (𝐹𝑥) = 𝑦)
16175ad6antr 734 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝐹 Fn (Base‘𝑉))
162 simpllr 774 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝑢 ∈ ((LSpan‘𝑉)‘𝑤))
163113ad8antr 738 . . . . . . . . . . . . . . . . . . . . . 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 7068 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹 Fn (Base‘𝑉) → (𝑢 ∈ (𝐹 “ { 0 }) ↔ (𝑢 ∈ (Base‘𝑉) ∧ (𝐹𝑢) = 0 )))
166165simplbda 498 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 Fn (Base‘𝑉) ∧ 𝑢 ∈ (𝐹 “ { 0 })) → (𝐹𝑢) = 0 )
167161, 164, 166syl2anc 582 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → (𝐹𝑢) = 0 )
168167oveq1d 7434 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → ((𝐹𝑢)(+g𝑈)(𝐹𝑣)) = ( 0 (+g𝑈)(𝐹𝑣)))
169 simpr 483 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝑥 = (𝑢(+g𝑉)𝑣))
170169fveq2d 6900 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → (𝐹𝑥) = (𝐹‘(𝑢(+g𝑉)𝑣)))
17163ad6antr 734 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝐹 ∈ (𝑉 GrpHom 𝑈))
17248, 52lspss 20880 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑉 ∈ LMod ∧ 𝑏 ⊆ (Base‘𝑉) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ ((LSpan‘𝑉)‘𝑏))
17342, 65, 18, 172syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ ((LSpan‘𝑉)‘𝑏))
17448, 23, 52lbssp 20976 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 ∈ (LBasis‘𝑉) → ((LSpan‘𝑉)‘𝑏) = (Base‘𝑉))
17521, 174syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘𝑏) = (Base‘𝑉))
176173, 175sseqtrd 4017 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉))
177176ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) → ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉))
178177ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉))
179178, 162sseldd 3977 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝑢 ∈ (Base‘𝑉))
18077ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) → ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉))
181180ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉))
182 simplr 767 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤)))
183181, 182sseldd 3977 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝑣 ∈ (Base‘𝑉))
184 eqid 2725 . . . . . . . . . . . . . . . . . . . . . 22 (+g𝑉) = (+g𝑉)
185 eqid 2725 . . . . . . . . . . . . . . . . . . . . . 22 (+g𝑈) = (+g𝑈)
18648, 184, 185ghmlin 19184 . . . . . . . . . . . . . . . . . . . . 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 2766 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → ((𝐹𝑢)(+g𝑈)(𝐹𝑣)) = (𝐹𝑥))
189 lmhmlvec2 33445 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝑈 ∈ LVec)
190189lvecgrpd 21005 . . . . . . . . . . . . . . . . . . . . 21 ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝑈 ∈ Grp)
191190ad9antr 740 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝑈 ∈ Grp)
19274ad6antr 734 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈))
193192, 183ffvelcdmd 7094 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → (𝐹𝑣) ∈ (Base‘𝑈))
19472, 185, 1, 191, 193grplidd 18934 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → ( 0 (+g𝑈)(𝐹𝑣)) = (𝐹𝑣))
195168, 188, 1943eqtr3d 2773 . . . . . . . . . . . . . . . . . 18 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → (𝐹𝑥) = (𝐹𝑣))
196160, 195eqtr3d 2767 . . . . . . . . . . . . . . . . 17 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝑦 = (𝐹𝑣))
197161, 183, 182fnfvimad 7246 . . . . . . . . . . . . . . . . 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 787 . . . . . . . . . . . . . . . . 17 ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) → 𝑉 ∈ LVec)
200 simplr 767 . . . . . . . . . . . . . . . . . 18 ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) → 𝑥 ∈ (Base‘𝑉))
201109ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑤 ⊆ (𝐹 “ { 0 }))
202105ad4antlr 731 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 “ { 0 }) ⊆ (Base‘𝑉))
203201, 202sstrd 3987 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑤 ⊆ (Base‘𝑉))
204 eqid 2725 . . . . . . . . . . . . . . . . . . . . . 22 (LSSum‘𝑉) = (LSSum‘𝑉)
20548, 52, 204lsmsp2 20984 . . . . . . . . . . . . . . . . . . . . 21 ((𝑉 ∈ LMod ∧ 𝑤 ⊆ (Base‘𝑉) ∧ (𝑏𝑤) ⊆ (Base‘𝑉)) → (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏𝑤))) = ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏𝑤))))
20642, 203, 66, 205syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏𝑤))) = ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏𝑤))))
20720fveq2d 6900 . . . . . . . . . . . . . . . . . . . 20 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏𝑤))) = ((LSpan‘𝑉)‘𝑏))
208206, 207, 1753eqtrrd 2770 . . . . . . . . . . . . . . . . . . 19 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (Base‘𝑉) = (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏𝑤))))
209208ad3antrrr 728 . . . . . . . . . . . . . . . . . 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 19607 . . . . . . . . . . . . . . . . . 18 ((𝑉 ∈ LVec ∧ ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉) ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉)) → (𝑥 ∈ (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏𝑤))) ↔ ∃𝑢 ∈ ((LSpan‘𝑉)‘𝑤)∃𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))𝑥 = (𝑢(+g𝑉)𝑣)))
212211biimpa 475 . . . . . . . . . . . . . . . . 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 3203 . . . . . . . . . . . . . . 15 ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏𝑤))))
215 fvelrnb 6958 . . . . . . . . . . . . . . . . 17 (𝐹 Fn (Base‘𝑉) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ (Base‘𝑉)(𝐹𝑥) = 𝑦))
216215biimpa 475 . . . . . . . . . . . . . . . 16 ((𝐹 Fn (Base‘𝑉) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑥 ∈ (Base‘𝑉)(𝐹𝑥) = 𝑦)
21775, 216sylan 578 . . . . . . . . . . . . . . 15 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑥 ∈ (Base‘𝑉)(𝐹𝑥) = 𝑦)
218214, 217r19.29a 3151 . . . . . . . . . . . . . 14 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏𝑤))))
21939, 218eqelssd 3998 . . . . . . . . . . . . 13 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 “ ((LSpan‘𝑉)‘(𝑏𝑤))) = ran 𝐹)
22037, 219eqtr3id 2779 . . . . . . . . . . . 12 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) = ran 𝐹)
221220f1oeq3d 6835 . . . . . . . . . . 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 582 . . . . . . . . . . . 12 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉))
224223, 151syl 17 . . . . . . . . . . 11 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) = (Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
225 frn 6730 . . . . . . . . . . . 12 (𝐹:(Base‘𝑉)⟶(Base‘𝑈) → ran 𝐹 ⊆ (Base‘𝑈))
22629, 72ressbas2 17221 . . . . . . . . . . . 12 (ran 𝐹 ⊆ (Base‘𝑈) → ran 𝐹 = (Base‘𝐼))
22732, 73, 225, 2264syl 19 . . . . . . . . . . 11 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ran 𝐹 = (Base‘𝐼))
228150, 224, 227f1oeq123d 6832 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1-onto→ran 𝐹 ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):(Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))–1-1-onto→(Base‘𝐼)))
229222, 228mpbid 231 . . . . . . . . 9 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):(Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))–1-1-onto→(Base‘𝐼))
230 eqid 2725 . . . . . . . . . 10 (Base‘𝐼) = (Base‘𝐼)
231145, 230islmim 20959 . . . . . . . . 9 ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMIso 𝐼) ↔ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMHom 𝐼) ∧ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):(Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))–1-1-onto→(Base‘𝐼)))
23261, 229, 231sylanbrc 581 . . . . . . . 8 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMIso 𝐼))
23348, 52lspssid 20881 . . . . . . . . . . 11 ((𝑉 ∈ LMod ∧ (𝑏𝑤) ⊆ (Base‘𝑉)) → (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤)))
23442, 50, 233syl2anc 582 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤)))
23551, 55lsslinds 21782 . . . . . . . . . . 11 ((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤))) → ((𝑏𝑤) ∈ (LIndS‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))) ↔ (𝑏𝑤) ∈ (LIndS‘𝑉)))
236235biimpar 476 . . . . . . . . . 10 (((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ (𝑏𝑤) ∈ (LIndS‘𝑉)) → (𝑏𝑤) ∈ (LIndS‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
23742, 67, 234, 47, 236syl31anc 1370 . . . . . . . . 9 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ∈ (LIndS‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
238 eqid 2725 . . . . . . . . . . . . 13 (LSpan‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))) = (LSpan‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))
23955, 52, 238, 51lsslsp 20911 . . . . . . . . . . . 12 ((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤))) → ((LSpan‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))‘(𝑏𝑤)) = ((LSpan‘𝑉)‘(𝑏𝑤)))
240239eqcomd 2731 . . . . . . . . . . 11 ((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤))) → ((LSpan‘𝑉)‘(𝑏𝑤)) = ((LSpan‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))‘(𝑏𝑤)))
24142, 54, 234, 240syl3anc 1368 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) = ((LSpan‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))‘(𝑏𝑤)))
242241, 224eqtr3d 2767 . . . . . . . . 9 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))‘(𝑏𝑤)) = (Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
243 eqid 2725 . . . . . . . . . 10 (LBasis‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))) = (LBasis‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))
244145, 243, 238islbs4 21783 . . . . . . . . 9 ((𝑏𝑤) ∈ (LBasis‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))) ↔ ((𝑏𝑤) ∈ (LIndS‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))) ∧ ((LSpan‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))‘(𝑏𝑤)) = (Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))))
245237, 242, 244sylanbrc 581 . . . . . . . 8 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ∈ (LBasis‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
246 eqid 2725 . . . . . . . . 9 (LBasis‘𝐼) = (LBasis‘𝐼)
247243, 246lmimlbs 21787 . . . . . . . 8 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMIso 𝐼) ∧ (𝑏𝑤) ∈ (LBasis‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤)) ∈ (LBasis‘𝐼))
248232, 245, 247syl2anc 582 . . . . . . 7 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤)) ∈ (LBasis‘𝐼))
249246dimval 33426 . . . . . . 7 ((𝐼 ∈ LVec ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤)) ∈ (LBasis‘𝐼)) → (dim‘𝐼) = (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤))))
25031, 248, 249syl2anc 582 . . . . . 6 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (dim‘𝐼) = (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤))))
251 f1imaeng 9035 . . . . . . . 8 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1→ran 𝐹 ∧ (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤)) ∧ (𝑏𝑤) ∈ (LIndS‘𝑉)) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤)) ≈ (𝑏𝑤))
252 hasheni 14343 . . . . . . . 8 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤)) ≈ (𝑏𝑤) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤))) = (♯‘(𝑏𝑤)))
253251, 252syl 17 . . . . . . 7 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1→ran 𝐹 ∧ (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤)) ∧ (𝑏𝑤) ∈ (LIndS‘𝑉)) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤))) = (♯‘(𝑏𝑤)))
254157, 234, 47, 253syl3anc 1368 . . . . . 6 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤))) = (♯‘(𝑏𝑤)))
255250, 254eqtrd 2765 . . . . 5 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (dim‘𝐼) = (♯‘(𝑏𝑤)))
25628, 255oveq12d 7437 . . . 4 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((dim‘𝐾) +𝑒 (dim‘𝐼)) = ((♯‘𝑤) +𝑒 (♯‘(𝑏𝑤))))
25716, 25, 2563eqtr4d 2775 . . 3 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼)))
2584lbslinds 21784 . . . . . 6 (LBasis‘𝐾) ⊆ (LIndS‘𝐾)
259258, 93sselid 3974 . . . . 5 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LIndS‘𝐾))
26051, 2lsslinds 21782 . . . . . 6 ((𝑉 ∈ LMod ∧ (𝐹 “ { 0 }) ∈ (LSubSp‘𝑉) ∧ 𝑤 ⊆ (𝐹 “ { 0 })) → (𝑤 ∈ (LIndS‘𝐾) ↔ 𝑤 ∈ (LIndS‘𝑉)))
261260biimpa 475 . . . . 5 (((𝑉 ∈ LMod ∧ (𝐹 “ { 0 }) ∈ (LSubSp‘𝑉) ∧ 𝑤 ⊆ (𝐹 “ { 0 })) ∧ 𝑤 ∈ (LIndS‘𝐾)) → 𝑤 ∈ (LIndS‘𝑉))
26298, 101, 109, 259, 261syl31anc 1370 . . . 4 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LIndS‘𝑉))
26323islinds4 21786 . . . . 5 (𝑉 ∈ LVec → (𝑤 ∈ (LIndS‘𝑉) ↔ ∃𝑏 ∈ (LBasis‘𝑉)𝑤𝑏))
264263ad2antrr 724 . . . 4 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (𝑤 ∈ (LIndS‘𝑉) ↔ ∃𝑏 ∈ (LBasis‘𝑉)𝑤𝑏))
265262, 264mpbid 231 . . 3 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ∃𝑏 ∈ (LBasis‘𝑉)𝑤𝑏)
266257, 265r19.29a 3151 . 2 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼)))
2678, 266exlimddv 1930 1 ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wex 1773  wcel 2098  wne 2929  wrex 3059  Vcvv 3461  cdif 3941  cun 3942  cin 3943  wss 3944  c0 4322  {csn 4630   class class class wbr 5149  ccnv 5677  ran crn 5679  cres 5680  cima 5681   Fn wfn 6544  wf 6545  1-1wf1 6546  1-1-ontowf1o 6548  cfv 6549  (class class class)co 7419  cen 8961   +𝑒 cxad 13125  chash 14325  Basecbs 17183  s cress 17212  +gcplusg 17236  0gc0g 17424  Mndcmnd 18697  Grpcgrp 18898  SubGrpcsubg 19083   GrpHom cghm 19175  LSSumclsm 19601  LModclmod 20755  LSubSpclss 20827  LSpanclspn 20867   LMHom clmhm 20916   LMIso clmim 20917  LBasisclbs 20971  LVecclvec 20999  LIndSclinds 21756  dimcldim 33424
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 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-reg 9617  ax-inf2 9666  ax-ac2 10488  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-iin 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-isom 6558  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-of 7685  df-rpss 7729  df-om 7872  df-1st 7994  df-2nd 7995  df-supp 8166  df-tpos 8232  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-oadd 8491  df-er 8725  df-map 8847  df-ixp 8917  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fsupp 9388  df-sup 9467  df-oi 9535  df-r1 9789  df-rank 9790  df-dju 9926  df-card 9964  df-acn 9967  df-ac 10141  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-nn 12246  df-2 12308  df-3 12309  df-4 12310  df-5 12311  df-6 12312  df-7 12313  df-8 12314  df-9 12315  df-n0 12506  df-xnn0 12578  df-z 12592  df-dec 12711  df-uz 12856  df-xadd 13128  df-fz 13520  df-fzo 13663  df-seq 14003  df-hash 14326  df-struct 17119  df-sets 17136  df-slot 17154  df-ndx 17166  df-base 17184  df-ress 17213  df-plusg 17249  df-mulr 17250  df-sca 17252  df-vsca 17253  df-ip 17254  df-tset 17255  df-ple 17256  df-ocomp 17257  df-ds 17258  df-hom 17260  df-cco 17261  df-0g 17426  df-gsum 17427  df-prds 17432  df-pws 17434  df-mre 17569  df-mrc 17570  df-mri 17571  df-acs 17572  df-proset 18290  df-drs 18291  df-poset 18308  df-ipo 18523  df-mgm 18603  df-sgrp 18682  df-mnd 18698  df-mhm 18743  df-submnd 18744  df-grp 18901  df-minusg 18902  df-sbg 18903  df-mulg 19032  df-subg 19086  df-ghm 19176  df-cntz 19280  df-lsm 19603  df-cmn 19749  df-abl 19750  df-mgp 20087  df-rng 20105  df-ur 20134  df-ring 20187  df-oppr 20285  df-dvdsr 20308  df-unit 20309  df-invr 20339  df-nzr 20464  df-subrg 20520  df-drng 20638  df-lmod 20757  df-lss 20828  df-lsp 20868  df-lmhm 20919  df-lmim 20920  df-lbs 20972  df-lvec 21000  df-sra 21070  df-rgmod 21071  df-dsmm 21683  df-frlm 21698  df-uvc 21734  df-lindf 21757  df-linds 21758  df-dim 33425
This theorem is referenced by:  qusdimsum  33454
  Copyright terms: Public domain W3C validator