mplcoe1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mplcoe1		Structured version Visualization version GIF version

Theorem mplcoe1 22044

Description: Decompose a polynomial into a finite sum of monomials. (Contributed by Mario Carneiro, 9-Jan-2015.)

**Hypotheses**
Ref	Expression
mplcoe1.p	⊢ 𝑃 = (𝐼 mPoly 𝑅)
mplcoe1.d	⊢ 𝐷 = {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}
mplcoe1.z	⊢ 0 = (0_g‘𝑅)
mplcoe1.o	⊢ 1 = (1_r‘𝑅)
mplcoe1.i	⊢ (𝜑 → 𝐼 ∈ 𝑊)
mplcoe1.b	⊢ 𝐵 = (Base‘𝑃)
mplcoe1.n	⊢ · = ( ·_𝑠 ‘𝑃)
mplcoe1.r	⊢ (𝜑 → 𝑅 ∈ Ring)
mplcoe1.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)

**Assertion**
Ref	Expression
mplcoe1	⊢ (𝜑 → 𝑋 = (𝑃 Σ_g (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))

Distinct variable groups: 𝑦,𝑘, 1 𝐵,𝑘 𝑓,𝑘,𝑦,𝐼 𝜑,𝑘,𝑦 𝑅,𝑓,𝑦 𝐷,𝑘,𝑦 𝑃,𝑘 0 ,𝑓,𝑘,𝑦 𝑓,𝑋,𝑘,𝑦 𝑘,𝑊,𝑦 · ,𝑘 Allowed substitution hints: 𝜑(𝑓) 𝐵(𝑦,𝑓) 𝐷(𝑓) 𝑃(𝑦,𝑓) 𝑅(𝑘) · (𝑦,𝑓) 1 (𝑓) 𝑊(𝑓)

Proof of Theorem mplcoe1 Dummy variables 𝑤 𝑥 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mplcoe1.p	. . . . . 6 ⊢ 𝑃 = (𝐼 mPoly 𝑅)
2		eqid 2726	. . . . . 6 ⊢ (Base‘𝑅) = (Base‘𝑅)
3		mplcoe1.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝑃)
4		mplcoe1.d	. . . . . 6 ⊢ 𝐷 = {𝑓 ∈ (ℕ₀ ↑_m 𝐼) ∣ (^◡𝑓 “ ℕ) ∈ Fin}
5		mplcoe1.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
6	1, 2, 3, 4, 5	mplelf 22007	. . . . 5 ⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅))
7	6	feqmptd 6971	. . . 4 ⊢ (𝜑 → 𝑋 = (𝑦 ∈ 𝐷 ↦ (𝑋‘𝑦)))
8		iftrue 4539	. . . . . . 7 ⊢ (𝑦 ∈ (𝑋 supp 0 ) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦))
9	8	adantl 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝑋 supp 0 )) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦))
10		eldif 3957	. . . . . . . 8 ⊢ (𝑦 ∈ (𝐷 ∖ (𝑋 supp 0 )) ↔ (𝑦 ∈ 𝐷 ∧ ¬ 𝑦 ∈ (𝑋 supp 0 )))
11		ssidd 4003	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋 supp 0 ) ⊆ (𝑋 supp 0 ))
12		ovex 7457	. . . . . . . . . . . . 13 ⊢ (ℕ₀ ↑_m 𝐼) ∈ V
13	4, 12	rabex2 5341	. . . . . . . . . . . 12 ⊢ 𝐷 ∈ V
14	13	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ V)
15		mplcoe1.z	. . . . . . . . . . . . 13 ⊢ 0 = (0_g‘𝑅)
16	15	fvexi 6915	. . . . . . . . . . . 12 ⊢ 0 ∈ V
17	16	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ V)
18	6, 11, 14, 17	suppssr 8210	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → (𝑋‘𝑦) = 0 )
19	18	ifeq2d 4553	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), (𝑋‘𝑦)) = if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ))
20		ifid 4573	. . . . . . . . 9 ⊢ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), (𝑋‘𝑦)) = (𝑋‘𝑦)
21	19, 20	eqtr3di 2781	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦))
22	10, 21	sylan2br 593	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ∧ ¬ 𝑦 ∈ (𝑋 supp 0 ))) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦))
23	22	anassrs 466	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ (𝑋 supp 0 )) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦))
24	9, 23	pm2.61dan 811	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦))
25	24	mpteq2dva 5253	. . . 4 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ (𝑋‘𝑦)))
26	7, 25	eqtr4d 2769	. . 3 ⊢ (𝜑 → 𝑋 = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )))
27		suppssdm 8191	. . . . 5 ⊢ (𝑋 supp 0 ) ⊆ dom 𝑋
28	27, 6	fssdm 6747	. . . 4 ⊢ (𝜑 → (𝑋 supp 0 ) ⊆ 𝐷)
29		eqid 2726	. . . . . . . . 9 ⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅)
30		eqid 2726	. . . . . . . . 9 ⊢ (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑅))
31	1, 29, 30, 15, 3	mplelbas 22000	. . . . . . . 8 ⊢ (𝑋 ∈ 𝐵 ↔ (𝑋 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑋 finSupp 0 ))
32	31	simprbi 495	. . . . . . 7 ⊢ (𝑋 ∈ 𝐵 → 𝑋 finSupp 0 )
33	5, 32	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑋 finSupp 0 )
34	33	fsuppimpd 9413	. . . . 5 ⊢ (𝜑 → (𝑋 supp 0 ) ∈ Fin)
35		sseq1 4005	. . . . . . . 8 ⊢ (𝑤 = ∅ → (𝑤 ⊆ 𝐷 ↔ ∅ ⊆ 𝐷))
36		mpteq1 5246	. . . . . . . . . . . 12 ⊢ (𝑤 = ∅ → (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = (𝑘 ∈ ∅ ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))
37		mpt0 6703	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ∅ ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = ∅
38	36, 37	eqtrdi 2782	. . . . . . . . . . 11 ⊢ (𝑤 = ∅ → (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = ∅)
39	38	oveq2d 7440	. . . . . . . . . 10 ⊢ (𝑤 = ∅ → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σ_g ∅))
40		eqid 2726	. . . . . . . . . . 11 ⊢ (0_g‘𝑃) = (0_g‘𝑃)
41	40	gsum0 18677	. . . . . . . . . 10 ⊢ (𝑃 Σ_g ∅) = (0_g‘𝑃)
42	39, 41	eqtrdi 2782	. . . . . . . . 9 ⊢ (𝑤 = ∅ → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (0_g‘𝑃))
43		noel 4333	. . . . . . . . . . . 12 ⊢ ¬ 𝑦 ∈ ∅
44		eleq2 2815	. . . . . . . . . . . 12 ⊢ (𝑤 = ∅ → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ ∅))
45	43, 44	mtbiri 326	. . . . . . . . . . 11 ⊢ (𝑤 = ∅ → ¬ 𝑦 ∈ 𝑤)
46	45	iffalsed 4544	. . . . . . . . . 10 ⊢ (𝑤 = ∅ → if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ) = 0 )
47	46	mpteq2dv 5255	. . . . . . . . 9 ⊢ (𝑤 = ∅ → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ 0 ))
48	42, 47	eqeq12d 2742	. . . . . . . 8 ⊢ (𝑤 = ∅ → ((𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) ↔ (0_g‘𝑃) = (𝑦 ∈ 𝐷 ↦ 0 )))
49	35, 48	imbi12d 343	. . . . . . 7 ⊢ (𝑤 = ∅ → ((𝑤 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ))) ↔ (∅ ⊆ 𝐷 → (0_g‘𝑃) = (𝑦 ∈ 𝐷 ↦ 0 ))))
50	49	imbi2d 339	. . . . . 6 ⊢ (𝑤 = ∅ → ((𝜑 → (𝑤 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )))) ↔ (𝜑 → (∅ ⊆ 𝐷 → (0_g‘𝑃) = (𝑦 ∈ 𝐷 ↦ 0 )))))
51		sseq1 4005	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → (𝑤 ⊆ 𝐷 ↔ 𝑥 ⊆ 𝐷))
52		mpteq1 5246	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))
53	52	oveq2d 7440	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
54		eleq2 2815	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑥 → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑥))
55	54	ifbid 4556	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ) = if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))
56	55	mpteq2dv 5255	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )))
57	53, 56	eqeq12d 2742	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → ((𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) ↔ (𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))))
58	51, 57	imbi12d 343	. . . . . . 7 ⊢ (𝑤 = 𝑥 → ((𝑤 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ))) ↔ (𝑥 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )))))
59	58	imbi2d 339	. . . . . 6 ⊢ (𝑤 = 𝑥 → ((𝜑 → (𝑤 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )))) ↔ (𝜑 → (𝑥 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))))))
60		sseq1 4005	. . . . . . . 8 ⊢ (𝑤 = (𝑥 ∪ {𝑧}) → (𝑤 ⊆ 𝐷 ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐷))
61		mpteq1 5246	. . . . . . . . . 10 ⊢ (𝑤 = (𝑥 ∪ {𝑧}) → (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))
62	61	oveq2d 7440	. . . . . . . . 9 ⊢ (𝑤 = (𝑥 ∪ {𝑧}) → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
63		eleq2 2815	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑥 ∪ {𝑧}) → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ (𝑥 ∪ {𝑧})))
64	63	ifbid 4556	. . . . . . . . . 10 ⊢ (𝑤 = (𝑥 ∪ {𝑧}) → if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ) = if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))
65	64	mpteq2dv 5255	. . . . . . . . 9 ⊢ (𝑤 = (𝑥 ∪ {𝑧}) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )))
66	62, 65	eqeq12d 2742	. . . . . . . 8 ⊢ (𝑤 = (𝑥 ∪ {𝑧}) → ((𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) ↔ (𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))))
67	60, 66	imbi12d 343	. . . . . . 7 ⊢ (𝑤 = (𝑥 ∪ {𝑧}) → ((𝑤 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ))) ↔ ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )))))
68	67	imbi2d 339	. . . . . 6 ⊢ (𝑤 = (𝑥 ∪ {𝑧}) → ((𝜑 → (𝑤 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )))) ↔ (𝜑 → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))))))
69		sseq1 4005	. . . . . . . 8 ⊢ (𝑤 = (𝑋 supp 0 ) → (𝑤 ⊆ 𝐷 ↔ (𝑋 supp 0 ) ⊆ 𝐷))
70		mpteq1 5246	. . . . . . . . . 10 ⊢ (𝑤 = (𝑋 supp 0 ) → (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))
71	70	oveq2d 7440	. . . . . . . . 9 ⊢ (𝑤 = (𝑋 supp 0 ) → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σ_g (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
72		eleq2 2815	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑋 supp 0 ) → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ (𝑋 supp 0 )))
73	72	ifbid 4556	. . . . . . . . . 10 ⊢ (𝑤 = (𝑋 supp 0 ) → if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ) = if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ))
74	73	mpteq2dv 5255	. . . . . . . . 9 ⊢ (𝑤 = (𝑋 supp 0 ) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )))
75	71, 74	eqeq12d 2742	. . . . . . . 8 ⊢ (𝑤 = (𝑋 supp 0 ) → ((𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) ↔ (𝑃 Σ_g (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ))))
76	69, 75	imbi12d 343	. . . . . . 7 ⊢ (𝑤 = (𝑋 supp 0 ) → ((𝑤 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ))) ↔ ((𝑋 supp 0 ) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )))))
77	76	imbi2d 339	. . . . . 6 ⊢ (𝑤 = (𝑋 supp 0 ) → ((𝜑 → (𝑤 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )))) ↔ (𝜑 → ((𝑋 supp 0 ) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ))))))
78		mplcoe1.i	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ 𝑊)
79		mplcoe1.r	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ Ring)
80		ringgrp 20221	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
81	79, 80	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ Grp)
82	1, 4, 15, 40, 78, 81	mpl0 22015	. . . . . . . 8 ⊢ (𝜑 → (0_g‘𝑃) = (𝐷 × { 0 }))
83		fconstmpt 5744	. . . . . . . 8 ⊢ (𝐷 × { 0 }) = (𝑦 ∈ 𝐷 ↦ 0 )
84	82, 83	eqtrdi 2782	. . . . . . 7 ⊢ (𝜑 → (0_g‘𝑃) = (𝑦 ∈ 𝐷 ↦ 0 ))
85	84	a1d 25	. . . . . 6 ⊢ (𝜑 → (∅ ⊆ 𝐷 → (0_g‘𝑃) = (𝑦 ∈ 𝐷 ↦ 0 )))
86		ssun1 4173	. . . . . . . . . . 11 ⊢ 𝑥 ⊆ (𝑥 ∪ {𝑧})
87		sstr2 3986	. . . . . . . . . . 11 ⊢ (𝑥 ⊆ (𝑥 ∪ {𝑧}) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → 𝑥 ⊆ 𝐷))
88	86, 87	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → 𝑥 ⊆ 𝐷)
89	88	imim1i 63	. . . . . . . . 9 ⊢ ((𝑥 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))))
90		oveq1 7431	. . . . . . . . . . . 12 ⊢ ((𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) → ((𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))(+_g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) = ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))(+_g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))))
91		eqid 2726	. . . . . . . . . . . . . 14 ⊢ (+_g‘𝑃) = (+_g‘𝑃)
92	1, 78, 79	mplringd 22032	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ Ring)
93		ringcmn 20261	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd)
94	92, 93	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ CMnd)
95	94	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑃 ∈ CMnd)
96		simprll 777	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑥 ∈ Fin)
97		simprr 771	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑥 ∪ {𝑧}) ⊆ 𝐷)
98	97	unssad 4188	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑥 ⊆ 𝐷)
99	98	sselda 3979	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝐷)
100	78	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝐼 ∈ 𝑊)
101	79	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 ∈ Ring)
102	1, 100, 101	mpllmodd 22033	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑃 ∈ LMod)
103	6	ffvelcdmda 7098	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑋‘𝑘) ∈ (Base‘𝑅))
104	1, 78, 79	mplsca 22022	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑅 = (Scalar‘𝑃))
105	104	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 = (Scalar‘𝑃))
106	105	fveq2d 6905	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
107	103, 106	eleqtrd 2828	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑋‘𝑘) ∈ (Base‘(Scalar‘𝑃)))
108		mplcoe1.o	. . . . . . . . . . . . . . . . . 18 ⊢ 1 = (1_r‘𝑅)
109		simpr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑘 ∈ 𝐷)
110	1, 3, 15, 108, 4, 100, 101, 109	mplmon 22042	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )) ∈ 𝐵)
111		eqid 2726	. . . . . . . . . . . . . . . . . 18 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
112		mplcoe1.n	. . . . . . . . . . . . . . . . . 18 ⊢ · = ( ·_𝑠 ‘𝑃)
113		eqid 2726	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
114	3, 111, 112, 113	lmodvscl 20854	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ LMod ∧ (𝑋‘𝑘) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )) ∈ 𝐵) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) ∈ 𝐵)
115	102, 107, 110, 114	syl3anc 1368	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) ∈ 𝐵)
116	115	adantlr 713	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑘 ∈ 𝐷) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) ∈ 𝐵)
117	99, 116	syldan 589	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑘 ∈ 𝑥) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) ∈ 𝐵)
118		vex 3466	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
119	118	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑧 ∈ V)
120		simprlr 778	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ¬ 𝑧 ∈ 𝑥)
121	1, 78, 79	mpllmodd 22033	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ LMod)
122	121	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑃 ∈ LMod)
123	6	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑋:𝐷⟶(Base‘𝑅))
124	97	unssbd 4189	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → {𝑧} ⊆ 𝐷)
125	118	snss 4794	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝐷 ↔ {𝑧} ⊆ 𝐷)
126	124, 125	sylibr 233	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑧 ∈ 𝐷)
127	123, 126	ffvelcdmd 7099	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑋‘𝑧) ∈ (Base‘𝑅))
128	104	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑅 = (Scalar‘𝑃))
129	128	fveq2d 6905	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
130	127, 129	eleqtrd 2828	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑋‘𝑧) ∈ (Base‘(Scalar‘𝑃)))
131	78	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝐼 ∈ 𝑊)
132	79	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑅 ∈ Ring)
133	1, 3, 15, 108, 4, 131, 132, 126	mplmon 22042	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )) ∈ 𝐵)
134	3, 111, 112, 113	lmodvscl 20854	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ LMod ∧ (𝑋‘𝑧) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )) ∈ 𝐵) → ((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) ∈ 𝐵)
135	122, 130, 133, 134	syl3anc 1368	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) ∈ 𝐵)
136		fveq2 6901	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑧 → (𝑋‘𝑘) = (𝑋‘𝑧))
137		equequ2 2022	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑧 → (𝑦 = 𝑘 ↔ 𝑦 = 𝑧))
138	137	ifbid 4556	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑧 → if(𝑦 = 𝑘, 1 , 0 ) = if(𝑦 = 𝑧, 1 , 0 ))
139	138	mpteq2dv 5255	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑧 → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))
140	136, 139	oveq12d 7442	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑧 → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = ((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))))
141	3, 91, 95, 96, 117, 119, 120, 135, 140	gsumunsn 19958	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = ((𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))(+_g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))))
142		eqid 2726	. . . . . . . . . . . . . . 15 ⊢ (+_g‘𝑅) = (+_g‘𝑅)
143	123	ffvelcdmda 7098	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → (𝑋‘𝑦) ∈ (Base‘𝑅))
144	2, 15	ring0cl 20246	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅 ∈ Ring → 0 ∈ (Base‘𝑅))
145	79, 144	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 0 ∈ (Base‘𝑅))
146	145	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → 0 ∈ (Base‘𝑅))
147	143, 146	ifcld 4579	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ) ∈ (Base‘𝑅))
148	147	fmpttd 7129	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )):𝐷⟶(Base‘𝑅))
149		fvex 6914	. . . . . . . . . . . . . . . . . . 19 ⊢ (Base‘𝑅) ∈ V
150	149, 13	elmap 8900	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ ((Base‘𝑅) ↑_m 𝐷) ↔ (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )):𝐷⟶(Base‘𝑅))
151	148, 150	sylibr 233	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ ((Base‘𝑅) ↑_m 𝐷))
152	29, 2, 4, 30, 131	psrbas 21942	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (Base‘(𝐼 mPwSer 𝑅)) = ((Base‘𝑅) ↑_m 𝐷))
153	151, 152	eleqtrrd 2829	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ (Base‘(𝐼 mPwSer 𝑅)))
154	13	mptex 7240	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ V
155		funmpt 6597	. . . . . . . . . . . . . . . . . . 19 ⊢ Fun (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))
156	154, 155, 16	3pm3.2i 1336	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ V ∧ Fun (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∧ 0 ∈ V)
157	156	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ V ∧ Fun (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∧ 0 ∈ V))
158		eldifn 4127	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝐷 ∖ 𝑥) → ¬ 𝑦 ∈ 𝑥)
159	158	adantl 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ (𝐷 ∖ 𝑥)) → ¬ 𝑦 ∈ 𝑥)
160	159	iffalsed 4544	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ (𝐷 ∖ 𝑥)) → if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ) = 0 )
161	13	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝐷 ∈ V)
162	160, 161	suppss2 8215	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) supp 0 ) ⊆ 𝑥)
163		suppssfifsupp 9423	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ V ∧ Fun (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∧ 0 ∈ V) ∧ (𝑥 ∈ Fin ∧ ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) supp 0 ) ⊆ 𝑥)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) finSupp 0 )
164	157, 96, 162, 163	syl12anc 835	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) finSupp 0 )
165	1, 29, 30, 15, 3	mplelbas 22000	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ 𝐵 ↔ ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) finSupp 0 ))
166	153, 164, 165	sylanbrc 581	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ 𝐵)
167	1, 3, 142, 91, 166, 135	mpladd 22018	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))(+_g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) = ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∘_f (+_g‘𝑅)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))))
168		ovexd 7459	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → ((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )) ∈ V)
169		eqidd 2727	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )))
170		eqid 2726	. . . . . . . . . . . . . . . . 17 ⊢ (._r‘𝑅) = (._r‘𝑅)
171	1, 112, 2, 3, 170, 4, 127, 133	mplvsca 22024	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) = ((𝐷 × {(𝑋‘𝑧)}) ∘_f (._r‘𝑅)(𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))))
172	127	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → (𝑋‘𝑧) ∈ (Base‘𝑅))
173	2, 108	ringidcl 20245	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅 ∈ Ring → 1 ∈ (Base‘𝑅))
174	173, 144	ifcld 4579	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 ∈ Ring → if(𝑦 = 𝑧, 1 , 0 ) ∈ (Base‘𝑅))
175	79, 174	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → if(𝑦 = 𝑧, 1 , 0 ) ∈ (Base‘𝑅))
176	175	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → if(𝑦 = 𝑧, 1 , 0 ) ∈ (Base‘𝑅))
177		fconstmpt 5744	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐷 × {(𝑋‘𝑧)}) = (𝑦 ∈ 𝐷 ↦ (𝑋‘𝑧))
178	177	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝐷 × {(𝑋‘𝑧)}) = (𝑦 ∈ 𝐷 ↦ (𝑋‘𝑧)))
179		eqidd 2727	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))
180	161, 172, 176, 178, 179	offval2 7710	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝐷 × {(𝑋‘𝑧)}) ∘_f (._r‘𝑅)(𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) = (𝑦 ∈ 𝐷 ↦ ((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))))
181	171, 180	eqtrd 2766	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) = (𝑦 ∈ 𝐷 ↦ ((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))))
182	161, 147, 168, 169, 181	offval2 7710	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∘_f (+_g‘𝑅)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) = (𝑦 ∈ 𝐷 ↦ (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )(+_g‘𝑅)((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )))))
183	132, 80	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑅 ∈ Grp)
184	2, 142, 15	grplid 18962	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Grp ∧ (𝑋‘𝑧) ∈ (Base‘𝑅)) → ( 0 (+_g‘𝑅)(𝑋‘𝑧)) = (𝑋‘𝑧))
185	183, 127, 184	syl2anc 582	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ( 0 (+_g‘𝑅)(𝑋‘𝑧)) = (𝑋‘𝑧))
186	185	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ( 0 (+_g‘𝑅)(𝑋‘𝑧)) = (𝑋‘𝑧))
187		simpr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → 𝑦 ∈ {𝑧})
188		velsn 4649	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ {𝑧} ↔ 𝑦 = 𝑧)
189	187, 188	sylib 217	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → 𝑦 = 𝑧)
190	189	fveq2d 6905	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → (𝑋‘𝑦) = (𝑋‘𝑧))
191	186, 190	eqtr4d 2769	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ( 0 (+_g‘𝑅)(𝑋‘𝑧)) = (𝑋‘𝑦))
192	120	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ¬ 𝑧 ∈ 𝑥)
193	189, 192	eqneltrd 2846	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ¬ 𝑦 ∈ 𝑥)
194	193	iffalsed 4544	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ) = 0 )
195	189	iftrued 4541	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → if(𝑦 = 𝑧, 1 , 0 ) = 1 )
196	195	oveq2d 7440	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )) = ((𝑋‘𝑧)(._r‘𝑅) 1 ))
197	2, 170, 108	ringridm 20249	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑧) ∈ (Base‘𝑅)) → ((𝑋‘𝑧)(._r‘𝑅) 1 ) = (𝑋‘𝑧))
198	132, 127, 197	syl2anc 582	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋‘𝑧)(._r‘𝑅) 1 ) = (𝑋‘𝑧))
199	198	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(._r‘𝑅) 1 ) = (𝑋‘𝑧))
200	196, 199	eqtrd 2766	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )) = (𝑋‘𝑧))
201	194, 200	oveq12d 7442	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )(+_g‘𝑅)((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = ( 0 (+_g‘𝑅)(𝑋‘𝑧)))
202		elun2 4178	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ {𝑧} → 𝑦 ∈ (𝑥 ∪ {𝑧}))
203	202	adantl 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → 𝑦 ∈ (𝑥 ∪ {𝑧}))
204	203	iftrued 4541	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦))
205	191, 201, 204	3eqtr4d 2776	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )(+_g‘𝑅)((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))
206	81	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ Grp)
207	2, 142, 15	grprid 18963	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Grp ∧ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ) ∈ (Base‘𝑅)) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )(+_g‘𝑅) 0 ) = if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))
208	206, 147, 207	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )(+_g‘𝑅) 0 ) = if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))
209	208	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )(+_g‘𝑅) 0 ) = if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))
210		simpr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ¬ 𝑦 ∈ {𝑧})
211	210, 188	sylnib 327	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ¬ 𝑦 = 𝑧)
212	211	iffalsed 4544	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → if(𝑦 = 𝑧, 1 , 0 ) = 0 )
213	212	oveq2d 7440	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )) = ((𝑋‘𝑧)(._r‘𝑅) 0 ))
214	2, 170, 15	ringrz 20273	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑧) ∈ (Base‘𝑅)) → ((𝑋‘𝑧)(._r‘𝑅) 0 ) = 0 )
215	132, 127, 214	syl2anc 582	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋‘𝑧)(._r‘𝑅) 0 ) = 0 )
216	215	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(._r‘𝑅) 0 ) = 0 )
217	213, 216	eqtrd 2766	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )) = 0 )
218	217	oveq2d 7440	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )(+_g‘𝑅)((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )(+_g‘𝑅) 0 ))
219		elun 4148	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (𝑥 ∪ {𝑧}) ↔ (𝑦 ∈ 𝑥 ∨ 𝑦 ∈ {𝑧}))
220		orcom 868	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ 𝑥 ∨ 𝑦 ∈ {𝑧}) ↔ (𝑦 ∈ {𝑧} ∨ 𝑦 ∈ 𝑥))
221	219, 220	bitri 274	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝑥 ∪ {𝑧}) ↔ (𝑦 ∈ {𝑧} ∨ 𝑦 ∈ 𝑥))
222		biorf 934	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑦 ∈ {𝑧} → (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ {𝑧} ∨ 𝑦 ∈ 𝑥)))
223	221, 222	bitr4id 289	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑦 ∈ {𝑧} → (𝑦 ∈ (𝑥 ∪ {𝑧}) ↔ 𝑦 ∈ 𝑥))
224	223	adantl 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → (𝑦 ∈ (𝑥 ∪ {𝑧}) ↔ 𝑦 ∈ 𝑥))
225	224	ifbid 4556	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ) = if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))
226	209, 218, 225	3eqtr4d 2776	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )(+_g‘𝑅)((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))
227	205, 226	pm2.61dan 811	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )(+_g‘𝑅)((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))
228	227	mpteq2dva 5253	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )(+_g‘𝑅)((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )))
229	167, 182, 228	3eqtrrd 2771	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )) = ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))(+_g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))))
230	141, 229	eqeq12d 2742	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )) ↔ ((𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))(+_g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) = ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))(+_g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))))))
231	90, 230	imbitrrid 245	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) → (𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))))
232	231	expr 455	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥)) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → ((𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) → (𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )))))
233	232	a2d 29	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥)) → (((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )))))
234	89, 233	syl5 34	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥)) → ((𝑥 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )))))
235	234	expcom 412	. . . . . . 7 ⊢ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) → (𝜑 → ((𝑥 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))))))
236	235	a2d 29	. . . . . 6 ⊢ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) → ((𝜑 → (𝑥 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )))) → (𝜑 → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))))))
237	50, 59, 68, 77, 85, 236	findcard2s 9203	. . . . 5 ⊢ ((𝑋 supp 0 ) ∈ Fin → (𝜑 → ((𝑋 supp 0 ) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )))))
238	34, 237	mpcom 38	. . . 4 ⊢ (𝜑 → ((𝑋 supp 0 ) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ))))
239	28, 238	mpd 15	. . 3 ⊢ (𝜑 → (𝑃 Σ_g (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )))
240	26, 239	eqtr4d 2769	. 2 ⊢ (𝜑 → 𝑋 = (𝑃 Σ_g (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
241	28	resmptd 6049	. . . 4 ⊢ (𝜑 → ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ↾ (𝑋 supp 0 )) = (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))
242	241	oveq2d 7440	. . 3 ⊢ (𝜑 → (𝑃 Σ_g ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ↾ (𝑋 supp 0 ))) = (𝑃 Σ_g (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
243	115	fmpttd 7129	. . . 4 ⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))):𝐷⟶𝐵)
244	6, 11, 14, 17	suppssr 8210	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → (𝑋‘𝑘) = 0 )
245	244	oveq1d 7439	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = ( 0 · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))
246		eldifi 4126	. . . . . . 7 ⊢ (𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 )) → 𝑘 ∈ 𝐷)
247	105	fveq2d 6905	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (0_g‘𝑅) = (0_g‘(Scalar‘𝑃)))
248	15, 247	eqtrid 2778	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 0 = (0_g‘(Scalar‘𝑃)))
249	248	oveq1d 7439	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ( 0 · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = ((0_g‘(Scalar‘𝑃)) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))
250		eqid 2726	. . . . . . . . . 10 ⊢ (0_g‘(Scalar‘𝑃)) = (0_g‘(Scalar‘𝑃))
251	3, 111, 112, 250, 40	lmod0vs 20871	. . . . . . . . 9 ⊢ ((𝑃 ∈ LMod ∧ (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )) ∈ 𝐵) → ((0_g‘(Scalar‘𝑃)) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = (0_g‘𝑃))
252	102, 110, 251	syl2anc 582	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ((0_g‘(Scalar‘𝑃)) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = (0_g‘𝑃))
253	249, 252	eqtrd 2766	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ( 0 · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = (0_g‘𝑃))
254	246, 253	sylan2 591	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → ( 0 · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = (0_g‘𝑃))
255	245, 254	eqtrd 2766	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = (0_g‘𝑃))
256	255, 14	suppss2 8215	. . . 4 ⊢ (𝜑 → ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) supp (0_g‘𝑃)) ⊆ (𝑋 supp 0 ))
257	13	mptex 7240	. . . . . . 7 ⊢ (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∈ V
258		funmpt 6597	. . . . . . 7 ⊢ Fun (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))
259		fvex 6914	. . . . . . 7 ⊢ (0_g‘𝑃) ∈ V
260	257, 258, 259	3pm3.2i 1336	. . . . . 6 ⊢ ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∈ V ∧ Fun (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∧ (0_g‘𝑃) ∈ V)
261	260	a1i 11	. . . . 5 ⊢ (𝜑 → ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∈ V ∧ Fun (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∧ (0_g‘𝑃) ∈ V))
262		suppssfifsupp 9423	. . . . 5 ⊢ ((((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∈ V ∧ Fun (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∧ (0_g‘𝑃) ∈ V) ∧ ((𝑋 supp 0 ) ∈ Fin ∧ ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) supp (0_g‘𝑃)) ⊆ (𝑋 supp 0 ))) → (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) finSupp (0_g‘𝑃))
263	261, 34, 256, 262	syl12anc 835	. . . 4 ⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) finSupp (0_g‘𝑃))
264	3, 40, 94, 14, 243, 256, 263	gsumres 19911	. . 3 ⊢ (𝜑 → (𝑃 Σ_g ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ↾ (𝑋 supp 0 ))) = (𝑃 Σ_g (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
265	242, 264	eqtr3d 2768	. 2 ⊢ (𝜑 → (𝑃 Σ_g (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σ_g (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
266	240, 265	eqtrd 2766	1 ⊢ (𝜑 → 𝑋 = (𝑃 Σ_g (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 ∨ wo 845 ∧ w3a 1084 = wceq 1534 ∈ wcel 2099 {crab 3419 Vcvv 3462 ∖ cdif 3944 ∪ cun 3945 ⊆ wss 3947 ∅c0 4325 ifcif 4533 {csn 4633 class class class wbr 5153 ↦ cmpt 5236 × cxp 5680 ^◡ccnv 5681 ↾ cres 5684 “ cima 5685 Fun wfun 6548 ⟶wf 6550 ‘cfv 6554 (class class class)co 7424 ∘_f cof 7688 supp csupp 8174 ↑_m cmap 8855 Fincfn 8974 finSupp cfsupp 9405 ℕcn 12264 ℕ₀cn0 12524 Basecbs 17213 +_gcplusg 17266 ._rcmulr 17267 Scalarcsca 17269 ·_𝑠 cvsca 17270 0_gc0g 17454 Σ_g cgsu 17455 Grpcgrp 18928 CMndccmn 19778 1_rcur 20164 Ringcrg 20216 LModclmod 20836 mPwSer cmps 21901 mPoly cmpl 21903

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 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-rep 5290 ax-sep 5304 ax-nul 5311 ax-pow 5369 ax-pr 5433 ax-un 7746 ax-cnex 11214 ax-resscn 11215 ax-1cn 11216 ax-icn 11217 ax-addcl 11218 ax-addrcl 11219 ax-mulcl 11220 ax-mulrcl 11221 ax-mulcom 11222 ax-addass 11223 ax-mulass 11224 ax-distr 11225 ax-i2m1 11226 ax-1ne0 11227 ax-1rid 11228 ax-rnegex 11229 ax-rrecex 11230 ax-cnre 11231 ax-pre-lttri 11232 ax-pre-lttrn 11233 ax-pre-ltadd 11234 ax-pre-mulgt0 11235

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3464 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3967 df-nul 4326 df-if 4534 df-pw 4609 df-sn 4634 df-pr 4636 df-tp 4638 df-op 4640 df-uni 4914 df-int 4955 df-iun 5003 df-iin 5004 df-br 5154 df-opab 5216 df-mpt 5237 df-tr 5271 df-id 5580 df-eprel 5586 df-po 5594 df-so 5595 df-fr 5637 df-se 5638 df-we 5639 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-pred 6312 df-ord 6379 df-on 6380 df-lim 6381 df-suc 6382 df-iota 6506 df-fun 6556 df-fn 6557 df-f 6558 df-f1 6559 df-fo 6560 df-f1o 6561 df-fv 6562 df-isom 6563 df-riota 7380 df-ov 7427 df-oprab 7428 df-mpo 7429 df-of 7690 df-ofr 7691 df-om 7877 df-1st 8003 df-2nd 8004 df-supp 8175 df-frecs 8296 df-wrecs 8327 df-recs 8401 df-rdg 8440 df-1o 8496 df-2o 8497 df-er 8734 df-map 8857 df-pm 8858 df-ixp 8927 df-en 8975 df-dom 8976 df-sdom 8977 df-fin 8978 df-fsupp 9406 df-sup 9485 df-oi 9553 df-card 9982 df-pnf 11300 df-mnf 11301 df-xr 11302 df-ltxr 11303 df-le 11304 df-sub 11496 df-neg 11497 df-nn 12265 df-2 12327 df-3 12328 df-4 12329 df-5 12330 df-6 12331 df-7 12332 df-8 12333 df-9 12334 df-n0 12525 df-z 12611 df-dec 12730 df-uz 12875 df-fz 13539 df-fzo 13682 df-seq 14022 df-hash 14348 df-struct 17149 df-sets 17166 df-slot 17184 df-ndx 17196 df-base 17214 df-ress 17243 df-plusg 17279 df-mulr 17280 df-sca 17282 df-vsca 17283 df-ip 17284 df-tset 17285 df-ple 17286 df-ds 17288 df-hom 17290 df-cco 17291 df-0g 17456 df-gsum 17457 df-prds 17462 df-pws 17464 df-mre 17599 df-mrc 17600 df-acs 17602 df-mgm 18633 df-sgrp 18712 df-mnd 18728 df-mhm 18773 df-submnd 18774 df-grp 18931 df-minusg 18932 df-sbg 18933 df-mulg 19062 df-subg 19117 df-ghm 19207 df-cntz 19311 df-cmn 19780 df-abl 19781 df-mgp 20118 df-rng 20136 df-ur 20165 df-ring 20218 df-subrng 20528 df-subrg 20553 df-lmod 20838 df-lss 20909 df-psr 21906 df-mpl 21908

This theorem is referenced by: mplbas2 22049 mplcoe4 22084 ply1coe 22289

W3C validator