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 |`s A )
lsmfgcl.e 
|- E = ( W |`s B )
lsmfgcl.f 
|- F = ( W |`s ( A .(+) B ) )
lsmfgcl.w 
|- ( ph -> W e. LMod )
lsmfgcl.a 
|- ( ph -> A e. U )
lsmfgcl.b 
|- ( ph -> B e. U )
lsmfgcl.df 
|- ( ph -> D e. LFinGen )
lsmfgcl.ef 
|- ( ph -> E e. LFinGen )
Assertion lsmfgcl 
|- ( ph -> F e. LFinGen )

Proof

Step Hyp Ref Expression
1 lsmfgcl.u 
 |-  U = ( LSubSp ` W )
2 lsmfgcl.p 
 |-  .(+) = ( LSSum ` W )
3 lsmfgcl.d 
 |-  D = ( W |`s A )
4 lsmfgcl.e 
 |-  E = ( W |`s B )
5 lsmfgcl.f 
 |-  F = ( W |`s ( A .(+) B ) )
6 lsmfgcl.w 
 |-  ( ph -> W e. LMod )
7 lsmfgcl.a 
 |-  ( ph -> A e. U )
8 lsmfgcl.b 
 |-  ( ph -> B e. U )
9 lsmfgcl.df 
 |-  ( ph -> D e. LFinGen )
10 lsmfgcl.ef 
 |-  ( ph -> E e. LFinGen )
11 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
12 eqid 
 |-  ( Base ` W ) = ( Base ` W )
13 3 1 11 12 islssfg2 
 |-  ( ( W e. LMod /\ A e. U ) -> ( D e. LFinGen <-> E. a e. ( ~P ( Base ` W ) i^i Fin ) ( ( LSpan ` W ) ` a ) = A ) )
14 6 7 13 syl2anc 
 |-  ( ph -> ( D e. LFinGen <-> E. a e. ( ~P ( Base ` W ) i^i Fin ) ( ( LSpan ` W ) ` a ) = A ) )
15 9 14 mpbid 
 |-  ( ph -> E. a e. ( ~P ( Base ` W ) i^i Fin ) ( ( LSpan ` W ) ` a ) = A )
16 4 1 11 12 islssfg2 
 |-  ( ( W e. LMod /\ B e. U ) -> ( E e. LFinGen <-> E. b e. ( ~P ( Base ` W ) i^i Fin ) ( ( LSpan ` W ) ` b ) = B ) )
17 6 8 16 syl2anc 
 |-  ( ph -> ( E e. LFinGen <-> E. b e. ( ~P ( Base ` W ) i^i Fin ) ( ( LSpan ` W ) ` b ) = B ) )
18 10 17 mpbid 
 |-  ( ph -> E. b e. ( ~P ( Base ` W ) i^i Fin ) ( ( LSpan ` W ) ` b ) = B )
19 18 adantr 
 |-  ( ( ph /\ a e. ( ~P ( Base ` W ) i^i Fin ) ) -> E. b e. ( ~P ( Base ` W ) i^i Fin ) ( ( LSpan ` W ) ` b ) = B )
20 inss1 
 |-  ( ~P ( Base ` W ) i^i Fin ) C_ ~P ( Base ` W )
21 20 sseli 
 |-  ( a e. ( ~P ( Base ` W ) i^i Fin ) -> a e. ~P ( Base ` W ) )
22 21 elpwid 
 |-  ( a e. ( ~P ( Base ` W ) i^i Fin ) -> a C_ ( Base ` W ) )
23 20 sseli 
 |-  ( b e. ( ~P ( Base ` W ) i^i Fin ) -> b e. ~P ( Base ` W ) )
24 23 elpwid 
 |-  ( b e. ( ~P ( Base ` W ) i^i Fin ) -> b C_ ( Base ` W ) )
25 12 11 2 lsmsp2 
 |-  ( ( W e. LMod /\ a C_ ( Base ` W ) /\ b C_ ( Base ` W ) ) -> ( ( ( LSpan ` W ) ` a ) .(+) ( ( LSpan ` W ) ` b ) ) = ( ( LSpan ` W ) ` ( a u. b ) ) )
26 6 22 24 25 syl3an 
 |-  ( ( ph /\ a e. ( ~P ( Base ` W ) i^i Fin ) /\ b e. ( ~P ( Base ` W ) i^i Fin ) ) -> ( ( ( LSpan ` W ) ` a ) .(+) ( ( LSpan ` W ) ` b ) ) = ( ( LSpan ` W ) ` ( a u. b ) ) )
27 26 3expb 
 |-  ( ( ph /\ ( a e. ( ~P ( Base ` W ) i^i Fin ) /\ b e. ( ~P ( Base ` W ) i^i Fin ) ) ) -> ( ( ( LSpan ` W ) ` a ) .(+) ( ( LSpan ` W ) ` b ) ) = ( ( LSpan ` W ) ` ( a u. b ) ) )
28 27 oveq2d 
 |-  ( ( ph /\ ( a e. ( ~P ( Base ` W ) i^i Fin ) /\ b e. ( ~P ( Base ` W ) i^i Fin ) ) ) -> ( W |`s ( ( ( LSpan ` W ) ` a ) .(+) ( ( LSpan ` W ) ` b ) ) ) = ( W |`s ( ( LSpan ` W ) ` ( a u. b ) ) ) )
29 6 adantr 
 |-  ( ( ph /\ ( a e. ( ~P ( Base ` W ) i^i Fin ) /\ b e. ( ~P ( Base ` W ) i^i Fin ) ) ) -> W e. LMod )
30 unss 
 |-  ( ( a C_ ( Base ` W ) /\ b C_ ( Base ` W ) ) <-> ( a u. b ) C_ ( Base ` W ) )
31 30 biimpi 
 |-  ( ( a C_ ( Base ` W ) /\ b C_ ( Base ` W ) ) -> ( a u. b ) C_ ( Base ` W ) )
32 22 24 31 syl2an 
 |-  ( ( a e. ( ~P ( Base ` W ) i^i Fin ) /\ b e. ( ~P ( Base ` W ) i^i Fin ) ) -> ( a u. b ) C_ ( Base ` W ) )
33 32 adantl 
 |-  ( ( ph /\ ( a e. ( ~P ( Base ` W ) i^i Fin ) /\ b e. ( ~P ( Base ` W ) i^i Fin ) ) ) -> ( a u. b ) C_ ( Base ` W ) )
34 inss2 
 |-  ( ~P ( Base ` W ) i^i Fin ) C_ Fin
35 34 sseli 
 |-  ( a e. ( ~P ( Base ` W ) i^i Fin ) -> a e. Fin )
36 34 sseli 
 |-  ( b e. ( ~P ( Base ` W ) i^i Fin ) -> b e. Fin )
37 unfi 
 |-  ( ( a e. Fin /\ b e. Fin ) -> ( a u. b ) e. Fin )
38 35 36 37 syl2an 
 |-  ( ( a e. ( ~P ( Base ` W ) i^i Fin ) /\ b e. ( ~P ( Base ` W ) i^i Fin ) ) -> ( a u. b ) e. Fin )
39 38 adantl 
 |-  ( ( ph /\ ( a e. ( ~P ( Base ` W ) i^i Fin ) /\ b e. ( ~P ( Base ` W ) i^i Fin ) ) ) -> ( a u. b ) e. Fin )
40 eqid 
 |-  ( W |`s ( ( LSpan ` W ) ` ( a u. b ) ) ) = ( W |`s ( ( LSpan ` W ) ` ( a u. b ) ) )
41 11 12 40 islssfgi 
 |-  ( ( W e. LMod /\ ( a u. b ) C_ ( Base ` W ) /\ ( a u. b ) e. Fin ) -> ( W |`s ( ( LSpan ` W ) ` ( a u. b ) ) ) e. LFinGen )
42 29 33 39 41 syl3anc 
 |-  ( ( ph /\ ( a e. ( ~P ( Base ` W ) i^i Fin ) /\ b e. ( ~P ( Base ` W ) i^i Fin ) ) ) -> ( W |`s ( ( LSpan ` W ) ` ( a u. b ) ) ) e. LFinGen )
43 28 42 eqeltrd 
 |-  ( ( ph /\ ( a e. ( ~P ( Base ` W ) i^i Fin ) /\ b e. ( ~P ( Base ` W ) i^i Fin ) ) ) -> ( W |`s ( ( ( LSpan ` W ) ` a ) .(+) ( ( LSpan ` W ) ` b ) ) ) e. LFinGen )
44 43 anassrs 
 |-  ( ( ( ph /\ a e. ( ~P ( Base ` W ) i^i Fin ) ) /\ b e. ( ~P ( Base ` W ) i^i Fin ) ) -> ( W |`s ( ( ( LSpan ` W ) ` a ) .(+) ( ( LSpan ` W ) ` b ) ) ) e. 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 |`s ( ( ( LSpan ` W ) ` a ) .(+) ( ( LSpan ` W ) ` b ) ) ) = ( W |`s ( ( ( LSpan ` W ) ` a ) .(+) B ) ) )
47 46 eleq1d 
 |-  ( ( ( LSpan ` W ) ` b ) = B -> ( ( W |`s ( ( ( LSpan ` W ) ` a ) .(+) ( ( LSpan ` W ) ` b ) ) ) e. LFinGen <-> ( W |`s ( ( ( LSpan ` W ) ` a ) .(+) B ) ) e. LFinGen ) )
48 44 47 syl5ibcom 
 |-  ( ( ( ph /\ a e. ( ~P ( Base ` W ) i^i Fin ) ) /\ b e. ( ~P ( Base ` W ) i^i Fin ) ) -> ( ( ( LSpan ` W ) ` b ) = B -> ( W |`s ( ( ( LSpan ` W ) ` a ) .(+) B ) ) e. LFinGen ) )
49 48 rexlimdva 
 |-  ( ( ph /\ a e. ( ~P ( Base ` W ) i^i Fin ) ) -> ( E. b e. ( ~P ( Base ` W ) i^i Fin ) ( ( LSpan ` W ) ` b ) = B -> ( W |`s ( ( ( LSpan ` W ) ` a ) .(+) B ) ) e. LFinGen ) )
50 19 49 mpd 
 |-  ( ( ph /\ a e. ( ~P ( Base ` W ) i^i Fin ) ) -> ( W |`s ( ( ( LSpan ` W ) ` a ) .(+) B ) ) e. LFinGen )
51 oveq1 
 |-  ( ( ( LSpan ` W ) ` a ) = A -> ( ( ( LSpan ` W ) ` a ) .(+) B ) = ( A .(+) B ) )
52 51 oveq2d 
 |-  ( ( ( LSpan ` W ) ` a ) = A -> ( W |`s ( ( ( LSpan ` W ) ` a ) .(+) B ) ) = ( W |`s ( A .(+) B ) ) )
53 52 eleq1d 
 |-  ( ( ( LSpan ` W ) ` a ) = A -> ( ( W |`s ( ( ( LSpan ` W ) ` a ) .(+) B ) ) e. LFinGen <-> ( W |`s ( A .(+) B ) ) e. LFinGen ) )
54 50 53 syl5ibcom 
 |-  ( ( ph /\ a e. ( ~P ( Base ` W ) i^i Fin ) ) -> ( ( ( LSpan ` W ) ` a ) = A -> ( W |`s ( A .(+) B ) ) e. LFinGen ) )
55 54 rexlimdva 
 |-  ( ph -> ( E. a e. ( ~P ( Base ` W ) i^i Fin ) ( ( LSpan ` W ) ` a ) = A -> ( W |`s ( A .(+) B ) ) e. LFinGen ) )
56 15 55 mpd 
 |-  ( ph -> ( W |`s ( A .(+) B ) ) e. LFinGen )
57 5 56 eqeltrid 
 |-  ( ph -> F e. LFinGen )