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 32004
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 31999 . . . 4 ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝐾 ∈ LVec)
4 eqid 2737 . . . . 5 (LBasis‘𝐾) = (LBasis‘𝐾)
54lbsex 20532 . . . 4 (𝐾 ∈ LVec → (LBasis‘𝐾) ≠ ∅)
63, 5syl 17 . . 3 ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → (LBasis‘𝐾) ≠ ∅)
7 n0 4297 . . 3 ((LBasis‘𝐾) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ (LBasis‘𝐾))
86, 7sylib 217 . 2 ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → ∃𝑤 𝑤 ∈ (LBasis‘𝐾))
9 simpllr 774 . . . . 5 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑤 ∈ (LBasis‘𝐾))
10 vex 3446 . . . . . . 7 𝑏 ∈ V
1110difexi 5276 . . . . . 6 (𝑏𝑤) ∈ V
1211a1i 11 . . . . 5 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ∈ V)
13 disjdif 4422 . . . . . 6 (𝑤 ∩ (𝑏𝑤)) = ∅
1413a1i 11 . . . . 5 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑤 ∩ (𝑏𝑤)) = ∅)
15 hashunx 14205 . . . . 5 ((𝑤 ∈ (LBasis‘𝐾) ∧ (𝑏𝑤) ∈ V ∧ (𝑤 ∩ (𝑏𝑤)) = ∅) → (♯‘(𝑤 ∪ (𝑏𝑤))) = ((♯‘𝑤) +𝑒 (♯‘(𝑏𝑤))))
169, 12, 14, 15syl3anc 1371 . . . 4 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (♯‘(𝑤 ∪ (𝑏𝑤))) = ((♯‘𝑤) +𝑒 (♯‘(𝑏𝑤))))
17 simp-4l 781 . . . . 5 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑉 ∈ LVec)
18 simpr 486 . . . . . . 7 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑤𝑏)
19 undif 4432 . . . . . . 7 (𝑤𝑏 ↔ (𝑤 ∪ (𝑏𝑤)) = 𝑏)
2018, 19sylib 217 . . . . . 6 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑤 ∪ (𝑏𝑤)) = 𝑏)
21 simplr 767 . . . . . 6 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑏 ∈ (LBasis‘𝑉))
2220, 21eqeltrd 2838 . . . . 5 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑤 ∪ (𝑏𝑤)) ∈ (LBasis‘𝑉))
23 eqid 2737 . . . . . 6 (LBasis‘𝑉) = (LBasis‘𝑉)
2423dimval 31982 . . . . 5 ((𝑉 ∈ LVec ∧ (𝑤 ∪ (𝑏𝑤)) ∈ (LBasis‘𝑉)) → (dim‘𝑉) = (♯‘(𝑤 ∪ (𝑏𝑤))))
2517, 22, 24syl2anc 585 . . . 4 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (dim‘𝑉) = (♯‘(𝑤 ∪ (𝑏𝑤))))
263ad3antrrr 728 . . . . . 6 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝐾 ∈ LVec)
274dimval 31982 . . . . . 6 ((𝐾 ∈ LVec ∧ 𝑤 ∈ (LBasis‘𝐾)) → (dim‘𝐾) = (♯‘𝑤))
2826, 9, 27syl2anc 585 . . . . 5 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (dim‘𝐾) = (♯‘𝑤))
29 dimkerim.i . . . . . . . . 9 𝐼 = (𝑈s ran 𝐹)
3029imlmhm 32000 . . . . . . . 8 ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝐼 ∈ LVec)
3130ad3antrrr 728 . . . . . . 7 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝐼 ∈ LVec)
32 simp-4r 782 . . . . . . . . . . 11 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝐹 ∈ (𝑉 LMHom 𝑈))
33 lmhmlmod2 20399 . . . . . . . . . . 11 (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝑈 ∈ LMod)
3432, 33syl 17 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑈 ∈ LMod)
35 lmhmrnlss 20417 . . . . . . . . . . 11 (𝐹 ∈ (𝑉 LMHom 𝑈) → ran 𝐹 ∈ (LSubSp‘𝑈))
3632, 35syl 17 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ran 𝐹 ∈ (LSubSp‘𝑈))
37 df-ima 5637 . . . . . . . . . . 11 (𝐹 “ ((LSpan‘𝑉)‘(𝑏𝑤))) = ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))
38 imassrn 6014 . . . . . . . . . . . 12 (𝐹 “ ((LSpan‘𝑉)‘(𝑏𝑤))) ⊆ ran 𝐹
3938a1i 11 . . . . . . . . . . 11 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 “ ((LSpan‘𝑉)‘(𝑏𝑤))) ⊆ ran 𝐹)
4037, 39eqsstrrid 3984 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ⊆ ran 𝐹)
41 lveclmod 20473 . . . . . . . . . . . . 13 (𝑉 ∈ LVec → 𝑉 ∈ LMod)
4241ad4antr 730 . . . . . . . . . . . 12 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑉 ∈ LMod)
4323lbslinds 21145 . . . . . . . . . . . . . . 15 (LBasis‘𝑉) ⊆ (LIndS‘𝑉)
4443, 21sselid 3933 . . . . . . . . . . . . . 14 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑏 ∈ (LIndS‘𝑉))
45 difssd 4083 . . . . . . . . . . . . . 14 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ⊆ 𝑏)
46 lindsss 21136 . . . . . . . . . . . . . 14 ((𝑉 ∈ LMod ∧ 𝑏 ∈ (LIndS‘𝑉) ∧ (𝑏𝑤) ⊆ 𝑏) → (𝑏𝑤) ∈ (LIndS‘𝑉))
4742, 44, 45, 46syl3anc 1371 . . . . . . . . . . . . 13 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ∈ (LIndS‘𝑉))
48 eqid 2737 . . . . . . . . . . . . . 14 (Base‘𝑉) = (Base‘𝑉)
4948linds1 21122 . . . . . . . . . . . . 13 ((𝑏𝑤) ∈ (LIndS‘𝑉) → (𝑏𝑤) ⊆ (Base‘𝑉))
5047, 49syl 17 . . . . . . . . . . . 12 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ⊆ (Base‘𝑉))
51 eqid 2737 . . . . . . . . . . . . 13 (LSubSp‘𝑉) = (LSubSp‘𝑉)
52 eqid 2737 . . . . . . . . . . . . 13 (LSpan‘𝑉) = (LSpan‘𝑉)
5348, 51, 52lspcl 20343 . . . . . . . . . . . 12 ((𝑉 ∈ LMod ∧ (𝑏𝑤) ⊆ (Base‘𝑉)) → ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉))
5442, 50, 53syl2anc 585 . . . . . . . . . . 11 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉))
55 eqid 2737 . . . . . . . . . . . 12 (𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) = (𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))
5651, 55reslmhm 20419 . . . . . . . . . . 11 ((𝐹 ∈ (𝑉 LMHom 𝑈) ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉)) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMHom 𝑈))
5732, 54, 56syl2anc 585 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMHom 𝑈))
58 eqid 2737 . . . . . . . . . . . 12 (LSubSp‘𝑈) = (LSubSp‘𝑈)
5929, 58reslmhm2b 20421 . . . . . . . . . . 11 ((𝑈 ∈ LMod ∧ ran 𝐹 ∈ (LSubSp‘𝑈) ∧ ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ⊆ ran 𝐹) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMHom 𝑈) ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMHom 𝐼)))
6059biimpa 478 . . . . . . . . . 10 (((𝑈 ∈ LMod ∧ ran 𝐹 ∈ (LSubSp‘𝑈) ∧ ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ⊆ ran 𝐹) ∧ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMHom 𝑈)) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMHom 𝐼))
6134, 36, 40, 57, 60syl31anc 1373 . . . . . . . . 9 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMHom 𝐼))
62 lmghm 20398 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝐹 ∈ (𝑉 GrpHom 𝑈))
6362ad4antlr 731 . . . . . . . . . . . . . . . 16 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝐹 ∈ (𝑉 GrpHom 𝑈))
6448, 23lbsss 20444 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ (LBasis‘𝑉) → 𝑏 ⊆ (Base‘𝑉))
6521, 64syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑏 ⊆ (Base‘𝑉))
6645, 65sstrd 3945 . . . . . . . . . . . . . . . . . 18 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ⊆ (Base‘𝑉))
6742, 66, 53syl2anc 585 . . . . . . . . . . . . . . . . 17 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉))
6851lsssubg 20324 . . . . . . . . . . . . . . . . 17 ((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉)) → ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (SubGrp‘𝑉))
6942, 67, 68syl2anc 585 . . . . . . . . . . . . . . . 16 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (SubGrp‘𝑉))
7055resghm 18946 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ (𝑉 GrpHom 𝑈) ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (SubGrp‘𝑉)) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) GrpHom 𝑈))
7163, 69, 70syl2anc 585 . . . . . . . . . . . . . . 15 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) GrpHom 𝑈))
72 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Base‘𝑈) = (Base‘𝑈)
7348, 72lmhmf 20401 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈))
7473ad4antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈))
7574ffnd 6656 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝐹 Fn (Base‘𝑉))
7648, 52lspssv 20350 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑉 ∈ LMod ∧ (𝑏𝑤) ⊆ (Base‘𝑉)) → ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉))
7742, 66, 76syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉))
78 fnssres 6611 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 Fn (Base‘𝑉) ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉)) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) Fn ((LSpan‘𝑉)‘(𝑏𝑤)))
7975, 77, 78syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) Fn ((LSpan‘𝑉)‘(𝑏𝑤)))
80 fniniseg 6997 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) Fn ((LSpan‘𝑉)‘(𝑏𝑤)) → (𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }) ↔ (𝑥 ∈ ((LSpan‘𝑉)‘(𝑏𝑤)) ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘𝑥) = 0 )))
8180biimpa 478 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) Fn ((LSpan‘𝑉)‘(𝑏𝑤)) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → (𝑥 ∈ ((LSpan‘𝑉)‘(𝑏𝑤)) ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘𝑥) = 0 ))
8279, 81sylan 581 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → (𝑥 ∈ ((LSpan‘𝑉)‘(𝑏𝑤)) ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘𝑥) = 0 ))
8382simpld 496 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → 𝑥 ∈ ((LSpan‘𝑉)‘(𝑏𝑤)))
8475adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → 𝐹 Fn (Base‘𝑉))
8577adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉))
8685, 83sseldd 3936 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → 𝑥 ∈ (Base‘𝑉))
8783fvresd 6849 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘𝑥) = (𝐹𝑥))
8882simprd 497 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘𝑥) = 0 )
8987, 88eqtr3d 2779 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → (𝐹𝑥) = 0 )
90 fniniseg 6997 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 Fn (Base‘𝑉) → (𝑥 ∈ (𝐹 “ { 0 }) ↔ (𝑥 ∈ (Base‘𝑉) ∧ (𝐹𝑥) = 0 )))
9190biimpar 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 Fn (Base‘𝑉) ∧ (𝑥 ∈ (Base‘𝑉) ∧ (𝐹𝑥) = 0 )) → 𝑥 ∈ (𝐹 “ { 0 }))
9284, 86, 89, 91syl12anc 835 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → 𝑥 ∈ (𝐹 “ { 0 }))
9383, 92elind 4145 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → 𝑥 ∈ (((LSpan‘𝑉)‘(𝑏𝑤)) ∩ (𝐹 “ { 0 })))
94 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LBasis‘𝐾))
95 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (Base‘𝐾) = (Base‘𝐾)
96 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (LSpan‘𝐾) = (LSpan‘𝐾)
9795, 4, 96lbssp 20446 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ∈ (LBasis‘𝐾) → ((LSpan‘𝐾)‘𝑤) = (Base‘𝐾))
9894, 97syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝐾)‘𝑤) = (Base‘𝐾))
9941ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑉 ∈ LMod)
100 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐹 “ { 0 }) = (𝐹 “ { 0 })
101100, 1, 51lmhmkerlss 20418 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹 ∈ (𝑉 LMHom 𝑈) → (𝐹 “ { 0 }) ∈ (LSubSp‘𝑉))
102101ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (𝐹 “ { 0 }) ∈ (LSubSp‘𝑉))
10395, 4lbsss 20444 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 ∈ (LBasis‘𝐾) → 𝑤 ⊆ (Base‘𝐾))
10494, 103syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ⊆ (Base‘𝐾))
105 cnvimass 6023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐹 “ { 0 }) ⊆ dom 𝐹
106105, 73fssdm 6675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐹 ∈ (𝑉 LMHom 𝑈) → (𝐹 “ { 0 }) ⊆ (Base‘𝑉))
1072, 48ressbas2 17046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹 “ { 0 }) ⊆ (Base‘𝑉) → (𝐹 “ { 0 }) = (Base‘𝐾))
108106, 107syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐹 ∈ (𝑉 LMHom 𝑈) → (𝐹 “ { 0 }) = (Base‘𝐾))
109108ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (𝐹 “ { 0 }) = (Base‘𝐾))
110104, 109sseqtrrd 3976 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ⊆ (𝐹 “ { 0 }))
1112, 52, 96, 51lsslsp 20382 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑉 ∈ LMod ∧ (𝐹 “ { 0 }) ∈ (LSubSp‘𝑉) ∧ 𝑤 ⊆ (𝐹 “ { 0 })) → ((LSpan‘𝑉)‘𝑤) = ((LSpan‘𝐾)‘𝑤))
11299, 102, 110, 111syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝑉)‘𝑤) = ((LSpan‘𝐾)‘𝑤))
11398, 112, 1093eqtr4d 2787 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝑉)‘𝑤) = (𝐹 “ { 0 }))
114113ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘𝑤) = (𝐹 “ { 0 }))
115114ineq2d 4163 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (((LSpan‘𝑉)‘(𝑏𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = (((LSpan‘𝑉)‘(𝑏𝑤)) ∩ (𝐹 “ { 0 })))
116 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . 24 (0g𝑉) = (0g𝑉)
11723, 52, 116lbsdiflsp0 32003 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑉 ∈ LVec ∧ 𝑏 ∈ (LBasis‘𝑉) ∧ 𝑤𝑏) → (((LSpan‘𝑉)‘(𝑏𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = {(0g𝑉)})
118117ad5ant145 1369 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (((LSpan‘𝑉)‘(𝑏𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = {(0g𝑉)})
119115, 118eqtr3d 2779 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (((LSpan‘𝑉)‘(𝑏𝑤)) ∩ (𝐹 “ { 0 })) = {(0g𝑉)})
120119adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → (((LSpan‘𝑉)‘(𝑏𝑤)) ∩ (𝐹 “ { 0 })) = {(0g𝑉)})
12193, 120eleqtrd 2840 . . . . . . . . . . . . . . . . . . 19 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 })) → 𝑥 ∈ {(0g𝑉)})
122121ex 414 . . . . . . . . . . . . . . . . . 18 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑥 ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }) → 𝑥 ∈ {(0g𝑉)}))
123122ssrdv 3941 . . . . . . . . . . . . . . . . 17 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }) ⊆ {(0g𝑉)})
124116, 48, 520ellsp 31860 . . . . . . . . . . . . . . . . . . . 20 ((𝑉 ∈ LMod ∧ (𝑏𝑤) ⊆ (Base‘𝑉)) → (0g𝑉) ∈ ((LSpan‘𝑉)‘(𝑏𝑤)))
12542, 66, 124syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (0g𝑉) ∈ ((LSpan‘𝑉)‘(𝑏𝑤)))
126 fvexd 6844 . . . . . . . . . . . . . . . . . . . 20 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) ∈ V)
127125fvresd 6849 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) = (𝐹‘(0g𝑉)))
128116, 1ghmid 18936 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 ∈ (𝑉 GrpHom 𝑈) → (𝐹‘(0g𝑉)) = 0 )
12962, 128syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹 ∈ (𝑉 LMHom 𝑈) → (𝐹‘(0g𝑉)) = 0 )
130129ad4antlr 731 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹‘(0g𝑉)) = 0 )
131127, 130eqtrd 2777 . . . . . . . . . . . . . . . . . . . 20 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) = 0 )
132 elsng 4591 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) ∈ V → (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) ∈ { 0 } ↔ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) = 0 ))
133132biimpar 479 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) ∈ V ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) = 0 ) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) ∈ { 0 })
134126, 131, 133syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤)))‘(0g𝑉)) ∈ { 0 })
13579, 125, 134elpreimad 6996 . . . . . . . . . . . . . . . . . 18 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (0g𝑉) ∈ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }))
136135snssd 4760 . . . . . . . . . . . . . . . . 17 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → {(0g𝑉)} ⊆ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }))
137123, 136eqssd 3952 . . . . . . . . . . . . . . . 16 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }) = {(0g𝑉)})
138 lmodgrp 20235 . . . . . . . . . . . . . . . . . . 19 (𝑉 ∈ LMod → 𝑉 ∈ Grp)
139 grpmnd 18680 . . . . . . . . . . . . . . . . . . 19 (𝑉 ∈ Grp → 𝑉 ∈ Mnd)
14042, 138, 1393syl 18 . . . . . . . . . . . . . . . . . 18 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑉 ∈ Mnd)
14155, 48, 116ress0g 18510 . . . . . . . . . . . . . . . . . 18 ((𝑉 ∈ Mnd ∧ (0g𝑉) ∈ ((LSpan‘𝑉)‘(𝑏𝑤)) ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉)) → (0g𝑉) = (0g‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
142140, 125, 77, 141syl3anc 1371 . . . . . . . . . . . . . . . . 17 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (0g𝑉) = (0g‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
143142sneqd 4589 . . . . . . . . . . . . . . . 16 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → {(0g𝑉)} = {(0g‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))})
144137, 143eqtrd 2777 . . . . . . . . . . . . . . 15 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }) = {(0g‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))})
145 eqid 2737 . . . . . . . . . . . . . . . . 17 (Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))) = (Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))
146 eqid 2737 . . . . . . . . . . . . . . . . 17 (0g‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))) = (0g‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))
147145, 72, 146, 1kerf1ghm 20084 . . . . . . . . . . . . . . . 16 ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) GrpHom 𝑈) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):(Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))–1-1→(Base‘𝑈) ↔ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }) = {(0g‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))}))
148147biimpar 479 . . . . . . . . . . . . . . 15 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) GrpHom 𝑈) ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ { 0 }) = {(0g‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))}) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):(Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))–1-1→(Base‘𝑈))
14971, 144, 148syl2anc 585 . . . . . . . . . . . . . 14 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):(Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))–1-1→(Base‘𝑈))
150 eqidd 2738 . . . . . . . . . . . . . . 15 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) = (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))))
15155, 48ressbas2 17046 . . . . . . . . . . . . . . . 16 (((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉) → ((LSpan‘𝑉)‘(𝑏𝑤)) = (Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
15277, 151syl 17 . . . . . . . . . . . . . . 15 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) = (Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
153 eqidd 2738 . . . . . . . . . . . . . . 15 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (Base‘𝑈) = (Base‘𝑈))
154150, 152, 153f1eq123d 6763 . . . . . . . . . . . . . 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 6732 . . . . . . . . . . . . 13 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1→(Base‘𝑈) ∧ ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ⊆ ran 𝐹) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1→ran 𝐹)
157155, 40, 156syl2anc 585 . . . . . . . . . . . 12 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1→ran 𝐹)
158 f1f1orn 6782 . . . . . . . . . . . 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 2840 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝑢 ∈ (𝐹 “ { 0 }))
165 fniniseg 6997 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹 Fn (Base‘𝑉) → (𝑢 ∈ (𝐹 “ { 0 }) ↔ (𝑢 ∈ (Base‘𝑉) ∧ (𝐹𝑢) = 0 )))
166165simplbda 501 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 Fn (Base‘𝑉) ∧ 𝑢 ∈ (𝐹 “ { 0 })) → (𝐹𝑢) = 0 )
167161, 164, 166syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → (𝐹𝑢) = 0 )
168167oveq1d 7356 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → ((𝐹𝑢)(+g𝑈)(𝐹𝑣)) = ( 0 (+g𝑈)(𝐹𝑣)))
169 simpr 486 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝑥 = (𝑢(+g𝑉)𝑣))
170169fveq2d 6833 . . . . . . . . . . . . . . . . . . . 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 20351 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑉 ∈ LMod ∧ 𝑏 ⊆ (Base‘𝑉) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ ((LSpan‘𝑉)‘𝑏))
17342, 65, 18, 172syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ ((LSpan‘𝑉)‘𝑏))
17448, 23, 52lbssp 20446 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏 ∈ (LBasis‘𝑉) → ((LSpan‘𝑉)‘𝑏) = (Base‘𝑉))
17521, 174syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘𝑏) = (Base‘𝑉))
176173, 175sseqtrd 3975 . . . . . . . . . . . . . . . . . . . . . . . 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 3936 . . . . . . . . . . . . . . . . . . . . 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 3936 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝑣 ∈ (Base‘𝑉))
184 eqid 2737 . . . . . . . . . . . . . . . . . . . . . 22 (+g𝑉) = (+g𝑉)
185 eqid 2737 . . . . . . . . . . . . . . . . . . . . . 22 (+g𝑈) = (+g𝑈)
18648, 184, 185ghmlin 18935 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 ∈ (𝑉 GrpHom 𝑈) ∧ 𝑢 ∈ (Base‘𝑉) ∧ 𝑣 ∈ (Base‘𝑉)) → (𝐹‘(𝑢(+g𝑉)𝑣)) = ((𝐹𝑢)(+g𝑈)(𝐹𝑣)))
187171, 179, 183, 186syl3anc 1371 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → (𝐹‘(𝑢(+g𝑉)𝑣)) = ((𝐹𝑢)(+g𝑈)(𝐹𝑣)))
188170, 187eqtr2d 2778 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → ((𝐹𝑢)(+g𝑈)(𝐹𝑣)) = (𝐹𝑥))
189 lmhmlvec2 31998 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝑈 ∈ LVec)
190 lveclmod 20473 . . . . . . . . . . . . . . . . . . . . . 22 (𝑈 ∈ LVec → 𝑈 ∈ LMod)
191 lmodgrp 20235 . . . . . . . . . . . . . . . . . . . . . 22 (𝑈 ∈ LMod → 𝑈 ∈ Grp)
192189, 190, 1913syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝑈 ∈ Grp)
193192ad9antr 740 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝑈 ∈ Grp)
19474ad6antr 734 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈))
195194, 183ffvelcdmd 7022 . . . . . . . . . . . . . . . . . . . 20 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → (𝐹𝑣) ∈ (Base‘𝑈))
19672, 185, 1grplid 18705 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 ∈ Grp ∧ (𝐹𝑣) ∈ (Base‘𝑈)) → ( 0 (+g𝑈)(𝐹𝑣)) = (𝐹𝑣))
197193, 195, 196syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → ( 0 (+g𝑈)(𝐹𝑣)) = (𝐹𝑣))
198168, 188, 1973eqtr3d 2785 . . . . . . . . . . . . . . . . . 18 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → (𝐹𝑥) = (𝐹𝑣))
199160, 198eqtr3d 2779 . . . . . . . . . . . . . . . . 17 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝑦 = (𝐹𝑣))
200161, 183, 182fnfvimad 7170 . . . . . . . . . . . . . . . . 17 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → (𝐹𝑣) ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏𝑤))))
201199, 200eqeltrd 2838 . . . . . . . . . . . . . . . 16 (((((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ 𝑥 = (𝑢(+g𝑉)𝑣)) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏𝑤))))
202 simp-7l 787 . . . . . . . . . . . . . . . . 17 ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) → 𝑉 ∈ LVec)
203 simplr 767 . . . . . . . . . . . . . . . . . 18 ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) → 𝑥 ∈ (Base‘𝑉))
204110ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑤 ⊆ (𝐹 “ { 0 }))
205106ad4antlr 731 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 “ { 0 }) ⊆ (Base‘𝑉))
206204, 205sstrd 3945 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → 𝑤 ⊆ (Base‘𝑉))
207 eqid 2737 . . . . . . . . . . . . . . . . . . . . . 22 (LSSum‘𝑉) = (LSSum‘𝑉)
20848, 52, 207lsmsp2 20454 . . . . . . . . . . . . . . . . . . . . 21 ((𝑉 ∈ LMod ∧ 𝑤 ⊆ (Base‘𝑉) ∧ (𝑏𝑤) ⊆ (Base‘𝑉)) → (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏𝑤))) = ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏𝑤))))
20942, 206, 66, 208syl3anc 1371 . . . . . . . . . . . . . . . . . . . 20 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏𝑤))) = ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏𝑤))))
21020fveq2d 6833 . . . . . . . . . . . . . . . . . . . 20 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏𝑤))) = ((LSpan‘𝑉)‘𝑏))
211209, 210, 1753eqtrrd 2782 . . . . . . . . . . . . . . . . . . 19 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (Base‘𝑉) = (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏𝑤))))
212211ad3antrrr 728 . . . . . . . . . . . . . . . . . 18 ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) → (Base‘𝑉) = (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏𝑤))))
213203, 212eleqtrd 2840 . . . . . . . . . . . . . . . . 17 ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) → 𝑥 ∈ (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏𝑤))))
21448, 184, 207lsmelvalx 19341 . . . . . . . . . . . . . . . . . 18 ((𝑉 ∈ LVec ∧ ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉) ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉)) → (𝑥 ∈ (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏𝑤))) ↔ ∃𝑢 ∈ ((LSpan‘𝑉)‘𝑤)∃𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))𝑥 = (𝑢(+g𝑉)𝑣)))
215214biimpa 478 . . . . . . . . . . . . . . . . 17 (((𝑉 ∈ LVec ∧ ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉) ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉)) ∧ 𝑥 ∈ (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏𝑤)))) → ∃𝑢 ∈ ((LSpan‘𝑉)‘𝑤)∃𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))𝑥 = (𝑢(+g𝑉)𝑣))
216202, 177, 180, 213, 215syl31anc 1373 . . . . . . . . . . . . . . . 16 ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) → ∃𝑢 ∈ ((LSpan‘𝑉)‘𝑤)∃𝑣 ∈ ((LSpan‘𝑉)‘(𝑏𝑤))𝑥 = (𝑢(+g𝑉)𝑣))
217201, 216r19.29vva 3204 . . . . . . . . . . . . . . 15 ((((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹𝑥) = 𝑦) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏𝑤))))
218 fvelrnb 6890 . . . . . . . . . . . . . . . . 17 (𝐹 Fn (Base‘𝑉) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ (Base‘𝑉)(𝐹𝑥) = 𝑦))
219218biimpa 478 . . . . . . . . . . . . . . . 16 ((𝐹 Fn (Base‘𝑉) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑥 ∈ (Base‘𝑉)(𝐹𝑥) = 𝑦)
22075, 219sylan 581 . . . . . . . . . . . . . . 15 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑥 ∈ (Base‘𝑉)(𝐹𝑥) = 𝑦)
221217, 220r19.29a 3156 . . . . . . . . . . . . . 14 ((((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏𝑤))))
22239, 221eqelssd 3956 . . . . . . . . . . . . 13 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 “ ((LSpan‘𝑉)‘(𝑏𝑤))) = ran 𝐹)
22337, 222eqtr3id 2791 . . . . . . . . . . . 12 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) = ran 𝐹)
224223f1oeq3d 6768 . . . . . . . . . . 11 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1-onto→ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1-onto→ran 𝐹))
225159, 224mpbid 231 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1-onto→ran 𝐹)
22642, 50, 76syl2anc 585 . . . . . . . . . . . 12 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) ⊆ (Base‘𝑉))
227226, 151syl 17 . . . . . . . . . . 11 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) = (Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
228 frn 6662 . . . . . . . . . . . . 13 (𝐹:(Base‘𝑉)⟶(Base‘𝑈) → ran 𝐹 ⊆ (Base‘𝑈))
22929, 72ressbas2 17046 . . . . . . . . . . . . 13 (ran 𝐹 ⊆ (Base‘𝑈) → ran 𝐹 = (Base‘𝐼))
23073, 228, 2293syl 18 . . . . . . . . . . . 12 (𝐹 ∈ (𝑉 LMHom 𝑈) → ran 𝐹 = (Base‘𝐼))
23132, 230syl 17 . . . . . . . . . . 11 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ran 𝐹 = (Base‘𝐼))
232150, 227, 231f1oeq123d 6765 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1-onto→ran 𝐹 ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):(Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))–1-1-onto→(Base‘𝐼)))
233225, 232mpbid 231 . . . . . . . . 9 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):(Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))–1-1-onto→(Base‘𝐼))
234 eqid 2737 . . . . . . . . . 10 (Base‘𝐼) = (Base‘𝐼)
235145, 234islmim 20429 . . . . . . . . 9 ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMIso 𝐼) ↔ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMHom 𝐼) ∧ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):(Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))–1-1-onto→(Base‘𝐼)))
23661, 233, 235sylanbrc 584 . . . . . . . 8 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMIso 𝐼))
23748, 52lspssid 20352 . . . . . . . . . . 11 ((𝑉 ∈ LMod ∧ (𝑏𝑤) ⊆ (Base‘𝑉)) → (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤)))
23842, 50, 237syl2anc 585 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤)))
23951, 55lsslinds 21143 . . . . . . . . . . 11 ((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤))) → ((𝑏𝑤) ∈ (LIndS‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))) ↔ (𝑏𝑤) ∈ (LIndS‘𝑉)))
240239biimpar 479 . . . . . . . . . 10 (((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤))) ∧ (𝑏𝑤) ∈ (LIndS‘𝑉)) → (𝑏𝑤) ∈ (LIndS‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
24142, 67, 238, 47, 240syl31anc 1373 . . . . . . . . 9 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ∈ (LIndS‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
242 eqid 2737 . . . . . . . . . . . 12 (LSpan‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))) = (LSpan‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))
24355, 52, 242, 51lsslsp 20382 . . . . . . . . . . 11 ((𝑉 ∈ LMod ∧ ((LSpan‘𝑉)‘(𝑏𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤))) → ((LSpan‘𝑉)‘(𝑏𝑤)) = ((LSpan‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))‘(𝑏𝑤)))
24442, 54, 238, 243syl3anc 1371 . . . . . . . . . 10 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘𝑉)‘(𝑏𝑤)) = ((LSpan‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))‘(𝑏𝑤)))
245244, 227eqtr3d 2779 . . . . . . . . 9 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((LSpan‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))‘(𝑏𝑤)) = (Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
246 eqid 2737 . . . . . . . . . 10 (LBasis‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))) = (LBasis‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))
247145, 246, 242islbs4 21144 . . . . . . . . 9 ((𝑏𝑤) ∈ (LBasis‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))) ↔ ((𝑏𝑤) ∈ (LIndS‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))) ∧ ((LSpan‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))‘(𝑏𝑤)) = (Base‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))))
248241, 245, 247sylanbrc 584 . . . . . . . 8 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (𝑏𝑤) ∈ (LBasis‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤)))))
249 eqid 2737 . . . . . . . . 9 (LBasis‘𝐼) = (LBasis‘𝐼)
250246, 249lmimlbs 21148 . . . . . . . 8 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) ∈ ((𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))) LMIso 𝐼) ∧ (𝑏𝑤) ∈ (LBasis‘(𝑉s ((LSpan‘𝑉)‘(𝑏𝑤))))) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤)) ∈ (LBasis‘𝐼))
251236, 248, 250syl2anc 585 . . . . . . 7 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤)) ∈ (LBasis‘𝐼))
252249dimval 31982 . . . . . . 7 ((𝐼 ∈ LVec ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤)) ∈ (LBasis‘𝐼)) → (dim‘𝐼) = (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤))))
25331, 251, 252syl2anc 585 . . . . . 6 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (dim‘𝐼) = (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤))))
254 f1imaeng 8879 . . . . . . . 8 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1→ran 𝐹 ∧ (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤)) ∧ (𝑏𝑤) ∈ (LIndS‘𝑉)) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤)) ≈ (𝑏𝑤))
255 hasheni 14167 . . . . . . . 8 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤)) ≈ (𝑏𝑤) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤))) = (♯‘(𝑏𝑤)))
256254, 255syl 17 . . . . . . 7 (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))):((LSpan‘𝑉)‘(𝑏𝑤))–1-1→ran 𝐹 ∧ (𝑏𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏𝑤)) ∧ (𝑏𝑤) ∈ (LIndS‘𝑉)) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤))) = (♯‘(𝑏𝑤)))
257157, 238, 47, 256syl3anc 1371 . . . . . 6 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏𝑤))) “ (𝑏𝑤))) = (♯‘(𝑏𝑤)))
258253, 257eqtrd 2777 . . . . 5 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (dim‘𝐼) = (♯‘(𝑏𝑤)))
25928, 258oveq12d 7359 . . . 4 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → ((dim‘𝐾) +𝑒 (dim‘𝐼)) = ((♯‘𝑤) +𝑒 (♯‘(𝑏𝑤))))
26016, 25, 2593eqtr4d 2787 . . 3 (((((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤𝑏) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼)))
2614lbslinds 21145 . . . . . 6 (LBasis‘𝐾) ⊆ (LIndS‘𝐾)
262261, 94sselid 3933 . . . . 5 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LIndS‘𝐾))
26351, 2lsslinds 21143 . . . . . 6 ((𝑉 ∈ LMod ∧ (𝐹 “ { 0 }) ∈ (LSubSp‘𝑉) ∧ 𝑤 ⊆ (𝐹 “ { 0 })) → (𝑤 ∈ (LIndS‘𝐾) ↔ 𝑤 ∈ (LIndS‘𝑉)))
264263biimpa 478 . . . . 5 (((𝑉 ∈ LMod ∧ (𝐹 “ { 0 }) ∈ (LSubSp‘𝑉) ∧ 𝑤 ⊆ (𝐹 “ { 0 })) ∧ 𝑤 ∈ (LIndS‘𝐾)) → 𝑤 ∈ (LIndS‘𝑉))
26599, 102, 110, 262, 264syl31anc 1373 . . . 4 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LIndS‘𝑉))
26623islinds4 21147 . . . . 5 (𝑉 ∈ LVec → (𝑤 ∈ (LIndS‘𝑉) ↔ ∃𝑏 ∈ (LBasis‘𝑉)𝑤𝑏))
267266ad2antrr 724 . . . 4 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (𝑤 ∈ (LIndS‘𝑉) ↔ ∃𝑏 ∈ (LBasis‘𝑉)𝑤𝑏))
268265, 267mpbid 231 . . 3 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ∃𝑏 ∈ (LBasis‘𝑉)𝑤𝑏)
269260, 268r19.29a 3156 . 2 (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼)))
2708, 269exlimddv 1938 1 ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1087   = wceq 1541  wex 1781  wcel 2106  wne 2941  wrex 3071  Vcvv 3442  cdif 3898  cun 3899  cin 3900  wss 3901  c0 4273  {csn 4577   class class class wbr 5096  ccnv 5623  ran crn 5625  cres 5626  cima 5627   Fn wfn 6478  wf 6479  1-1wf1 6480  1-1-ontowf1o 6482  cfv 6483  (class class class)co 7341  cen 8805   +𝑒 cxad 12951  chash 14149  Basecbs 17009  s cress 17038  +gcplusg 17059  0gc0g 17247  Mndcmnd 18482  Grpcgrp 18673  SubGrpcsubg 18845   GrpHom cghm 18927  LSSumclsm 19335  LModclmod 20228  LSubSpclss 20298  LSpanclspn 20338   LMHom clmhm 20386   LMIso clmim 20387  LBasisclbs 20441  LVecclvec 20469  LIndSclinds 21117  dimcldim 31980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5233  ax-sep 5247  ax-nul 5254  ax-pow 5312  ax-pr 5376  ax-un 7654  ax-reg 9453  ax-inf2 9502  ax-ac2 10324  ax-cnex 11032  ax-resscn 11033  ax-1cn 11034  ax-icn 11035  ax-addcl 11036  ax-addrcl 11037  ax-mulcl 11038  ax-mulrcl 11039  ax-mulcom 11040  ax-addass 11041  ax-mulass 11042  ax-distr 11043  ax-i2m1 11044  ax-1ne0 11045  ax-1rid 11046  ax-rnegex 11047  ax-rrecex 11048  ax-cnre 11049  ax-pre-lttri 11050  ax-pre-lttrn 11051  ax-pre-ltadd 11052  ax-pre-mulgt0 11053
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3444  df-sbc 3731  df-csb 3847  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3920  df-nul 4274  df-if 4478  df-pw 4553  df-sn 4578  df-pr 4580  df-tp 4582  df-op 4584  df-uni 4857  df-int 4899  df-iun 4947  df-iin 4948  df-br 5097  df-opab 5159  df-mpt 5180  df-tr 5214  df-id 5522  df-eprel 5528  df-po 5536  df-so 5537  df-fr 5579  df-se 5580  df-we 5581  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6242  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6435  df-fun 6485  df-fn 6486  df-f 6487  df-f1 6488  df-fo 6489  df-f1o 6490  df-fv 6491  df-isom 6492  df-riota 7297  df-ov 7344  df-oprab 7345  df-mpo 7346  df-of 7599  df-rpss 7642  df-om 7785  df-1st 7903  df-2nd 7904  df-supp 8052  df-tpos 8116  df-frecs 8171  df-wrecs 8202  df-recs 8276  df-rdg 8315  df-1o 8371  df-oadd 8375  df-er 8573  df-map 8692  df-ixp 8761  df-en 8809  df-dom 8810  df-sdom 8811  df-fin 8812  df-fsupp 9231  df-sup 9303  df-oi 9371  df-r1 9625  df-rank 9626  df-dju 9762  df-card 9800  df-acn 9803  df-ac 9977  df-pnf 11116  df-mnf 11117  df-xr 11118  df-ltxr 11119  df-le 11120  df-sub 11312  df-neg 11313  df-nn 12079  df-2 12141  df-3 12142  df-4 12143  df-5 12144  df-6 12145  df-7 12146  df-8 12147  df-9 12148  df-n0 12339  df-xnn0 12411  df-z 12425  df-dec 12543  df-uz 12688  df-xadd 12954  df-fz 13345  df-fzo 13488  df-seq 13827  df-hash 14150  df-struct 16945  df-sets 16962  df-slot 16980  df-ndx 16992  df-base 17010  df-ress 17039  df-plusg 17072  df-mulr 17073  df-sca 17075  df-vsca 17076  df-ip 17077  df-tset 17078  df-ple 17079  df-ocomp 17080  df-ds 17081  df-hom 17083  df-cco 17084  df-0g 17249  df-gsum 17250  df-prds 17255  df-pws 17257  df-mre 17392  df-mrc 17393  df-mri 17394  df-acs 17395  df-proset 18110  df-drs 18111  df-poset 18128  df-ipo 18343  df-mgm 18423  df-sgrp 18472  df-mnd 18483  df-mhm 18527  df-submnd 18528  df-grp 18676  df-minusg 18677  df-sbg 18678  df-mulg 18797  df-subg 18848  df-ghm 18928  df-cntz 19019  df-lsm 19337  df-cmn 19483  df-abl 19484  df-mgp 19815  df-ur 19832  df-ring 19879  df-oppr 19956  df-dvdsr 19977  df-unit 19978  df-invr 20008  df-drng 20094  df-subrg 20126  df-lmod 20230  df-lss 20299  df-lsp 20339  df-lmhm 20389  df-lmim 20390  df-lbs 20442  df-lvec 20470  df-sra 20539  df-rgmod 20540  df-nzr 20634  df-dsmm 21044  df-frlm 21059  df-uvc 21095  df-lindf 21118  df-linds 21119  df-dim 31981
This theorem is referenced by:  qusdimsum  32005
  Copyright terms: Public domain W3C validator