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 ⊢ 𝐴 ∈ V
pwslnmlem2.b ⊢ 𝐵 ∈ V
pwslnmlem2.x ⊢ 𝑋 = ( 𝑊 ↑s 𝐴 )
pwslnmlem2.y ⊢ 𝑌 = ( 𝑊 ↑s 𝐵 )
pwslnmlem2.z ⊢ 𝑍 = ( 𝑊 ↑s ( 𝐴 ∪ 𝐵 ) )
pwslnmlem2.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
pwslnmlem2.dj ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
pwslnmlem2.xn ⊢ ( 𝜑 → 𝑋 ∈ LNoeM )
pwslnmlem2.yn ⊢ ( 𝜑 → 𝑌 ∈ LNoeM )
Assertion pwslnmlem2 ( 𝜑 → 𝑍 ∈ LNoeM )

Proof

Step Hyp Ref Expression
1 pwslnmlem2.a ⊢ 𝐴 ∈ V
2 pwslnmlem2.b ⊢ 𝐵 ∈ V
3 pwslnmlem2.x ⊢ 𝑋 = ( 𝑊 ↑s 𝐴 )
4 pwslnmlem2.y ⊢ 𝑌 = ( 𝑊 ↑s 𝐵 )
5 pwslnmlem2.z ⊢ 𝑍 = ( 𝑊 ↑s ( 𝐴 ∪ 𝐵 ) )
6 pwslnmlem2.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
7 pwslnmlem2.dj ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
8 pwslnmlem2.xn ⊢ ( 𝜑 → 𝑋 ∈ LNoeM )
9 pwslnmlem2.yn ⊢ ( 𝜑 → 𝑌 ∈ LNoeM )
10 1 2 unex ⊢ ( 𝐴 ∪ 𝐵 ) ∈ V
11 10 a1i ⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ∈ V )
12 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
13 12 a1i ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) )
14 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
15 eqid ⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
16 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) )
17 5 3 14 15 16 pwssplit3 ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐴 ∪ 𝐵 ) ∈ V ∧ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) ∈ ( 𝑍 LMHom 𝑋 ) )
18 6 11 13 17 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) ∈ ( 𝑍 LMHom 𝑋 ) )
19 fvex ⊢ ( 0g ‘ 𝑋 ) ∈ V
20 16 mptiniseg ⊢ ( ( 0g ‘ 𝑋 ) ∈ V → ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) “ { ( 0g ‘ 𝑋 ) } ) = { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 0g ‘ 𝑋 ) } )
21 19 20 ax-mp ⊢ ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) “ { ( 0g ‘ 𝑋 ) } ) = { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 0g ‘ 𝑋 ) }
22 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
23 grpmnd ⊢ ( 𝑊 ∈ Grp → 𝑊 ∈ Mnd )
24 6 22 23 3syl ⊢ ( 𝜑 → 𝑊 ∈ Mnd )
25 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
26 3 25 pws0g ⊢ ( ( 𝑊 ∈ Mnd ∧ 𝐴 ∈ V ) → ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) = ( 0g ‘ 𝑋 ) )
27 24 1 26 sylancl ⊢ ( 𝜑 → ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) = ( 0g ‘ 𝑋 ) )
28 27 eqcomd ⊢ ( 𝜑 → ( 0g ‘ 𝑋 ) = ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) )
29 28 eqeq2d ⊢ ( 𝜑 → ( ( 𝑥 ↾ 𝐴 ) = ( 0g ‘ 𝑋 ) ↔ ( 𝑥 ↾ 𝐴 ) = ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) ) )
30 29 rabbidv ⊢ ( 𝜑 → { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 0g ‘ 𝑋 ) } = { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) } )
31 21 30 syl5eq ⊢ ( 𝜑 → ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) “ { ( 0g ‘ 𝑋 ) } ) = { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) } )
32 31 oveq2d ⊢ ( 𝜑 → ( 𝑍 ↾s ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) “ { ( 0g ‘ 𝑋 ) } ) ) = ( 𝑍 ↾s { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) } ) )
33 eqid ⊢ { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) } = { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) }
34 eqid ⊢ ( 𝑦 ∈ { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) } ↦ ( 𝑦 ↾ 𝐵 ) ) = ( 𝑦 ∈ { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) } ↦ ( 𝑦 ↾ 𝐵 ) )
35 eqid ⊢ ( 𝑍 ↾s { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) } ) = ( 𝑍 ↾s { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) } )
36 5 14 25 33 34 3 4 35 pwssplit4 ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐴 ∪ 𝐵 ) ∈ V ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝑦 ∈ { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) } ↦ ( 𝑦 ↾ 𝐵 ) ) ∈ ( ( 𝑍 ↾s { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) } ) LMIso 𝑌 ) )
37 6 11 7 36 syl3anc ⊢ ( 𝜑 → ( 𝑦 ∈ { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) } ↦ ( 𝑦 ↾ 𝐵 ) ) ∈ ( ( 𝑍 ↾s { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) } ) LMIso 𝑌 ) )
38 brlmici ⊢ ( ( 𝑦 ∈ { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) } ↦ ( 𝑦 ↾ 𝐵 ) ) ∈ ( ( 𝑍 ↾s { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) } ) LMIso 𝑌 ) → ( 𝑍 ↾s { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) } ) ≃𝑚 𝑌 )
39 lnmlmic ⊢ ( ( 𝑍 ↾s { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) } ) ≃𝑚 𝑌 → ( ( 𝑍 ↾s { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) } ) ∈ LNoeM ↔ 𝑌 ∈ LNoeM ) )
40 37 38 39 3syl ⊢ ( 𝜑 → ( ( 𝑍 ↾s { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) } ) ∈ LNoeM ↔ 𝑌 ∈ LNoeM ) )
41 9 40 mpbird ⊢ ( 𝜑 → ( 𝑍 ↾s { 𝑥 ∈ ( Base ‘ 𝑍 ) ∣ ( 𝑥 ↾ 𝐴 ) = ( 𝐴 × { ( 0g ‘ 𝑊 ) } ) } ) ∈ LNoeM )
42 32 41 eqeltrd ⊢ ( 𝜑 → ( 𝑍 ↾s ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) “ { ( 0g ‘ 𝑋 ) } ) ) ∈ LNoeM )
43 5 3 14 15 16 pwssplit1 ⊢ ( ( 𝑊 ∈ Mnd ∧ ( 𝐴 ∪ 𝐵 ) ∈ V ∧ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) : ( Base ‘ 𝑍 ) –onto→ ( Base ‘ 𝑋 ) )
44 24 11 13 43 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) : ( Base ‘ 𝑍 ) –onto→ ( Base ‘ 𝑋 ) )
45 forn ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) : ( Base ‘ 𝑍 ) –onto→ ( Base ‘ 𝑋 ) → ran ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) = ( Base ‘ 𝑋 ) )
46 44 45 syl ⊢ ( 𝜑 → ran ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) = ( Base ‘ 𝑋 ) )
47 46 oveq2d ⊢ ( 𝜑 → ( 𝑋 ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) ) = ( 𝑋 ↾s ( Base ‘ 𝑋 ) ) )
48 15 ressid ⊢ ( 𝑋 ∈ LNoeM → ( 𝑋 ↾s ( Base ‘ 𝑋 ) ) = 𝑋 )
49 8 48 syl ⊢ ( 𝜑 → ( 𝑋 ↾s ( Base ‘ 𝑋 ) ) = 𝑋 )
50 47 49 eqtrd ⊢ ( 𝜑 → ( 𝑋 ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) ) = 𝑋 )
51 50 8 eqeltrd ⊢ ( 𝜑 → ( 𝑋 ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) ) ∈ LNoeM )
52 eqid ⊢ ( 0g ‘ 𝑋 ) = ( 0g ‘ 𝑋 )
53 eqid ⊢ ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) “ { ( 0g ‘ 𝑋 ) } ) = ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) “ { ( 0g ‘ 𝑋 ) } )
54 eqid ⊢ ( 𝑍 ↾s ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) “ { ( 0g ‘ 𝑋 ) } ) ) = ( 𝑍 ↾s ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) “ { ( 0g ‘ 𝑋 ) } ) )
55 eqid ⊢ ( 𝑋 ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) ) = ( 𝑋 ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) )
56 52 53 54 55 lmhmlnmsplit ⊢ ( ( ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) ∈ ( 𝑍 LMHom 𝑋 ) ∧ ( 𝑍 ↾s ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) “ { ( 0g ‘ 𝑋 ) } ) ) ∈ LNoeM ∧ ( 𝑋 ↾s ran ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 𝑥 ↾ 𝐴 ) ) ) ∈ LNoeM ) → 𝑍 ∈ LNoeM )
57 18 42 51 56 syl3anc ⊢ ( 𝜑 → 𝑍 ∈ LNoeM )