Step | Hyp | Ref
| Expression |
1 | | dimkerim.0 |
. . . . 5
⊢ 0 =
(0g‘𝑈) |
2 | | dimkerim.k |
. . . . 5
⊢ 𝐾 = (𝑉 ↾s (◡𝐹 “ { 0 })) |
3 | 1, 2 | kerlmhm 33150 |
. . . 4
⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝐾 ∈ LVec) |
4 | | eqid 2724 |
. . . . 5
⊢
(LBasis‘𝐾) =
(LBasis‘𝐾) |
5 | 4 | lbsex 21005 |
. . . 4
⊢ (𝐾 ∈ LVec →
(LBasis‘𝐾) ≠
∅) |
6 | 3, 5 | syl 17 |
. . 3
⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → (LBasis‘𝐾) ≠ ∅) |
7 | | n0 4338 |
. . 3
⊢
((LBasis‘𝐾)
≠ ∅ ↔ ∃𝑤 𝑤 ∈ (LBasis‘𝐾)) |
8 | 6, 7 | sylib 217 |
. 2
⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → ∃𝑤 𝑤 ∈ (LBasis‘𝐾)) |
9 | | simpllr 773 |
. . . . 5
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑤 ∈ (LBasis‘𝐾)) |
10 | | vex 3470 |
. . . . . . 7
⊢ 𝑏 ∈ V |
11 | 10 | difexi 5318 |
. . . . . 6
⊢ (𝑏 ∖ 𝑤) ∈ V |
12 | 11 | a1i 11 |
. . . . 5
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ V) |
13 | | disjdif 4463 |
. . . . . 6
⊢ (𝑤 ∩ (𝑏 ∖ 𝑤)) = ∅ |
14 | 13 | a1i 11 |
. . . . 5
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑤 ∩ (𝑏 ∖ 𝑤)) = ∅) |
15 | | hashunx 14342 |
. . . . 5
⊢ ((𝑤 ∈ (LBasis‘𝐾) ∧ (𝑏 ∖ 𝑤) ∈ V ∧ (𝑤 ∩ (𝑏 ∖ 𝑤)) = ∅) → (♯‘(𝑤 ∪ (𝑏 ∖ 𝑤))) = ((♯‘𝑤) +𝑒 (♯‘(𝑏 ∖ 𝑤)))) |
16 | 9, 12, 14, 15 | syl3anc 1368 |
. . . 4
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (♯‘(𝑤 ∪ (𝑏 ∖ 𝑤))) = ((♯‘𝑤) +𝑒 (♯‘(𝑏 ∖ 𝑤)))) |
17 | | simp-4l 780 |
. . . . 5
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑉 ∈ LVec) |
18 | | simpr 484 |
. . . . . . 7
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑤 ⊆ 𝑏) |
19 | | undif 4473 |
. . . . . . 7
⊢ (𝑤 ⊆ 𝑏 ↔ (𝑤 ∪ (𝑏 ∖ 𝑤)) = 𝑏) |
20 | 18, 19 | sylib 217 |
. . . . . 6
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑤 ∪ (𝑏 ∖ 𝑤)) = 𝑏) |
21 | | simplr 766 |
. . . . . 6
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑏 ∈ (LBasis‘𝑉)) |
22 | 20, 21 | eqeltrd 2825 |
. . . . 5
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑤 ∪ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝑉)) |
23 | | eqid 2724 |
. . . . . 6
⊢
(LBasis‘𝑉) =
(LBasis‘𝑉) |
24 | 23 | dimval 33130 |
. . . . 5
⊢ ((𝑉 ∈ LVec ∧ (𝑤 ∪ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝑉)) → (dim‘𝑉) = (♯‘(𝑤 ∪ (𝑏 ∖ 𝑤)))) |
25 | 17, 22, 24 | syl2anc 583 |
. . . 4
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝑉) = (♯‘(𝑤 ∪ (𝑏 ∖ 𝑤)))) |
26 | 3 | ad3antrrr 727 |
. . . . . 6
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐾 ∈ LVec) |
27 | 4 | dimval 33130 |
. . . . . 6
⊢ ((𝐾 ∈ LVec ∧ 𝑤 ∈ (LBasis‘𝐾)) → (dim‘𝐾) = (♯‘𝑤)) |
28 | 26, 9, 27 | syl2anc 583 |
. . . . 5
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝐾) = (♯‘𝑤)) |
29 | | dimkerim.i |
. . . . . . . . 9
⊢ 𝐼 = (𝑈 ↾s ran 𝐹) |
30 | 29 | imlmhm 33151 |
. . . . . . . 8
⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝐼 ∈ LVec) |
31 | 30 | ad3antrrr 727 |
. . . . . . 7
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐼 ∈ LVec) |
32 | | simp-4r 781 |
. . . . . . . . . . 11
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐹 ∈ (𝑉 LMHom 𝑈)) |
33 | | lmhmlmod2 20869 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝑈 ∈ LMod) |
34 | 32, 33 | syl 17 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑈 ∈ LMod) |
35 | | lmhmrnlss 20887 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → ran 𝐹 ∈ (LSubSp‘𝑈)) |
36 | 32, 35 | syl 17 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ran 𝐹 ∈ (LSubSp‘𝑈)) |
37 | | df-ima 5679 |
. . . . . . . . . . 11
⊢ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) |
38 | | imassrn 6060 |
. . . . . . . . . . . 12
⊢ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹 |
39 | 38 | a1i 11 |
. . . . . . . . . . 11
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹) |
40 | 37, 39 | eqsstrrid 4023 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹) |
41 | | lveclmod 20943 |
. . . . . . . . . . . . 13
⊢ (𝑉 ∈ LVec → 𝑉 ∈ LMod) |
42 | 41 | ad4antr 729 |
. . . . . . . . . . . 12
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑉 ∈ LMod) |
43 | 23 | lbslinds 21695 |
. . . . . . . . . . . . . . 15
⊢
(LBasis‘𝑉)
⊆ (LIndS‘𝑉) |
44 | 43, 21 | sselid 3972 |
. . . . . . . . . . . . . 14
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑏 ∈ (LIndS‘𝑉)) |
45 | | difssd 4124 |
. . . . . . . . . . . . . 14
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ⊆ 𝑏) |
46 | | lindsss 21686 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 ∈ LMod ∧ 𝑏 ∈ (LIndS‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉)) |
47 | 42, 44, 45, 46 | syl3anc 1368 |
. . . . . . . . . . . . 13
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉)) |
48 | | eqid 2724 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑉) =
(Base‘𝑉) |
49 | 48 | linds1 21672 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉) → (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) |
50 | 47, 49 | syl 17 |
. . . . . . . . . . . 12
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) |
51 | | eqid 2724 |
. . . . . . . . . . . . 13
⊢
(LSubSp‘𝑉) =
(LSubSp‘𝑉) |
52 | | eqid 2724 |
. . . . . . . . . . . . 13
⊢
(LSpan‘𝑉) =
(LSpan‘𝑉) |
53 | 48, 51, 52 | lspcl 20812 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ LMod ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉)) |
54 | 42, 50, 53 | syl2anc 583 |
. . . . . . . . . . 11
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉)) |
55 | | eqid 2724 |
. . . . . . . . . . . 12
⊢ (𝑉 ↾s
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = (𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) |
56 | 51, 55 | reslmhm 20889 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝑉 LMHom 𝑈) ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉)) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝑈)) |
57 | 32, 54, 56 | syl2anc 583 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝑈)) |
58 | | eqid 2724 |
. . . . . . . . . . . 12
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
59 | 29, 58 | reslmhm2b 20891 |
. . . . . . . . . . 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 1370 |
. . . . . . . . 9
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝐼)) |
62 | | lmghm 20868 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝐹 ∈ (𝑉 GrpHom 𝑈)) |
63 | 62 | ad4antlr 730 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐹 ∈ (𝑉 GrpHom 𝑈)) |
64 | 48, 23 | lbsss 20914 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 ∈ (LBasis‘𝑉) → 𝑏 ⊆ (Base‘𝑉)) |
65 | 21, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑏 ⊆ (Base‘𝑉)) |
66 | 45, 65 | sstrd 3984 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) |
67 | 42, 66, 53 | syl2anc 583 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉)) |
68 | 51 | lsssubg 20793 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑉 ∈ LMod ∧
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉)) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (SubGrp‘𝑉)) |
69 | 42, 67, 68 | syl2anc 583 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (SubGrp‘𝑉)) |
70 | 55 | resghm 19146 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ (𝑉 GrpHom 𝑈) ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (SubGrp‘𝑉)) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) GrpHom 𝑈)) |
71 | 63, 69, 70 | syl2anc 583 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) GrpHom 𝑈)) |
72 | | eqid 2724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(Base‘𝑈) =
(Base‘𝑈) |
73 | 48, 72 | lmhmf 20871 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈)) |
74 | 73 | ad4antlr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈)) |
75 | 74 | ffnd 6708 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝐹 Fn (Base‘𝑉)) |
76 | 48, 52 | lspssv 20819 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑉 ∈ LMod ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉)) |
77 | 42, 66, 76 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉)) |
78 | 75, 77 | fnssresd 6664 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) Fn ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) |
79 | | fniniseg 7051 |
. . . . . . . . . . . . . . . . . . . . . . . 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 579 |
. . . . . . . . . . . . . . . . . . . . . 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 3975 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈ (Base‘𝑉)) |
86 | 82 | fvresd 6901 |
. . . . . . . . . . . . . . . . . . . . . . 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 2766 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → (𝐹‘𝑥) = 0 ) |
89 | | fniniseg 7051 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹 Fn (Base‘𝑉) → (𝑥 ∈ (◡𝐹 “ { 0 }) ↔ (𝑥 ∈ (Base‘𝑉) ∧ (𝐹‘𝑥) = 0 ))) |
90 | 89 | biimpar 477 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 Fn (Base‘𝑉) ∧ (𝑥 ∈ (Base‘𝑉) ∧ (𝐹‘𝑥) = 0 )) → 𝑥 ∈ (◡𝐹 “ { 0 })) |
91 | 83, 85, 88, 90 | syl12anc 834 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈ (◡𝐹 “ { 0 })) |
92 | 82, 91 | elind 4186 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈ (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ (◡𝐹 “ { 0 }))) |
93 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LBasis‘𝐾)) |
94 | | eqid 2724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(Base‘𝐾) =
(Base‘𝐾) |
95 | | eqid 2724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(LSpan‘𝐾) =
(LSpan‘𝐾) |
96 | 94, 4, 95 | lbssp 20916 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 ∈ (LBasis‘𝐾) → ((LSpan‘𝐾)‘𝑤) = (Base‘𝐾)) |
97 | 93, 96 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝐾)‘𝑤) = (Base‘𝐾)) |
98 | 41 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑉 ∈ LMod) |
99 | | eqid 2724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (◡𝐹 “ { 0 }) = (◡𝐹 “ { 0 }) |
100 | 99, 1, 51 | lmhmkerlss 20888 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → (◡𝐹 “ { 0 }) ∈
(LSubSp‘𝑉)) |
101 | 100 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (◡𝐹 “ { 0 }) ∈
(LSubSp‘𝑉)) |
102 | 94, 4 | lbsss 20914 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 ∈ (LBasis‘𝐾) → 𝑤 ⊆ (Base‘𝐾)) |
103 | 93, 102 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ⊆ (Base‘𝐾)) |
104 | | cnvimass 6070 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (◡𝐹 “ { 0 }) ⊆ dom 𝐹 |
105 | 104, 73 | fssdm 6727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → (◡𝐹 “ { 0 }) ⊆
(Base‘𝑉)) |
106 | 2, 48 | ressbas2 17180 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((◡𝐹 “ { 0 }) ⊆
(Base‘𝑉) →
(◡𝐹 “ { 0 }) = (Base‘𝐾)) |
107 | 105, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → (◡𝐹 “ { 0 }) = (Base‘𝐾)) |
108 | 107 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (◡𝐹 “ { 0 }) = (Base‘𝐾)) |
109 | 103, 108 | sseqtrrd 4015 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ⊆ (◡𝐹 “ { 0 })) |
110 | 2, 52, 95, 51 | lsslsp 20851 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑉 ∈ LMod ∧ (◡𝐹 “ { 0 }) ∈
(LSubSp‘𝑉) ∧
𝑤 ⊆ (◡𝐹 “ { 0 })) →
((LSpan‘𝐾)‘𝑤) = ((LSpan‘𝑉)‘𝑤)) |
111 | 110 | eqcomd 2730 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑉 ∈ LMod ∧ (◡𝐹 “ { 0 }) ∈
(LSubSp‘𝑉) ∧
𝑤 ⊆ (◡𝐹 “ { 0 })) →
((LSpan‘𝑉)‘𝑤) = ((LSpan‘𝐾)‘𝑤)) |
112 | 98, 101, 109, 111 | syl3anc 1368 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝑉)‘𝑤) = ((LSpan‘𝐾)‘𝑤)) |
113 | 97, 112, 108 | 3eqtr4d 2774 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ((LSpan‘𝑉)‘𝑤) = (◡𝐹 “ { 0 })) |
114 | 113 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑤) = (◡𝐹 “ { 0 })) |
115 | 114 | ineq2d 4204 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ (◡𝐹 “ { 0 }))) |
116 | | eqid 2724 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(0g‘𝑉) = (0g‘𝑉) |
117 | 23, 52, 116 | lbsdiflsp0 33156 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑉 ∈ LVec ∧ 𝑏 ∈ (LBasis‘𝑉) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = {(0g‘𝑉)}) |
118 | 117 | ad5ant145 1366 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∩ ((LSpan‘𝑉)‘𝑤)) = {(0g‘𝑉)}) |
119 | 115, 118 | eqtr3d 2766 |
. . . . . . . . . . . . . . . . . . . . 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 2827 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) → 𝑥 ∈
{(0g‘𝑉)}) |
122 | 121 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑥 ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) → 𝑥 ∈
{(0g‘𝑉)})) |
123 | 122 | ssrdv 3980 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) ⊆
{(0g‘𝑉)}) |
124 | 116, 48, 52 | 0ellsp 32917 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 ∈ LMod ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → (0g‘𝑉) ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) |
125 | 42, 66, 124 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (0g‘𝑉) ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) |
126 | | fvexd 6896 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) ∈ V) |
127 | 125 | fvresd 6901 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) = (𝐹‘(0g‘𝑉))) |
128 | 116, 1 | ghmid 19136 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹 ∈ (𝑉 GrpHom 𝑈) → (𝐹‘(0g‘𝑉)) = 0 ) |
129 | 62, 128 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → (𝐹‘(0g‘𝑉)) = 0 ) |
130 | 129 | ad4antlr 730 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹‘(0g‘𝑉)) = 0 ) |
131 | 127, 130 | eqtrd 2764 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) = 0 ) |
132 | | elsng 4634 |
. . . . . . . . . . . . . . . . . . . . 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 583 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))‘(0g‘𝑉)) ∈ { 0 }) |
135 | 78, 125, 134 | elpreimad 7050 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (0g‘𝑉) ∈ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) |
136 | 135 | snssd 4804 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → {(0g‘𝑉)} ⊆ (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 })) |
137 | 123, 136 | eqssd 3991 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) =
{(0g‘𝑉)}) |
138 | | lmodgrp 20702 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑉 ∈ LMod → 𝑉 ∈ Grp) |
139 | | grpmnd 18859 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑉 ∈ Grp → 𝑉 ∈ Mnd) |
140 | 42, 138, 139 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑉 ∈ Mnd) |
141 | 55, 48, 116 | ress0g 18684 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑉 ∈ Mnd ∧
(0g‘𝑉)
∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉)) → (0g‘𝑉) = (0g‘(𝑉 ↾s
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) |
142 | 140, 125,
77, 141 | syl3anc 1368 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (0g‘𝑉) = (0g‘(𝑉 ↾s
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) |
143 | 142 | sneqd 4632 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → {(0g‘𝑉)} =
{(0g‘(𝑉
↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))}) |
144 | 137, 143 | eqtrd 2764 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (◡(𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ { 0 }) =
{(0g‘(𝑉
↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))}) |
145 | | eqid 2724 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘(𝑉
↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) |
146 | | eqid 2724 |
. . . . . . . . . . . . . . . . 17
⊢
(0g‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) = (0g‘(𝑉 ↾s
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) |
147 | 145, 72, 146, 1 | kerf1ghm 19161 |
. . . . . . . . . . . . . . . 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 583 |
. . . . . . . . . . . . . 14
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))–1-1→(Base‘𝑈)) |
150 | | eqidd 2725 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) |
151 | 55, 48 | ressbas2 17180 |
. . . . . . . . . . . . . . . 16
⊢
(((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) |
152 | 77, 151 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) |
153 | | eqidd 2725 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (Base‘𝑈) = (Base‘𝑈)) |
154 | 150, 152,
153 | f1eq123d 6815 |
. . . . . . . . . . . . . 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 6784 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→(Base‘𝑈) ∧ ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ⊆ ran 𝐹) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→ran 𝐹) |
157 | 155, 40, 156 | syl2anc 583 |
. . . . . . . . . . . 12
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→ran 𝐹) |
158 | | f1f1orn 6834 |
. . . . . . . . . . . 12
⊢ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→ran 𝐹 → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1-onto→ran
(𝐹 ↾
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) |
159 | 157, 158 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1-onto→ran
(𝐹 ↾
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) |
160 | | simp-4r 781 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑥) = 𝑦) |
161 | 75 | ad6antr 733 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝐹 Fn (Base‘𝑉)) |
162 | | simpllr 773 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) |
163 | 113 | ad8antr 737 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((LSpan‘𝑉)‘𝑤) = (◡𝐹 “ { 0 })) |
164 | 162, 163 | eleqtrd 2827 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑢 ∈ (◡𝐹 “ { 0 })) |
165 | | fniniseg 7051 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹 Fn (Base‘𝑉) → (𝑢 ∈ (◡𝐹 “ { 0 }) ↔ (𝑢 ∈ (Base‘𝑉) ∧ (𝐹‘𝑢) = 0 ))) |
166 | 165 | simplbda 499 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹 Fn (Base‘𝑉) ∧ 𝑢 ∈ (◡𝐹 “ { 0 })) → (𝐹‘𝑢) = 0 ) |
167 | 161, 164,
166 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑢) = 0 ) |
168 | 167 | oveq1d 7416 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((𝐹‘𝑢)(+g‘𝑈)(𝐹‘𝑣)) = ( 0 (+g‘𝑈)(𝐹‘𝑣))) |
169 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑥 = (𝑢(+g‘𝑉)𝑣)) |
170 | 169 | fveq2d 6885 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑥) = (𝐹‘(𝑢(+g‘𝑉)𝑣))) |
171 | 63 | ad6antr 733 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝐹 ∈ (𝑉 GrpHom 𝑈)) |
172 | 48, 52 | lspss 20820 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑉 ∈ LMod ∧ 𝑏 ⊆ (Base‘𝑉) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ ((LSpan‘𝑉)‘𝑏)) |
173 | 42, 65, 18, 172 | syl3anc 1368 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ ((LSpan‘𝑉)‘𝑏)) |
174 | 48, 23, 52 | lbssp 20916 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑏 ∈ (LBasis‘𝑉) → ((LSpan‘𝑉)‘𝑏) = (Base‘𝑉)) |
175 | 21, 174 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑏) = (Base‘𝑉)) |
176 | 173, 175 | sseqtrd 4014 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉)) |
177 | 176 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉)) |
178 | 177 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((LSpan‘𝑉)‘𝑤) ⊆ (Base‘𝑉)) |
179 | 178, 162 | sseldd 3975 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑢 ∈ (Base‘𝑉)) |
180 | 77 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉)) |
181 | 180 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉)) |
182 | | simplr 766 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) |
183 | 181, 182 | sseldd 3975 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑣 ∈ (Base‘𝑉)) |
184 | | eqid 2724 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(+g‘𝑉) = (+g‘𝑉) |
185 | | eqid 2724 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(+g‘𝑈) = (+g‘𝑈) |
186 | 48, 184, 185 | ghmlin 19135 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹 ∈ (𝑉 GrpHom 𝑈) ∧ 𝑢 ∈ (Base‘𝑉) ∧ 𝑣 ∈ (Base‘𝑉)) → (𝐹‘(𝑢(+g‘𝑉)𝑣)) = ((𝐹‘𝑢)(+g‘𝑈)(𝐹‘𝑣))) |
187 | 171, 179,
183, 186 | syl3anc 1368 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘(𝑢(+g‘𝑉)𝑣)) = ((𝐹‘𝑢)(+g‘𝑈)(𝐹‘𝑣))) |
188 | 170, 187 | eqtr2d 2765 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ((𝐹‘𝑢)(+g‘𝑈)(𝐹‘𝑣)) = (𝐹‘𝑥)) |
189 | | lmhmlvec2 33149 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝑈 ∈ LVec) |
190 | 189 | lvecgrpd 20945 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → 𝑈 ∈ Grp) |
191 | 190 | ad9antr 739 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑈 ∈ Grp) |
192 | 74 | ad6antr 733 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝐹:(Base‘𝑉)⟶(Base‘𝑈)) |
193 | 192, 183 | ffvelcdmd 7077 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑣) ∈ (Base‘𝑈)) |
194 | 72, 185, 1, 191, 193 | grplidd 18888 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → ( 0 (+g‘𝑈)(𝐹‘𝑣)) = (𝐹‘𝑣)) |
195 | 168, 188,
194 | 3eqtr3d 2772 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑥) = (𝐹‘𝑣)) |
196 | 160, 195 | eqtr3d 2766 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑦 = (𝐹‘𝑣)) |
197 | 161, 183,
182 | fnfvimad 7227 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → (𝐹‘𝑣) ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) |
198 | 196, 197 | eqeltrd 2825 |
. . . . . . . . . . . . . . . 16
⊢
(((((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) ∧ 𝑢 ∈ ((LSpan‘𝑉)‘𝑤)) ∧ 𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ 𝑥 = (𝑢(+g‘𝑉)𝑣)) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) |
199 | | simp-7l 786 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → 𝑉 ∈ LVec) |
200 | | simplr 766 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → 𝑥 ∈ (Base‘𝑉)) |
201 | 109 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑤 ⊆ (◡𝐹 “ { 0 })) |
202 | 105 | ad4antlr 730 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (◡𝐹 “ { 0 }) ⊆
(Base‘𝑉)) |
203 | 201, 202 | sstrd 3984 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → 𝑤 ⊆ (Base‘𝑉)) |
204 | | eqid 2724 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(LSSum‘𝑉) =
(LSSum‘𝑉) |
205 | 48, 52, 204 | lsmsp2 20924 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑉 ∈ LMod ∧ 𝑤 ⊆ (Base‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏 ∖ 𝑤)))) |
206 | 42, 203, 66, 205 | syl3anc 1368 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏 ∖ 𝑤)))) |
207 | 20 | fveq2d 6885 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑤 ∪ (𝑏 ∖ 𝑤))) = ((LSpan‘𝑉)‘𝑏)) |
208 | 206, 207,
175 | 3eqtrrd 2769 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (Base‘𝑉) = (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) |
209 | 208 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → (Base‘𝑉) = (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) |
210 | 200, 209 | eleqtrd 2827 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → 𝑥 ∈ (((LSpan‘𝑉)‘𝑤)(LSSum‘𝑉)((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) |
211 | 48, 184, 204 | lsmelvalx 19549 |
. . . . . . . . . . . . . . . . . 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 1370 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → ∃𝑢 ∈ ((LSpan‘𝑉)‘𝑤)∃𝑣 ∈ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))𝑥 = (𝑢(+g‘𝑉)𝑣)) |
214 | 198, 213 | r19.29vva 3205 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝑉 ∈
LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) ∧ 𝑥 ∈ (Base‘𝑉)) ∧ (𝐹‘𝑥) = 𝑦) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) |
215 | | fvelrnb 6942 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 Fn (Base‘𝑉) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ (Base‘𝑉)(𝐹‘𝑥) = 𝑦)) |
216 | 215 | biimpa 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 Fn (Base‘𝑉) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑥 ∈ (Base‘𝑉)(𝐹‘𝑥) = 𝑦) |
217 | 75, 216 | sylan 579 |
. . . . . . . . . . . . . . 15
⊢
((((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑥 ∈ (Base‘𝑉)(𝐹‘𝑥) = 𝑦) |
218 | 214, 217 | r19.29a 3154 |
. . . . . . . . . . . . . 14
⊢
((((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) |
219 | 39, 218 | eqelssd 3995 |
. . . . . . . . . . . . 13
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 “ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ran 𝐹) |
220 | 37, 219 | eqtr3id 2778 |
. . . . . . . . . . . 12
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ran (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) = ran 𝐹) |
221 | 220 | f1oeq3d 6820 |
. . . . . . . . . . 11
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1-onto→ran
(𝐹 ↾
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1-onto→ran
𝐹)) |
222 | 159, 221 | mpbid 231 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1-onto→ran
𝐹) |
223 | 42, 50, 76 | syl2anc 583 |
. . . . . . . . . . . 12
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ⊆ (Base‘𝑉)) |
224 | 223, 151 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) |
225 | | frn 6714 |
. . . . . . . . . . . . 13
⊢ (𝐹:(Base‘𝑉)⟶(Base‘𝑈) → ran 𝐹 ⊆ (Base‘𝑈)) |
226 | 29, 72 | ressbas2 17180 |
. . . . . . . . . . . . 13
⊢ (ran
𝐹 ⊆ (Base‘𝑈) → ran 𝐹 = (Base‘𝐼)) |
227 | 73, 225, 226 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (𝑉 LMHom 𝑈) → ran 𝐹 = (Base‘𝐼)) |
228 | 32, 227 | syl 17 |
. . . . . . . . . . 11
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ran 𝐹 = (Base‘𝐼)) |
229 | 150, 224,
228 | f1oeq123d 6817 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1-onto→ran
𝐹 ↔ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))–1-1-onto→(Base‘𝐼))) |
230 | 222, 229 | mpbid 231 |
. . . . . . . . 9
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))–1-1-onto→(Base‘𝐼)) |
231 | | eqid 2724 |
. . . . . . . . . 10
⊢
(Base‘𝐼) =
(Base‘𝐼) |
232 | 145, 231 | islmim 20899 |
. . . . . . . . 9
⊢ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMIso 𝐼) ↔ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMHom 𝐼) ∧ (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):(Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))–1-1-onto→(Base‘𝐼))) |
233 | 61, 230, 232 | sylanbrc 582 |
. . . . . . . 8
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMIso 𝐼)) |
234 | 48, 52 | lspssid 20821 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ LMod ∧ (𝑏 ∖ 𝑤) ⊆ (Base‘𝑉)) → (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) |
235 | 42, 50, 234 | syl2anc 583 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) |
236 | 51, 55 | lsslinds 21693 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ LMod ∧
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) → ((𝑏 ∖ 𝑤) ∈ (LIndS‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) ↔ (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉))) |
237 | 236 | biimpar 477 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ LMod ∧
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∧ (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉)) → (𝑏 ∖ 𝑤) ∈ (LIndS‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) |
238 | 42, 67, 235, 47, 237 | syl31anc 1370 |
. . . . . . . . 9
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ (LIndS‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) |
239 | | eqid 2724 |
. . . . . . . . . . . . 13
⊢
(LSpan‘(𝑉
↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) = (LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) |
240 | 55, 52, 239, 51 | lsslsp 20851 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ LMod ∧
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) → ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤)) = ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) |
241 | 240 | eqcomd 2730 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ LMod ∧
((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∈ (LSubSp‘𝑉) ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤))) |
242 | 42, 54, 235, 241 | syl3anc 1368 |
. . . . . . . . . 10
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) = ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤))) |
243 | 242, 224 | eqtr3d 2766 |
. . . . . . . . 9
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) |
244 | | eqid 2724 |
. . . . . . . . . 10
⊢
(LBasis‘(𝑉
↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) = (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) |
245 | 145, 244,
239 | islbs4 21694 |
. . . . . . . . 9
⊢ ((𝑏 ∖ 𝑤) ∈ (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) ↔ ((𝑏 ∖ 𝑤) ∈ (LIndS‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))) ∧ ((LSpan‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))‘(𝑏 ∖ 𝑤)) = (Base‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)))))) |
246 | 238, 243,
245 | sylanbrc 582 |
. . . . . . . 8
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (𝑏 ∖ 𝑤) ∈ (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) |
247 | | eqid 2724 |
. . . . . . . . 9
⊢
(LBasis‘𝐼) =
(LBasis‘𝐼) |
248 | 244, 247 | lmimlbs 21698 |
. . . . . . . 8
⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) ∈ ((𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) LMIso 𝐼) ∧ (𝑏 ∖ 𝑤) ∈ (LBasis‘(𝑉 ↾s ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))))) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝐼)) |
249 | 233, 246,
248 | syl2anc 583 |
. . . . . . 7
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝐼)) |
250 | 247 | dimval 33130 |
. . . . . . 7
⊢ ((𝐼 ∈ LVec ∧ ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ∈ (LBasis‘𝐼)) → (dim‘𝐼) = (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)))) |
251 | 31, 249, 250 | syl2anc 583 |
. . . . . 6
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝐼) = (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)))) |
252 | | f1imaeng 9005 |
. . . . . . . 8
⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→ran 𝐹 ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉)) → ((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ≈ (𝑏 ∖ 𝑤)) |
253 | | hasheni 14304 |
. . . . . . . 8
⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤)) ≈ (𝑏 ∖ 𝑤) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤))) = (♯‘(𝑏 ∖ 𝑤))) |
254 | 252, 253 | syl 17 |
. . . . . . 7
⊢ (((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))):((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))–1-1→ran 𝐹 ∧ (𝑏 ∖ 𝑤) ⊆ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤)) ∧ (𝑏 ∖ 𝑤) ∈ (LIndS‘𝑉)) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤))) = (♯‘(𝑏 ∖ 𝑤))) |
255 | 157, 235,
47, 254 | syl3anc 1368 |
. . . . . 6
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (♯‘((𝐹 ↾ ((LSpan‘𝑉)‘(𝑏 ∖ 𝑤))) “ (𝑏 ∖ 𝑤))) = (♯‘(𝑏 ∖ 𝑤))) |
256 | 251, 255 | eqtrd 2764 |
. . . . 5
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝐼) = (♯‘(𝑏 ∖ 𝑤))) |
257 | 28, 256 | oveq12d 7419 |
. . . 4
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → ((dim‘𝐾) +𝑒 (dim‘𝐼)) = ((♯‘𝑤) +𝑒
(♯‘(𝑏 ∖
𝑤)))) |
258 | 16, 25, 257 | 3eqtr4d 2774 |
. . 3
⊢
(((((𝑉 ∈ LVec
∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) ∧ 𝑏 ∈ (LBasis‘𝑉)) ∧ 𝑤 ⊆ 𝑏) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼))) |
259 | 4 | lbslinds 21695 |
. . . . . 6
⊢
(LBasis‘𝐾)
⊆ (LIndS‘𝐾) |
260 | 259, 93 | sselid 3972 |
. . . . 5
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LIndS‘𝐾)) |
261 | 51, 2 | lsslinds 21693 |
. . . . . 6
⊢ ((𝑉 ∈ LMod ∧ (◡𝐹 “ { 0 }) ∈
(LSubSp‘𝑉) ∧
𝑤 ⊆ (◡𝐹 “ { 0 })) → (𝑤 ∈ (LIndS‘𝐾) ↔ 𝑤 ∈ (LIndS‘𝑉))) |
262 | 261 | biimpa 476 |
. . . . 5
⊢ (((𝑉 ∈ LMod ∧ (◡𝐹 “ { 0 }) ∈
(LSubSp‘𝑉) ∧
𝑤 ⊆ (◡𝐹 “ { 0 })) ∧ 𝑤 ∈ (LIndS‘𝐾)) → 𝑤 ∈ (LIndS‘𝑉)) |
263 | 98, 101, 109, 260, 262 | syl31anc 1370 |
. . . 4
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → 𝑤 ∈ (LIndS‘𝑉)) |
264 | 23 | islinds4 21697 |
. . . . 5
⊢ (𝑉 ∈ LVec → (𝑤 ∈ (LIndS‘𝑉) ↔ ∃𝑏 ∈ (LBasis‘𝑉)𝑤 ⊆ 𝑏)) |
265 | 264 | ad2antrr 723 |
. . . 4
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (𝑤 ∈ (LIndS‘𝑉) ↔ ∃𝑏 ∈ (LBasis‘𝑉)𝑤 ⊆ 𝑏)) |
266 | 263, 265 | mpbid 231 |
. . 3
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → ∃𝑏 ∈ (LBasis‘𝑉)𝑤 ⊆ 𝑏) |
267 | 258, 266 | r19.29a 3154 |
. 2
⊢ (((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) ∧ 𝑤 ∈ (LBasis‘𝐾)) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼))) |
268 | 8, 267 | exlimddv 1930 |
1
⊢ ((𝑉 ∈ LVec ∧ 𝐹 ∈ (𝑉 LMHom 𝑈)) → (dim‘𝑉) = ((dim‘𝐾) +𝑒 (dim‘𝐼))) |