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 )