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 22308

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 2760	. . . . . 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 22267	. . . . 5 ⊢ (𝜑 → 𝑋:𝐷⟶(Base‘𝑅))
7	6	feqmptd 6941	. . . 4 ⊢ (𝜑 → 𝑋 = (𝑦 ∈ 𝐷 ↦ (𝑋‘𝑦)))
8		iftrue 4487	. . . . . . 7 ⊢ (𝑦 ∈ (𝑋 supp 0 ) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦))
9	8	adantl 487	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝑋 supp 0 )) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦))
10		eldif 3908	. . . . . . . 8 ⊢ (𝑦 ∈ (𝐷 ∖ (𝑋 supp 0 )) ↔ (𝑦 ∈ 𝐷 ∧ ¬ 𝑦 ∈ (𝑋 supp 0 )))
11		ssidd 3953	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋 supp 0 ) ⊆ (𝑋 supp 0 ))
12		ovex 7441	. . . . . . . . . . . . 13 ⊢ (ℕ₀ ↑_m 𝐼) ∈ V
13	4, 12	rabex2 5301	. . . . . . . . . . . 12 ⊢ 𝐷 ∈ V
14	13	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ V)
15		mplcoe1.z	. . . . . . . . . . . . 13 ⊢ 0 = (0_g‘𝑅)
16	15	fvexi 6887	. . . . . . . . . . . 12 ⊢ 0 ∈ V
17	16	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 0 ∈ V)
18	6, 11, 14, 17	suppssr 8190	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → (𝑋‘𝑦) = 0 )
19	18	ifeq2d 4502	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), (𝑋‘𝑦)) = if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ))
20		ifid 4522	. . . . . . . . 9 ⊢ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), (𝑋‘𝑦)) = (𝑋‘𝑦)
21	19, 20	eqtr3di 2810	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦))
22	10, 21	sylan2br 607	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ∧ ¬ 𝑦 ∈ (𝑋 supp 0 ))) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦))
23	22	anassrs 473	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ (𝑋 supp 0 )) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦))
24	9, 23	pm2.61dan 825	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦))
25	24	mpteq2dva 5197	. . . 4 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ (𝑋‘𝑦)))
26	7, 25	eqtr4d 2798	. . 3 ⊢ (𝜑 → 𝑋 = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )))
27		suppssdm 8172	. . . . 5 ⊢ (𝑋 supp 0 ) ⊆ dom 𝑋
28	27, 6	fssdm 6717	. . . 4 ⊢ (𝜑 → (𝑋 supp 0 ) ⊆ 𝐷)
29		eqid 2760	. . . . . . . . 9 ⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅)
30		eqid 2760	. . . . . . . . 9 ⊢ (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑅))
31	1, 29, 30, 15, 3	mplelbas 22260	. . . . . . . 8 ⊢ (𝑋 ∈ 𝐵 ↔ (𝑋 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑋 finSupp 0 ))
32	31	simprbi 503	. . . . . . 7 ⊢ (𝑋 ∈ 𝐵 → 𝑋 finSupp 0 )
33	5, 32	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑋 finSupp 0 )
34	33	fsuppimpd 9339	. . . . 5 ⊢ (𝜑 → (𝑋 supp 0 ) ∈ Fin)
35		sseq1 3955	. . . . . . . 8 ⊢ (𝑤 = ∅ → (𝑤 ⊆ 𝐷 ↔ ∅ ⊆ 𝐷))
36		mpteq1 5193	. . . . . . . . . . . 12 ⊢ (𝑤 = ∅ → (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = (𝑘 ∈ ∅ ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))
37		mpt0 6669	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ∅ ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = ∅
38	36, 37	eqtrdi 2811	. . . . . . . . . . 11 ⊢ (𝑤 = ∅ → (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = ∅)
39	38	oveq2d 7424	. . . . . . . . . 10 ⊢ (𝑤 = ∅ → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σ_g ∅))
40		eqid 2760	. . . . . . . . . . 11 ⊢ (0_g‘𝑃) = (0_g‘𝑃)
41	40	gsum0 18835	. . . . . . . . . 10 ⊢ (𝑃 Σ_g ∅) = (0_g‘𝑃)
42	39, 41	eqtrdi 2811	. . . . . . . . 9 ⊢ (𝑤 = ∅ → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (0_g‘𝑃))
43		noel 4283	. . . . . . . . . . . 12 ⊢ ¬ 𝑦 ∈ ∅
44		eleq2 2849	. . . . . . . . . . . 12 ⊢ (𝑤 = ∅ → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ ∅))
45	43, 44	mtbiri 330	. . . . . . . . . . 11 ⊢ (𝑤 = ∅ → ¬ 𝑦 ∈ 𝑤)
46	45	iffalsed 4492	. . . . . . . . . 10 ⊢ (𝑤 = ∅ → if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ) = 0 )
47	46	mpteq2dv 5198	. . . . . . . . 9 ⊢ (𝑤 = ∅ → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ 0 ))
48	42, 47	eqeq12d 2776	. . . . . . . 8 ⊢ (𝑤 = ∅ → ((𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) ↔ (0_g‘𝑃) = (𝑦 ∈ 𝐷 ↦ 0 )))
49	35, 48	imbi12d 347	. . . . . . 7 ⊢ (𝑤 = ∅ → ((𝑤 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ))) ↔ (∅ ⊆ 𝐷 → (0_g‘𝑃) = (𝑦 ∈ 𝐷 ↦ 0 ))))
50	49	imbi2d 343	. . . . . 6 ⊢ (𝑤 = ∅ → ((𝜑 → (𝑤 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )))) ↔ (𝜑 → (∅ ⊆ 𝐷 → (0_g‘𝑃) = (𝑦 ∈ 𝐷 ↦ 0 )))))
51		sseq1 3955	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → (𝑤 ⊆ 𝐷 ↔ 𝑥 ⊆ 𝐷))
52		mpteq1 5193	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))
53	52	oveq2d 7424	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
54		eleq2 2849	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑥 → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑥))
55	54	ifbid 4505	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ) = if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))
56	55	mpteq2dv 5198	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )))
57	53, 56	eqeq12d 2776	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → ((𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) ↔ (𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))))
58	51, 57	imbi12d 347	. . . . . . 7 ⊢ (𝑤 = 𝑥 → ((𝑤 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ))) ↔ (𝑥 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )))))
59	58	imbi2d 343	. . . . . 6 ⊢ (𝑤 = 𝑥 → ((𝜑 → (𝑤 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )))) ↔ (𝜑 → (𝑥 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))))))
60		sseq1 3955	. . . . . . . 8 ⊢ (𝑤 = (𝑥 ∪ {𝑧}) → (𝑤 ⊆ 𝐷 ↔ (𝑥 ∪ {𝑧}) ⊆ 𝐷))
61		mpteq1 5193	. . . . . . . . . 10 ⊢ (𝑤 = (𝑥 ∪ {𝑧}) → (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))
62	61	oveq2d 7424	. . . . . . . . 9 ⊢ (𝑤 = (𝑥 ∪ {𝑧}) → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
63		eleq2 2849	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑥 ∪ {𝑧}) → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ (𝑥 ∪ {𝑧})))
64	63	ifbid 4505	. . . . . . . . . 10 ⊢ (𝑤 = (𝑥 ∪ {𝑧}) → if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ) = if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))
65	64	mpteq2dv 5198	. . . . . . . . 9 ⊢ (𝑤 = (𝑥 ∪ {𝑧}) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )))
66	62, 65	eqeq12d 2776	. . . . . . . 8 ⊢ (𝑤 = (𝑥 ∪ {𝑧}) → ((𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) ↔ (𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))))
67	60, 66	imbi12d 347	. . . . . . 7 ⊢ (𝑤 = (𝑥 ∪ {𝑧}) → ((𝑤 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ))) ↔ ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )))))
68	67	imbi2d 343	. . . . . 6 ⊢ (𝑤 = (𝑥 ∪ {𝑧}) → ((𝜑 → (𝑤 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )))) ↔ (𝜑 → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))))))
69		sseq1 3955	. . . . . . . 8 ⊢ (𝑤 = (𝑋 supp 0 ) → (𝑤 ⊆ 𝐷 ↔ (𝑋 supp 0 ) ⊆ 𝐷))
70		mpteq1 5193	. . . . . . . . . 10 ⊢ (𝑤 = (𝑋 supp 0 ) → (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) = (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))
71	70	oveq2d 7424	. . . . . . . . 9 ⊢ (𝑤 = (𝑋 supp 0 ) → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σ_g (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
72		eleq2 2849	. . . . . . . . . . 11 ⊢ (𝑤 = (𝑋 supp 0 ) → (𝑦 ∈ 𝑤 ↔ 𝑦 ∈ (𝑋 supp 0 )))
73	72	ifbid 4505	. . . . . . . . . 10 ⊢ (𝑤 = (𝑋 supp 0 ) → if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ) = if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ))
74	73	mpteq2dv 5198	. . . . . . . . 9 ⊢ (𝑤 = (𝑋 supp 0 ) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )))
75	71, 74	eqeq12d 2776	. . . . . . . 8 ⊢ (𝑤 = (𝑋 supp 0 ) → ((𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 )) ↔ (𝑃 Σ_g (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ))))
76	69, 75	imbi12d 347	. . . . . . 7 ⊢ (𝑤 = (𝑋 supp 0 ) → ((𝑤 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑤 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑤, (𝑋‘𝑦), 0 ))) ↔ ((𝑋 supp 0 ) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )))))
77	76	imbi2d 343	. . . . . 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 20426	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
81	79, 80	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ Grp)
82	1, 4, 15, 40, 78, 81	mpl0 22275	. . . . . . . 8 ⊢ (𝜑 → (0_g‘𝑃) = (𝐷 × { 0 }))
83		fconstmpt 5709	. . . . . . . 8 ⊢ (𝐷 × { 0 }) = (𝑦 ∈ 𝐷 ↦ 0 )
84	82, 83	eqtrdi 2811	. . . . . . 7 ⊢ (𝜑 → (0_g‘𝑃) = (𝑦 ∈ 𝐷 ↦ 0 ))
85	84	a1d 26	. . . . . 6 ⊢ (𝜑 → (∅ ⊆ 𝐷 → (0_g‘𝑃) = (𝑦 ∈ 𝐷 ↦ 0 )))
86		ssun1 4123	. . . . . . . . . . 11 ⊢ 𝑥 ⊆ (𝑥 ∪ {𝑧})
87		sstr2 3937	. . . . . . . . . . 11 ⊢ (𝑥 ⊆ (𝑥 ∪ {𝑧}) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → 𝑥 ⊆ 𝐷))
88	86, 87	ax-mp 5	. . . . . . . . . 10 ⊢ ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → 𝑥 ⊆ 𝐷)
89	88	imim1i 64	. . . . . . . . 9 ⊢ ((𝑥 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))))
90		oveq1 7415	. . . . . . . . . . . 12 ⊢ ((𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) → ((𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))(+_g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) = ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))(+_g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))))
91		eqid 2760	. . . . . . . . . . . . . 14 ⊢ (+_g‘𝑃) = (+_g‘𝑃)
92	1, 78, 79	mplringd 22292	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ Ring)
93		ringcmn 20473	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ CMnd)
94	92, 93	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ CMnd)
95	94	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑃 ∈ CMnd)
96		simprll 791	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑥 ∈ Fin)
97		simprr 785	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑥 ∪ {𝑧}) ⊆ 𝐷)
98	97	unssad 4138	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑥 ⊆ 𝐷)
99	98	sselda 3930	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝐷)
100	78	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝐼 ∈ 𝑊)
101	79	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 ∈ Ring)
102	1, 100, 101	mpllmodd 22294	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑃 ∈ LMod)
103	6	ffvelcdmda 7072	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑋‘𝑘) ∈ (Base‘𝑅))
104	1, 78, 79	mplsca 22282	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑅 = (Scalar‘𝑃))
105	104	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 = (Scalar‘𝑃))
106	105	fveq2d 6877	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
107	103, 106	eleqtrd 2862	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑋‘𝑘) ∈ (Base‘(Scalar‘𝑃)))
108		mplcoe1.o	. . . . . . . . . . . . . . . . . 18 ⊢ 1 = (1_r‘𝑅)
109		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑘 ∈ 𝐷)
110	1, 3, 15, 108, 4, 100, 101, 109	mplmon 22306	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )) ∈ 𝐵)
111		eqid 2760	. . . . . . . . . . . . . . . . . 18 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
112		mplcoe1.n	. . . . . . . . . . . . . . . . . 18 ⊢ · = ( ·_𝑠 ‘𝑃)
113		eqid 2760	. . . . . . . . . . . . . . . . . 18 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
114	3, 111, 112, 113	lmodvscl 21115	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ LMod ∧ (𝑋‘𝑘) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )) ∈ 𝐵) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) ∈ 𝐵)
115	102, 107, 110, 114	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) ∈ 𝐵)
116	115	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑘 ∈ 𝐷) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) ∈ 𝐵)
117	99, 116	syldan 603	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑘 ∈ 𝑥) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) ∈ 𝐵)
118		vex 3454	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
119	118	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑧 ∈ V)
120		simprlr 792	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ¬ 𝑧 ∈ 𝑥)
121	1, 78, 79	mpllmodd 22294	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ LMod)
122	121	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑃 ∈ LMod)
123	6	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑋:𝐷⟶(Base‘𝑅))
124	97	unssbd 4139	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → {𝑧} ⊆ 𝐷)
125	118	snss 4744	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ 𝐷 ↔ {𝑧} ⊆ 𝐷)
126	124, 125	sylibr 237	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑧 ∈ 𝐷)
127	123, 126	ffvelcdmd 7073	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑋‘𝑧) ∈ (Base‘𝑅))
128	104	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑅 = (Scalar‘𝑃))
129	128	fveq2d 6877	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
130	127, 129	eleqtrd 2862	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑋‘𝑧) ∈ (Base‘(Scalar‘𝑃)))
131	78	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝐼 ∈ 𝑊)
132	79	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑅 ∈ Ring)
133	1, 3, 15, 108, 4, 131, 132, 126	mplmon 22306	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )) ∈ 𝐵)
134	3, 111, 112, 113	lmodvscl 21115	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ LMod ∧ (𝑋‘𝑧) ∈ (Base‘(Scalar‘𝑃)) ∧ (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )) ∈ 𝐵) → ((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) ∈ 𝐵)
135	122, 130, 133, 134	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) ∈ 𝐵)
136		fveq2 6873	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑧 → (𝑋‘𝑘) = (𝑋‘𝑧))
137		equequ2 2059	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑧 → (𝑦 = 𝑘 ↔ 𝑦 = 𝑧))
138	137	ifbid 4505	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑧 → if(𝑦 = 𝑘, 1 , 0 ) = if(𝑦 = 𝑧, 1 , 0 ))
139	138	mpteq2dv 5198	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑧 → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))
140	136, 139	oveq12d 7426	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑧 → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = ((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))))
141	3, 91, 95, 96, 117, 119, 120, 135, 140	gsumunsn 20136	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = ((𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))(+_g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))))
142		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ (+_g‘𝑅) = (+_g‘𝑅)
143	123	ffvelcdmda 7072	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → (𝑋‘𝑦) ∈ (Base‘𝑅))
144	2, 15	ring0cl 20458	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅 ∈ Ring → 0 ∈ (Base‘𝑅))
145	79, 144	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 0 ∈ (Base‘𝑅))
146	145	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → 0 ∈ (Base‘𝑅))
147	143, 146	ifcld 4528	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ) ∈ (Base‘𝑅))
148	147	fmpttd 7103	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )):𝐷⟶(Base‘𝑅))
149		fvex 6886	. . . . . . . . . . . . . . . . . . 19 ⊢ (Base‘𝑅) ∈ V
150	149, 13	elmap 8877	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ ((Base‘𝑅) ↑_m 𝐷) ↔ (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )):𝐷⟶(Base‘𝑅))
151	148, 150	sylibr 237	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ ((Base‘𝑅) ↑_m 𝐷))
152	29, 2, 4, 30, 131	psrbas 22204	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (Base‘(𝐼 mPwSer 𝑅)) = ((Base‘𝑅) ↑_m 𝐷))
153	151, 152	eleqtrrd 2863	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ (Base‘(𝐼 mPwSer 𝑅)))
154	13	mptex 7217	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ V
155		funmpt 6566	. . . . . . . . . . . . . . . . . . 19 ⊢ Fun (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))
156	154, 155, 16	3pm3.2i 1358	. . . . . . . . . . . . . . . . . 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 4078	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝐷 ∖ 𝑥) → ¬ 𝑦 ∈ 𝑥)
159	158	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ (𝐷 ∖ 𝑥)) → ¬ 𝑦 ∈ 𝑥)
160	159	iffalsed 4492	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ (𝐷 ∖ 𝑥)) → if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ) = 0 )
161	13	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝐷 ∈ V)
162	160, 161	suppss2 8195	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) supp 0 ) ⊆ 𝑥)
163		suppssfifsupp 9350	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ V ∧ Fun (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∧ 0 ∈ V) ∧ (𝑥 ∈ Fin ∧ ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) supp 0 ) ⊆ 𝑥)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) finSupp 0 )
164	157, 96, 162, 163	syl12anc 850	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) finSupp 0 )
165	1, 29, 30, 15, 3	mplelbas 22260	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ 𝐵 ↔ ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) finSupp 0 ))
166	153, 164, 165	sylanbrc 595	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∈ 𝐵)
167	1, 3, 142, 91, 166, 135	mpladd 22278	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))(+_g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) = ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∘_f (+_g‘𝑅)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))))
168		ovexd 7443	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → ((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )) ∈ V)
169		eqidd 2761	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )))
170		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ (._r‘𝑅) = (._r‘𝑅)
171	1, 112, 2, 3, 170, 4, 127, 133	mplvsca 22284	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) = ((𝐷 × {(𝑋‘𝑧)}) ∘_f (._r‘𝑅)(𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))))
172	127	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → (𝑋‘𝑧) ∈ (Base‘𝑅))
173	2, 108	ringidcl 20456	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅 ∈ Ring → 1 ∈ (Base‘𝑅))
174	173, 144	ifcld 4528	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑅 ∈ Ring → if(𝑦 = 𝑧, 1 , 0 ) ∈ (Base‘𝑅))
175	79, 174	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → if(𝑦 = 𝑧, 1 , 0 ) ∈ (Base‘𝑅))
176	175	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → if(𝑦 = 𝑧, 1 , 0 ) ∈ (Base‘𝑅))
177		fconstmpt 5709	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐷 × {(𝑋‘𝑧)}) = (𝑦 ∈ 𝐷 ↦ (𝑋‘𝑧))
178	177	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝐷 × {(𝑋‘𝑧)}) = (𝑦 ∈ 𝐷 ↦ (𝑋‘𝑧)))
179		eqidd 2761	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))
180	161, 172, 176, 178, 179	offval2 7696	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝐷 × {(𝑋‘𝑧)}) ∘_f (._r‘𝑅)(𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) = (𝑦 ∈ 𝐷 ↦ ((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))))
181	171, 180	eqtrd 2795	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))) = (𝑦 ∈ 𝐷 ↦ ((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))))
182	161, 147, 168, 169, 181	offval2 7696	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) ∘_f (+_g‘𝑅)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) = (𝑦 ∈ 𝐷 ↦ (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )(+_g‘𝑅)((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )))))
183	132, 80	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → 𝑅 ∈ Grp)
184	2, 142, 15	grplid 19140	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ Grp ∧ (𝑋‘𝑧) ∈ (Base‘𝑅)) → ( 0 (+_g‘𝑅)(𝑋‘𝑧)) = (𝑋‘𝑧))
185	183, 127, 184	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ( 0 (+_g‘𝑅)(𝑋‘𝑧)) = (𝑋‘𝑧))
186	185	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ( 0 (+_g‘𝑅)(𝑋‘𝑧)) = (𝑋‘𝑧))
187		velsn 4599	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ {𝑧} ↔ 𝑦 = 𝑧)
188	187	bilani 510	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → 𝑦 = 𝑧)
189	188	fveq2d 6877	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → (𝑋‘𝑦) = (𝑋‘𝑧))
190	186, 189	eqtr4d 2798	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ( 0 (+_g‘𝑅)(𝑋‘𝑧)) = (𝑋‘𝑦))
191	120	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ¬ 𝑧 ∈ 𝑥)
192	188, 191	eqneltrd 2880	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ¬ 𝑦 ∈ 𝑥)
193	192	iffalsed 4492	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ) = 0 )
194	188	iftrued 4489	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → if(𝑦 = 𝑧, 1 , 0 ) = 1 )
195	194	oveq2d 7424	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )) = ((𝑋‘𝑧)(._r‘𝑅) 1 ))
196	2, 170, 108	ringridm 20461	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑧) ∈ (Base‘𝑅)) → ((𝑋‘𝑧)(._r‘𝑅) 1 ) = (𝑋‘𝑧))
197	132, 127, 196	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋‘𝑧)(._r‘𝑅) 1 ) = (𝑋‘𝑧))
198	197	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(._r‘𝑅) 1 ) = (𝑋‘𝑧))
199	195, 198	eqtrd 2795	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )) = (𝑋‘𝑧))
200	193, 199	oveq12d 7426	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )(+_g‘𝑅)((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = ( 0 (+_g‘𝑅)(𝑋‘𝑧)))
201		elun2 4128	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ {𝑧} → 𝑦 ∈ (𝑥 ∪ {𝑧}))
202	201	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → 𝑦 ∈ (𝑥 ∪ {𝑧}))
203	202	iftrued 4489	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ) = (𝑋‘𝑦))
204	190, 200, 203	3eqtr4d 2805	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ {𝑧}) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )(+_g‘𝑅)((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))
205	81	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → 𝑅 ∈ Grp)
206	2, 142, 15	grprid 19141	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Grp ∧ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ) ∈ (Base‘𝑅)) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )(+_g‘𝑅) 0 ) = if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))
207	205, 147, 206	syl2anc 596	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )(+_g‘𝑅) 0 ) = if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))
208	207	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )(+_g‘𝑅) 0 ) = if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))
209		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ¬ 𝑦 ∈ {𝑧})
210	209, 187	sylnib 331	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ¬ 𝑦 = 𝑧)
211	210	iffalsed 4492	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → if(𝑦 = 𝑧, 1 , 0 ) = 0 )
212	211	oveq2d 7424	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )) = ((𝑋‘𝑧)(._r‘𝑅) 0 ))
213	2, 170, 15	ringrz 20487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ Ring ∧ (𝑋‘𝑧) ∈ (Base‘𝑅)) → ((𝑋‘𝑧)(._r‘𝑅) 0 ) = 0 )
214	132, 127, 213	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑋‘𝑧)(._r‘𝑅) 0 ) = 0 )
215	214	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(._r‘𝑅) 0 ) = 0 )
216	212, 215	eqtrd 2795	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → ((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )) = 0 )
217	216	oveq2d 7424	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )(+_g‘𝑅)((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )(+_g‘𝑅) 0 ))
218		elun 4099	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (𝑥 ∪ {𝑧}) ↔ (𝑦 ∈ 𝑥 ∨ 𝑦 ∈ {𝑧}))
219		orcom 884	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ 𝑥 ∨ 𝑦 ∈ {𝑧}) ↔ (𝑦 ∈ {𝑧} ∨ 𝑦 ∈ 𝑥))
220	218, 219	bitri 278	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝑥 ∪ {𝑧}) ↔ (𝑦 ∈ {𝑧} ∨ 𝑦 ∈ 𝑥))
221		biorf 950	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑦 ∈ {𝑧} → (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ {𝑧} ∨ 𝑦 ∈ 𝑥)))
222	220, 221	bitr4id 293	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑦 ∈ {𝑧} → (𝑦 ∈ (𝑥 ∪ {𝑧}) ↔ 𝑦 ∈ 𝑥))
223	222	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → (𝑦 ∈ (𝑥 ∪ {𝑧}) ↔ 𝑦 ∈ 𝑥))
224	223	ifbid 4505	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ) = if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))
225	208, 217, 224	3eqtr4d 2805	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) ∧ ¬ 𝑦 ∈ {𝑧}) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )(+_g‘𝑅)((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))
226	204, 225	pm2.61dan 825	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) ∧ 𝑦 ∈ 𝐷) → (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )(+_g‘𝑅)((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 ))) = if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))
227	226	mpteq2dva 5197	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ (if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )(+_g‘𝑅)((𝑋‘𝑧)(._r‘𝑅)if(𝑦 = 𝑧, 1 , 0 )))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )))
228	167, 182, 227	3eqtrrd 2800	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )) = ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))(+_g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))))
229	141, 228	eqeq12d 2776	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )) ↔ ((𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))(+_g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 )))) = ((𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))(+_g‘𝑃)((𝑋‘𝑧) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑧, 1 , 0 ))))))
230	90, 229	imbitrrid 249	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) ∧ (𝑥 ∪ {𝑧}) ⊆ 𝐷)) → ((𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) → (𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))))
231	230	expr 462	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥)) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → ((𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )) → (𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )))))
232	231	a2d 30	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥)) → (((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )))))
233	89, 232	syl5 35	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥)) → ((𝑥 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 )))))
234	233	expcom 419	. . . . . . 7 ⊢ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) → (𝜑 → ((𝑥 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 ))) → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))))))
235	234	a2d 30	. . . . . 6 ⊢ ((𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥) → ((𝜑 → (𝑥 ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ 𝑥 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑥, (𝑋‘𝑦), 0 )))) → (𝜑 → ((𝑥 ∪ {𝑧}) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ (𝑥 ∪ {𝑧}) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑥 ∪ {𝑧}), (𝑋‘𝑦), 0 ))))))
236	50, 59, 68, 77, 85, 235	findcard2s 9159	. . . . 5 ⊢ ((𝑋 supp 0 ) ∈ Fin → (𝜑 → ((𝑋 supp 0 ) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )))))
237	34, 236	mpcom 39	. . . 4 ⊢ (𝜑 → ((𝑋 supp 0 ) ⊆ 𝐷 → (𝑃 Σ_g (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 ))))
238	28, 237	mpd 16	. . 3 ⊢ (𝜑 → (𝑃 Σ_g (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ (𝑋 supp 0 ), (𝑋‘𝑦), 0 )))
239	26, 238	eqtr4d 2798	. 2 ⊢ (𝜑 → 𝑋 = (𝑃 Σ_g (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
240	28	resmptd 6030	. . . 4 ⊢ (𝜑 → ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ↾ (𝑋 supp 0 )) = (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))))
241	240	oveq2d 7424	. . 3 ⊢ (𝜑 → (𝑃 Σ_g ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ↾ (𝑋 supp 0 ))) = (𝑃 Σ_g (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
242	115	fmpttd 7103	. . . 4 ⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))):𝐷⟶𝐵)
243	6, 11, 14, 17	suppssr 8190	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → (𝑋‘𝑘) = 0 )
244	243	oveq1d 7423	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = ( 0 · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))
245		eldifi 4077	. . . . . . 7 ⊢ (𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 )) → 𝑘 ∈ 𝐷)
246	105	fveq2d 6877	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (0_g‘𝑅) = (0_g‘(Scalar‘𝑃)))
247	15, 246	eqtrid 2807	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 0 = (0_g‘(Scalar‘𝑃)))
248	247	oveq1d 7423	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ( 0 · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = ((0_g‘(Scalar‘𝑃)) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))
249		eqid 2760	. . . . . . . . . 10 ⊢ (0_g‘(Scalar‘𝑃)) = (0_g‘(Scalar‘𝑃))
250	3, 111, 112, 249, 40	lmod0vs 21132	. . . . . . . . 9 ⊢ ((𝑃 ∈ LMod ∧ (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )) ∈ 𝐵) → ((0_g‘(Scalar‘𝑃)) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = (0_g‘𝑃))
251	102, 110, 250	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ((0_g‘(Scalar‘𝑃)) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = (0_g‘𝑃))
252	248, 251	eqtrd 2795	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ( 0 · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = (0_g‘𝑃))
253	245, 252	sylan2 605	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → ( 0 · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = (0_g‘𝑃))
254	244, 253	eqtrd 2795	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐷 ∖ (𝑋 supp 0 ))) → ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))) = (0_g‘𝑃))
255	254, 14	suppss2 8195	. . . 4 ⊢ (𝜑 → ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) supp (0_g‘𝑃)) ⊆ (𝑋 supp 0 ))
256	13	mptex 7217	. . . . . . 7 ⊢ (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∈ V
257		funmpt 6566	. . . . . . 7 ⊢ Fun (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))
258		fvex 6886	. . . . . . 7 ⊢ (0_g‘𝑃) ∈ V
259	256, 257, 258	3pm3.2i 1358	. . . . . 6 ⊢ ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∈ V ∧ Fun (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∧ (0_g‘𝑃) ∈ V)
260	259	a1i 11	. . . . 5 ⊢ (𝜑 → ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∈ V ∧ Fun (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ∧ (0_g‘𝑃) ∈ V))
261		suppssfifsupp 9350	. . . . 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‘𝑃))
262	260, 34, 255, 261	syl12anc 850	. . . 4 ⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) finSupp (0_g‘𝑃))
263	3, 40, 94, 14, 242, 255, 262	gsumres 20089	. . 3 ⊢ (𝜑 → (𝑃 Σ_g ((𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 )))) ↾ (𝑋 supp 0 ))) = (𝑃 Σ_g (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
264	241, 263	eqtr3d 2797	. 2 ⊢ (𝜑 → (𝑃 Σ_g (𝑘 ∈ (𝑋 supp 0 ) ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))) = (𝑃 Σ_g (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))
265	239, 264	eqtrd 2795	1 ⊢ (𝜑 → 𝑋 = (𝑃 Σ_g (𝑘 ∈ 𝐷 ↦ ((𝑋‘𝑘) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑘, 1 , 0 ))))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 {crab 3412 Vcvv 3450 ∖ cdif 3895 ∪ cun 3896 ⊆ wss 3898 ∅c0 4278 ifcif 4481 {csn 4583 class class class wbr 5102 ↦ cmpt 5185 × cxp 5645 ^◡ccnv 5646 ↾ cres 5649 “ cima 5650 Fun wfun 6521 ⟶wf 6523 ‘cfv 6527 (class class class)co 7408 ∘_f cof 7674 supp csupp 8155 ↑_m cmap 8825 Fincfn 8951 finSupp cfsupp 9331 ℕcn 12305 ℕ₀cn0 12576 Basecbs 17349 +_gcplusg 17390 ._rcmulr 17391 Scalarcsca 17393 ·_𝑠 cvsca 17394 0_gc0g 17572 Σ_g cgsu 17573 Grpcgrp 19106 CMndccmn 19956 1_rcur 20369 Ringcrg 20421 LModclmod 21097 mPwSer cmps 22174 mPoly cmpl 22176

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7734 ax-cnex 11228 ax-resscn 11229 ax-1cn 11230 ax-icn 11231 ax-addcl 11232 ax-addrcl 11233 ax-mulcl 11234 ax-mulrcl 11235 ax-mulcom 11236 ax-addass 11237 ax-mulass 11238 ax-distr 11239 ax-i2m1 11240 ax-1ne0 11241 ax-1rid 11242 ax-rnegex 11243 ax-rrecex 11244 ax-cnre 11245 ax-pre-lttri 11246 ax-pre-lttrn 11247 ax-pre-ltadd 11248 ax-pre-mulgt0 11249

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-tp 4588 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-se 5601 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6293 df-ord 6354 df-on 6355 df-lim 6356 df-suc 6357 df-iota 6483 df-fun 6529 df-fn 6530 df-f 6531 df-f1 6532 df-fo 6533 df-f1o 6534 df-fv 6535 df-isom 6536 df-riota 7365 df-ov 7411 df-oprab 7412 df-mpo 7413 df-of 7676 df-ofr 7677 df-om 7861 df-1st 7984 df-2nd 7985 df-supp 8156 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8454 df-2o 8455 df-er 8695 df-map 8827 df-pm 8828 df-ixp 8904 df-en 8952 df-dom 8953 df-sdom 8954 df-fin 8955 df-fsupp 9332 df-sup 9412 df-oi 9482 df-card 9992 df-pnf 11317 df-mnf 11318 df-xr 11319 df-ltxr 11320 df-le 11321 df-sub 11515 df-neg 11516 df-nn 12306 df-2 12375 df-3 12376 df-4 12377 df-5 12378 df-6 12379 df-7 12380 df-8 12381 df-9 12382 df-n0 12577 df-z 12664 df-dec 12785 df-uz 12936 df-fz 13610 df-fzo 13758 df-seq 14114 df-hash 14443 df-struct 17287 df-sets 17304 df-slot 17322 df-ndx 17334 df-base 17350 df-ress 17371 df-plusg 17403 df-mulr 17404 df-sca 17406 df-vsca 17407 df-ip 17408 df-tset 17409 df-ple 17410 df-ds 17412 df-hom 17414 df-cco 17415 df-0g 17574 df-gsum 17575 df-prds 17580 df-pws 17582 df-mre 17718 df-mrc 17719 df-acs 17721 df-mgm 18778 df-sgrp 18870 df-mnd 18886 df-mhm 18940 df-submnd 18941 df-grp 19109 df-minusg 19110 df-sbg 19111 df-mulg 19240 df-subg 19295 df-ghm 19390 df-cntz 19493 df-cmn 19958 df-abl 19959 df-mgp 20323 df-rng 20337 df-ur 20370 df-ring 20423 df-subrng 20760 df-subrg 20784 df-lmod 21099 df-lss 21169 df-psr 22179 df-mpl 22181

This theorem is used by: mplbas2 22313 mplcoe4 22342 ply1coe 22578

W3C validator