Step | Hyp | Ref
| Expression |
1 | | lmhmfgima.y |
. 2
⊢ 𝑌 = (𝑇 ↾s (𝐹 “ 𝐴)) |
2 | | lmhmfgima.xf |
. . . 4
⊢ (𝜑 → 𝑋 ∈ LFinGen) |
3 | | lmhmfgima.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) |
4 | | lmhmlmod1 19033 |
. . . . . 6
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod) |
5 | 3, 4 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ LMod) |
6 | | lmhmfgima.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑈) |
7 | | lmhmfgima.x |
. . . . . 6
⊢ 𝑋 = (𝑆 ↾s 𝐴) |
8 | | lmhmfgima.u |
. . . . . 6
⊢ 𝑈 = (LSubSp‘𝑆) |
9 | | eqid 2622 |
. . . . . 6
⊢
(LSpan‘𝑆) =
(LSpan‘𝑆) |
10 | | eqid 2622 |
. . . . . 6
⊢
(Base‘𝑆) =
(Base‘𝑆) |
11 | 7, 8, 9, 10 | islssfg2 37641 |
. . . . 5
⊢ ((𝑆 ∈ LMod ∧ 𝐴 ∈ 𝑈) → (𝑋 ∈ LFinGen ↔ ∃𝑥 ∈ (𝒫
(Base‘𝑆) ∩
Fin)((LSpan‘𝑆)‘𝑥) = 𝐴)) |
12 | 5, 6, 11 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (𝑋 ∈ LFinGen ↔ ∃𝑥 ∈ (𝒫
(Base‘𝑆) ∩
Fin)((LSpan‘𝑆)‘𝑥) = 𝐴)) |
13 | 2, 12 | mpbid 222 |
. . 3
⊢ (𝜑 → ∃𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)((LSpan‘𝑆)‘𝑥) = 𝐴) |
14 | | inss1 3833 |
. . . . . . . . . 10
⊢
(𝒫 (Base‘𝑆) ∩ Fin) ⊆ 𝒫
(Base‘𝑆) |
15 | 14 | sseli 3599 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫
(Base‘𝑆) ∩ Fin)
→ 𝑥 ∈ 𝒫
(Base‘𝑆)) |
16 | 15 | elpwid 4170 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫
(Base‘𝑆) ∩ Fin)
→ 𝑥 ⊆
(Base‘𝑆)) |
17 | | eqid 2622 |
. . . . . . . . 9
⊢
(LSpan‘𝑇) =
(LSpan‘𝑇) |
18 | 10, 9, 17 | lmhmlsp 19049 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑥 ⊆ (Base‘𝑆)) → (𝐹 “ ((LSpan‘𝑆)‘𝑥)) = ((LSpan‘𝑇)‘(𝐹 “ 𝑥))) |
19 | 3, 16, 18 | syl2an 494 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → (𝐹 “ ((LSpan‘𝑆)‘𝑥)) = ((LSpan‘𝑇)‘(𝐹 “ 𝑥))) |
20 | 19 | oveq2d 6666 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → (𝑇 ↾s (𝐹 “ ((LSpan‘𝑆)‘𝑥))) = (𝑇 ↾s ((LSpan‘𝑇)‘(𝐹 “ 𝑥)))) |
21 | | lmhmlmod2 19032 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod) |
22 | 3, 21 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ LMod) |
23 | 22 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → 𝑇 ∈ LMod) |
24 | | imassrn 5477 |
. . . . . . . . 9
⊢ (𝐹 “ 𝑥) ⊆ ran 𝐹 |
25 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(Base‘𝑇) =
(Base‘𝑇) |
26 | 10, 25 | lmhmf 19034 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
27 | 3, 26 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
28 | | frn 6053 |
. . . . . . . . . 10
⊢ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) → ran 𝐹 ⊆ (Base‘𝑇)) |
29 | 27, 28 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐹 ⊆ (Base‘𝑇)) |
30 | 24, 29 | syl5ss 3614 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 “ 𝑥) ⊆ (Base‘𝑇)) |
31 | 30 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → (𝐹 “ 𝑥) ⊆ (Base‘𝑇)) |
32 | | inss2 3834 |
. . . . . . . . . 10
⊢
(𝒫 (Base‘𝑆) ∩ Fin) ⊆ Fin |
33 | 32 | sseli 3599 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫
(Base‘𝑆) ∩ Fin)
→ 𝑥 ∈
Fin) |
34 | 33 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → 𝑥 ∈ Fin) |
35 | | ffun 6048 |
. . . . . . . . . . 11
⊢ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) → Fun 𝐹) |
36 | 27, 35 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → Fun 𝐹) |
37 | 36 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → Fun 𝐹) |
38 | 16 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → 𝑥 ⊆ (Base‘𝑆)) |
39 | | fdm 6051 |
. . . . . . . . . . . 12
⊢ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) → dom 𝐹 = (Base‘𝑆)) |
40 | 27, 39 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐹 = (Base‘𝑆)) |
41 | 40 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → dom 𝐹 = (Base‘𝑆)) |
42 | 38, 41 | sseqtr4d 3642 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → 𝑥 ⊆ dom 𝐹) |
43 | | fores 6124 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑥 ⊆ dom 𝐹) → (𝐹 ↾ 𝑥):𝑥–onto→(𝐹 “ 𝑥)) |
44 | 37, 42, 43 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥–onto→(𝐹 “ 𝑥)) |
45 | | fofi 8252 |
. . . . . . . 8
⊢ ((𝑥 ∈ Fin ∧ (𝐹 ↾ 𝑥):𝑥–onto→(𝐹 “ 𝑥)) → (𝐹 “ 𝑥) ∈ Fin) |
46 | 34, 44, 45 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → (𝐹 “ 𝑥) ∈ Fin) |
47 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑇 ↾s
((LSpan‘𝑇)‘(𝐹 “ 𝑥))) = (𝑇 ↾s ((LSpan‘𝑇)‘(𝐹 “ 𝑥))) |
48 | 17, 25, 47 | islssfgi 37642 |
. . . . . . 7
⊢ ((𝑇 ∈ LMod ∧ (𝐹 “ 𝑥) ⊆ (Base‘𝑇) ∧ (𝐹 “ 𝑥) ∈ Fin) → (𝑇 ↾s ((LSpan‘𝑇)‘(𝐹 “ 𝑥))) ∈ LFinGen) |
49 | 23, 31, 46, 48 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → (𝑇 ↾s
((LSpan‘𝑇)‘(𝐹 “ 𝑥))) ∈ LFinGen) |
50 | 20, 49 | eqeltrd 2701 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → (𝑇 ↾s (𝐹 “ ((LSpan‘𝑆)‘𝑥))) ∈ LFinGen) |
51 | | imaeq2 5462 |
. . . . . . 7
⊢
(((LSpan‘𝑆)‘𝑥) = 𝐴 → (𝐹 “ ((LSpan‘𝑆)‘𝑥)) = (𝐹 “ 𝐴)) |
52 | 51 | oveq2d 6666 |
. . . . . 6
⊢
(((LSpan‘𝑆)‘𝑥) = 𝐴 → (𝑇 ↾s (𝐹 “ ((LSpan‘𝑆)‘𝑥))) = (𝑇 ↾s (𝐹 “ 𝐴))) |
53 | 52 | eleq1d 2686 |
. . . . 5
⊢
(((LSpan‘𝑆)‘𝑥) = 𝐴 → ((𝑇 ↾s (𝐹 “ ((LSpan‘𝑆)‘𝑥))) ∈ LFinGen ↔ (𝑇 ↾s (𝐹 “ 𝐴)) ∈ LFinGen)) |
54 | 50, 53 | syl5ibcom 235 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) →
(((LSpan‘𝑆)‘𝑥) = 𝐴 → (𝑇 ↾s (𝐹 “ 𝐴)) ∈ LFinGen)) |
55 | 54 | rexlimdva 3031 |
. . 3
⊢ (𝜑 → (∃𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)((LSpan‘𝑆)‘𝑥) = 𝐴 → (𝑇 ↾s (𝐹 “ 𝐴)) ∈ LFinGen)) |
56 | 13, 55 | mpd 15 |
. 2
⊢ (𝜑 → (𝑇 ↾s (𝐹 “ 𝐴)) ∈ LFinGen) |
57 | 1, 56 | syl5eqel 2705 |
1
⊢ (𝜑 → 𝑌 ∈ LFinGen) |