Theorem pwslnmlem2 39686

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

Hypotheses

Ref	Expression
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

Ref	Expression
pwslnmlem2	⊢ (𝜑 → 𝑍 ∈ LNoeM)

Proof of Theorem pwslnmlem2

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533   ∈ wcel 2110  {crab 3142  Vcvv 3494   ∪ cun 3933   ∩ cin 3934   ⊆ wss 3935  ∅c0 4290  {csn 4560   class class class wbr 5058   ↦ cmpt 5138   × cxp 5547  ^◡ccnv 5548  ran crn 5550   ↾ cres 5551   “ cima 5552  –onto→wfo 6347  ‘cfv 6349  (class class class)co 7150  Basecbs 16477   ↾_s cress 16478  0_gc0g 16707   ↑_s cpws 16714  Mndcmnd 17905  Grpcgrp 18097  LModclmod 19628   LMHom clmhm 19785   LMIso clmim 19786   ≃_𝑚 clmic 19787  LNoeMclnm 39668

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-int 4869  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7403  df-om 7575  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-oadd 8100  df-er 8283  df-map 8402  df-ixp 8456  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-sup 8900  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-nn 11633  df-2 11694  df-3 11695  df-4 11696  df-5 11697  df-6 11698  df-7 11699  df-8 11700  df-9 11701  df-n0 11892  df-z 11976  df-dec 12093  df-uz 12238  df-fz 12887  df-struct 16479  df-ndx 16480  df-slot 16481  df-base 16483  df-sets 16484  df-ress 16485  df-plusg 16572  df-mulr 16573  df-sca 16575  df-vsca 16576  df-ip 16577  df-tset 16578  df-ple 16579  df-ds 16581  df-hom 16583  df-cco 16584  df-0g 16709  df-prds 16715  df-pws 16717  df-mgm 17846  df-sgrp 17895  df-mnd 17906  df-submnd 17951  df-grp 18100  df-minusg 18101  df-sbg 18102  df-subg 18270  df-ghm 18350  df-cntz 18441  df-lsm 18755  df-cmn 18902  df-abl 18903  df-mgp 19234  df-ur 19246  df-ring 19293  df-lmod 19630  df-lss 19698  df-lsp 19738  df-lmhm 19788  df-lmim 19789  df-lmic 19790  df-lfig 39661  df-lnm 39669

This theorem is referenced by:  pwslnm  39687