Metamath Proof Explorer

Theorem pwslnmlem2

Description: A sum of powers is Noetherian. (Contributed by Stefan O'Rear, 25-Jan-2015)

Ref Expression
Hypotheses pwslnmlem2.a 
|- A e. _V
pwslnmlem2.b 
|- B e. _V
pwslnmlem2.x 
|- X = ( W ^s A )
pwslnmlem2.y 
|- Y = ( W ^s B )
pwslnmlem2.z 
|- Z = ( W ^s ( A u. B ) )
pwslnmlem2.w 
|- ( ph -> W e. LMod )
pwslnmlem2.dj 
|- ( ph -> ( A i^i B ) = (/) )
pwslnmlem2.xn 
|- ( ph -> X e. LNoeM )
pwslnmlem2.yn 
|- ( ph -> Y e. LNoeM )
Assertion pwslnmlem2 
|- ( ph -> Z e. LNoeM )

Proof

Step Hyp Ref Expression
1 pwslnmlem2.a 
 |-  A e. _V
2 pwslnmlem2.b 
 |-  B e. _V
3 pwslnmlem2.x 
 |-  X = ( W ^s A )
4 pwslnmlem2.y 
 |-  Y = ( W ^s B )
5 pwslnmlem2.z 
 |-  Z = ( W ^s ( A u. B ) )
6 pwslnmlem2.w 
 |-  ( ph -> W e. LMod )
7 pwslnmlem2.dj 
 |-  ( ph -> ( A i^i B ) = (/) )
8 pwslnmlem2.xn 
 |-  ( ph -> X e. LNoeM )
9 pwslnmlem2.yn 
 |-  ( ph -> Y e. LNoeM )
10 1 2 unex 
 |-  ( A u. B ) e. _V
11 10 a1i 
 |-  ( ph -> ( A u. B ) e. _V )
12 ssun1 
 |-  A C_ ( A u. B )
13 12 a1i 
 |-  ( ph -> A C_ ( A u. B ) )
14 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
15 eqid 
 |-  ( Base ` X ) = ( Base ` X )
16 eqid 
 |-  ( x e. ( Base ` Z ) |-> ( x |` A ) ) = ( x e. ( Base ` Z ) |-> ( x |` A ) )
17 5 3 14 15 16 pwssplit3 
 |-  ( ( W e. LMod /\ ( A u. B ) e. _V /\ A C_ ( A u. B ) ) -> ( x e. ( Base ` Z ) |-> ( x |` A ) ) e. ( Z LMHom X ) )
18 6 11 13 17 syl3anc 
 |-  ( ph -> ( x e. ( Base ` Z ) |-> ( x |` A ) ) e. ( Z LMHom X ) )
19 fvex 
 |-  ( 0g ` X ) e. _V
20 16 mptiniseg 
 |-  ( ( 0g ` X ) e. _V -> ( `' ( x e. ( Base ` Z ) |-> ( x |` A ) ) " { ( 0g ` X ) } ) = { x e. ( Base ` Z ) | ( x |` A ) = ( 0g ` X ) } )
21 19 20 ax-mp 
 |-  ( `' ( x e. ( Base ` Z ) |-> ( x |` A ) ) " { ( 0g ` X ) } ) = { x e. ( Base ` Z ) | ( x |` A ) = ( 0g ` X ) }
22 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
23 grpmnd 
 |-  ( W e. Grp -> W e. Mnd )
24 6 22 23 3syl 
 |-  ( ph -> W e. Mnd )
25 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
26 3 25 pws0g 
 |-  ( ( W e. Mnd /\ A e. _V ) -> ( A X. { ( 0g ` W ) } ) = ( 0g ` X ) )
27 24 1 26 sylancl 
 |-  ( ph -> ( A X. { ( 0g ` W ) } ) = ( 0g ` X ) )
28 27 eqcomd 
 |-  ( ph -> ( 0g ` X ) = ( A X. { ( 0g ` W ) } ) )
29 28 eqeq2d 
 |-  ( ph -> ( ( x |` A ) = ( 0g ` X ) <-> ( x |` A ) = ( A X. { ( 0g ` W ) } ) ) )
30 29 rabbidv 
 |-  ( ph -> { x e. ( Base ` Z ) | ( x |` A ) = ( 0g ` X ) } = { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } )
31 21 30 syl5eq 
 |-  ( ph -> ( `' ( x e. ( Base ` Z ) |-> ( x |` A ) ) " { ( 0g ` X ) } ) = { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } )
32 31 oveq2d 
 |-  ( ph -> ( Z |`s ( `' ( x e. ( Base ` Z ) |-> ( x |` A ) ) " { ( 0g ` X ) } ) ) = ( Z |`s { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) )
33 eqid 
 |-  { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } = { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) }
34 eqid 
 |-  ( y e. { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } |-> ( y |` B ) ) = ( y e. { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } |-> ( y |` B ) )
35 eqid 
 |-  ( Z |`s { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) = ( Z |`s { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } )
36 5 14 25 33 34 3 4 35 pwssplit4 
 |-  ( ( W e. LMod /\ ( A u. B ) e. _V /\ ( A i^i B ) = (/) ) -> ( y e. { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } |-> ( y |` B ) ) e. ( ( Z |`s { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) LMIso Y ) )
37 6 11 7 36 syl3anc 
 |-  ( ph -> ( y e. { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } |-> ( y |` B ) ) e. ( ( Z |`s { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) LMIso Y ) )
38 brlmici 
 |-  ( ( y e. { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } |-> ( y |` B ) ) e. ( ( Z |`s { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) LMIso Y ) -> ( Z |`s { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) ~=m Y )
39 lnmlmic 
 |-  ( ( Z |`s { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) ~=m Y -> ( ( Z |`s { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) e. LNoeM <-> Y e. LNoeM ) )
40 37 38 39 3syl 
 |-  ( ph -> ( ( Z |`s { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) e. LNoeM <-> Y e. LNoeM ) )
41 9 40 mpbird 
 |-  ( ph -> ( Z |`s { x e. ( Base ` Z ) | ( x |` A ) = ( A X. { ( 0g ` W ) } ) } ) e. LNoeM )
42 32 41 eqeltrd 
 |-  ( ph -> ( Z |`s ( `' ( x e. ( Base ` Z ) |-> ( x |` A ) ) " { ( 0g ` X ) } ) ) e. LNoeM )
43 5 3 14 15 16 pwssplit1 
 |-  ( ( W e. Mnd /\ ( A u. B ) e. _V /\ A C_ ( A u. B ) ) -> ( x e. ( Base ` Z ) |-> ( x |` A ) ) : ( Base ` Z ) -onto-> ( Base ` X ) )
44 24 11 13 43 syl3anc 
 |-  ( ph -> ( x e. ( Base ` Z ) |-> ( x |` A ) ) : ( Base ` Z ) -onto-> ( Base ` X ) )
45 forn 
 |-  ( ( x e. ( Base ` Z ) |-> ( x |` A ) ) : ( Base ` Z ) -onto-> ( Base ` X ) -> ran ( x e. ( Base ` Z ) |-> ( x |` A ) ) = ( Base ` X ) )
46 44 45 syl 
 |-  ( ph -> ran ( x e. ( Base ` Z ) |-> ( x |` A ) ) = ( Base ` X ) )
47 46 oveq2d 
 |-  ( ph -> ( X |`s ran ( x e. ( Base ` Z ) |-> ( x |` A ) ) ) = ( X |`s ( Base ` X ) ) )
48 15 ressid 
 |-  ( X e. LNoeM -> ( X |`s ( Base ` X ) ) = X )
49 8 48 syl 
 |-  ( ph -> ( X |`s ( Base ` X ) ) = X )
50 47 49 eqtrd 
 |-  ( ph -> ( X |`s ran ( x e. ( Base ` Z ) |-> ( x |` A ) ) ) = X )
51 50 8 eqeltrd 
 |-  ( ph -> ( X |`s ran ( x e. ( Base ` Z ) |-> ( x |` A ) ) ) e. LNoeM )
52 eqid 
 |-  ( 0g ` X ) = ( 0g ` X )
53 eqid 
 |-  ( `' ( x e. ( Base ` Z ) |-> ( x |` A ) ) " { ( 0g ` X ) } ) = ( `' ( x e. ( Base ` Z ) |-> ( x |` A ) ) " { ( 0g ` X ) } )
54 eqid 
 |-  ( Z |`s ( `' ( x e. ( Base ` Z ) |-> ( x |` A ) ) " { ( 0g ` X ) } ) ) = ( Z |`s ( `' ( x e. ( Base ` Z ) |-> ( x |` A ) ) " { ( 0g ` X ) } ) )
55 eqid 
 |-  ( X |`s ran ( x e. ( Base ` Z ) |-> ( x |` A ) ) ) = ( X |`s ran ( x e. ( Base ` Z ) |-> ( x |` A ) ) )
56 52 53 54 55 lmhmlnmsplit 
 |-  ( ( ( x e. ( Base ` Z ) |-> ( x |` A ) ) e. ( Z LMHom X ) /\ ( Z |`s ( `' ( x e. ( Base ` Z ) |-> ( x |` A ) ) " { ( 0g ` X ) } ) ) e. LNoeM /\ ( X |`s ran ( x e. ( Base ` Z ) |-> ( x |` A ) ) ) e. LNoeM ) -> Z e. LNoeM )
57 18 42 51 56 syl3anc 
 |-  ( ph -> Z e. LNoeM )