Step | Hyp | Ref
| Expression |
1 | | lmhmlmod1 18854 |
. . 3
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod) |
2 | 1 | 3ad2ant1 1075 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) → 𝑆 ∈ LMod) |
3 | | eqid 2610 |
. . . . . 6
⊢
(LSubSp‘𝑆) =
(LSubSp‘𝑆) |
4 | | eqid 2610 |
. . . . . 6
⊢ (𝑆 ↾s 𝑎) = (𝑆 ↾s 𝑎) |
5 | 3, 4 | reslmhm 18873 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝐹 ↾ 𝑎) ∈ ((𝑆 ↾s 𝑎) LMHom 𝑇)) |
6 | 5 | 3ad2antl1 1216 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝐹 ↾ 𝑎) ∈ ((𝑆 ↾s 𝑎) LMHom 𝑇)) |
7 | | cnvresima 5541 |
. . . . . . . 8
⊢ (◡(𝐹 ↾ 𝑎) “ { 0 }) = ((◡𝐹 “ { 0 }) ∩ 𝑎) |
8 | | lmhmfgsplit.k |
. . . . . . . . . 10
⊢ 𝐾 = (◡𝐹 “ { 0 }) |
9 | 8 | eqcomi 2619 |
. . . . . . . . 9
⊢ (◡𝐹 “ { 0 }) = 𝐾 |
10 | 9 | ineq1i 3772 |
. . . . . . . 8
⊢ ((◡𝐹 “ { 0 }) ∩ 𝑎) = (𝐾 ∩ 𝑎) |
11 | | incom 3767 |
. . . . . . . 8
⊢ (𝐾 ∩ 𝑎) = (𝑎 ∩ 𝐾) |
12 | 7, 10, 11 | 3eqtri 2636 |
. . . . . . 7
⊢ (◡(𝐹 ↾ 𝑎) “ { 0 }) = (𝑎 ∩ 𝐾) |
13 | 12 | oveq2i 6560 |
. . . . . 6
⊢ ((𝑆 ↾s 𝑎) ↾s (◡(𝐹 ↾ 𝑎) “ { 0 })) = ((𝑆 ↾s 𝑎) ↾s (𝑎 ∩ 𝐾)) |
14 | | lmhmfgsplit.u |
. . . . . . . . 9
⊢ 𝑈 = (𝑆 ↾s 𝐾) |
15 | 14 | oveq1i 6559 |
. . . . . . . 8
⊢ (𝑈 ↾s (𝑎 ∩ 𝐾)) = ((𝑆 ↾s 𝐾) ↾s (𝑎 ∩ 𝐾)) |
16 | | simpl1 1057 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝐹 ∈ (𝑆 LMHom 𝑇)) |
17 | | cnvexg 7005 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ◡𝐹 ∈ V) |
18 | | imaexg 6995 |
. . . . . . . . . . . 12
⊢ (◡𝐹 ∈ V → (◡𝐹 “ { 0 }) ∈
V) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (◡𝐹 “ { 0 }) ∈
V) |
20 | 8, 19 | syl5eqel 2692 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐾 ∈ V) |
21 | 16, 20 | syl 17 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝐾 ∈ V) |
22 | | inss2 3796 |
. . . . . . . . 9
⊢ (𝑎 ∩ 𝐾) ⊆ 𝐾 |
23 | | ressabs 15766 |
. . . . . . . . 9
⊢ ((𝐾 ∈ V ∧ (𝑎 ∩ 𝐾) ⊆ 𝐾) → ((𝑆 ↾s 𝐾) ↾s (𝑎 ∩ 𝐾)) = (𝑆 ↾s (𝑎 ∩ 𝐾))) |
24 | 21, 22, 23 | sylancl 693 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ((𝑆 ↾s 𝐾) ↾s (𝑎 ∩ 𝐾)) = (𝑆 ↾s (𝑎 ∩ 𝐾))) |
25 | 15, 24 | syl5eq 2656 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑈 ↾s (𝑎 ∩ 𝐾)) = (𝑆 ↾s (𝑎 ∩ 𝐾))) |
26 | | vex 3176 |
. . . . . . . 8
⊢ 𝑎 ∈ V |
27 | | inss1 3795 |
. . . . . . . 8
⊢ (𝑎 ∩ 𝐾) ⊆ 𝑎 |
28 | | ressabs 15766 |
. . . . . . . 8
⊢ ((𝑎 ∈ V ∧ (𝑎 ∩ 𝐾) ⊆ 𝑎) → ((𝑆 ↾s 𝑎) ↾s (𝑎 ∩ 𝐾)) = (𝑆 ↾s (𝑎 ∩ 𝐾))) |
29 | 26, 27, 28 | mp2an 704 |
. . . . . . 7
⊢ ((𝑆 ↾s 𝑎) ↾s (𝑎 ∩ 𝐾)) = (𝑆 ↾s (𝑎 ∩ 𝐾)) |
30 | 25, 29 | syl6reqr 2663 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ((𝑆 ↾s 𝑎) ↾s (𝑎 ∩ 𝐾)) = (𝑈 ↾s (𝑎 ∩ 𝐾))) |
31 | 13, 30 | syl5eq 2656 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ((𝑆 ↾s 𝑎) ↾s (◡(𝐹 ↾ 𝑎) “ { 0 })) = (𝑈 ↾s (𝑎 ∩ 𝐾))) |
32 | | simpl2 1058 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝑈 ∈ LNoeM) |
33 | 2 | adantr 480 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝑆 ∈ LMod) |
34 | | simpr 476 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝑎 ∈ (LSubSp‘𝑆)) |
35 | | lmhmfgsplit.z |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑇) |
36 | 8, 35, 3 | lmhmkerlss 18872 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐾 ∈ (LSubSp‘𝑆)) |
37 | 16, 36 | syl 17 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝐾 ∈ (LSubSp‘𝑆)) |
38 | 3 | lssincl 18786 |
. . . . . . . 8
⊢ ((𝑆 ∈ LMod ∧ 𝑎 ∈ (LSubSp‘𝑆) ∧ 𝐾 ∈ (LSubSp‘𝑆)) → (𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑆)) |
39 | 33, 34, 37, 38 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑆)) |
40 | 22 | a1i 11 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑎 ∩ 𝐾) ⊆ 𝐾) |
41 | | eqid 2610 |
. . . . . . . . 9
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
42 | 14, 3, 41 | lsslss 18782 |
. . . . . . . 8
⊢ ((𝑆 ∈ LMod ∧ 𝐾 ∈ (LSubSp‘𝑆)) → ((𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑈) ↔ ((𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑆) ∧ (𝑎 ∩ 𝐾) ⊆ 𝐾))) |
43 | 33, 37, 42 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ((𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑈) ↔ ((𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑆) ∧ (𝑎 ∩ 𝐾) ⊆ 𝐾))) |
44 | 39, 40, 43 | mpbir2and 959 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑈)) |
45 | | eqid 2610 |
. . . . . . 7
⊢ (𝑈 ↾s (𝑎 ∩ 𝐾)) = (𝑈 ↾s (𝑎 ∩ 𝐾)) |
46 | 41, 45 | lnmlssfg 36668 |
. . . . . 6
⊢ ((𝑈 ∈ LNoeM ∧ (𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑈)) → (𝑈 ↾s (𝑎 ∩ 𝐾)) ∈ LFinGen) |
47 | 32, 44, 46 | syl2anc 691 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑈 ↾s (𝑎 ∩ 𝐾)) ∈ LFinGen) |
48 | 31, 47 | eqeltrd 2688 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ((𝑆 ↾s 𝑎) ↾s (◡(𝐹 ↾ 𝑎) “ { 0 })) ∈
LFinGen) |
49 | | lmhmfgsplit.v |
. . . . . . . . 9
⊢ 𝑉 = (𝑇 ↾s ran 𝐹) |
50 | 49 | oveq1i 6559 |
. . . . . . . 8
⊢ (𝑉 ↾s ran (𝐹 ↾ 𝑎)) = ((𝑇 ↾s ran 𝐹) ↾s ran (𝐹 ↾ 𝑎)) |
51 | | rnexg 6990 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ran 𝐹 ∈ V) |
52 | | resexg 5362 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝐹 ↾ 𝑎) ∈ V) |
53 | | rnexg 6990 |
. . . . . . . . . 10
⊢ ((𝐹 ↾ 𝑎) ∈ V → ran (𝐹 ↾ 𝑎) ∈ V) |
54 | 52, 53 | syl 17 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ran (𝐹 ↾ 𝑎) ∈ V) |
55 | | ressress 15765 |
. . . . . . . . 9
⊢ ((ran
𝐹 ∈ V ∧ ran (𝐹 ↾ 𝑎) ∈ V) → ((𝑇 ↾s ran 𝐹) ↾s ran (𝐹 ↾ 𝑎)) = (𝑇 ↾s (ran 𝐹 ∩ ran (𝐹 ↾ 𝑎)))) |
56 | 51, 54, 55 | syl2anc 691 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ((𝑇 ↾s ran 𝐹) ↾s ran (𝐹 ↾ 𝑎)) = (𝑇 ↾s (ran 𝐹 ∩ ran (𝐹 ↾ 𝑎)))) |
57 | 50, 56 | syl5eq 2656 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝑉 ↾s ran (𝐹 ↾ 𝑎)) = (𝑇 ↾s (ran 𝐹 ∩ ran (𝐹 ↾ 𝑎)))) |
58 | | incom 3767 |
. . . . . . . . 9
⊢ (ran
𝐹 ∩ ran (𝐹 ↾ 𝑎)) = (ran (𝐹 ↾ 𝑎) ∩ ran 𝐹) |
59 | | resss 5342 |
. . . . . . . . . . 11
⊢ (𝐹 ↾ 𝑎) ⊆ 𝐹 |
60 | | rnss 5275 |
. . . . . . . . . . 11
⊢ ((𝐹 ↾ 𝑎) ⊆ 𝐹 → ran (𝐹 ↾ 𝑎) ⊆ ran 𝐹) |
61 | 59, 60 | ax-mp 5 |
. . . . . . . . . 10
⊢ ran
(𝐹 ↾ 𝑎) ⊆ ran 𝐹 |
62 | | df-ss 3554 |
. . . . . . . . . 10
⊢ (ran
(𝐹 ↾ 𝑎) ⊆ ran 𝐹 ↔ (ran (𝐹 ↾ 𝑎) ∩ ran 𝐹) = ran (𝐹 ↾ 𝑎)) |
63 | 61, 62 | mpbi 219 |
. . . . . . . . 9
⊢ (ran
(𝐹 ↾ 𝑎) ∩ ran 𝐹) = ran (𝐹 ↾ 𝑎) |
64 | 58, 63 | eqtr2i 2633 |
. . . . . . . 8
⊢ ran
(𝐹 ↾ 𝑎) = (ran 𝐹 ∩ ran (𝐹 ↾ 𝑎)) |
65 | 64 | oveq2i 6560 |
. . . . . . 7
⊢ (𝑇 ↾s ran (𝐹 ↾ 𝑎)) = (𝑇 ↾s (ran 𝐹 ∩ ran (𝐹 ↾ 𝑎))) |
66 | 57, 65 | syl6reqr 2663 |
. . . . . 6
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝑇 ↾s ran (𝐹 ↾ 𝑎)) = (𝑉 ↾s ran (𝐹 ↾ 𝑎))) |
67 | 16, 66 | syl 17 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑇 ↾s ran (𝐹 ↾ 𝑎)) = (𝑉 ↾s ran (𝐹 ↾ 𝑎))) |
68 | | simpl3 1059 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝑉 ∈ LNoeM) |
69 | | lmhmrnlss 18871 |
. . . . . . . 8
⊢ ((𝐹 ↾ 𝑎) ∈ ((𝑆 ↾s 𝑎) LMHom 𝑇) → ran (𝐹 ↾ 𝑎) ∈ (LSubSp‘𝑇)) |
70 | 6, 69 | syl 17 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ran (𝐹 ↾ 𝑎) ∈ (LSubSp‘𝑇)) |
71 | 61 | a1i 11 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ran (𝐹 ↾ 𝑎) ⊆ ran 𝐹) |
72 | | lmhmlmod2 18853 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod) |
73 | 16, 72 | syl 17 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝑇 ∈ LMod) |
74 | | lmhmrnlss 18871 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ran 𝐹 ∈ (LSubSp‘𝑇)) |
75 | 16, 74 | syl 17 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ran 𝐹 ∈ (LSubSp‘𝑇)) |
76 | | eqid 2610 |
. . . . . . . . 9
⊢
(LSubSp‘𝑇) =
(LSubSp‘𝑇) |
77 | | eqid 2610 |
. . . . . . . . 9
⊢
(LSubSp‘𝑉) =
(LSubSp‘𝑉) |
78 | 49, 76, 77 | lsslss 18782 |
. . . . . . . 8
⊢ ((𝑇 ∈ LMod ∧ ran 𝐹 ∈ (LSubSp‘𝑇)) → (ran (𝐹 ↾ 𝑎) ∈ (LSubSp‘𝑉) ↔ (ran (𝐹 ↾ 𝑎) ∈ (LSubSp‘𝑇) ∧ ran (𝐹 ↾ 𝑎) ⊆ ran 𝐹))) |
79 | 73, 75, 78 | syl2anc 691 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (ran (𝐹 ↾ 𝑎) ∈ (LSubSp‘𝑉) ↔ (ran (𝐹 ↾ 𝑎) ∈ (LSubSp‘𝑇) ∧ ran (𝐹 ↾ 𝑎) ⊆ ran 𝐹))) |
80 | 70, 71, 79 | mpbir2and 959 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ran (𝐹 ↾ 𝑎) ∈ (LSubSp‘𝑉)) |
81 | | eqid 2610 |
. . . . . . 7
⊢ (𝑉 ↾s ran (𝐹 ↾ 𝑎)) = (𝑉 ↾s ran (𝐹 ↾ 𝑎)) |
82 | 77, 81 | lnmlssfg 36668 |
. . . . . 6
⊢ ((𝑉 ∈ LNoeM ∧ ran (𝐹 ↾ 𝑎) ∈ (LSubSp‘𝑉)) → (𝑉 ↾s ran (𝐹 ↾ 𝑎)) ∈ LFinGen) |
83 | 68, 80, 82 | syl2anc 691 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑉 ↾s ran (𝐹 ↾ 𝑎)) ∈ LFinGen) |
84 | 67, 83 | eqeltrd 2688 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑇 ↾s ran (𝐹 ↾ 𝑎)) ∈ LFinGen) |
85 | | eqid 2610 |
. . . . 5
⊢ (◡(𝐹 ↾ 𝑎) “ { 0 }) = (◡(𝐹 ↾ 𝑎) “ { 0 }) |
86 | | eqid 2610 |
. . . . 5
⊢ ((𝑆 ↾s 𝑎) ↾s (◡(𝐹 ↾ 𝑎) “ { 0 })) = ((𝑆 ↾s 𝑎) ↾s (◡(𝐹 ↾ 𝑎) “ { 0 })) |
87 | | eqid 2610 |
. . . . 5
⊢ (𝑇 ↾s ran (𝐹 ↾ 𝑎)) = (𝑇 ↾s ran (𝐹 ↾ 𝑎)) |
88 | 35, 85, 86, 87 | lmhmfgsplit 36674 |
. . . 4
⊢ (((𝐹 ↾ 𝑎) ∈ ((𝑆 ↾s 𝑎) LMHom 𝑇) ∧ ((𝑆 ↾s 𝑎) ↾s (◡(𝐹 ↾ 𝑎) “ { 0 })) ∈ LFinGen ∧
(𝑇 ↾s ran
(𝐹 ↾ 𝑎)) ∈ LFinGen) → (𝑆 ↾s 𝑎) ∈
LFinGen) |
89 | 6, 48, 84, 88 | syl3anc 1318 |
. . 3
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑆 ↾s 𝑎) ∈ LFinGen) |
90 | 89 | ralrimiva 2949 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) → ∀𝑎 ∈ (LSubSp‘𝑆)(𝑆 ↾s 𝑎) ∈ LFinGen) |
91 | 3 | islnm 36665 |
. 2
⊢ (𝑆 ∈ LNoeM ↔ (𝑆 ∈ LMod ∧ ∀𝑎 ∈ (LSubSp‘𝑆)(𝑆 ↾s 𝑎) ∈ LFinGen)) |
92 | 2, 90, 91 | sylanbrc 695 |
1
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) → 𝑆 ∈ LNoeM) |