Metamath Proof Explorer

Theorem lsmfgcl

Description: The sum of two finitely generated submodules is finitely generated. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Hypotheses lsmfgcl.u ⊢ U = LSubSp ⁡ W
lsmfgcl.p ⊢ ⊕ ˙ = LSSum ⁡ W
lsmfgcl.d ⊢ D = W ↾ 𝑠 A
lsmfgcl.e ⊢ E = W ↾ 𝑠 B
lsmfgcl.f ⊢ F = W ↾ 𝑠 A ⊕ ˙ B
lsmfgcl.w ⊢ φ → W ∈ LMod
lsmfgcl.a ⊢ φ → A ∈ U
lsmfgcl.b ⊢ φ → B ∈ U
lsmfgcl.df ⊢ φ → D ∈ LFinGen
lsmfgcl.ef ⊢ φ → E ∈ LFinGen
Assertion lsmfgcl ⊢ φ → F ∈ LFinGen

Proof

Step Hyp Ref Expression
1 lsmfgcl.u ⊢ U = LSubSp ⁡ W
2 lsmfgcl.p ⊢ ⊕ ˙ = LSSum ⁡ W
3 lsmfgcl.d ⊢ D = W ↾ 𝑠 A
4 lsmfgcl.e ⊢ E = W ↾ 𝑠 B
5 lsmfgcl.f ⊢ F = W ↾ 𝑠 A ⊕ ˙ B
6 lsmfgcl.w ⊢ φ → W ∈ LMod
7 lsmfgcl.a ⊢ φ → A ∈ U
8 lsmfgcl.b ⊢ φ → B ∈ U
9 lsmfgcl.df ⊢ φ → D ∈ LFinGen
10 lsmfgcl.ef ⊢ φ → E ∈ LFinGen
11 eqid ⊢ LSpan ⁡ W = LSpan ⁡ W
12 eqid ⊢ Base W = Base W
13 3 1 11 12 islssfg2 ⊢ W ∈ LMod ∧ A ∈ U → D ∈ LFinGen ↔ ∃ a ∈ 𝒫 Base W ∩ Fin LSpan ⁡ W ⁡ a = A
14 6 7 13 syl2anc ⊢ φ → D ∈ LFinGen ↔ ∃ a ∈ 𝒫 Base W ∩ Fin LSpan ⁡ W ⁡ a = A
15 9 14 mpbid ⊢ φ → ∃ a ∈ 𝒫 Base W ∩ Fin LSpan ⁡ W ⁡ a = A
16 4 1 11 12 islssfg2 ⊢ W ∈ LMod ∧ B ∈ U → E ∈ LFinGen ↔ ∃ b ∈ 𝒫 Base W ∩ Fin LSpan ⁡ W ⁡ b = B
17 6 8 16 syl2anc ⊢ φ → E ∈ LFinGen ↔ ∃ b ∈ 𝒫 Base W ∩ Fin LSpan ⁡ W ⁡ b = B
18 10 17 mpbid ⊢ φ → ∃ b ∈ 𝒫 Base W ∩ Fin LSpan ⁡ W ⁡ b = B
19 18 adantr ⊢ φ ∧ a ∈ 𝒫 Base W ∩ Fin → ∃ b ∈ 𝒫 Base W ∩ Fin LSpan ⁡ W ⁡ b = B
20 inss1 ⊢ 𝒫 Base W ∩ Fin ⊆ 𝒫 Base W
21 20 sseli ⊢ a ∈ 𝒫 Base W ∩ Fin → a ∈ 𝒫 Base W
22 21 elpwid ⊢ a ∈ 𝒫 Base W ∩ Fin → a ⊆ Base W
23 20 sseli ⊢ b ∈ 𝒫 Base W ∩ Fin → b ∈ 𝒫 Base W
24 23 elpwid ⊢ b ∈ 𝒫 Base W ∩ Fin → b ⊆ Base W
25 12 11 2 lsmsp2 ⊢ W ∈ LMod ∧ a ⊆ Base W ∧ b ⊆ Base W → LSpan ⁡ W ⁡ a ⊕ ˙ LSpan ⁡ W ⁡ b = LSpan ⁡ W ⁡ a ∪ b
26 6 22 24 25 syl3an ⊢ φ ∧ a ∈ 𝒫 Base W ∩ Fin ∧ b ∈ 𝒫 Base W ∩ Fin → LSpan ⁡ W ⁡ a ⊕ ˙ LSpan ⁡ W ⁡ b = LSpan ⁡ W ⁡ a ∪ b
27 26 3expb ⊢ φ ∧ a ∈ 𝒫 Base W ∩ Fin ∧ b ∈ 𝒫 Base W ∩ Fin → LSpan ⁡ W ⁡ a ⊕ ˙ LSpan ⁡ W ⁡ b = LSpan ⁡ W ⁡ a ∪ b
28 27 oveq2d ⊢ φ ∧ a ∈ 𝒫 Base W ∩ Fin ∧ b ∈ 𝒫 Base W ∩ Fin → W ↾ 𝑠 LSpan ⁡ W ⁡ a ⊕ ˙ LSpan ⁡ W ⁡ b = W ↾ 𝑠 LSpan ⁡ W ⁡ a ∪ b
29 6 adantr ⊢ φ ∧ a ∈ 𝒫 Base W ∩ Fin ∧ b ∈ 𝒫 Base W ∩ Fin → W ∈ LMod
30 unss ⊢ a ⊆ Base W ∧ b ⊆ Base W ↔ a ∪ b ⊆ Base W
31 30 biimpi ⊢ a ⊆ Base W ∧ b ⊆ Base W → a ∪ b ⊆ Base W
32 22 24 31 syl2an ⊢ a ∈ 𝒫 Base W ∩ Fin ∧ b ∈ 𝒫 Base W ∩ Fin → a ∪ b ⊆ Base W
33 32 adantl ⊢ φ ∧ a ∈ 𝒫 Base W ∩ Fin ∧ b ∈ 𝒫 Base W ∩ Fin → a ∪ b ⊆ Base W
34 inss2 ⊢ 𝒫 Base W ∩ Fin ⊆ Fin
35 34 sseli ⊢ a ∈ 𝒫 Base W ∩ Fin → a ∈ Fin
36 34 sseli ⊢ b ∈ 𝒫 Base W ∩ Fin → b ∈ Fin
37 unfi ⊢ a ∈ Fin ∧ b ∈ Fin → a ∪ b ∈ Fin
38 35 36 37 syl2an ⊢ a ∈ 𝒫 Base W ∩ Fin ∧ b ∈ 𝒫 Base W ∩ Fin → a ∪ b ∈ Fin
39 38 adantl ⊢ φ ∧ a ∈ 𝒫 Base W ∩ Fin ∧ b ∈ 𝒫 Base W ∩ Fin → a ∪ b ∈ Fin
40 eqid ⊢ W ↾ 𝑠 LSpan ⁡ W ⁡ a ∪ b = W ↾ 𝑠 LSpan ⁡ W ⁡ a ∪ b
41 11 12 40 islssfgi ⊢ W ∈ LMod ∧ a ∪ b ⊆ Base W ∧ a ∪ b ∈ Fin → W ↾ 𝑠 LSpan ⁡ W ⁡ a ∪ b ∈ LFinGen
42 29 33 39 41 syl3anc ⊢ φ ∧ a ∈ 𝒫 Base W ∩ Fin ∧ b ∈ 𝒫 Base W ∩ Fin → W ↾ 𝑠 LSpan ⁡ W ⁡ a ∪ b ∈ LFinGen
43 28 42 eqeltrd ⊢ φ ∧ a ∈ 𝒫 Base W ∩ Fin ∧ b ∈ 𝒫 Base W ∩ Fin → W ↾ 𝑠 LSpan ⁡ W ⁡ a ⊕ ˙ LSpan ⁡ W ⁡ b ∈ LFinGen
44 43 anassrs ⊢ φ ∧ a ∈ 𝒫 Base W ∩ Fin ∧ b ∈ 𝒫 Base W ∩ Fin → W ↾ 𝑠 LSpan ⁡ W ⁡ a ⊕ ˙ LSpan ⁡ W ⁡ b ∈ LFinGen
45 oveq2 ⊢ LSpan ⁡ W ⁡ b = B → LSpan ⁡ W ⁡ a ⊕ ˙ LSpan ⁡ W ⁡ b = LSpan ⁡ W ⁡ a ⊕ ˙ B
46 45 oveq2d ⊢ LSpan ⁡ W ⁡ b = B → W ↾ 𝑠 LSpan ⁡ W ⁡ a ⊕ ˙ LSpan ⁡ W ⁡ b = W ↾ 𝑠 LSpan ⁡ W ⁡ a ⊕ ˙ B
47 46 eleq1d ⊢ LSpan ⁡ W ⁡ b = B → W ↾ 𝑠 LSpan ⁡ W ⁡ a ⊕ ˙ LSpan ⁡ W ⁡ b ∈ LFinGen ↔ W ↾ 𝑠 LSpan ⁡ W ⁡ a ⊕ ˙ B ∈ LFinGen
48 44 47 syl5ibcom ⊢ φ ∧ a ∈ 𝒫 Base W ∩ Fin ∧ b ∈ 𝒫 Base W ∩ Fin → LSpan ⁡ W ⁡ b = B → W ↾ 𝑠 LSpan ⁡ W ⁡ a ⊕ ˙ B ∈ LFinGen
49 48 rexlimdva ⊢ φ ∧ a ∈ 𝒫 Base W ∩ Fin → ∃ b ∈ 𝒫 Base W ∩ Fin LSpan ⁡ W ⁡ b = B → W ↾ 𝑠 LSpan ⁡ W ⁡ a ⊕ ˙ B ∈ LFinGen
50 19 49 mpd ⊢ φ ∧ a ∈ 𝒫 Base W ∩ Fin → W ↾ 𝑠 LSpan ⁡ W ⁡ a ⊕ ˙ B ∈ LFinGen
51 oveq1 ⊢ LSpan ⁡ W ⁡ a = A → LSpan ⁡ W ⁡ a ⊕ ˙ B = A ⊕ ˙ B
52 51 oveq2d ⊢ LSpan ⁡ W ⁡ a = A → W ↾ 𝑠 LSpan ⁡ W ⁡ a ⊕ ˙ B = W ↾ 𝑠 A ⊕ ˙ B
53 52 eleq1d ⊢ LSpan ⁡ W ⁡ a = A → W ↾ 𝑠 LSpan ⁡ W ⁡ a ⊕ ˙ B ∈ LFinGen ↔ W ↾ 𝑠 A ⊕ ˙ B ∈ LFinGen
54 50 53 syl5ibcom ⊢ φ ∧ a ∈ 𝒫 Base W ∩ Fin → LSpan ⁡ W ⁡ a = A → W ↾ 𝑠 A ⊕ ˙ B ∈ LFinGen
55 54 rexlimdva ⊢ φ → ∃ a ∈ 𝒫 Base W ∩ Fin LSpan ⁡ W ⁡ a = A → W ↾ 𝑠 A ⊕ ˙ B ∈ LFinGen
56 15 55 mpd ⊢ φ → W ↾ 𝑠 A ⊕ ˙ B ∈ LFinGen
57 5 56 eqeltrid ⊢ φ → F ∈ LFinGen