Step | Hyp | Ref
| Expression |
1 | | lmhmlmod1 20293 |
. . 3
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod) |
2 | 1 | 3ad2ant1 1132 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) → 𝑆 ∈ LMod) |
3 | | eqid 2740 |
. . . . . 6
⊢
(LSubSp‘𝑆) =
(LSubSp‘𝑆) |
4 | | eqid 2740 |
. . . . . 6
⊢ (𝑆 ↾s 𝑎) = (𝑆 ↾s 𝑎) |
5 | 3, 4 | reslmhm 20312 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝐹 ↾ 𝑎) ∈ ((𝑆 ↾s 𝑎) LMHom 𝑇)) |
6 | 5 | 3ad2antl1 1184 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝐹 ↾ 𝑎) ∈ ((𝑆 ↾s 𝑎) LMHom 𝑇)) |
7 | | cnvresima 6132 |
. . . . . . . 8
⊢ (◡(𝐹 ↾ 𝑎) “ { 0 }) = ((◡𝐹 “ { 0 }) ∩ 𝑎) |
8 | | lmhmfgsplit.k |
. . . . . . . . . 10
⊢ 𝐾 = (◡𝐹 “ { 0 }) |
9 | 8 | eqcomi 2749 |
. . . . . . . . 9
⊢ (◡𝐹 “ { 0 }) = 𝐾 |
10 | 9 | ineq1i 4148 |
. . . . . . . 8
⊢ ((◡𝐹 “ { 0 }) ∩ 𝑎) = (𝐾 ∩ 𝑎) |
11 | | incom 4140 |
. . . . . . . 8
⊢ (𝐾 ∩ 𝑎) = (𝑎 ∩ 𝐾) |
12 | 7, 10, 11 | 3eqtri 2772 |
. . . . . . 7
⊢ (◡(𝐹 ↾ 𝑎) “ { 0 }) = (𝑎 ∩ 𝐾) |
13 | 12 | oveq2i 7282 |
. . . . . 6
⊢ ((𝑆 ↾s 𝑎) ↾s (◡(𝐹 ↾ 𝑎) “ { 0 })) = ((𝑆 ↾s 𝑎) ↾s (𝑎 ∩ 𝐾)) |
14 | | vex 3435 |
. . . . . . . 8
⊢ 𝑎 ∈ V |
15 | | inss1 4168 |
. . . . . . . 8
⊢ (𝑎 ∩ 𝐾) ⊆ 𝑎 |
16 | | ressabs 16957 |
. . . . . . . 8
⊢ ((𝑎 ∈ V ∧ (𝑎 ∩ 𝐾) ⊆ 𝑎) → ((𝑆 ↾s 𝑎) ↾s (𝑎 ∩ 𝐾)) = (𝑆 ↾s (𝑎 ∩ 𝐾))) |
17 | 14, 15, 16 | mp2an 689 |
. . . . . . 7
⊢ ((𝑆 ↾s 𝑎) ↾s (𝑎 ∩ 𝐾)) = (𝑆 ↾s (𝑎 ∩ 𝐾)) |
18 | | lmhmfgsplit.u |
. . . . . . . . 9
⊢ 𝑈 = (𝑆 ↾s 𝐾) |
19 | 18 | oveq1i 7281 |
. . . . . . . 8
⊢ (𝑈 ↾s (𝑎 ∩ 𝐾)) = ((𝑆 ↾s 𝐾) ↾s (𝑎 ∩ 𝐾)) |
20 | | simpl1 1190 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝐹 ∈ (𝑆 LMHom 𝑇)) |
21 | | cnvexg 7765 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ◡𝐹 ∈ V) |
22 | | imaexg 7756 |
. . . . . . . . . . . 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 4169 |
. . . . . . . . 9
⊢ (𝑎 ∩ 𝐾) ⊆ 𝐾 |
27 | | ressabs 16957 |
. . . . . . . . 9
⊢ ((𝐾 ∈ V ∧ (𝑎 ∩ 𝐾) ⊆ 𝐾) → ((𝑆 ↾s 𝐾) ↾s (𝑎 ∩ 𝐾)) = (𝑆 ↾s (𝑎 ∩ 𝐾))) |
28 | 25, 26, 27 | sylancl 586 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ((𝑆 ↾s 𝐾) ↾s (𝑎 ∩ 𝐾)) = (𝑆 ↾s (𝑎 ∩ 𝐾))) |
29 | 19, 28 | eqtrid 2792 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑈 ↾s (𝑎 ∩ 𝐾)) = (𝑆 ↾s (𝑎 ∩ 𝐾))) |
30 | 17, 29 | eqtr4id 2799 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ((𝑆 ↾s 𝑎) ↾s (𝑎 ∩ 𝐾)) = (𝑈 ↾s (𝑎 ∩ 𝐾))) |
31 | 13, 30 | eqtrid 2792 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ((𝑆 ↾s 𝑎) ↾s (◡(𝐹 ↾ 𝑎) “ { 0 })) = (𝑈 ↾s (𝑎 ∩ 𝐾))) |
32 | | simpl2 1191 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝑈 ∈ LNoeM) |
33 | 2 | adantr 481 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝑆 ∈ LMod) |
34 | | simpr 485 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝑎 ∈ (LSubSp‘𝑆)) |
35 | | lmhmfgsplit.z |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑇) |
36 | 8, 35, 3 | lmhmkerlss 20311 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐾 ∈ (LSubSp‘𝑆)) |
37 | 20, 36 | syl 17 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝐾 ∈ (LSubSp‘𝑆)) |
38 | 3 | lssincl 20225 |
. . . . . . . 8
⊢ ((𝑆 ∈ LMod ∧ 𝑎 ∈ (LSubSp‘𝑆) ∧ 𝐾 ∈ (LSubSp‘𝑆)) → (𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑆)) |
39 | 33, 34, 37, 38 | syl3anc 1370 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑆)) |
40 | 26 | a1i 11 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑎 ∩ 𝐾) ⊆ 𝐾) |
41 | | eqid 2740 |
. . . . . . . . 9
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
42 | 18, 3, 41 | lsslss 20221 |
. . . . . . . 8
⊢ ((𝑆 ∈ LMod ∧ 𝐾 ∈ (LSubSp‘𝑆)) → ((𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑈) ↔ ((𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑆) ∧ (𝑎 ∩ 𝐾) ⊆ 𝐾))) |
43 | 33, 37, 42 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ((𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑈) ↔ ((𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑆) ∧ (𝑎 ∩ 𝐾) ⊆ 𝐾))) |
44 | 39, 40, 43 | mpbir2and 710 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑎 ∩ 𝐾) ∈ (LSubSp‘𝑈)) |
45 | | eqid 2740 |
. . . . . . 7
⊢ (𝑈 ↾s (𝑎 ∩ 𝐾)) = (𝑈 ↾s (𝑎 ∩ 𝐾)) |
46 | 41, 45 | lnmlssfg 40902 |
. . . . . 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 4140 |
. . . . . . . . 9
⊢ (ran
𝐹 ∩ ran (𝐹 ↾ 𝑎)) = (ran (𝐹 ↾ 𝑎) ∩ ran 𝐹) |
50 | | resss 5915 |
. . . . . . . . . . 11
⊢ (𝐹 ↾ 𝑎) ⊆ 𝐹 |
51 | | rnss 5847 |
. . . . . . . . . . 11
⊢ ((𝐹 ↾ 𝑎) ⊆ 𝐹 → ran (𝐹 ↾ 𝑎) ⊆ ran 𝐹) |
52 | 50, 51 | ax-mp 5 |
. . . . . . . . . 10
⊢ ran
(𝐹 ↾ 𝑎) ⊆ ran 𝐹 |
53 | | df-ss 3909 |
. . . . . . . . . 10
⊢ (ran
(𝐹 ↾ 𝑎) ⊆ ran 𝐹 ↔ (ran (𝐹 ↾ 𝑎) ∩ ran 𝐹) = ran (𝐹 ↾ 𝑎)) |
54 | 52, 53 | mpbi 229 |
. . . . . . . . 9
⊢ (ran
(𝐹 ↾ 𝑎) ∩ ran 𝐹) = ran (𝐹 ↾ 𝑎) |
55 | 49, 54 | eqtr2i 2769 |
. . . . . . . 8
⊢ ran
(𝐹 ↾ 𝑎) = (ran 𝐹 ∩ ran (𝐹 ↾ 𝑎)) |
56 | 55 | oveq2i 7282 |
. . . . . . 7
⊢ (𝑇 ↾s ran (𝐹 ↾ 𝑎)) = (𝑇 ↾s (ran 𝐹 ∩ ran (𝐹 ↾ 𝑎))) |
57 | | lmhmfgsplit.v |
. . . . . . . . 9
⊢ 𝑉 = (𝑇 ↾s ran 𝐹) |
58 | 57 | oveq1i 7281 |
. . . . . . . 8
⊢ (𝑉 ↾s ran (𝐹 ↾ 𝑎)) = ((𝑇 ↾s ran 𝐹) ↾s ran (𝐹 ↾ 𝑎)) |
59 | | rnexg 7745 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ran 𝐹 ∈ V) |
60 | | resexg 5936 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝐹 ↾ 𝑎) ∈ V) |
61 | | rnexg 7745 |
. . . . . . . . . 10
⊢ ((𝐹 ↾ 𝑎) ∈ V → ran (𝐹 ↾ 𝑎) ∈ V) |
62 | 60, 61 | syl 17 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ran (𝐹 ↾ 𝑎) ∈ V) |
63 | | ressress 16956 |
. . . . . . . . 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 2792 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝑉 ↾s ran (𝐹 ↾ 𝑎)) = (𝑇 ↾s (ran 𝐹 ∩ ran (𝐹 ↾ 𝑎)))) |
66 | 56, 65 | eqtr4id 2799 |
. . . . . 6
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → (𝑇 ↾s ran (𝐹 ↾ 𝑎)) = (𝑉 ↾s ran (𝐹 ↾ 𝑎))) |
67 | 20, 66 | syl 17 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑇 ↾s ran (𝐹 ↾ 𝑎)) = (𝑉 ↾s ran (𝐹 ↾ 𝑎))) |
68 | | simpl3 1192 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝑉 ∈ LNoeM) |
69 | | lmhmrnlss 20310 |
. . . . . . . 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 20292 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod) |
73 | 20, 72 | syl 17 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → 𝑇 ∈ LMod) |
74 | | lmhmrnlss 20310 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ran 𝐹 ∈ (LSubSp‘𝑇)) |
75 | 20, 74 | syl 17 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ran 𝐹 ∈ (LSubSp‘𝑇)) |
76 | | eqid 2740 |
. . . . . . . . 9
⊢
(LSubSp‘𝑇) =
(LSubSp‘𝑇) |
77 | | eqid 2740 |
. . . . . . . . 9
⊢
(LSubSp‘𝑉) =
(LSubSp‘𝑉) |
78 | 57, 76, 77 | lsslss 20221 |
. . . . . . . 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 710 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → ran (𝐹 ↾ 𝑎) ∈ (LSubSp‘𝑉)) |
81 | | eqid 2740 |
. . . . . . 7
⊢ (𝑉 ↾s ran (𝐹 ↾ 𝑎)) = (𝑉 ↾s ran (𝐹 ↾ 𝑎)) |
82 | 77, 81 | lnmlssfg 40902 |
. . . . . 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 2740 |
. . . . 5
⊢ (◡(𝐹 ↾ 𝑎) “ { 0 }) = (◡(𝐹 ↾ 𝑎) “ { 0 }) |
86 | | eqid 2740 |
. . . . 5
⊢ ((𝑆 ↾s 𝑎) ↾s (◡(𝐹 ↾ 𝑎) “ { 0 })) = ((𝑆 ↾s 𝑎) ↾s (◡(𝐹 ↾ 𝑎) “ { 0 })) |
87 | | eqid 2740 |
. . . . 5
⊢ (𝑇 ↾s ran (𝐹 ↾ 𝑎)) = (𝑇 ↾s ran (𝐹 ↾ 𝑎)) |
88 | 35, 85, 86, 87 | lmhmfgsplit 40908 |
. . . 4
⊢ (((𝐹 ↾ 𝑎) ∈ ((𝑆 ↾s 𝑎) LMHom 𝑇) ∧ ((𝑆 ↾s 𝑎) ↾s (◡(𝐹 ↾ 𝑎) “ { 0 })) ∈ LFinGen ∧
(𝑇 ↾s ran
(𝐹 ↾ 𝑎)) ∈ LFinGen) → (𝑆 ↾s 𝑎) ∈
LFinGen) |
89 | 6, 48, 84, 88 | syl3anc 1370 |
. . 3
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) ∧ 𝑎 ∈ (LSubSp‘𝑆)) → (𝑆 ↾s 𝑎) ∈ LFinGen) |
90 | 89 | ralrimiva 3110 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) → ∀𝑎 ∈ (LSubSp‘𝑆)(𝑆 ↾s 𝑎) ∈ LFinGen) |
91 | 3 | islnm 40899 |
. 2
⊢ (𝑆 ∈ LNoeM ↔ (𝑆 ∈ LMod ∧ ∀𝑎 ∈ (LSubSp‘𝑆)(𝑆 ↾s 𝑎) ∈ LFinGen)) |
92 | 2, 90, 91 | sylanbrc 583 |
1
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑈 ∈ LNoeM ∧ 𝑉 ∈ LNoeM) → 𝑆 ∈ LNoeM) |