Step | Hyp | Ref
| Expression |
1 | | lmhmfgima.y |
. 2
⊢ 𝑌 = (𝑇 ↾s (𝐹 “ 𝐴)) |
2 | | lmhmfgima.xf |
. . . 4
⊢ (𝜑 → 𝑋 ∈ LFinGen) |
3 | | lmhmfgima.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) |
4 | | lmhmlmod1 20075 |
. . . . . 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 2737 |
. . . . . 6
⊢
(LSpan‘𝑆) =
(LSpan‘𝑆) |
10 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑆) =
(Base‘𝑆) |
11 | 7, 8, 9, 10 | islssfg2 40607 |
. . . . 5
⊢ ((𝑆 ∈ LMod ∧ 𝐴 ∈ 𝑈) → (𝑋 ∈ LFinGen ↔ ∃𝑥 ∈ (𝒫
(Base‘𝑆) ∩
Fin)((LSpan‘𝑆)‘𝑥) = 𝐴)) |
12 | 5, 6, 11 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (𝑋 ∈ LFinGen ↔ ∃𝑥 ∈ (𝒫
(Base‘𝑆) ∩
Fin)((LSpan‘𝑆)‘𝑥) = 𝐴)) |
13 | 2, 12 | mpbid 235 |
. . 3
⊢ (𝜑 → ∃𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)((LSpan‘𝑆)‘𝑥) = 𝐴) |
14 | | inss1 4148 |
. . . . . . . . . 10
⊢
(𝒫 (Base‘𝑆) ∩ Fin) ⊆ 𝒫
(Base‘𝑆) |
15 | 14 | sseli 3901 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫
(Base‘𝑆) ∩ Fin)
→ 𝑥 ∈ 𝒫
(Base‘𝑆)) |
16 | 15 | elpwid 4529 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫
(Base‘𝑆) ∩ Fin)
→ 𝑥 ⊆
(Base‘𝑆)) |
17 | | eqid 2737 |
. . . . . . . . 9
⊢
(LSpan‘𝑇) =
(LSpan‘𝑇) |
18 | 10, 9, 17 | lmhmlsp 20091 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑥 ⊆ (Base‘𝑆)) → (𝐹 “ ((LSpan‘𝑆)‘𝑥)) = ((LSpan‘𝑇)‘(𝐹 “ 𝑥))) |
19 | 3, 16, 18 | syl2an 599 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → (𝐹 “ ((LSpan‘𝑆)‘𝑥)) = ((LSpan‘𝑇)‘(𝐹 “ 𝑥))) |
20 | 19 | oveq2d 7234 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → (𝑇 ↾s (𝐹 “ ((LSpan‘𝑆)‘𝑥))) = (𝑇 ↾s ((LSpan‘𝑇)‘(𝐹 “ 𝑥)))) |
21 | | lmhmlmod2 20074 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod) |
22 | 3, 21 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ LMod) |
23 | 22 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → 𝑇 ∈ LMod) |
24 | | imassrn 5945 |
. . . . . . . . 9
⊢ (𝐹 “ 𝑥) ⊆ ran 𝐹 |
25 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘𝑇) =
(Base‘𝑇) |
26 | 10, 25 | lmhmf 20076 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
27 | 3, 26 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
28 | 27 | frnd 6558 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐹 ⊆ (Base‘𝑇)) |
29 | 24, 28 | sstrid 3917 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 “ 𝑥) ⊆ (Base‘𝑇)) |
30 | 29 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → (𝐹 “ 𝑥) ⊆ (Base‘𝑇)) |
31 | | inss2 4149 |
. . . . . . . . . 10
⊢
(𝒫 (Base‘𝑆) ∩ Fin) ⊆ Fin |
32 | 31 | sseli 3901 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫
(Base‘𝑆) ∩ Fin)
→ 𝑥 ∈
Fin) |
33 | 32 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → 𝑥 ∈ Fin) |
34 | 27 | ffund 6554 |
. . . . . . . . . 10
⊢ (𝜑 → Fun 𝐹) |
35 | 34 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → Fun 𝐹) |
36 | 16 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → 𝑥 ⊆ (Base‘𝑆)) |
37 | 27 | fdmd 6561 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐹 = (Base‘𝑆)) |
38 | 37 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → dom 𝐹 = (Base‘𝑆)) |
39 | 36, 38 | sseqtrrd 3947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → 𝑥 ⊆ dom 𝐹) |
40 | | fores 6648 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑥 ⊆ dom 𝐹) → (𝐹 ↾ 𝑥):𝑥–onto→(𝐹 “ 𝑥)) |
41 | 35, 39, 40 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → (𝐹 ↾ 𝑥):𝑥–onto→(𝐹 “ 𝑥)) |
42 | | fofi 8967 |
. . . . . . . 8
⊢ ((𝑥 ∈ Fin ∧ (𝐹 ↾ 𝑥):𝑥–onto→(𝐹 “ 𝑥)) → (𝐹 “ 𝑥) ∈ Fin) |
43 | 33, 41, 42 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → (𝐹 “ 𝑥) ∈ Fin) |
44 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑇 ↾s
((LSpan‘𝑇)‘(𝐹 “ 𝑥))) = (𝑇 ↾s ((LSpan‘𝑇)‘(𝐹 “ 𝑥))) |
45 | 17, 25, 44 | islssfgi 40608 |
. . . . . . 7
⊢ ((𝑇 ∈ LMod ∧ (𝐹 “ 𝑥) ⊆ (Base‘𝑇) ∧ (𝐹 “ 𝑥) ∈ Fin) → (𝑇 ↾s ((LSpan‘𝑇)‘(𝐹 “ 𝑥))) ∈ LFinGen) |
46 | 23, 30, 43, 45 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → (𝑇 ↾s
((LSpan‘𝑇)‘(𝐹 “ 𝑥))) ∈ LFinGen) |
47 | 20, 46 | eqeltrd 2838 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) → (𝑇 ↾s (𝐹 “ ((LSpan‘𝑆)‘𝑥))) ∈ LFinGen) |
48 | | imaeq2 5930 |
. . . . . . 7
⊢
(((LSpan‘𝑆)‘𝑥) = 𝐴 → (𝐹 “ ((LSpan‘𝑆)‘𝑥)) = (𝐹 “ 𝐴)) |
49 | 48 | oveq2d 7234 |
. . . . . 6
⊢
(((LSpan‘𝑆)‘𝑥) = 𝐴 → (𝑇 ↾s (𝐹 “ ((LSpan‘𝑆)‘𝑥))) = (𝑇 ↾s (𝐹 “ 𝐴))) |
50 | 49 | eleq1d 2822 |
. . . . 5
⊢
(((LSpan‘𝑆)‘𝑥) = 𝐴 → ((𝑇 ↾s (𝐹 “ ((LSpan‘𝑆)‘𝑥))) ∈ LFinGen ↔ (𝑇 ↾s (𝐹 “ 𝐴)) ∈ LFinGen)) |
51 | 47, 50 | syl5ibcom 248 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)) →
(((LSpan‘𝑆)‘𝑥) = 𝐴 → (𝑇 ↾s (𝐹 “ 𝐴)) ∈ LFinGen)) |
52 | 51 | rexlimdva 3208 |
. . 3
⊢ (𝜑 → (∃𝑥 ∈ (𝒫 (Base‘𝑆) ∩ Fin)((LSpan‘𝑆)‘𝑥) = 𝐴 → (𝑇 ↾s (𝐹 “ 𝐴)) ∈ LFinGen)) |
53 | 13, 52 | mpd 15 |
. 2
⊢ (𝜑 → (𝑇 ↾s (𝐹 “ 𝐴)) ∈ LFinGen) |
54 | 1, 53 | eqeltrid 2842 |
1
⊢ (𝜑 → 𝑌 ∈ LFinGen) |