| Step | Hyp | Ref
| Expression |
| 1 | | lmhmlmod1 21032 |
. . 3
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod) |
| 2 | 1 | 3ad2ant1 1134 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) → 𝑆 ∈ LMod) |
| 3 | | eqid 2737 |
. . . . . 6
⊢
(LSubSp‘𝑆) =
(LSubSp‘𝑆) |
| 4 | | eqid 2737 |
. . . . . 6
⊢ (𝑆 ↾s 𝑎) = (𝑆 ↾s 𝑎) |
| 5 | 3, 4 | reslmhm 21051 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝐹 ↾ 𝑎) ∈ ((𝑆 ↾s 𝑎) LMHom 𝑇)) |
| 6 | 5 | 3ad2antl1 1186 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝐹 ↾ 𝑎) ∈ ((𝑆 ↾s 𝑎) LMHom 𝑇)) |
| 7 | | cnvresima 6250 |
. . . . . . . 8
⊢ (◡(𝐹 ↾ 𝑎) “ { 0 }) = ((◡𝐹 “ { 0 }) ∩ 𝑎) |
| 8 | | lmhmfgsplit.k |
. . . . . . . . . 10
⊢ 𝐾 = (◡𝐹 “ { 0 }) |
| 9 | 8 | eqcomi 2746 |
. . . . . . . . 9
⊢ (◡𝐹 “ { 0 }) = 𝐾 |
| 10 | 9 | ineq1i 4216 |
. . . . . . . 8
⊢ ((◡𝐹 “ { 0 }) ∩ 𝑎) = (𝐾 ∩ 𝑎) |
| 11 | | incom 4209 |
. . . . . . . 8
⊢ (𝐾 ∩ 𝑎) = (𝑎 ∩ 𝐾) |
| 12 | 7, 10, 11 | 3eqtri 2769 |
. . . . . . 7
⊢ (◡(𝐹 ↾ 𝑎) “ { 0 }) = (𝑎 ∩ 𝐾) |
| 13 | 12 | oveq2i 7442 |
. . . . . 6
⊢ ((𝑆 ↾s 𝑎) ↾s (◡(𝐹 ↾ 𝑎) “ { 0 })) = ((𝑆 ↾s 𝑎) ↾s (𝑎 ∩ 𝐾)) |
| 14 | | vex 3484 |
. . . . . . . 8
⊢ 𝑎 ∈ V |
| 15 | | inss1 4237 |
. . . . . . . 8
⊢ (𝑎 ∩ 𝐾) ⊆ 𝑎 |
| 16 | | ressabs 17294 |
. . . . . . . 8
⊢ ((𝑎 ∈ V ∧ (𝑎 ∩ 𝐾) ⊆ 𝑎) → ((𝑆 ↾s 𝑎) ↾s (𝑎 ∩ 𝐾)) = (𝑆 ↾s (𝑎 ∩ 𝐾))) |
| 17 | 14, 15, 16 | mp2an 692 |
. . . . . . 7
⊢ ((𝑆 ↾s 𝑎) ↾s (𝑎 ∩ 𝐾)) = (𝑆 ↾s (𝑎 ∩ 𝐾)) |
| 18 | | lmhmfgsplit.u |
. . . . . . . . 9
⊢ 𝑈 = (𝑆 ↾s 𝐾) |
| 19 | 18 | oveq1i 7441 |
. . . . . . . 8
⊢ (𝑈 ↾s (𝑎 ∩ 𝐾)) = ((𝑆 ↾s 𝐾) ↾s (𝑎 ∩ 𝐾)) |
| 20 | | simpl1 1192 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝐹 ∈ (𝑆 LMHom 𝑇)) |
| 21 | | cnvexg 7946 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ◡𝐹 ∈ V) |
| 22 | | imaexg 7935 |
. . . . . . . . . . . 12
⊢ (◡𝐹 ∈ V → (◡𝐹 “ { 0 }) ∈
V) |
| 23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (◡𝐹 “ { 0 }) ∈
V) |
| 24 | 8, 23 | eqeltrid 2845 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐾 ∈ V) |
| 25 | 20, 24 | syl 17 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝐾 ∈ V) |
| 26 | | inss2 4238 |
. . . . . . . . 9
⊢ (𝑎 ∩ 𝐾) ⊆ 𝐾 |
| 27 | | ressabs 17294 |
. . . . . . . . 9
⊢ ((𝐾 ∈ V ∧ (𝑎 ∩ 𝐾) ⊆ 𝐾) → ((𝑆 ↾s 𝐾) ↾s (𝑎 ∩ 𝐾)) = (𝑆 ↾s (𝑎 ∩ 𝐾))) |
| 28 | 25, 26, 27 | sylancl 586 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ((𝑆 ↾s 𝐾) ↾s (𝑎 ∩ 𝐾)) = (𝑆 ↾s (𝑎 ∩ 𝐾))) |
| 29 | 19, 28 | eqtrid 2789 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑈 ↾s (𝑎 ∩ 𝐾)) = (𝑆 ↾s (𝑎 ∩ 𝐾))) |
| 30 | 17, 29 | eqtr4id 2796 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ((𝑆 ↾s 𝑎) ↾s (𝑎 ∩ 𝐾)) = (𝑈 ↾s (𝑎 ∩ 𝐾))) |
| 31 | 13, 30 | eqtrid 2789 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ((𝑆 ↾s 𝑎) ↾s (◡(𝐹 ↾ 𝑎) “ { 0 })) = (𝑈 ↾s (𝑎 ∩ 𝐾))) |
| 32 | | simpl2 1193 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝑈 ∈ LNoeM) |
| 33 | 2 | adantr 480 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝑆 ∈ LMod) |
| 34 | | simpr 484 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝑎 ∈ (LSubSp‘𝑆)) |
| 35 | | lmhmfgsplit.z |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑇) |
| 36 | 8, 35, 3 | lmhmkerlss 21050 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐾 ∈ (LSubSp‘𝑆)) |
| 37 | 20, 36 | syl 17 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝐾 ∈ (LSubSp‘𝑆)) |
| 38 | 3 | lssincl 20963 |
. . . . . . . 8
⊢ ((𝑆 ∈ LMod ∧ 𝑎 ∈ (LSubSp‘𝑆) ∧ 𝐾 ∈ (LSubSp‘𝑆)) → (𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑆)) |
| 39 | 33, 34, 37, 38 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑆)) |
| 40 | 26 | a1i 11 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑎 ∩ 𝐾) ⊆ 𝐾) |
| 41 | | eqid 2737 |
. . . . . . . . 9
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
| 42 | 18, 3, 41 | lsslss 20959 |
. . . . . . . 8
⊢ ((𝑆 ∈ LMod ∧ 𝐾 ∈ (LSubSp‘𝑆)) → ((𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑈) ↔ ((𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑆) ∧ (𝑎 ∩ 𝐾) ⊆ 𝐾))) |
| 43 | 33, 37, 42 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ((𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑈) ↔ ((𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑆) ∧ (𝑎 ∩ 𝐾) ⊆ 𝐾))) |
| 44 | 39, 40, 43 | mpbir2and 713 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑈)) |
| 45 | | eqid 2737 |
. . . . . . 7
⊢ (𝑈 ↾s (𝑎 ∩ 𝐾)) = (𝑈 ↾s (𝑎 ∩ 𝐾)) |
| 46 | 41, 45 | lnmlssfg 43092 |
. . . . . 6
⊢ ((𝑈 ∈ LNoeM ∧ (𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑈)) → (𝑈 ↾s (𝑎 ∩ 𝐾)) ∈ LFinGen) |
| 47 | 32, 44, 46 | syl2anc 584 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑈 ↾s (𝑎 ∩ 𝐾)) ∈ LFinGen) |
| 48 | 31, 47 | eqeltrd 2841 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ((𝑆 ↾s 𝑎) ↾s (◡(𝐹 ↾ 𝑎) “ { 0 })) ∈
LFinGen) |
| 49 | | incom 4209 |
. . . . . . . . 9
⊢ (ran
𝐹 ∩ ran (𝐹 ↾ 𝑎)) = (ran (𝐹 ↾ 𝑎) ∩ ran 𝐹) |
| 50 | | resss 6019 |
. . . . . . . . . . 11
⊢ (𝐹 ↾ 𝑎) ⊆ 𝐹 |
| 51 | | rnss 5950 |
. . . . . . . . . . 11
⊢ ((𝐹 ↾ 𝑎) ⊆ 𝐹 → ran (𝐹 ↾ 𝑎) ⊆ ran 𝐹) |
| 52 | 50, 51 | ax-mp 5 |
. . . . . . . . . 10
⊢ ran
(𝐹 ↾ 𝑎) ⊆ ran 𝐹 |
| 53 | | dfss2 3969 |
. . . . . . . . . 10
⊢ (ran
(𝐹 ↾ 𝑎) ⊆ ran 𝐹 ↔ (ran (𝐹 ↾ 𝑎) ∩ ran 𝐹) = ran (𝐹 ↾ 𝑎)) |
| 54 | 52, 53 | mpbi 230 |
. . . . . . . . 9
⊢ (ran
(𝐹 ↾ 𝑎) ∩ ran 𝐹) = ran (𝐹 ↾ 𝑎) |
| 55 | 49, 54 | eqtr2i 2766 |
. . . . . . . 8
⊢ ran
(𝐹 ↾ 𝑎) = (ran 𝐹 ∩ ran (𝐹 ↾ 𝑎)) |
| 56 | 55 | oveq2i 7442 |
. . . . . . 7
⊢ (𝑇 ↾s ran (𝐹 ↾ 𝑎)) = (𝑇 ↾s (ran 𝐹 ∩ ran (𝐹 ↾ 𝑎))) |
| 57 | | lmhmfgsplit.v |
. . . . . . . . 9
⊢ 𝑉 = (𝑇 ↾s ran 𝐹) |
| 58 | 57 | oveq1i 7441 |
. . . . . . . 8
⊢ (𝑉 ↾s ran (𝐹 ↾ 𝑎)) = ((𝑇 ↾s ran 𝐹) ↾s ran (𝐹 ↾ 𝑎)) |
| 59 | | rnexg 7924 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ran 𝐹 ∈ V) |
| 60 | | resexg 6045 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝐹 ↾ 𝑎) ∈ V) |
| 61 | | rnexg 7924 |
. . . . . . . . . 10
⊢ ((𝐹 ↾ 𝑎) ∈ V → ran (𝐹 ↾ 𝑎) ∈ V) |
| 62 | 60, 61 | syl 17 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ran (𝐹 ↾ 𝑎) ∈ V) |
| 63 | | ressress 17293 |
. . . . . . . . 9
⊢ ((ran
𝐹 ∈ V ∧ ran (𝐹 ↾ 𝑎) ∈ V) → ((𝑇 ↾s ran 𝐹) ↾s ran (𝐹 ↾ 𝑎)) = (𝑇 ↾s (ran 𝐹 ∩ ran (𝐹 ↾ 𝑎)))) |
| 64 | 59, 62, 63 | syl2anc 584 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ((𝑇 ↾s ran 𝐹) ↾s ran (𝐹 ↾ 𝑎)) = (𝑇 ↾s (ran 𝐹 ∩ ran (𝐹 ↾ 𝑎)))) |
| 65 | 58, 64 | eqtrid 2789 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝑉 ↾s ran (𝐹 ↾ 𝑎)) = (𝑇 ↾s (ran 𝐹 ∩ ran (𝐹 ↾ 𝑎)))) |
| 66 | 56, 65 | eqtr4id 2796 |
. . . . . 6
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝑇 ↾s ran (𝐹 ↾ 𝑎)) = (𝑉 ↾s ran (𝐹 ↾ 𝑎))) |
| 67 | 20, 66 | syl 17 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑇 ↾s ran (𝐹 ↾ 𝑎)) = (𝑉 ↾s ran (𝐹 ↾ 𝑎))) |
| 68 | | simpl3 1194 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝑉 ∈ LNoeM) |
| 69 | | lmhmrnlss 21049 |
. . . . . . . 8
⊢ ((𝐹 ↾ 𝑎) ∈ ((𝑆 ↾s 𝑎) LMHom 𝑇) → ran (𝐹 ↾ 𝑎) ∈ (LSubSp‘𝑇)) |
| 70 | 6, 69 | syl 17 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ran (𝐹 ↾ 𝑎) ∈ (LSubSp‘𝑇)) |
| 71 | 52 | a1i 11 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ran (𝐹 ↾ 𝑎) ⊆ ran 𝐹) |
| 72 | | lmhmlmod2 21031 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod) |
| 73 | 20, 72 | syl 17 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝑇 ∈ LMod) |
| 74 | | lmhmrnlss 21049 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ran 𝐹 ∈ (LSubSp‘𝑇)) |
| 75 | 20, 74 | syl 17 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ran 𝐹 ∈ (LSubSp‘𝑇)) |
| 76 | | eqid 2737 |
. . . . . . . . 9
⊢
(LSubSp‘𝑇) =
(LSubSp‘𝑇) |
| 77 | | eqid 2737 |
. . . . . . . . 9
⊢
(LSubSp‘𝑉) =
(LSubSp‘𝑉) |
| 78 | 57, 76, 77 | lsslss 20959 |
. . . . . . . 8
⊢ ((𝑇 ∈ LMod ∧ ran 𝐹 ∈ (LSubSp‘𝑇)) → (ran (𝐹 ↾ 𝑎) ∈ (LSubSp‘𝑉) ↔ (ran (𝐹 ↾ 𝑎) ∈ (LSubSp‘𝑇) ∧ ran (𝐹 ↾ 𝑎) ⊆ ran 𝐹))) |
| 79 | 73, 75, 78 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (ran (𝐹 ↾ 𝑎) ∈ (LSubSp‘𝑉) ↔ (ran (𝐹 ↾ 𝑎) ∈ (LSubSp‘𝑇) ∧ ran (𝐹 ↾ 𝑎) ⊆ ran 𝐹))) |
| 80 | 70, 71, 79 | mpbir2and 713 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ran (𝐹 ↾ 𝑎) ∈ (LSubSp‘𝑉)) |
| 81 | | eqid 2737 |
. . . . . . 7
⊢ (𝑉 ↾s ran (𝐹 ↾ 𝑎)) = (𝑉 ↾s ran (𝐹 ↾ 𝑎)) |
| 82 | 77, 81 | lnmlssfg 43092 |
. . . . . 6
⊢ ((𝑉 ∈ LNoeM ∧ ran (𝐹 ↾ 𝑎) ∈ (LSubSp‘𝑉)) → (𝑉 ↾s ran (𝐹 ↾ 𝑎)) ∈ LFinGen) |
| 83 | 68, 80, 82 | syl2anc 584 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑉 ↾s ran (𝐹 ↾ 𝑎)) ∈ LFinGen) |
| 84 | 67, 83 | eqeltrd 2841 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑇 ↾s ran (𝐹 ↾ 𝑎)) ∈ LFinGen) |
| 85 | | eqid 2737 |
. . . . 5
⊢ (◡(𝐹 ↾ 𝑎) “ { 0 }) = (◡(𝐹 ↾ 𝑎) “ { 0 }) |
| 86 | | eqid 2737 |
. . . . 5
⊢ ((𝑆 ↾s 𝑎) ↾s (◡(𝐹 ↾ 𝑎) “ { 0 })) = ((𝑆 ↾s 𝑎) ↾s (◡(𝐹 ↾ 𝑎) “ { 0 })) |
| 87 | | eqid 2737 |
. . . . 5
⊢ (𝑇 ↾s ran (𝐹 ↾ 𝑎)) = (𝑇 ↾s ran (𝐹 ↾ 𝑎)) |
| 88 | 35, 85, 86, 87 | lmhmfgsplit 43098 |
. . . 4
⊢ (((𝐹 ↾ 𝑎) ∈ ((𝑆 ↾s 𝑎) LMHom 𝑇) ∧ ((𝑆 ↾s 𝑎) ↾s (◡(𝐹 ↾ 𝑎) “ { 0 })) ∈ LFinGen ∧
(𝑇 ↾s ran
(𝐹 ↾ 𝑎)) ∈ LFinGen) → (𝑆 ↾s 𝑎) ∈
LFinGen) |
| 89 | 6, 48, 84, 88 | syl3anc 1373 |
. . 3
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑆 ↾s 𝑎) ∈ LFinGen) |
| 90 | 89 | ralrimiva 3146 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) → ∀𝑎 ∈ (LSubSp‘𝑆)(𝑆 ↾s 𝑎) ∈ LFinGen) |
| 91 | 3 | islnm 43089 |
. 2
⊢ (𝑆 ∈ LNoeM ↔ (𝑆 ∈ LMod ∧ ∀𝑎 ∈ (LSubSp‘𝑆)(𝑆 ↾s 𝑎) ∈ LFinGen)) |
| 92 | 2, 90, 91 | sylanbrc 583 |
1
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) → 𝑆 ∈ LNoeM) |