Theorem pwslnmlem2 39683

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 7461	. . . 4 ⊢ (𝐴 ∪ 𝐵) ∈ V
5	4	a1i 11	. . 3 ⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ V)
6		ssun1 4146	. . . 4 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
7	6	a1i 11	. . 3 ⊢ (𝜑 → 𝐴 ⊆ (𝐴 ∪ 𝐵))
8		pwslnmlem2.z	. . . 4 ⊢ 𝑍 = (𝑊 ↑s (𝐴 ∪ 𝐵))
9		pwslnmlem2.x	. . . 4 ⊢ 𝑋 = (𝑊 ↑s 𝐴)
10		eqid 2819	. . . 4 ⊢ (Base‘𝑍) = (Base‘𝑍)
11		eqid 2819	. . . 4 ⊢ (Base‘𝑋) = (Base‘𝑋)
12		eqid 2819	. . . 4 ⊢ (𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴)) = (𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴))
13	8, 9, 10, 11, 12	pwssplit3 19825	. . 3 ⊢ ((𝑊 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ V ∧ 𝐴 ⊆ (𝐴 ∪ 𝐵)) → (𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴)) ∈ (𝑍 LMHom 𝑋))
14	1, 5, 7, 13	syl3anc 1366	. 2 ⊢ (𝜑 → (𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴)) ∈ (𝑍 LMHom 𝑋))
15		fvex 6676	. . . . . 6 ⊢ (0g‘𝑋) ∈ V
16	12	mptiniseg 6086	. . . . . 6 ⊢ ((0g‘𝑋) ∈ V → (◡(𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴)) “ {(0g‘𝑋)}) = {𝑥 ∈ (Base‘𝑍) ∣ (𝑥 ↾ 𝐴) = (0g‘𝑋)})
17	15, 16	ax-mp 5	. . . . 5 ⊢ (◡(𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴)) “ {(0g‘𝑋)}) = {𝑥 ∈ (Base‘𝑍) ∣ (𝑥 ↾ 𝐴) = (0g‘𝑋)}
18		lmodgrp 19633	. . . . . . . . . 10 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
19		grpmnd 18102	. . . . . . . . . 10 ⊢ (𝑊 ∈ Grp → 𝑊 ∈ Mnd)
20	1, 18, 19	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ Mnd)
21		eqid 2819	. . . . . . . . . 10 ⊢ (0g‘𝑊) = (0g‘𝑊)
22	9, 21	pws0g 17939	. . . . . . . . 9 ⊢ ((𝑊 ∈ Mnd ∧ 𝐴 ∈ V) → (𝐴 × {(0g‘𝑊)}) = (0g‘𝑋))
23	20, 2, 22	sylancl 588	. . . . . . . 8 ⊢ (𝜑 → (𝐴 × {(0g‘𝑊)}) = (0g‘𝑋))
24	23	eqcomd 2825	. . . . . . 7 ⊢ (𝜑 → (0g‘𝑋) = (𝐴 × {(0g‘𝑊)}))
25	24	eqeq2d 2830	. . . . . 6 ⊢ (𝜑 → ((𝑥 ↾ 𝐴) = (0g‘𝑋) ↔ (𝑥 ↾ 𝐴) = (𝐴 × {(0g‘𝑊)})))
26	25	rabbidv 3479	. . . . 5 ⊢ (𝜑 → {𝑥 ∈ (Base‘𝑍) ∣ (𝑥 ↾ 𝐴) = (0g‘𝑋)} = {𝑥 ∈ (Base‘𝑍) ∣ (𝑥 ↾ 𝐴) = (𝐴 × {(0g‘𝑊)})})
27	17, 26	syl5eq 2866	. . . 4 ⊢ (𝜑 → (◡(𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴)) “ {(0g‘𝑋)}) = {𝑥 ∈ (Base‘𝑍) ∣ (𝑥 ↾ 𝐴) = (𝐴 × {(0g‘𝑊)})})
28	27	oveq2d 7164	. . 3 ⊢ (𝜑 → (𝑍 ↾s (◡(𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴)) “ {(0g‘𝑋)})) = (𝑍 ↾s {𝑥 ∈ (Base‘𝑍) ∣ (𝑥 ↾ 𝐴) = (𝐴 × {(0g‘𝑊)})}))
29		pwslnmlem2.yn	. . . 4 ⊢ (𝜑 → 𝑌 ∈ LNoeM)
30		pwslnmlem2.dj	. . . . . 6 ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)
31		eqid 2819	. . . . . . 7 ⊢ {𝑥 ∈ (Base‘𝑍) ∣ (𝑥 ↾ 𝐴) = (𝐴 × {(0g‘𝑊)})} = {𝑥 ∈ (Base‘𝑍) ∣ (𝑥 ↾ 𝐴) = (𝐴 × {(0g‘𝑊)})}
32		eqid 2819	. . . . . . 7 ⊢ (𝑦 ∈ {𝑥 ∈ (Base‘𝑍) ∣ (𝑥 ↾ 𝐴) = (𝐴 × {(0g‘𝑊)})} ↦ (𝑦 ↾ 𝐵)) = (𝑦 ∈ {𝑥 ∈ (Base‘𝑍) ∣ (𝑥 ↾ 𝐴) = (𝐴 × {(0g‘𝑊)})} ↦ (𝑦 ↾ 𝐵))
33		pwslnmlem2.y	. . . . . . 7 ⊢ 𝑌 = (𝑊 ↑s 𝐵)
34		eqid 2819	. . . . . . 7 ⊢ (𝑍 ↾s {𝑥 ∈ (Base‘𝑍) ∣ (𝑥 ↾ 𝐴) = (𝐴 × {(0g‘𝑊)})}) = (𝑍 ↾s {𝑥 ∈ (Base‘𝑍) ∣ (𝑥 ↾ 𝐴) = (𝐴 × {(0g‘𝑊)})})
35	8, 10, 21, 31, 32, 9, 33, 34	pwssplit4 39679	. . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ (𝐴 ∪ 𝐵) ∈ V ∧ (𝐴 ∩ 𝐵) = ∅) → (𝑦 ∈ {𝑥 ∈ (Base‘𝑍) ∣ (𝑥 ↾ 𝐴) = (𝐴 × {(0g‘𝑊)})} ↦ (𝑦 ↾ 𝐵)) ∈ ((𝑍 ↾s {𝑥 ∈ (Base‘𝑍) ∣ (𝑥 ↾ 𝐴) = (𝐴 × {(0g‘𝑊)})}) LMIso 𝑌))
36	1, 5, 30, 35	syl3anc 1366	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ {𝑥 ∈ (Base‘𝑍) ∣ (𝑥 ↾ 𝐴) = (𝐴 × {(0g‘𝑊)})} ↦ (𝑦 ↾ 𝐵)) ∈ ((𝑍 ↾s {𝑥 ∈ (Base‘𝑍) ∣ (𝑥 ↾ 𝐴) = (𝐴 × {(0g‘𝑊)})}) LMIso 𝑌))
37		brlmici 19833	. . . . 5 ⊢ ((𝑦 ∈ {𝑥 ∈ (Base‘𝑍) ∣ (𝑥 ↾ 𝐴) = (𝐴 × {(0g‘𝑊)})} ↦ (𝑦 ↾ 𝐵)) ∈ ((𝑍 ↾s {𝑥 ∈ (Base‘𝑍) ∣ (𝑥 ↾ 𝐴) = (𝐴 × {(0g‘𝑊)})}) LMIso 𝑌) → (𝑍 ↾s {𝑥 ∈ (Base‘𝑍) ∣ (𝑥 ↾ 𝐴) = (𝐴 × {(0g‘𝑊)})}) ≃𝑚 𝑌)
38		lnmlmic 39678	. . . . 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 2911	. 2 ⊢ (𝜑 → (𝑍 ↾s (◡(𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴)) “ {(0g‘𝑋)})) ∈ LNoeM)
42	8, 9, 10, 11, 12	pwssplit1 19823	. . . . . . 7 ⊢ ((𝑊 ∈ Mnd ∧ (𝐴 ∪ 𝐵) ∈ V ∧ 𝐴 ⊆ (𝐴 ∪ 𝐵)) → (𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴)):(Base‘𝑍)–onto→(Base‘𝑋))
43	20, 5, 7, 42	syl3anc 1366	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴)):(Base‘𝑍)–onto→(Base‘𝑋))
44		forn 6586	. . . . . 6 ⊢ ((𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴)):(Base‘𝑍)–onto→(Base‘𝑋) → ran (𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴)) = (Base‘𝑋))
45	43, 44	syl 17	. . . . 5 ⊢ (𝜑 → ran (𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴)) = (Base‘𝑋))
46	45	oveq2d 7164	. . . 4 ⊢ (𝜑 → (𝑋 ↾s ran (𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴))) = (𝑋 ↾s (Base‘𝑋)))
47		pwslnmlem2.xn	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ LNoeM)
48	11	ressid 16551	. . . . 5 ⊢ (𝑋 ∈ LNoeM → (𝑋 ↾s (Base‘𝑋)) = 𝑋)
49	47, 48	syl 17	. . . 4 ⊢ (𝜑 → (𝑋 ↾s (Base‘𝑋)) = 𝑋)
50	46, 49	eqtrd 2854	. . 3 ⊢ (𝜑 → (𝑋 ↾s ran (𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴))) = 𝑋)
51	50, 47	eqeltrd 2911	. 2 ⊢ (𝜑 → (𝑋 ↾s ran (𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴))) ∈ LNoeM)
52		eqid 2819	. . 3 ⊢ (0g‘𝑋) = (0g‘𝑋)
53		eqid 2819	. . 3 ⊢ (◡(𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴)) “ {(0g‘𝑋)}) = (◡(𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴)) “ {(0g‘𝑋)})
54		eqid 2819	. . 3 ⊢ (𝑍 ↾s (◡(𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴)) “ {(0g‘𝑋)})) = (𝑍 ↾s (◡(𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴)) “ {(0g‘𝑋)}))
55		eqid 2819	. . 3 ⊢ (𝑋 ↾s ran (𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴))) = (𝑋 ↾s ran (𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴)))
56	52, 53, 54, 55	lmhmlnmsplit 39677	. 2 ⊢ (((𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴)) ∈ (𝑍 LMHom 𝑋) ∧ (𝑍 ↾s (◡(𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴)) “ {(0g‘𝑋)})) ∈ LNoeM ∧ (𝑋 ↾s ran (𝑥 ∈ (Base‘𝑍) ↦ (𝑥 ↾ 𝐴))) ∈ LNoeM) → 𝑍 ∈ LNoeM)
57	14, 41, 51, 56	syl3anc 1366	1 ⊢ (𝜑 → 𝑍 ∈ LNoeM)

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1531   ∈ wcel 2108  {crab 3140  Vcvv 3493   ∪ cun 3932   ∩ cin 3933   ⊆ wss 3934  ∅c0 4289  {csn 4559   class class class wbr 5057   ↦ cmpt 5137   × cxp 5546  ^◡ccnv 5547  ran crn 5549   ↾ cres 5550   “ cima 5551  –onto→wfo 6346  ‘cfv 6348  (class class class)co 7148  Basecbs 16475   ↾_s cress 16476  0_gc0g 16705   ↑_s cpws 16712  Mndcmnd 17903  Grpcgrp 18095  LModclmod 19626   LMHom clmhm 19783   LMIso clmim 19784   ≃_𝑚 clmic 19785  LNoeMclnm 39665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-of 7401  df-om 7573  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-oadd 8098  df-er 8281  df-map 8400  df-ixp 8454  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-sup 8898  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-fz 12885  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-sca 16573  df-vsca 16574  df-ip 16575  df-tset 16576  df-ple 16577  df-ds 16579  df-hom 16581  df-cco 16582  df-0g 16707  df-prds 16713  df-pws 16715  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-submnd 17949  df-grp 18098  df-minusg 18099  df-sbg 18100  df-subg 18268  df-ghm 18348  df-cntz 18439  df-lsm 18753  df-cmn 18900  df-abl 18901  df-mgp 19232  df-ur 19244  df-ring 19291  df-lmod 19628  df-lss 19696  df-lsp 19736  df-lmhm 19786  df-lmim 19787  df-lmic 19788  df-lfig 39658  df-lnm 39666

This theorem is referenced by:  pwslnm  39684