| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dimkerim.0 | . . . . 5
⊢  0 =
(0g‘𝑈) | 
| 2 |  | dimkerim.k | . . . . 5
⊢ 𝐾 = (𝑉 ↾s (◡𝐹 “ { 0 })) | 
| 3 | 1, 2 | kerlmhm 33672 | . . . 4
⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝐾 ∈ LVec) | 
| 4 |  | eqid 2736 | . . . . 5
⊢
(LBasis‘𝐾) =
(LBasis‘𝐾) | 
| 5 | 4 | lbsex 21168 | . . . 4
⊢ (𝐾 ∈ LVec →
(LBasis‘𝐾) ≠
∅) | 
| 6 | 3, 5 | syl 17 | . . 3
⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → (LBasis‘𝐾) ≠ ∅) | 
| 7 |  | n0 4352 | . . 3
⊢
((LBasis‘𝐾)
≠ ∅ ↔ ∃𝑤 𝑤 ∈ (LBasis‘𝐾)) | 
| 8 | 6, 7 | sylib 218 | . 2
⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → ∃𝑤 𝑤 ∈ (LBasis‘𝐾)) | 
| 9 |  | simpllr 775 | . . . . 5
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑤 ∈ (LBasis‘𝐾)) | 
| 10 |  | vex 3483 | . . . . . . 7
⊢ 𝑏 ∈ V | 
| 11 | 10 | difexi 5329 | . . . . . 6
⊢ (𝑏 ∖ 𝑤) ∈ V | 
| 12 | 11 | a1i 11 | . . . . 5
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ V) | 
| 13 |  | disjdif 4471 | . . . . . 6
⊢ (𝑤 ∩ (𝑏 ∖ 𝑤)) = ∅ | 
| 14 | 13 | a1i 11 | . . . . 5
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑤 ∩ (𝑏 ∖ 𝑤)) = ∅) | 
| 15 |  | hashunx 14426 | . . . . 5
⊢ ((𝑤 ∈ (LBasis‘𝐾) ∧ (𝑏 ∖ 𝑤) ∈ V ∧ (𝑤 ∩ (𝑏 ∖ 𝑤)) = ∅) → (♯‘(𝑤 ∪ (𝑏 ∖ 𝑤))) = ((♯‘𝑤) +𝑒 (♯‘(𝑏 ∖ 𝑤)))) | 
| 16 | 9, 12, 14, 15 | syl3anc 1372 | . . . 4
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (♯‘(𝑤 ∪ (𝑏 ∖ 𝑤))) = ((♯‘𝑤) +𝑒 (♯‘(𝑏 ∖ 𝑤)))) | 
| 17 |  | simp-4l 782 | . . . . 5
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑉 ∈ LVec) | 
| 18 |  | simpr 484 | . . . . . . 7
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑤 ⊆ 𝑏) | 
| 19 |  | undif 4481 | . . . . . . 7
⊢ (𝑤 ⊆ 𝑏 ↔ (𝑤 ∪ (𝑏 ∖ 𝑤)) = 𝑏) | 
| 20 | 18, 19 | sylib 218 | . . . . . 6
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑤 ∪ (𝑏 ∖ 𝑤)) = 𝑏) | 
| 21 |  | simplr 768 | . . . . . 6
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑏 ∈ (LBasis‘𝑉)) | 
| 22 | 20, 21 | eqeltrd 2840 | . . . . 5
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑤 ∪ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝑉)) | 
| 23 |  | eqid 2736 | . . . . . 6
⊢
(LBasis‘𝑉) =
(LBasis‘𝑉) | 
| 24 | 23 | dimval 33652 | . . . . 5
⊢ ((𝑉 ∈ LVec ∧ (𝑤 ∪ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝑉)) → (dim‘𝑉) = (♯‘(𝑤 ∪ (𝑏 ∖ 𝑤)))) | 
| 25 | 17, 22, 24 | syl2anc 584 | . . . 4
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝑉) = (♯‘(𝑤 ∪ (𝑏 ∖ 𝑤)))) | 
| 26 | 3 | ad3antrrr 730 | . . . . . 6
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐾 ∈ LVec) | 
| 27 | 4 | dimval 33652 | . . . . . 6
⊢ ((𝐾 ∈ LVec ∧ 𝑤 ∈ (LBasis‘𝐾)) → (dim‘𝐾) = (♯‘𝑤)) | 
| 28 | 26, 9, 27 | syl2anc 584 | . . . . 5
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝐾) = (♯‘𝑤)) | 
| 29 |  | dimkerim.i | . . . . . . . . 9
⊢ 𝐼 = (𝑈 ↾s ran 𝐹) | 
| 30 | 29 | imlmhm 33673 | . . . . . . . 8
⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝐼 ∈ LVec) | 
| 31 | 30 | ad3antrrr 730 | . . . . . . 7
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐼 ∈ LVec) | 
| 32 |  | simp-4r 783 | . . . . . . . . . . 11
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐹 ∈ (𝑉 LMHom 𝑈)) | 
| 33 |  | lmhmlmod2 21032 | . . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝑈 ∈ LMod) | 
| 34 | 32, 33 | syl 17 | . . . . . . . . . 10
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑈 ∈ LMod) | 
| 35 |  | lmhmrnlss 21050 | . . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → ran 𝐹 ∈ (LSubSp‘𝑈)) | 
| 36 | 32, 35 | syl 17 | . . . . . . . . . 10
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ran 𝐹 ∈ (LSubSp‘𝑈)) | 
| 37 |  | df-ima 5697 | . . . . . . . . . . 11
⊢ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) | 
| 38 |  | imassrn 6088 | . . . . . . . . . . . 12
⊢ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹 | 
| 39 | 38 | a1i 11 | . . . . . . . . . . 11
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹) | 
| 40 | 37, 39 | eqsstrrid 4022 | . . . . . . . . . 10
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹) | 
| 41 |  | lveclmod 21106 | . . . . . . . . . . . . 13
⊢ (𝑉 ∈ LVec → 𝑉 ∈ LMod) | 
| 42 | 41 | ad4antr 732 | . . . . . . . . . . . 12
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑉 ∈ LMod) | 
| 43 | 23 | lbslinds 21854 | . . . . . . . . . . . . . . 15
⊢
(LBasis‘𝑉)
⊆ (LIndS‘𝑉) | 
| 44 | 43, 21 | sselid 3980 | . . . . . . . . . . . . . 14
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑏 ∈ (LIndS‘𝑉)) | 
| 45 |  | difssd 4136 | . . . . . . . . . . . . . 14
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ⊆ 𝑏) | 
| 46 |  | lindsss 21845 | . . . . . . . . . . . . . 14
⊢ ((𝑉 ∈ LMod ∧ 𝑏 ∈ (LIndS‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉)) | 
| 47 | 42, 44, 45, 46 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉)) | 
| 48 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(Base‘𝑉) =
(Base‘𝑉) | 
| 49 | 48 | linds1 21831 | . . . . . . . . . . . . 13
⊢ ((𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉) → (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) | 
| 50 | 47, 49 | syl 17 | . . . . . . . . . . . 12
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) | 
| 51 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(LSubSp‘𝑉) =
(LSubSp‘𝑉) | 
| 52 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(LSpan‘𝑉) =
(LSpan‘𝑉) | 
| 53 | 48, 51, 52 | lspcl 20975 | . . . . . . . . . . . 12
⊢ ((𝑉 ∈ LMod ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉)) | 
| 54 | 42, 50, 53 | syl2anc 584 | . . . . . . . . . . 11
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉)) | 
| 55 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ (𝑉 ↾s
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = (𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) | 
| 56 | 51, 55 | reslmhm 21052 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝑉 LMHom 𝑈) ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉)) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝑈)) | 
| 57 | 32, 54, 56 | syl2anc 584 | . . . . . . . . . 10
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝑈)) | 
| 58 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) | 
| 59 | 29, 58 | reslmhm2b 21054 | . . . . . . . . . . 11
⊢ ((𝑈 ∈ LMod ∧ ran 𝐹 ∈ (LSubSp‘𝑈) ∧ ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝑈) ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝐼))) | 
| 60 | 59 | biimpa 476 | . . . . . . . . . 10
⊢ (((𝑈 ∈ LMod ∧ ran 𝐹 ∈ (LSubSp‘𝑈) ∧ ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹) ∧ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝑈)) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝐼)) | 
| 61 | 34, 36, 40, 57, 60 | syl31anc 1374 | . . . . . . . . 9
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝐼)) | 
| 62 |  | lmghm 21031 | . . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝐹 ∈ (𝑉 GrpHom 𝑈)) | 
| 63 | 62 | ad4antlr 733 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐹 ∈ (𝑉 GrpHom 𝑈)) | 
| 64 | 48, 23 | lbsss 21077 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 ∈ (LBasis‘𝑉) → 𝑏 ⊆ (Base‘𝑉)) | 
| 65 | 21, 64 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑏 ⊆ (Base‘𝑉)) | 
| 66 | 45, 65 | sstrd 3993 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) | 
| 67 | 42, 66, 53 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉)) | 
| 68 | 51 | lsssubg 20956 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑉 ∈ LMod ∧
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉)) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (SubGrp‘𝑉)) | 
| 69 | 42, 67, 68 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (SubGrp‘𝑉)) | 
| 70 | 55 | resghm 19251 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ (𝑉 GrpHom 𝑈) ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (SubGrp‘𝑉)) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) GrpHom 𝑈)) | 
| 71 | 63, 69, 70 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) GrpHom 𝑈)) | 
| 72 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(Base‘𝑈) =
(Base‘𝑈) | 
| 73 | 48, 72 | lmhmf 21034 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈)) | 
| 74 | 73 | ad4antlr 733 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈)) | 
| 75 | 74 | ffnd 6736 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐹 Fn (Base‘𝑉)) | 
| 76 | 48, 52 | lspssv 20982 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑉 ∈ LMod ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉)) | 
| 77 | 42, 66, 76 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉)) | 
| 78 | 75, 77 | fnssresd 6691 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) Fn ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) | 
| 79 |  | fniniseg 7079 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) Fn ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) → (𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) ↔ (𝑥 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘𝑥) = 0 ))) | 
| 80 | 79 | biimpa 476 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) Fn ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → (𝑥 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘𝑥) = 0 )) | 
| 81 | 78, 80 | sylan 580 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → (𝑥 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘𝑥) = 0 )) | 
| 82 | 81 | simpld 494 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) | 
| 83 | 75 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝐹 Fn (Base‘𝑉)) | 
| 84 | 77 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) →
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉)) | 
| 85 | 84, 82 | sseldd 3983 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈ (Base‘𝑉)) | 
| 86 | 82 | fvresd 6925 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘𝑥) = (𝐹‘𝑥)) | 
| 87 | 81 | simprd 495 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘𝑥) = 0 ) | 
| 88 | 86, 87 | eqtr3d 2778 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → (𝐹‘𝑥) = 0 ) | 
| 89 |  | fniniseg 7079 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹 Fn (Base‘𝑉) → (𝑥 ∈ (◡𝐹 “ { 0 }) ↔ (𝑥 ∈ (Base‘𝑉) ∧ (𝐹‘𝑥) = 0 ))) | 
| 90 | 89 | biimpar 477 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 Fn (Base‘𝑉) ∧ (𝑥 ∈ (Base‘𝑉) ∧ (𝐹‘𝑥) = 0 )) → 𝑥 ∈ (◡𝐹 “ { 0 })) | 
| 91 | 83, 85, 88, 90 | syl12anc 836 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈ (◡𝐹 “ { 0 })) | 
| 92 | 82, 91 | elind 4199 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈ (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ (◡𝐹 “ { 0 }))) | 
| 93 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LBasis‘𝐾)) | 
| 94 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(Base‘𝐾) =
(Base‘𝐾) | 
| 95 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(LSpan‘𝐾) =
(LSpan‘𝐾) | 
| 96 | 94, 4, 95 | lbssp 21079 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 ∈ (LBasis‘𝐾) → ((LSpan‘𝐾)‘𝑤) = (Base‘𝐾)) | 
| 97 | 93, 96 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝐾)‘𝑤) = (Base‘𝐾)) | 
| 98 | 41 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑉 ∈ LMod) | 
| 99 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (◡𝐹 “ { 0 }) = (◡𝐹 “ { 0 }) | 
| 100 | 99, 1, 51 | lmhmkerlss 21051 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → (◡𝐹 “ { 0 }) ∈
(LSubSp‘𝑉)) | 
| 101 | 100 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (◡𝐹 “ { 0 }) ∈
(LSubSp‘𝑉)) | 
| 102 | 94, 4 | lbsss 21077 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 ∈ (LBasis‘𝐾) → 𝑤 ⊆ (Base‘𝐾)) | 
| 103 | 93, 102 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ⊆ (Base‘𝐾)) | 
| 104 |  | cnvimass 6099 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (◡𝐹 “ { 0 }) ⊆ dom 𝐹 | 
| 105 | 104, 73 | fssdm 6754 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → (◡𝐹 “ { 0 }) ⊆
(Base‘𝑉)) | 
| 106 | 2, 48 | ressbas2 17284 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((◡𝐹 “ { 0 }) ⊆
(Base‘𝑉) →
(◡𝐹 “ { 0 }) = (Base‘𝐾)) | 
| 107 | 105, 106 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → (◡𝐹 “ { 0 }) = (Base‘𝐾)) | 
| 108 | 107 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (◡𝐹 “ { 0 }) = (Base‘𝐾)) | 
| 109 | 103, 108 | sseqtrrd 4020 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ⊆ (◡𝐹 “ { 0 })) | 
| 110 | 2, 52, 95, 51 | lsslsp 21014 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑉 ∈ LMod ∧ (◡𝐹 “ { 0 }) ∈
(LSubSp‘𝑉) ∧
𝑤 ⊆ (◡𝐹 “ { 0 })) →
((LSpan‘𝐾)‘𝑤) = ((LSpan‘𝑉)‘𝑤)) | 
| 111 | 110 | eqcomd 2742 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑉 ∈ LMod ∧ (◡𝐹 “ { 0 }) ∈
(LSubSp‘𝑉) ∧
𝑤 ⊆ (◡𝐹 “ { 0 })) →
((LSpan‘𝑉)‘𝑤) = ((LSpan‘𝐾)‘𝑤)) | 
| 112 | 98, 101, 109, 111 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝑉)‘𝑤) = ((LSpan‘𝐾)‘𝑤)) | 
| 113 | 97, 112, 108 | 3eqtr4d 2786 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝑉)‘𝑤) = (◡𝐹 “ { 0 })) | 
| 114 | 113 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑤) = (◡𝐹 “ { 0 })) | 
| 115 | 114 | ineq2d 4219 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ (◡𝐹 “ { 0 }))) | 
| 116 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(0g‘𝑉) = (0g‘𝑉) | 
| 117 | 23, 52, 116 | lbsdiflsp0 33678 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑉 ∈ LVec ∧ 𝑏 ∈ (LBasis‘𝑉) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = {(0g‘𝑉)}) | 
| 118 | 117 | ad5ant145 1370 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = {(0g‘𝑉)}) | 
| 119 | 115, 118 | eqtr3d 2778 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ (◡𝐹 “ { 0 })) =
{(0g‘𝑉)}) | 
| 120 | 119 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) →
(((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ (◡𝐹 “ { 0 })) =
{(0g‘𝑉)}) | 
| 121 | 92, 120 | eleqtrd 2842 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈
{(0g‘𝑉)}) | 
| 122 | 121 | ex 412 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) → 𝑥 ∈
{(0g‘𝑉)})) | 
| 123 | 122 | ssrdv 3988 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) ⊆
{(0g‘𝑉)}) | 
| 124 | 116, 48, 52 | 0ellsp 33398 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 ∈ LMod ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → (0g‘𝑉) ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) | 
| 125 | 42, 66, 124 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (0g‘𝑉) ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) | 
| 126 |  | fvexd 6920 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) ∈ V) | 
| 127 | 125 | fvresd 6925 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) = (𝐹‘(0g‘𝑉))) | 
| 128 | 116, 1 | ghmid 19241 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹 ∈ (𝑉 GrpHom 𝑈) → (𝐹‘(0g‘𝑉)) = 0 ) | 
| 129 | 62, 128 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → (𝐹‘(0g‘𝑉)) = 0 ) | 
| 130 | 129 | ad4antlr 733 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹‘(0g‘𝑉)) = 0 ) | 
| 131 | 127, 130 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) = 0 ) | 
| 132 |  | elsng 4639 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) ∈ V → (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) ∈ { 0 } ↔ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) = 0 )) | 
| 133 | 132 | biimpar 477 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) ∈ V ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) = 0 ) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) ∈ { 0 }) | 
| 134 | 126, 131,
133 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) ∈ { 0 }) | 
| 135 | 78, 125, 134 | elpreimad 7078 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (0g‘𝑉) ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) | 
| 136 | 135 | snssd 4808 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → {(0g‘𝑉)} ⊆ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) | 
| 137 | 123, 136 | eqssd 4000 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) =
{(0g‘𝑉)}) | 
| 138 |  | lmodgrp 20866 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑉 ∈ LMod → 𝑉 ∈ Grp) | 
| 139 |  | grpmnd 18959 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑉 ∈ Grp → 𝑉 ∈ Mnd) | 
| 140 | 42, 138, 139 | 3syl 18 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑉 ∈ Mnd) | 
| 141 | 55, 48, 116 | ress0g 18776 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑉 ∈ Mnd ∧
(0g‘𝑉)
∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉)) → (0g‘𝑉) = (0g‘(𝑉 ↾s
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) | 
| 142 | 140, 125,
77, 141 | syl3anc 1372 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (0g‘𝑉) = (0g‘(𝑉 ↾s
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) | 
| 143 | 142 | sneqd 4637 | . . . . . . . . . . . . . . . 16
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → {(0g‘𝑉)} =
{(0g‘(𝑉
↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))}) | 
| 144 | 137, 143 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) =
{(0g‘(𝑉
↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))}) | 
| 145 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢
(Base‘(𝑉
↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) | 
| 146 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢
(0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) = (0g‘(𝑉 ↾s
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) | 
| 147 | 145, 72, 146, 1 | kerf1ghm 19266 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) GrpHom 𝑈) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))–1-1→(Base‘𝑈) ↔ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) =
{(0g‘(𝑉
↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))})) | 
| 148 | 147 | biimpar 477 | . . . . . . . . . . . . . . 15
⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) GrpHom 𝑈) ∧ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) =
{(0g‘(𝑉
↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))}) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))–1-1→(Base‘𝑈)) | 
| 149 | 71, 144, 148 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))–1-1→(Base‘𝑈)) | 
| 150 |  | eqidd 2737 | . . . . . . . . . . . . . . 15
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) | 
| 151 | 55, 48 | ressbas2 17284 | . . . . . . . . . . . . . . . 16
⊢
(((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) | 
| 152 | 77, 151 | syl 17 | . . . . . . . . . . . . . . 15
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) | 
| 153 |  | eqidd 2737 | . . . . . . . . . . . . . . 15
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (Base‘𝑈) = (Base‘𝑈)) | 
| 154 | 150, 152,
153 | f1eq123d 6839 | . . . . . . . . . . . . . 14
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→(Base‘𝑈) ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))–1-1→(Base‘𝑈))) | 
| 155 | 149, 154 | mpbird 257 | . . . . . . . . . . . . 13
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→(Base‘𝑈)) | 
| 156 |  | f1ssr 6809 | . . . . . . . . . . . . 13
⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→(Base‘𝑈) ∧ ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→ran 𝐹) | 
| 157 | 155, 40, 156 | syl2anc 584 | . . . . . . . . . . . 12
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→ran 𝐹) | 
| 158 |  | f1f1orn 6858 | . . . . . . . . . . . 12
⊢ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→ran 𝐹 → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1-onto→ran
(𝐹 ↾
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) | 
| 159 | 157, 158 | syl 17 | . . . . . . . . . . 11
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1-onto→ran
(𝐹 ↾
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) | 
| 160 |  | simp-4r 783 | . . . . . . . . . . . . . . . . . 18
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑥) = 𝑦) | 
| 161 | 75 | ad6antr 736 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝐹 Fn (Base‘𝑉)) | 
| 162 |  | simpllr 775 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) | 
| 163 | 113 | ad8antr 740 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((LSpan‘𝑉)‘𝑤) = (◡𝐹 “ { 0 })) | 
| 164 | 162, 163 | eleqtrd 2842 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑢 ∈ (◡𝐹 “ { 0 })) | 
| 165 |  | fniniseg 7079 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹 Fn (Base‘𝑉) → (𝑢 ∈ (◡𝐹 “ { 0 }) ↔ (𝑢 ∈ (Base‘𝑉) ∧ (𝐹‘𝑢) = 0 ))) | 
| 166 | 165 | simplbda 499 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹 Fn (Base‘𝑉) ∧ 𝑢 ∈ (◡𝐹 “ { 0 })) → (𝐹‘𝑢) = 0 ) | 
| 167 | 161, 164,
166 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑢) = 0 ) | 
| 168 | 167 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((𝐹‘𝑢)(+g‘𝑈)(𝐹‘𝑣)) = ( 0 (+g‘𝑈)(𝐹‘𝑣))) | 
| 169 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑥 = (𝑢(+g‘𝑉)𝑣)) | 
| 170 | 169 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑥) = (𝐹‘(𝑢(+g‘𝑉)𝑣))) | 
| 171 | 63 | ad6antr 736 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝐹 ∈ (𝑉 GrpHom 𝑈)) | 
| 172 | 48, 52 | lspss 20983 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑉 ∈ LMod ∧ 𝑏 ⊆ (Base‘𝑉) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ ((LSpan‘𝑉)‘𝑏)) | 
| 173 | 42, 65, 18, 172 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ ((LSpan‘𝑉)‘𝑏)) | 
| 174 | 48, 23, 52 | lbssp 21079 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑏 ∈ (LBasis‘𝑉) → ((LSpan‘𝑉)‘𝑏) = (Base‘𝑉)) | 
| 175 | 21, 174 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑏) = (Base‘𝑉)) | 
| 176 | 173, 175 | sseqtrd 4019 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉)) | 
| 177 | 176 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉)) | 
| 178 | 177 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉)) | 
| 179 | 178, 162 | sseldd 3983 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑢 ∈ (Base‘𝑉)) | 
| 180 | 77 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉)) | 
| 181 | 180 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉)) | 
| 182 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) | 
| 183 | 181, 182 | sseldd 3983 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑣 ∈ (Base‘𝑉)) | 
| 184 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(+g‘𝑉) = (+g‘𝑉) | 
| 185 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(+g‘𝑈) = (+g‘𝑈) | 
| 186 | 48, 184, 185 | ghmlin 19240 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹 ∈ (𝑉 GrpHom 𝑈) ∧ 𝑢 ∈ (Base‘𝑉) ∧ 𝑣 ∈ (Base‘𝑉)) → (𝐹‘(𝑢(+g‘𝑉)𝑣)) = ((𝐹‘𝑢)(+g‘𝑈)(𝐹‘𝑣))) | 
| 187 | 171, 179,
183, 186 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘(𝑢(+g‘𝑉)𝑣)) = ((𝐹‘𝑢)(+g‘𝑈)(𝐹‘𝑣))) | 
| 188 | 170, 187 | eqtr2d 2777 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((𝐹‘𝑢)(+g‘𝑈)(𝐹‘𝑣)) = (𝐹‘𝑥)) | 
| 189 |  | lmhmlvec2 33671 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝑈 ∈ LVec) | 
| 190 | 189 | lvecgrpd 21108 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝑈 ∈ Grp) | 
| 191 | 190 | ad9antr 742 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑈 ∈ Grp) | 
| 192 | 74 | ad6antr 736 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈)) | 
| 193 | 192, 183 | ffvelcdmd 7104 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑣) ∈ (Base‘𝑈)) | 
| 194 | 72, 185, 1, 191, 193 | grplidd 18988 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ( 0 (+g‘𝑈)(𝐹‘𝑣)) = (𝐹‘𝑣)) | 
| 195 | 168, 188,
194 | 3eqtr3d 2784 | . . . . . . . . . . . . . . . . . 18
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑥) = (𝐹‘𝑣)) | 
| 196 | 160, 195 | eqtr3d 2778 | . . . . . . . . . . . . . . . . 17
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑦 = (𝐹‘𝑣)) | 
| 197 | 161, 183,
182 | fnfvimad 7255 | . . . . . . . . . . . . . . . . 17
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑣) ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) | 
| 198 | 196, 197 | eqeltrd 2840 | . . . . . . . . . . . . . . . 16
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) | 
| 199 |  | simp-7l 788 | . . . . . . . . . . . . . . . . 17
⊢
((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → 𝑉 ∈ LVec) | 
| 200 |  | simplr 768 | . . . . . . . . . . . . . . . . . 18
⊢
((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → 𝑥 ∈ (Base‘𝑉)) | 
| 201 | 109 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑤 ⊆ (◡𝐹 “ { 0 })) | 
| 202 | 105 | ad4antlr 733 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (◡𝐹 “ { 0 }) ⊆
(Base‘𝑉)) | 
| 203 | 201, 202 | sstrd 3993 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑤 ⊆ (Base‘𝑉)) | 
| 204 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(LSSum‘𝑉) =
(LSSum‘𝑉) | 
| 205 | 48, 52, 204 | lsmsp2 21087 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑉 ∈ LMod ∧ 𝑤 ⊆ (Base‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏 ∖ 𝑤)))) | 
| 206 | 42, 203, 66, 205 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏 ∖ 𝑤)))) | 
| 207 | 20 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏 ∖ 𝑤))) = ((LSpan‘𝑉)‘𝑏)) | 
| 208 | 206, 207,
175 | 3eqtrrd 2781 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (Base‘𝑉) = (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) | 
| 209 | 208 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . 18
⊢
((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → (Base‘𝑉) = (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) | 
| 210 | 200, 209 | eleqtrd 2842 | . . . . . . . . . . . . . . . . 17
⊢
((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → 𝑥 ∈ (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) | 
| 211 | 48, 184, 204 | lsmelvalx 19659 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑉 ∈ LVec ∧
((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉) ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉)) → (𝑥 ∈ (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ↔ ∃𝑢 ∈ ((LSpan‘𝑉)‘𝑤)∃𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))𝑥 = (𝑢(+g‘𝑉)𝑣))) | 
| 212 | 211 | biimpa 476 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑉 ∈ LVec ∧
((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉) ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉)) ∧ 𝑥 ∈ (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) → ∃𝑢 ∈ ((LSpan‘𝑉)‘𝑤)∃𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))𝑥 = (𝑢(+g‘𝑉)𝑣)) | 
| 213 | 199, 177,
180, 210, 212 | syl31anc 1374 | . . . . . . . . . . . . . . . 16
⊢
((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → ∃𝑢 ∈ ((LSpan‘𝑉)‘𝑤)∃𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))𝑥 = (𝑢(+g‘𝑉)𝑣)) | 
| 214 | 198, 213 | r19.29vva 3215 | . . . . . . . . . . . . . . 15
⊢
((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) | 
| 215 |  | fvelrnb 6968 | . . . . . . . . . . . . . . . . 17
⊢ (𝐹 Fn (Base‘𝑉) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ (Base‘𝑉)(𝐹‘𝑥) = 𝑦)) | 
| 216 | 215 | biimpa 476 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹 Fn (Base‘𝑉) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑥 ∈ (Base‘𝑉)(𝐹‘𝑥) = 𝑦) | 
| 217 | 75, 216 | sylan 580 | . . . . . . . . . . . . . . 15
⊢
((((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑥 ∈ (Base‘𝑉)(𝐹‘𝑥) = 𝑦) | 
| 218 | 214, 217 | r19.29a 3161 | . . . . . . . . . . . . . 14
⊢
((((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) | 
| 219 | 39, 218 | eqelssd 4004 | . . . . . . . . . . . . 13
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ran 𝐹) | 
| 220 | 37, 219 | eqtr3id 2790 | . . . . . . . . . . . 12
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ran 𝐹) | 
| 221 | 220 | f1oeq3d 6844 | . . . . . . . . . . 11
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1-onto→ran
(𝐹 ↾
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1-onto→ran
𝐹)) | 
| 222 | 159, 221 | mpbid 232 | . . . . . . . . . 10
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1-onto→ran
𝐹) | 
| 223 | 42, 50, 76 | syl2anc 584 | . . . . . . . . . . . 12
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉)) | 
| 224 | 223, 151 | syl 17 | . . . . . . . . . . 11
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) | 
| 225 |  | frn 6742 | . . . . . . . . . . . 12
⊢ (𝐹:(Base‘𝑉)⟶(Base‘𝑈) → ran 𝐹 ⊆ (Base‘𝑈)) | 
| 226 | 29, 72 | ressbas2 17284 | . . . . . . . . . . . 12
⊢ (ran
𝐹 ⊆ (Base‘𝑈) → ran 𝐹 = (Base‘𝐼)) | 
| 227 | 32, 73, 225, 226 | 4syl 19 | . . . . . . . . . . 11
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ran 𝐹 = (Base‘𝐼)) | 
| 228 | 150, 224,
227 | f1oeq123d 6841 | . . . . . . . . . 10
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1-onto→ran
𝐹 ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))–1-1-onto→(Base‘𝐼))) | 
| 229 | 222, 228 | mpbid 232 | . . . . . . . . 9
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))–1-1-onto→(Base‘𝐼)) | 
| 230 |  | eqid 2736 | . . . . . . . . . 10
⊢
(Base‘𝐼) =
(Base‘𝐼) | 
| 231 | 145, 230 | islmim 21062 | . . . . . . . . 9
⊢ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMIso 𝐼) ↔ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝐼) ∧ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))–1-1-onto→(Base‘𝐼))) | 
| 232 | 61, 229, 231 | sylanbrc 583 | . . . . . . . 8
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMIso 𝐼)) | 
| 233 | 48, 52 | lspssid 20984 | . . . . . . . . . . 11
⊢ ((𝑉 ∈ LMod ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) | 
| 234 | 42, 50, 233 | syl2anc 584 | . . . . . . . . . 10
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) | 
| 235 | 51, 55 | lsslinds 21852 | . . . . . . . . . . 11
⊢ ((𝑉 ∈ LMod ∧
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) → ((𝑏 ∖ 𝑤) ∈ (LIndS‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) ↔ (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉))) | 
| 236 | 235 | biimpar 477 | . . . . . . . . . 10
⊢ (((𝑉 ∈ LMod ∧
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉)) → (𝑏 ∖ 𝑤) ∈ (LIndS‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) | 
| 237 | 42, 67, 234, 47, 236 | syl31anc 1374 | . . . . . . . . 9
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ (LIndS‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) | 
| 238 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(LSpan‘(𝑉
↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) = (LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) | 
| 239 | 55, 52, 238, 51 | lsslsp 21014 | . . . . . . . . . . . 12
⊢ ((𝑉 ∈ LMod ∧
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) → ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤)) = ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) | 
| 240 | 239 | eqcomd 2742 | . . . . . . . . . . 11
⊢ ((𝑉 ∈ LMod ∧
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤))) | 
| 241 | 42, 54, 234, 240 | syl3anc 1372 | . . . . . . . . . 10
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤))) | 
| 242 | 241, 224 | eqtr3d 2778 | . . . . . . . . 9
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) | 
| 243 |  | eqid 2736 | . . . . . . . . . 10
⊢
(LBasis‘(𝑉
↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) = (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) | 
| 244 | 145, 243,
238 | islbs4 21853 | . . . . . . . . 9
⊢ ((𝑏 ∖ 𝑤) ∈ (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) ↔ ((𝑏 ∖ 𝑤) ∈ (LIndS‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) ∧ ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))) | 
| 245 | 237, 242,
244 | sylanbrc 583 | . . . . . . . 8
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) | 
| 246 |  | eqid 2736 | . . . . . . . . 9
⊢
(LBasis‘𝐼) =
(LBasis‘𝐼) | 
| 247 | 243, 246 | lmimlbs 21857 | . . . . . . . 8
⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMIso 𝐼) ∧ (𝑏 ∖ 𝑤) ∈ (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝐼)) | 
| 248 | 232, 245,
247 | syl2anc 584 | . . . . . . 7
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝐼)) | 
| 249 | 246 | dimval 33652 | . . . . . . 7
⊢ ((𝐼 ∈ LVec ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝐼)) → (dim‘𝐼) = (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)))) | 
| 250 | 31, 248, 249 | syl2anc 584 | . . . . . 6
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝐼) = (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)))) | 
| 251 |  | f1imaeng 9055 | . . . . . . . 8
⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→ran 𝐹 ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉)) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ≈ (𝑏 ∖ 𝑤)) | 
| 252 |  | hasheni 14388 | . . . . . . . 8
⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ≈ (𝑏 ∖ 𝑤) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤))) = (♯‘(𝑏 ∖ 𝑤))) | 
| 253 | 251, 252 | syl 17 | . . . . . . 7
⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→ran 𝐹 ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉)) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤))) = (♯‘(𝑏 ∖ 𝑤))) | 
| 254 | 157, 234,
47, 253 | syl3anc 1372 | . . . . . 6
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤))) = (♯‘(𝑏 ∖ 𝑤))) | 
| 255 | 250, 254 | eqtrd 2776 | . . . . 5
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝐼) = (♯‘(𝑏 ∖ 𝑤))) | 
| 256 | 28, 255 | oveq12d 7450 | . . . 4
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((dim‘𝐾) +𝑒 (dim‘𝐼)) = ((♯‘𝑤) +𝑒
(♯‘(𝑏 ∖
𝑤)))) | 
| 257 | 16, 25, 256 | 3eqtr4d 2786 | . . 3
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼))) | 
| 258 | 4 | lbslinds 21854 | . . . . . 6
⊢
(LBasis‘𝐾)
⊆ (LIndS‘𝐾) | 
| 259 | 258, 93 | sselid 3980 | . . . . 5
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LIndS‘𝐾)) | 
| 260 | 51, 2 | lsslinds 21852 | . . . . . 6
⊢ ((𝑉 ∈ LMod ∧ (◡𝐹 “ { 0 }) ∈
(LSubSp‘𝑉) ∧
𝑤 ⊆ (◡𝐹 “ { 0 })) → (𝑤 ∈ (LIndS‘𝐾) ↔ 𝑤 ∈ (LIndS‘𝑉))) | 
| 261 | 260 | biimpa 476 | . . . . 5
⊢ (((𝑉 ∈ LMod ∧ (◡𝐹 “ { 0 }) ∈
(LSubSp‘𝑉) ∧
𝑤 ⊆ (◡𝐹 “ { 0 })) ∧ 𝑤 ∈ (LIndS‘𝐾)) → 𝑤 ∈ (LIndS‘𝑉)) | 
| 262 | 98, 101, 109, 259, 261 | syl31anc 1374 | . . . 4
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LIndS‘𝑉)) | 
| 263 | 23 | islinds4 21856 | . . . . 5
⊢ (𝑉 ∈ LVec → (𝑤 ∈ (LIndS‘𝑉) ↔ ∃𝑏 ∈ (LBasis‘𝑉)𝑤 ⊆ 𝑏)) | 
| 264 | 263 | ad2antrr 726 | . . . 4
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (𝑤 ∈ (LIndS‘𝑉) ↔ ∃𝑏 ∈ (LBasis‘𝑉)𝑤 ⊆ 𝑏)) | 
| 265 | 262, 264 | mpbid 232 | . . 3
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ∃𝑏 ∈ (LBasis‘𝑉)𝑤 ⊆ 𝑏) | 
| 266 | 257, 265 | r19.29a 3161 | . 2
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼))) | 
| 267 | 8, 266 | exlimddv 1934 | 1
⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼))) |