| 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 43083 | . . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑈) → (𝐷 ∈ LFinGen ↔ ∃𝑎 ∈ (𝒫
(Base‘𝑊) ∩
Fin)((LSpan‘𝑊)‘𝑎) = 𝐴)) | 
| 10 | 3, 4, 9 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝐷 ∈ LFinGen ↔ ∃𝑎 ∈ (𝒫
(Base‘𝑊) ∩
Fin)((LSpan‘𝑊)‘𝑎) = 𝐴)) | 
| 11 | 2, 10 | mpbid 232 | . . 3
⊢ (𝜑 → ∃𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin)((LSpan‘𝑊)‘𝑎) = 𝐴) | 
| 12 |  | lsmfgcl.ef | . . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ LFinGen) | 
| 13 |  | lsmfgcl.b | . . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ 𝑈) | 
| 14 |  | lsmfgcl.e | . . . . . . . . . 10
⊢ 𝐸 = (𝑊 ↾s 𝐵) | 
| 15 | 14, 6, 7, 8 | islssfg2 43083 | . . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝐵 ∈ 𝑈) → (𝐸 ∈ LFinGen ↔ ∃𝑏 ∈ (𝒫
(Base‘𝑊) ∩
Fin)((LSpan‘𝑊)‘𝑏) = 𝐵)) | 
| 16 | 3, 13, 15 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝐸 ∈ LFinGen ↔ ∃𝑏 ∈ (𝒫
(Base‘𝑊) ∩
Fin)((LSpan‘𝑊)‘𝑏) = 𝐵)) | 
| 17 | 12, 16 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → ∃𝑏 ∈ (𝒫 (Base‘𝑊) ∩ Fin)((LSpan‘𝑊)‘𝑏) = 𝐵) | 
| 18 | 17 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin)) →
∃𝑏 ∈ (𝒫
(Base‘𝑊) ∩
Fin)((LSpan‘𝑊)‘𝑏) = 𝐵) | 
| 19 |  | inss1 4237 | . . . . . . . . . . . . . . 15
⊢
(𝒫 (Base‘𝑊) ∩ Fin) ⊆ 𝒫
(Base‘𝑊) | 
| 20 | 19 | sseli 3979 | . . . . . . . . . . . . . 14
⊢ (𝑎 ∈ (𝒫
(Base‘𝑊) ∩ Fin)
→ 𝑎 ∈ 𝒫
(Base‘𝑊)) | 
| 21 | 20 | elpwid 4609 | . . . . . . . . . . . . 13
⊢ (𝑎 ∈ (𝒫
(Base‘𝑊) ∩ Fin)
→ 𝑎 ⊆
(Base‘𝑊)) | 
| 22 | 19 | sseli 3979 | . . . . . . . . . . . . . 14
⊢ (𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin)
→ 𝑏 ∈ 𝒫
(Base‘𝑊)) | 
| 23 | 22 | elpwid 4609 | . . . . . . . . . . . . 13
⊢ (𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin)
→ 𝑏 ⊆
(Base‘𝑊)) | 
| 24 |  | lsmfgcl.p | . . . . . . . . . . . . . 14
⊢  ⊕ =
(LSSum‘𝑊) | 
| 25 | 8, 7, 24 | lsmsp2 21086 | . . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ 𝑎 ⊆ (Base‘𝑊) ∧ 𝑏 ⊆ (Base‘𝑊)) → (((LSpan‘𝑊)‘𝑎) ⊕ ((LSpan‘𝑊)‘𝑏)) = ((LSpan‘𝑊)‘(𝑎 ∪ 𝑏))) | 
| 26 | 3, 21, 23, 25 | syl3an 1161 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin) ∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin))
→ (((LSpan‘𝑊)‘𝑎) ⊕ ((LSpan‘𝑊)‘𝑏)) = ((LSpan‘𝑊)‘(𝑎 ∪ 𝑏))) | 
| 27 | 26 | 3expb 1121 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin) ∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin)))
→ (((LSpan‘𝑊)‘𝑎) ⊕ ((LSpan‘𝑊)‘𝑏)) = ((LSpan‘𝑊)‘(𝑎 ∪ 𝑏))) | 
| 28 | 27 | oveq2d 7447 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin) ∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin)))
→ (𝑊
↾s (((LSpan‘𝑊)‘𝑎) ⊕ ((LSpan‘𝑊)‘𝑏))) = (𝑊 ↾s ((LSpan‘𝑊)‘(𝑎 ∪ 𝑏)))) | 
| 29 | 3 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin) ∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin)))
→ 𝑊 ∈
LMod) | 
| 30 |  | unss 4190 | . . . . . . . . . . . . . 14
⊢ ((𝑎 ⊆ (Base‘𝑊) ∧ 𝑏 ⊆ (Base‘𝑊)) ↔ (𝑎 ∪ 𝑏) ⊆ (Base‘𝑊)) | 
| 31 | 30 | biimpi 216 | . . . . . . . . . . . . 13
⊢ ((𝑎 ⊆ (Base‘𝑊) ∧ 𝑏 ⊆ (Base‘𝑊)) → (𝑎 ∪ 𝑏) ⊆ (Base‘𝑊)) | 
| 32 | 21, 23, 31 | syl2an 596 | . . . . . . . . . . . 12
⊢ ((𝑎 ∈ (𝒫
(Base‘𝑊) ∩ Fin)
∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin))
→ (𝑎 ∪ 𝑏) ⊆ (Base‘𝑊)) | 
| 33 | 32 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin) ∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin)))
→ (𝑎 ∪ 𝑏) ⊆ (Base‘𝑊)) | 
| 34 |  | inss2 4238 | . . . . . . . . . . . . . 14
⊢
(𝒫 (Base‘𝑊) ∩ Fin) ⊆ Fin | 
| 35 | 34 | sseli 3979 | . . . . . . . . . . . . 13
⊢ (𝑎 ∈ (𝒫
(Base‘𝑊) ∩ Fin)
→ 𝑎 ∈
Fin) | 
| 36 | 34 | sseli 3979 | . . . . . . . . . . . . 13
⊢ (𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin)
→ 𝑏 ∈
Fin) | 
| 37 |  | unfi 9211 | . . . . . . . . . . . . 13
⊢ ((𝑎 ∈ Fin ∧ 𝑏 ∈ Fin) → (𝑎 ∪ 𝑏) ∈ Fin) | 
| 38 | 35, 36, 37 | syl2an 596 | . . . . . . . . . . . 12
⊢ ((𝑎 ∈ (𝒫
(Base‘𝑊) ∩ Fin)
∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin))
→ (𝑎 ∪ 𝑏) ∈ Fin) | 
| 39 | 38 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin) ∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin)))
→ (𝑎 ∪ 𝑏) ∈ Fin) | 
| 40 |  | eqid 2737 | . . . . . . . . . . . 12
⊢ (𝑊 ↾s
((LSpan‘𝑊)‘(𝑎 ∪ 𝑏))) = (𝑊 ↾s ((LSpan‘𝑊)‘(𝑎 ∪ 𝑏))) | 
| 41 | 7, 8, 40 | islssfgi 43084 | . . . . . . . . . . 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 2841 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin) ∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin)))
→ (𝑊
↾s (((LSpan‘𝑊)‘𝑎) ⊕ ((LSpan‘𝑊)‘𝑏))) ∈ LFinGen) | 
| 44 | 43 | anassrs 467 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin)) ∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin))
→ (𝑊
↾s (((LSpan‘𝑊)‘𝑎) ⊕ ((LSpan‘𝑊)‘𝑏))) ∈ LFinGen) | 
| 45 |  | oveq2 7439 | . . . . . . . . . 10
⊢
(((LSpan‘𝑊)‘𝑏) = 𝐵 → (((LSpan‘𝑊)‘𝑎) ⊕ ((LSpan‘𝑊)‘𝑏)) = (((LSpan‘𝑊)‘𝑎) ⊕ 𝐵)) | 
| 46 | 45 | oveq2d 7447 | . . . . . . . . 9
⊢
(((LSpan‘𝑊)‘𝑏) = 𝐵 → (𝑊 ↾s (((LSpan‘𝑊)‘𝑎) ⊕ ((LSpan‘𝑊)‘𝑏))) = (𝑊 ↾s (((LSpan‘𝑊)‘𝑎) ⊕ 𝐵))) | 
| 47 | 46 | eleq1d 2826 | . . . . . . . 8
⊢
(((LSpan‘𝑊)‘𝑏) = 𝐵 → ((𝑊 ↾s (((LSpan‘𝑊)‘𝑎) ⊕ ((LSpan‘𝑊)‘𝑏))) ∈ LFinGen ↔ (𝑊 ↾s (((LSpan‘𝑊)‘𝑎) ⊕ 𝐵)) ∈ LFinGen)) | 
| 48 | 44, 47 | syl5ibcom 245 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin)) ∧ 𝑏 ∈ (𝒫
(Base‘𝑊) ∩ Fin))
→ (((LSpan‘𝑊)‘𝑏) = 𝐵 → (𝑊 ↾s (((LSpan‘𝑊)‘𝑎) ⊕ 𝐵)) ∈ LFinGen)) | 
| 49 | 48 | rexlimdva 3155 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin)) →
(∃𝑏 ∈ (𝒫
(Base‘𝑊) ∩
Fin)((LSpan‘𝑊)‘𝑏) = 𝐵 → (𝑊 ↾s (((LSpan‘𝑊)‘𝑎) ⊕ 𝐵)) ∈ LFinGen)) | 
| 50 | 18, 49 | mpd 15 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin)) → (𝑊 ↾s
(((LSpan‘𝑊)‘𝑎) ⊕ 𝐵)) ∈ LFinGen) | 
| 51 |  | oveq1 7438 | . . . . . . 7
⊢
(((LSpan‘𝑊)‘𝑎) = 𝐴 → (((LSpan‘𝑊)‘𝑎) ⊕ 𝐵) = (𝐴 ⊕ 𝐵)) | 
| 52 | 51 | oveq2d 7447 | . . . . . 6
⊢
(((LSpan‘𝑊)‘𝑎) = 𝐴 → (𝑊 ↾s (((LSpan‘𝑊)‘𝑎) ⊕ 𝐵)) = (𝑊 ↾s (𝐴 ⊕ 𝐵))) | 
| 53 | 52 | eleq1d 2826 | . . . . 5
⊢
(((LSpan‘𝑊)‘𝑎) = 𝐴 → ((𝑊 ↾s (((LSpan‘𝑊)‘𝑎) ⊕ 𝐵)) ∈ LFinGen ↔ (𝑊 ↾s (𝐴 ⊕ 𝐵)) ∈ LFinGen)) | 
| 54 | 50, 53 | syl5ibcom 245 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin)) →
(((LSpan‘𝑊)‘𝑎) = 𝐴 → (𝑊 ↾s (𝐴 ⊕ 𝐵)) ∈ LFinGen)) | 
| 55 | 54 | rexlimdva 3155 | . . 3
⊢ (𝜑 → (∃𝑎 ∈ (𝒫 (Base‘𝑊) ∩ Fin)((LSpan‘𝑊)‘𝑎) = 𝐴 → (𝑊 ↾s (𝐴 ⊕ 𝐵)) ∈ LFinGen)) | 
| 56 | 11, 55 | mpd 15 | . 2
⊢ (𝜑 → (𝑊 ↾s (𝐴 ⊕ 𝐵)) ∈ LFinGen) | 
| 57 | 1, 56 | eqeltrid 2845 | 1
⊢ (𝜑 → 𝐹 ∈ LFinGen) |