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 ⊢ 𝑈 = ( LSubSp ‘ 𝑊 )
lsmfgcl.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
lsmfgcl.d ⊢ 𝐷 = ( 𝑊 ↾s 𝐴 )
lsmfgcl.e ⊢ 𝐸 = ( 𝑊 ↾s 𝐵 )
lsmfgcl.f ⊢ 𝐹 = ( 𝑊 ↾s ( 𝐴 ⊕ 𝐵 ) )
lsmfgcl.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lsmfgcl.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
lsmfgcl.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
lsmfgcl.df ⊢ ( 𝜑 → 𝐷 ∈ LFinGen )
lsmfgcl.ef ⊢ ( 𝜑 → 𝐸 ∈ LFinGen )
Assertion lsmfgcl ( 𝜑 → 𝐹 ∈ LFinGen )

Proof

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