Step | Hyp | Ref
| Expression |
1 | | lsmfgcl.f |
. 2
⊢ 𝐹 = (𝑊 ↾s (𝐴 ⊕ 𝐵)) |
2 | | lsmfgcl.df |
. . . 4
⊢ (𝜑 → 𝐷 ∈ LFinGen) |
3 | | lsmfgcl.w |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ LMod) |
4 | | lsmfgcl.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑈) |
5 | | lsmfgcl.d |
. . . . . 6
⊢ 𝐷 = (𝑊 ↾s 𝐴) |
6 | | lsmfgcl.u |
. . . . . 6
⊢ 𝑈 = (LSubSp‘𝑊) |
7 | | eqid 2737 |
. . . . . 6
⊢
(LSpan‘𝑊) =
(LSpan‘𝑊) |
8 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑊) =
(Base‘𝑊) |
9 | 5, 6, 7, 8 | islssfg2 40599 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑈) → (𝐷 ∈ LFinGen ↔ ∃𝑎 ∈ (𝒫
(Base‘𝑊) ∩
Fin)((LSpan‘𝑊)‘𝑎) = 𝐴)) |
10 | 3, 4, 9 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (𝐷 ∈ LFinGen ↔ ∃𝑎 ∈ (𝒫
(Base‘𝑊) ∩
Fin)((LSpan‘𝑊)‘𝑎) = 𝐴)) |
11 | 2, 10 | mpbid 235 |
. . 3
⊢ (𝜑 → ∃𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin)((LSpan‘𝑊)‘𝑎) = 𝐴) |
12 | | lsmfgcl.ef |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ LFinGen) |
13 | | lsmfgcl.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ 𝑈) |
14 | | lsmfgcl.e |
. . . . . . . . . 10
⊢ 𝐸 = (𝑊 ↾s 𝐵) |
15 | 14, 6, 7, 8 | islssfg2 40599 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝐵 ∈ 𝑈) → (𝐸 ∈ LFinGen ↔ ∃𝑏 ∈ (𝒫
(Base‘𝑊) ∩
Fin)((LSpan‘𝑊)‘𝑏) = 𝐵)) |
16 | 3, 13, 15 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (𝐸 ∈ LFinGen ↔ ∃𝑏 ∈ (𝒫
(Base‘𝑊) ∩
Fin)((LSpan‘𝑊)‘𝑏) = 𝐵)) |
17 | 12, 16 | mpbid 235 |
. . . . . . 7
⊢ (𝜑 → ∃𝑏 ∈ (𝒫 (Base‘𝑊) ∩ Fin)((LSpan‘𝑊)‘𝑏) = 𝐵) |
18 | 17 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin)) →
∃𝑏 ∈ (𝒫
(Base‘𝑊) ∩
Fin)((LSpan‘𝑊)‘𝑏) = 𝐵) |
19 | | inss1 4143 |
. . . . . . . . . . . . . . 15
⊢
(𝒫 (Base‘𝑊) ∩ Fin) ⊆ 𝒫
(Base‘𝑊) |
20 | 19 | sseli 3896 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ (𝒫
(Base‘𝑊) ∩ Fin)
→ 𝑎 ∈ 𝒫
(Base‘𝑊)) |
21 | 20 | elpwid 4524 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ (𝒫
(Base‘𝑊) ∩ Fin)
→ 𝑎 ⊆
(Base‘𝑊)) |
22 | 19 | sseli 3896 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin)
→ 𝑏 ∈ 𝒫
(Base‘𝑊)) |
23 | 22 | elpwid 4524 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin)
→ 𝑏 ⊆
(Base‘𝑊)) |
24 | | lsmfgcl.p |
. . . . . . . . . . . . . 14
⊢ ⊕ =
(LSSum‘𝑊) |
25 | 8, 7, 24 | lsmsp2 20124 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ 𝑎 ⊆ (Base‘𝑊) ∧ 𝑏 ⊆ (Base‘𝑊)) → (((LSpan‘𝑊)‘𝑎) ⊕ ((LSpan‘𝑊)‘𝑏)) = ((LSpan‘𝑊)‘(𝑎 ∪ 𝑏))) |
26 | 3, 21, 23, 25 | syl3an 1162 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin) ∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin))
→ (((LSpan‘𝑊)‘𝑎) ⊕ ((LSpan‘𝑊)‘𝑏)) = ((LSpan‘𝑊)‘(𝑎 ∪ 𝑏))) |
27 | 26 | 3expb 1122 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin) ∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin)))
→ (((LSpan‘𝑊)‘𝑎) ⊕ ((LSpan‘𝑊)‘𝑏)) = ((LSpan‘𝑊)‘(𝑎 ∪ 𝑏))) |
28 | 27 | oveq2d 7229 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin) ∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin)))
→ (𝑊
↾s (((LSpan‘𝑊)‘𝑎) ⊕ ((LSpan‘𝑊)‘𝑏))) = (𝑊 ↾s ((LSpan‘𝑊)‘(𝑎 ∪ 𝑏)))) |
29 | 3 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin) ∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin)))
→ 𝑊 ∈
LMod) |
30 | | unss 4098 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ⊆ (Base‘𝑊) ∧ 𝑏 ⊆ (Base‘𝑊)) ↔ (𝑎 ∪ 𝑏) ⊆ (Base‘𝑊)) |
31 | 30 | biimpi 219 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ⊆ (Base‘𝑊) ∧ 𝑏 ⊆ (Base‘𝑊)) → (𝑎 ∪ 𝑏) ⊆ (Base‘𝑊)) |
32 | 21, 23, 31 | syl2an 599 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ (𝒫
(Base‘𝑊) ∩ Fin)
∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin))
→ (𝑎 ∪ 𝑏) ⊆ (Base‘𝑊)) |
33 | 32 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin) ∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin)))
→ (𝑎 ∪ 𝑏) ⊆ (Base‘𝑊)) |
34 | | inss2 4144 |
. . . . . . . . . . . . . 14
⊢
(𝒫 (Base‘𝑊) ∩ Fin) ⊆ Fin |
35 | 34 | sseli 3896 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ (𝒫
(Base‘𝑊) ∩ Fin)
→ 𝑎 ∈
Fin) |
36 | 34 | sseli 3896 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin)
→ 𝑏 ∈
Fin) |
37 | | unfi 8850 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ Fin ∧ 𝑏 ∈ Fin) → (𝑎 ∪ 𝑏) ∈ Fin) |
38 | 35, 36, 37 | syl2an 599 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ (𝒫
(Base‘𝑊) ∩ Fin)
∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin))
→ (𝑎 ∪ 𝑏) ∈ Fin) |
39 | 38 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin) ∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin)))
→ (𝑎 ∪ 𝑏) ∈ Fin) |
40 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑊 ↾s
((LSpan‘𝑊)‘(𝑎 ∪ 𝑏))) = (𝑊 ↾s ((LSpan‘𝑊)‘(𝑎 ∪ 𝑏))) |
41 | 7, 8, 40 | islssfgi 40600 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ LMod ∧ (𝑎 ∪ 𝑏) ⊆ (Base‘𝑊) ∧ (𝑎 ∪ 𝑏) ∈ Fin) → (𝑊 ↾s ((LSpan‘𝑊)‘(𝑎 ∪ 𝑏))) ∈ LFinGen) |
42 | 29, 33, 39, 41 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin) ∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin)))
→ (𝑊
↾s ((LSpan‘𝑊)‘(𝑎 ∪ 𝑏))) ∈ LFinGen) |
43 | 28, 42 | eqeltrd 2838 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin) ∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin)))
→ (𝑊
↾s (((LSpan‘𝑊)‘𝑎) ⊕ ((LSpan‘𝑊)‘𝑏))) ∈ LFinGen) |
44 | 43 | anassrs 471 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin)) ∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin))
→ (𝑊
↾s (((LSpan‘𝑊)‘𝑎) ⊕ ((LSpan‘𝑊)‘𝑏))) ∈ LFinGen) |
45 | | oveq2 7221 |
. . . . . . . . . 10
⊢
(((LSpan‘𝑊)‘𝑏) = 𝐵 → (((LSpan‘𝑊)‘𝑎) ⊕ ((LSpan‘𝑊)‘𝑏)) = (((LSpan‘𝑊)‘𝑎) ⊕ 𝐵)) |
46 | 45 | oveq2d 7229 |
. . . . . . . . 9
⊢
(((LSpan‘𝑊)‘𝑏) = 𝐵 → (𝑊 ↾s (((LSpan‘𝑊)‘𝑎) ⊕ ((LSpan‘𝑊)‘𝑏))) = (𝑊 ↾s (((LSpan‘𝑊)‘𝑎) ⊕ 𝐵))) |
47 | 46 | eleq1d 2822 |
. . . . . . . 8
⊢
(((LSpan‘𝑊)‘𝑏) = 𝐵 → ((𝑊 ↾s (((LSpan‘𝑊)‘𝑎) ⊕ ((LSpan‘𝑊)‘𝑏))) ∈ LFinGen ↔ (𝑊 ↾s (((LSpan‘𝑊)‘𝑎) ⊕ 𝐵)) ∈ LFinGen)) |
48 | 44, 47 | syl5ibcom 248 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin)) ∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin))
→ (((LSpan‘𝑊)‘𝑏) = 𝐵 → (𝑊 ↾s (((LSpan‘𝑊)‘𝑎) ⊕ 𝐵)) ∈ LFinGen)) |
49 | 48 | rexlimdva 3203 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin)) →
(∃𝑏 ∈ (𝒫
(Base‘𝑊) ∩
Fin)((LSpan‘𝑊)‘𝑏) = 𝐵 → (𝑊 ↾s (((LSpan‘𝑊)‘𝑎) ⊕ 𝐵)) ∈ LFinGen)) |
50 | 18, 49 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin)) → (𝑊 ↾s
(((LSpan‘𝑊)‘𝑎) ⊕ 𝐵)) ∈ LFinGen) |
51 | | oveq1 7220 |
. . . . . . 7
⊢
(((LSpan‘𝑊)‘𝑎) = 𝐴 → (((LSpan‘𝑊)‘𝑎) ⊕ 𝐵) = (𝐴 ⊕ 𝐵)) |
52 | 51 | oveq2d 7229 |
. . . . . 6
⊢
(((LSpan‘𝑊)‘𝑎) = 𝐴 → (𝑊 ↾s (((LSpan‘𝑊)‘𝑎) ⊕ 𝐵)) = (𝑊 ↾s (𝐴 ⊕ 𝐵))) |
53 | 52 | eleq1d 2822 |
. . . . 5
⊢
(((LSpan‘𝑊)‘𝑎) = 𝐴 → ((𝑊 ↾s (((LSpan‘𝑊)‘𝑎) ⊕ 𝐵)) ∈ LFinGen ↔ (𝑊 ↾s (𝐴 ⊕ 𝐵)) ∈ LFinGen)) |
54 | 50, 53 | syl5ibcom 248 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin)) →
(((LSpan‘𝑊)‘𝑎) = 𝐴 → (𝑊 ↾s (𝐴 ⊕ 𝐵)) ∈ LFinGen)) |
55 | 54 | rexlimdva 3203 |
. . 3
⊢ (𝜑 → (∃𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin)((LSpan‘𝑊)‘𝑎) = 𝐴 → (𝑊 ↾s (𝐴 ⊕ 𝐵)) ∈ LFinGen)) |
56 | 11, 55 | mpd 15 |
. 2
⊢ (𝜑 → (𝑊 ↾s (𝐴 ⊕ 𝐵)) ∈ LFinGen) |
57 | 1, 56 | eqeltrid 2842 |
1
⊢ (𝜑 → 𝐹 ∈ LFinGen) |