Theorem mplcoe1

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

	Ref	Expression
Hypotheses	mplcoe1.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mplcoe1.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
	mplcoe1.z	⊢ 0 = ( 0g ‘ 𝑅 )
	mplcoe1.o	⊢ 1 = ( 1r ‘ 𝑅 )
	mplcoe1.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	mplcoe1.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	mplcoe1.n	⊢ · = ( ·𝑠 ‘ 𝑃 )
	mplcoe1.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	mplcoe1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	mplcoe1	⊢ ( 𝜑 → 𝑋 = ( 𝑃 Σg ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mplcoe1.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		mplcoe1.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
3		mplcoe1.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		mplcoe1.o	⊢ 1 = ( 1r ‘ 𝑅 )
5		mplcoe1.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
6		mplcoe1.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
7		mplcoe1.n	⊢ · = ( ·𝑠 ‘ 𝑃 )
8		mplcoe1.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
9		mplcoe1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
10		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11	1 10 6 2 9	mplelf	⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
12	11	feqmptd	⊢ ( 𝜑 → 𝑋 = ( 𝑦 ∈ 𝐷 ↦ ( 𝑋 ‘ 𝑦 ) ) )
13		iftrue	⊢ ( 𝑦 ∈ ( 𝑋 supp 0 ) → if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) = ( 𝑋 ‘ 𝑦 ) )
14	13	adantl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝑋 supp 0 ) ) → if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) = ( 𝑋 ‘ 𝑦 ) )
15		eldif	⊢ ( 𝑦 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ↔ ( 𝑦 ∈ 𝐷 ∧ ¬ 𝑦 ∈ ( 𝑋 supp 0 ) ) )
16		ssidd	⊢ ( 𝜑 → ( 𝑋 supp 0 ) ⊆ ( 𝑋 supp 0 ) )
17		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
18	2 17	rabex2	⊢ 𝐷 ∈ V
19	18	a1i	⊢ ( 𝜑 → 𝐷 ∈ V )
20	3	fvexi	⊢ 0 ∈ V
21	20	a1i	⊢ ( 𝜑 → 0 ∈ V )
22	11 16 19 21	suppssr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ) → ( 𝑋 ‘ 𝑦 ) = 0 )
23	22	ifeq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ) → if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , ( 𝑋 ‘ 𝑦 ) ) = if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) )
24		ifid	⊢ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , ( 𝑋 ‘ 𝑦 ) ) = ( 𝑋 ‘ 𝑦 )
25	23 24	eqtr3di	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ) → if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) = ( 𝑋 ‘ 𝑦 ) )
26	15 25	sylan2br	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐷 ∧ ¬ 𝑦 ∈ ( 𝑋 supp 0 ) ) ) → if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) = ( 𝑋 ‘ 𝑦 ) )
27	26	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ ( 𝑋 supp 0 ) ) → if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) = ( 𝑋 ‘ 𝑦 ) )
28	14 27	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) = ( 𝑋 ‘ 𝑦 ) )
29	28	mpteq2dva	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑋 ‘ 𝑦 ) ) )
30	12 29	eqtr4d	⊢ ( 𝜑 → 𝑋 = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) )
31		suppssdm	⊢ ( 𝑋 supp 0 ) ⊆ dom 𝑋
32	31 11	fssdm	⊢ ( 𝜑 → ( 𝑋 supp 0 ) ⊆ 𝐷 )
33		eqid	⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
34		eqid	⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
35	1 33 34 3 6	mplelbas	⊢ ( 𝑋 ∈ 𝐵 ↔ ( 𝑋 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑋 finSupp 0 ) )
36	35	simprbi	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 finSupp 0 )
37	9 36	syl	⊢ ( 𝜑 → 𝑋 finSupp 0 )
38	37	fsuppimpd	⊢ ( 𝜑 → ( 𝑋 supp 0 ) ∈ Fin )
39		sseq1	⊢ ( 𝑤 = ∅ → ( 𝑤 ⊆ 𝐷 ↔ ∅ ⊆ 𝐷 ) )
40		mpteq1	⊢ ( 𝑤 = ∅ → ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) = ( 𝑘 ∈ ∅ ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) )
41		mpt0	⊢ ( 𝑘 ∈ ∅ ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) = ∅
42	40 41	eqtrdi	⊢ ( 𝑤 = ∅ → ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) = ∅ )
43	42	oveq2d	⊢ ( 𝑤 = ∅ → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑃 Σg ∅ ) )
44		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
45	44	gsum0	⊢ ( 𝑃 Σg ∅ ) = ( 0g ‘ 𝑃 )
46	43 45	eqtrdi	⊢ ( 𝑤 = ∅ → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 0g ‘ 𝑃 ) )
47		noel	⊢ ¬ 𝑦 ∈ ∅
48		eleq2	⊢ ( 𝑤 = ∅ → ( 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ ∅ ) )
49	47 48	mtbiri	⊢ ( 𝑤 = ∅ → ¬ 𝑦 ∈ 𝑤 )
50	49	iffalsed	⊢ ( 𝑤 = ∅ → if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) = 0 )
51	50	mpteq2dv	⊢ ( 𝑤 = ∅ → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ 0 ) )
52	46 51	eqeq12d	⊢ ( 𝑤 = ∅ → ( ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ↔ ( 0g ‘ 𝑃 ) = ( 𝑦 ∈ 𝐷 ↦ 0 ) ) )
53	39 52	imbi12d	⊢ ( 𝑤 = ∅ → ( ( 𝑤 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ↔ ( ∅ ⊆ 𝐷 → ( 0g ‘ 𝑃 ) = ( 𝑦 ∈ 𝐷 ↦ 0 ) ) ) )
54	53	imbi2d	⊢ ( 𝑤 = ∅ → ( ( 𝜑 → ( 𝑤 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) ↔ ( 𝜑 → ( ∅ ⊆ 𝐷 → ( 0g ‘ 𝑃 ) = ( 𝑦 ∈ 𝐷 ↦ 0 ) ) ) ) )
55		sseq1	⊢ ( 𝑤 = 𝑥 → ( 𝑤 ⊆ 𝐷 ↔ 𝑥 ⊆ 𝐷 ) )
56		mpteq1	⊢ ( 𝑤 = 𝑥 → ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) = ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) )
57	56	oveq2d	⊢ ( 𝑤 = 𝑥 → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )
58		eleq2	⊢ ( 𝑤 = 𝑥 → ( 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑥 ) )
59	58	ifbid	⊢ ( 𝑤 = 𝑥 → if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) = if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) )
60	59	mpteq2dv	⊢ ( 𝑤 = 𝑥 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) )
61	57 60	eqeq12d	⊢ ( 𝑤 = 𝑥 → ( ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ↔ ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) )
62	55 61	imbi12d	⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ↔ ( 𝑥 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) )
63	62	imbi2d	⊢ ( 𝑤 = 𝑥 → ( ( 𝜑 → ( 𝑤 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) ↔ ( 𝜑 → ( 𝑥 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) ) )
64		sseq1	⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( 𝑤 ⊆ 𝐷 ↔ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) )
65		mpteq1	⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) = ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) )
66	65	oveq2d	⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )
67		eleq2	⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) ) )
68	67	ifbid	⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) = if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) )
69	68	mpteq2dv	⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) )
70	66 69	eqeq12d	⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ↔ ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) )
71	64 70	imbi12d	⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( ( 𝑤 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ↔ ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) )
72	71	imbi2d	⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( ( 𝜑 → ( 𝑤 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) ↔ ( 𝜑 → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) ) )
73		sseq1	⊢ ( 𝑤 = ( 𝑋 supp 0 ) → ( 𝑤 ⊆ 𝐷 ↔ ( 𝑋 supp 0 ) ⊆ 𝐷 ) )
74		mpteq1	⊢ ( 𝑤 = ( 𝑋 supp 0 ) → ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) = ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) )
75	74	oveq2d	⊢ ( 𝑤 = ( 𝑋 supp 0 ) → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )
76		eleq2	⊢ ( 𝑤 = ( 𝑋 supp 0 ) → ( 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ ( 𝑋 supp 0 ) ) )
77	76	ifbid	⊢ ( 𝑤 = ( 𝑋 supp 0 ) → if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) = if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) )
78	77	mpteq2dv	⊢ ( 𝑤 = ( 𝑋 supp 0 ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) )
79	75 78	eqeq12d	⊢ ( 𝑤 = ( 𝑋 supp 0 ) → ( ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ↔ ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) )
80	73 79	imbi12d	⊢ ( 𝑤 = ( 𝑋 supp 0 ) → ( ( 𝑤 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ↔ ( ( 𝑋 supp 0 ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) )
81	80	imbi2d	⊢ ( 𝑤 = ( 𝑋 supp 0 ) → ( ( 𝜑 → ( 𝑤 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑤 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) ↔ ( 𝜑 → ( ( 𝑋 supp 0 ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) ) )
82		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
83	8 82	syl	⊢ ( 𝜑 → 𝑅 ∈ Grp )
84	1 2 3 44 5 83	mpl0	⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) = ( 𝐷 × { 0 } ) )
85		fconstmpt	⊢ ( 𝐷 × { 0 } ) = ( 𝑦 ∈ 𝐷 ↦ 0 )
86	84 85	eqtrdi	⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) = ( 𝑦 ∈ 𝐷 ↦ 0 ) )
87	86	a1d	⊢ ( 𝜑 → ( ∅ ⊆ 𝐷 → ( 0g ‘ 𝑃 ) = ( 𝑦 ∈ 𝐷 ↦ 0 ) ) )
88		ssun1	⊢ 𝑥 ⊆ ( 𝑥 ∪ { 𝑧 } )
89		sstr2	⊢ ( 𝑥 ⊆ ( 𝑥 ∪ { 𝑧 } ) → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → 𝑥 ⊆ 𝐷 ) )
90	88 89	ax-mp	⊢ ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → 𝑥 ⊆ 𝐷 )
91	90	imim1i	⊢ ( ( 𝑥 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) )
92		oveq1	⊢ ( ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) → ( ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) ( +g ‘ 𝑃 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) = ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ( +g ‘ 𝑃 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) )
93		eqid	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
94	1	mplring	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ Ring )
95	5 8 94	syl2anc	⊢ ( 𝜑 → 𝑃 ∈ Ring )
96		ringcmn	⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ CMnd )
97	95 96	syl	⊢ ( 𝜑 → 𝑃 ∈ CMnd )
98	97	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑃 ∈ CMnd )
99		simprll	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑥 ∈ Fin )
100		simprr	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 )
101	100	unssad	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑥 ⊆ 𝐷 )
102	101	sselda	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝑘 ∈ 𝐷 )
103	5	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝐼 ∈ 𝑊 )
104	8	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑅 ∈ Ring )
105	1	mpllmod	⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ LMod )
106	103 104 105	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑃 ∈ LMod )
107	11	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑋 ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
108	1 5 8	mplsca	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
109	108	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
110	109	fveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
111	107 110	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑋 ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
112		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑘 ∈ 𝐷 )
113	1 6 3 4 2 103 104 112	mplmon	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ∈ 𝐵 )
114		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
115		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
116	6 114 7 115	lmodvscl	⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝑋 ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ∈ 𝐵 ) → ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ∈ 𝐵 )
117	106 111 113 116	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ∈ 𝐵 )
118	117	adantlr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑘 ∈ 𝐷 ) → ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ∈ 𝐵 )
119	102 118	syldan	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑘 ∈ 𝑥 ) → ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ∈ 𝐵 )
120		vex	⊢ 𝑧 ∈ V
121	120	a1i	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑧 ∈ V )
122		simprlr	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ¬ 𝑧 ∈ 𝑥 )
123	5 8 105	syl2anc	⊢ ( 𝜑 → 𝑃 ∈ LMod )
124	123	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑃 ∈ LMod )
125	11	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
126	100	unssbd	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → { 𝑧 } ⊆ 𝐷 )
127	120	snss	⊢ ( 𝑧 ∈ 𝐷 ↔ { 𝑧 } ⊆ 𝐷 )
128	126 127	sylibr	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑧 ∈ 𝐷 )
129	125 128	ffvelrnd	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) )
130	108	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
131	130	fveq2d	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
132	129 131	eleqtrd	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
133	5	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝐼 ∈ 𝑊 )
134	8	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑅 ∈ Ring )
135	1 6 3 4 2 133 134 128	mplmon	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ∈ 𝐵 )
136	6 114 7 115	lmodvscl	⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ∈ 𝐵 ) → ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ∈ 𝐵 )
137	124 132 135 136	syl3anc	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ∈ 𝐵 )
138		fveq2	⊢ ( 𝑘 = 𝑧 → ( 𝑋 ‘ 𝑘 ) = ( 𝑋 ‘ 𝑧 ) )
139		equequ2	⊢ ( 𝑘 = 𝑧 → ( 𝑦 = 𝑘 ↔ 𝑦 = 𝑧 ) )
140	139	ifbid	⊢ ( 𝑘 = 𝑧 → if ( 𝑦 = 𝑘 , 1 , 0 ) = if ( 𝑦 = 𝑧 , 1 , 0 ) )
141	140	mpteq2dv	⊢ ( 𝑘 = 𝑧 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) )
142	138 141	oveq12d	⊢ ( 𝑘 = 𝑧 → ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) )
143	6 93 98 99 119 121 122 137 142	gsumunsn	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) ( +g ‘ 𝑃 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) )
144		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
145	125	ffvelrnda	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → ( 𝑋 ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
146	10 3	ring0cl	⊢ ( 𝑅 ∈ Ring → 0 ∈ ( Base ‘ 𝑅 ) )
147	8 146	syl	⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝑅 ) )
148	147	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → 0 ∈ ( Base ‘ 𝑅 ) )
149	145 148	ifcld	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ∈ ( Base ‘ 𝑅 ) )
150	149	fmpttd	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
151		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
152	151 18	elmap	⊢ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) ↔ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
153	150 152	sylibr	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
154	33 10 2 34 133	psrbas	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
155	153 154	eleqtrrd	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
156	18	mptex	⊢ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ V
157		funmpt	⊢ Fun ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) )
158	156 157 20	3pm3.2i	⊢ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ V ∧ Fun ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∧ 0 ∈ V )
159	158	a1i	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ V ∧ Fun ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∧ 0 ∈ V ) )
160		eldifn	⊢ ( 𝑦 ∈ ( 𝐷 ∖ 𝑥 ) → ¬ 𝑦 ∈ 𝑥 )
161	160	adantl	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ 𝑥 ) ) → ¬ 𝑦 ∈ 𝑥 )
162	161	iffalsed	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ ( 𝐷 ∖ 𝑥 ) ) → if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) = 0 )
163	18	a1i	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝐷 ∈ V )
164	162 163	suppss2	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) supp 0 ) ⊆ 𝑥 )
165		suppssfifsupp	⊢ ( ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ V ∧ Fun ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∧ 0 ∈ V ) ∧ ( 𝑥 ∈ Fin ∧ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) supp 0 ) ⊆ 𝑥 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) finSupp 0 )
166	159 99 164 165	syl12anc	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) finSupp 0 )
167	1 33 34 3 6	mplelbas	⊢ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ 𝐵 ↔ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) finSupp 0 ) )
168	155 166 167	sylanbrc	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∈ 𝐵 )
169	1 6 144 93 168 137	mpladd	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ( +g ‘ 𝑃 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) = ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∘f ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) )
170		ovexd	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ∈ V )
171		eqidd	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) )
172		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
173	1 7 10 6 172 2 129 135	mplvsca	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = ( ( 𝐷 × { ( 𝑋 ‘ 𝑧 ) } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) )
174	129	adantr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) )
175	10 4	ringidcl	⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
176	175 146	ifcld	⊢ ( 𝑅 ∈ Ring → if ( 𝑦 = 𝑧 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
177	8 176	syl	⊢ ( 𝜑 → if ( 𝑦 = 𝑧 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
178	177	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → if ( 𝑦 = 𝑧 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
179		fconstmpt	⊢ ( 𝐷 × { ( 𝑋 ‘ 𝑧 ) } ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑋 ‘ 𝑧 ) )
180	179	a1i	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝐷 × { ( 𝑋 ‘ 𝑧 ) } ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑋 ‘ 𝑧 ) ) )
181		eqidd	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) )
182	163 174 178 180 181	offval2	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝐷 × { ( 𝑋 ‘ 𝑧 ) } ) ∘f ( .r ‘ 𝑅 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) )
183	173 182	eqtrd	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) )
184	163 149 170 171 183	offval2	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ∘f ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) )
185	134 82	syl	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → 𝑅 ∈ Grp )
186	10 144 3	grplid	⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) ) → ( 0 ( +g ‘ 𝑅 ) ( 𝑋 ‘ 𝑧 ) ) = ( 𝑋 ‘ 𝑧 ) )
187	185 129 186	syl2anc	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 0 ( +g ‘ 𝑅 ) ( 𝑋 ‘ 𝑧 ) ) = ( 𝑋 ‘ 𝑧 ) )
188	187	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( 0 ( +g ‘ 𝑅 ) ( 𝑋 ‘ 𝑧 ) ) = ( 𝑋 ‘ 𝑧 ) )
189		simpr	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → 𝑦 ∈ { 𝑧 } )
190		velsn	⊢ ( 𝑦 ∈ { 𝑧 } ↔ 𝑦 = 𝑧 )
191	189 190	sylib	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → 𝑦 = 𝑧 )
192	191	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( 𝑋 ‘ 𝑦 ) = ( 𝑋 ‘ 𝑧 ) )
193	188 192	eqtr4d	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( 0 ( +g ‘ 𝑅 ) ( 𝑋 ‘ 𝑧 ) ) = ( 𝑋 ‘ 𝑦 ) )
194	122	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ¬ 𝑧 ∈ 𝑥 )
195	191 194	eqneltrd	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ¬ 𝑦 ∈ 𝑥 )
196	195	iffalsed	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) = 0 )
197	191	iftrued	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → if ( 𝑦 = 𝑧 , 1 , 0 ) = 1 )
198	197	oveq2d	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) = ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 1 ) )
199	10 172 4	ringridm	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 1 ) = ( 𝑋 ‘ 𝑧 ) )
200	134 129 199	syl2anc	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 1 ) = ( 𝑋 ‘ 𝑧 ) )
201	200	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 1 ) = ( 𝑋 ‘ 𝑧 ) )
202	198 201	eqtrd	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) = ( 𝑋 ‘ 𝑧 ) )
203	196 202	oveq12d	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = ( 0 ( +g ‘ 𝑅 ) ( 𝑋 ‘ 𝑧 ) ) )
204		elun2	⊢ ( 𝑦 ∈ { 𝑧 } → 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) )
205	204	adantl	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) )
206	205	iftrued	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) = ( 𝑋 ‘ 𝑦 ) )
207	193 203 206	3eqtr4d	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ { 𝑧 } ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) )
208	83	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → 𝑅 ∈ Grp )
209	10 144 3	grprid	⊢ ( ( 𝑅 ∈ Grp ∧ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ∈ ( Base ‘ 𝑅 ) ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) 0 ) = if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) )
210	208 149 209	syl2anc	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) 0 ) = if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) )
211	210	adantr	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) 0 ) = if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) )
212		simpr	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ¬ 𝑦 ∈ { 𝑧 } )
213	212 190	sylnib	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ¬ 𝑦 = 𝑧 )
214	213	iffalsed	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → if ( 𝑦 = 𝑧 , 1 , 0 ) = 0 )
215	214	oveq2d	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) = ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 0 ) )
216	10 172 3	ringrz	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 0 ) = 0 )
217	134 129 216	syl2anc	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 0 ) = 0 )
218	217	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) 0 ) = 0 )
219	215 218	eqtrd	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) = 0 )
220	219	oveq2d	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) 0 ) )
221		elun	⊢ ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) ↔ ( 𝑦 ∈ 𝑥 ∨ 𝑦 ∈ { 𝑧 } ) )
222		orcom	⊢ ( ( 𝑦 ∈ 𝑥 ∨ 𝑦 ∈ { 𝑧 } ) ↔ ( 𝑦 ∈ { 𝑧 } ∨ 𝑦 ∈ 𝑥 ) )
223	221 222	bitri	⊢ ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) ↔ ( 𝑦 ∈ { 𝑧 } ∨ 𝑦 ∈ 𝑥 ) )
224		biorf	⊢ ( ¬ 𝑦 ∈ { 𝑧 } → ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ { 𝑧 } ∨ 𝑦 ∈ 𝑥 ) ) )
225	223 224	bitr4id	⊢ ( ¬ 𝑦 ∈ { 𝑧 } → ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) ↔ 𝑦 ∈ 𝑥 ) )
226	225	adantl	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) ↔ 𝑦 ∈ 𝑥 ) )
227	226	ifbid	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) = if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) )
228	211 220 227	3eqtr4d	⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ ¬ 𝑦 ∈ { 𝑧 } ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) )
229	207 228	pm2.61dan	⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) ∧ 𝑦 ∈ 𝐷 ) → ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) = if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) )
230	229	mpteq2dva	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ ( if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ( +g ‘ 𝑅 ) ( ( 𝑋 ‘ 𝑧 ) ( .r ‘ 𝑅 ) if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) )
231	169 184 230	3eqtrrd	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) = ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ( +g ‘ 𝑃 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) )
232	143 231	eqeq12d	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ↔ ( ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) ( +g ‘ 𝑃 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) = ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ( +g ‘ 𝑃 ) ( ( 𝑋 ‘ 𝑧 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑧 , 1 , 0 ) ) ) ) ) )
233	92 232	syl5ibr	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 ) ) → ( ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) )
234	233	expr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ) → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → ( ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) )
235	234	a2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ) → ( ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) )
236	91 235	syl5	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ) → ( ( 𝑥 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) )
237	236	expcom	⊢ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) → ( 𝜑 → ( ( 𝑥 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) ) )
238	237	a2d	⊢ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) → ( ( 𝜑 → ( 𝑥 ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ 𝑥 , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) → ( 𝜑 → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) ) )
239	54 63 72 81 87 238	findcard2s	⊢ ( ( 𝑋 supp 0 ) ∈ Fin → ( 𝜑 → ( ( 𝑋 supp 0 ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) ) )
240	38 239	mpcom	⊢ ( 𝜑 → ( ( 𝑋 supp 0 ) ⊆ 𝐷 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) ) )
241	32 240	mpd	⊢ ( 𝜑 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 ∈ ( 𝑋 supp 0 ) , ( 𝑋 ‘ 𝑦 ) , 0 ) ) )
242	30 241	eqtr4d	⊢ ( 𝜑 → 𝑋 = ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )
243	32	resmptd	⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ↾ ( 𝑋 supp 0 ) ) = ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) )
244	243	oveq2d	⊢ ( 𝜑 → ( 𝑃 Σg ( ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ↾ ( 𝑋 supp 0 ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )
245	117	fmpttd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) : 𝐷 ⟶ 𝐵 )
246	11 16 19 21	suppssr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ) → ( 𝑋 ‘ 𝑘 ) = 0 )
247	246	oveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ) → ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( 0 · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) )
248		eldifi	⊢ ( 𝑘 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) → 𝑘 ∈ 𝐷 )
249	109	fveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
250	3 249	eqtrid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 0 = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
251	250	oveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 0 · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) )
252		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑃 ) ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) )
253	6 114 7 252 44	lmod0vs	⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ∈ 𝐵 ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( 0g ‘ 𝑃 ) )
254	106 113 253	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( 0g ‘ 𝑃 ) )
255	251 254	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 0 · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( 0g ‘ 𝑃 ) )
256	248 255	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ) → ( 0 · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( 0g ‘ 𝑃 ) )
257	247 256	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ) → ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) = ( 0g ‘ 𝑃 ) )
258	257 19	suppss2	⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) supp ( 0g ‘ 𝑃 ) ) ⊆ ( 𝑋 supp 0 ) )
259	18	mptex	⊢ ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ∈ V
260		funmpt	⊢ Fun ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) )
261		fvex	⊢ ( 0g ‘ 𝑃 ) ∈ V
262	259 260 261	3pm3.2i	⊢ ( ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ∧ ( 0g ‘ 𝑃 ) ∈ V )
263	262	a1i	⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ∧ ( 0g ‘ 𝑃 ) ∈ V ) )
264		suppssfifsupp	⊢ ( ( ( ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ∧ ( 0g ‘ 𝑃 ) ∈ V ) ∧ ( ( 𝑋 supp 0 ) ∈ Fin ∧ ( ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) supp ( 0g ‘ 𝑃 ) ) ⊆ ( 𝑋 supp 0 ) ) ) → ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) finSupp ( 0g ‘ 𝑃 ) )
265	263 38 258 264	syl12anc	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) finSupp ( 0g ‘ 𝑃 ) )
266	6 44 97 19 245 258 265	gsumres	⊢ ( 𝜑 → ( 𝑃 Σg ( ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ↾ ( 𝑋 supp 0 ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )
267	244 266	eqtr3d	⊢ ( 𝜑 → ( 𝑃 Σg ( 𝑘 ∈ ( 𝑋 supp 0 ) ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )
268	242 267	eqtrd	⊢ ( 𝜑 → 𝑋 = ( 𝑃 Σg ( 𝑘 ∈ 𝐷 ↦ ( ( 𝑋 ‘ 𝑘 ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑘 , 1 , 0 ) ) ) ) ) )