Theorem mplmonmul

Description: The product of two monomials adds the exponent vectors together. For example, the product of ( x ^ 2 ) ( y ^ 2 ) with ( y ^ 1 ) ( z ^ 3 ) is ( x ^ 2 ) ( y ^ 3 ) ( z ^ 3 ) , where the exponent vectors <. 2 , 2 , 0 >. and <. 0 , 1 , 3 >. are added to give <. 2 , 3 , 3 >. . (Contributed by Mario Carneiro, 9-Jan-2015)

	Ref	Expression
Hypotheses	mplmon.s	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mplmon.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	mplmon.z	⊢ 0 = ( 0g ‘ 𝑅 )
	mplmon.o	⊢ 1 = ( 1r ‘ 𝑅 )
	mplmon.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
	mplmon.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	mplmon.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	mplmon.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
	mplmonmul.t	⊢ · = ( .r ‘ 𝑃 )
	mplmonmul.x	⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
Assertion	mplmonmul	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mplmon.s	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		mplmon.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		mplmon.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		mplmon.o	⊢ 1 = ( 1r ‘ 𝑅 )
5		mplmon.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
6		mplmon.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
7		mplmon.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
8		mplmon.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
9		mplmonmul.t	⊢ · = ( .r ‘ 𝑃 )
10		mplmonmul.x	⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
11		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
12	1 2 3 4 5 6 7 8	mplmon	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ∈ 𝐵 )
13	1 2 3 4 5 6 7 10	mplmon	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ∈ 𝐵 )
14	1 2 11 9 5 12 13	mplmul	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ) ) )
15		eqeq1	⊢ ( 𝑦 = 𝑘 → ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) ↔ 𝑘 = ( 𝑋 ∘f + 𝑌 ) ) )
16	15	ifbid	⊢ ( 𝑦 = 𝑘 → if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) = if ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) )
17	16	cbvmptv	⊢ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) ) = ( 𝑘 ∈ 𝐷 ↦ if ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) )
18		simpr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } )
19	18	snssd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → { 𝑋 } ⊆ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } )
20	19	resmptd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ↾ { 𝑋 } ) = ( 𝑗 ∈ { 𝑋 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) )
21	20	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑅 Σg ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ↾ { 𝑋 } ) ) = ( 𝑅 Σg ( 𝑗 ∈ { 𝑋 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ) )
22	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑅 ∈ Ring )
23		ringmnd	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
24	22 23	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑅 ∈ Mnd )
25	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑋 ∈ 𝐷 )
26		iftrue	⊢ ( 𝑦 = 𝑋 → if ( 𝑦 = 𝑋 , 1 , 0 ) = 1 )
27		eqid	⊢ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) )
28	4	fvexi	⊢ 1 ∈ V
29	26 27 28	fvmpt	⊢ ( 𝑋 ∈ 𝐷 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑋 ) = 1 )
30	25 29	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑋 ) = 1 )
31		ssrab2	⊢ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ⊆ 𝐷
32		simplr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑘 ∈ 𝐷 )
33		eqid	⊢ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } = { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 }
34	5 33	psrbagconcl	⊢ ( ( 𝑘 ∈ 𝐷 ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑋 ) ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } )
35	32 18 34	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑋 ) ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } )
36	31 35	sselid	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑋 ) ∈ 𝐷 )
37		eqeq1	⊢ ( 𝑦 = ( 𝑘 ∘f − 𝑋 ) → ( 𝑦 = 𝑌 ↔ ( 𝑘 ∘f − 𝑋 ) = 𝑌 ) )
38	37	ifbid	⊢ ( 𝑦 = ( 𝑘 ∘f − 𝑋 ) → if ( 𝑦 = 𝑌 , 1 , 0 ) = if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) )
39		eqid	⊢ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) )
40	3	fvexi	⊢ 0 ∈ V
41	28 40	ifex	⊢ if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) ∈ V
42	38 39 41	fvmpt	⊢ ( ( 𝑘 ∘f − 𝑋 ) ∈ 𝐷 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑋 ) ) = if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) )
43	36 42	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑋 ) ) = if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) )
44	30 43	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑋 ) ) ) = ( 1 ( .r ‘ 𝑅 ) if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) ) )
45		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
46	45 4	ringidcl	⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
47	45 3	ring0cl	⊢ ( 𝑅 ∈ Ring → 0 ∈ ( Base ‘ 𝑅 ) )
48	46 47	ifcld	⊢ ( 𝑅 ∈ Ring → if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
49	22 48	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
50	45 11 4	ringlidm	⊢ ( ( 𝑅 ∈ Ring ∧ if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) ) → ( 1 ( .r ‘ 𝑅 ) if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) ) = if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) )
51	22 49 50	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 1 ( .r ‘ 𝑅 ) if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) ) = if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) )
52	5	psrbagf	⊢ ( 𝑘 ∈ 𝐷 → 𝑘 : 𝐼 ⟶ ℕ0 )
53	32 52	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑘 : 𝐼 ⟶ ℕ0 )
54	53	ffvelcdmda	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑘 ‘ 𝑧 ) ∈ ℕ0 )
55	8	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑋 ∈ 𝐷 )
56	5	psrbagf	⊢ ( 𝑋 ∈ 𝐷 → 𝑋 : 𝐼 ⟶ ℕ0 )
57	55 56	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑋 : 𝐼 ⟶ ℕ0 )
58	57	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑧 ) ∈ ℕ0 )
59	58	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑧 ) ∈ ℕ0 )
60	5	psrbagf	⊢ ( 𝑌 ∈ 𝐷 → 𝑌 : 𝐼 ⟶ ℕ0 )
61	10 60	syl	⊢ ( 𝜑 → 𝑌 : 𝐼 ⟶ ℕ0 )
62	61	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑌 : 𝐼 ⟶ ℕ0 )
63	62	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑌 ‘ 𝑧 ) ∈ ℕ0 )
64	63	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑌 ‘ 𝑧 ) ∈ ℕ0 )
65		nn0cn	⊢ ( ( 𝑘 ‘ 𝑧 ) ∈ ℕ0 → ( 𝑘 ‘ 𝑧 ) ∈ ℂ )
66		nn0cn	⊢ ( ( 𝑋 ‘ 𝑧 ) ∈ ℕ0 → ( 𝑋 ‘ 𝑧 ) ∈ ℂ )
67		nn0cn	⊢ ( ( 𝑌 ‘ 𝑧 ) ∈ ℕ0 → ( 𝑌 ‘ 𝑧 ) ∈ ℂ )
68		subadd	⊢ ( ( ( 𝑘 ‘ 𝑧 ) ∈ ℂ ∧ ( 𝑋 ‘ 𝑧 ) ∈ ℂ ∧ ( 𝑌 ‘ 𝑧 ) ∈ ℂ ) → ( ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) = ( 𝑌 ‘ 𝑧 ) ↔ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) = ( 𝑘 ‘ 𝑧 ) ) )
69	65 66 67 68	syl3an	⊢ ( ( ( 𝑘 ‘ 𝑧 ) ∈ ℕ0 ∧ ( 𝑋 ‘ 𝑧 ) ∈ ℕ0 ∧ ( 𝑌 ‘ 𝑧 ) ∈ ℕ0 ) → ( ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) = ( 𝑌 ‘ 𝑧 ) ↔ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) = ( 𝑘 ‘ 𝑧 ) ) )
70	54 59 64 69	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) ∧ 𝑧 ∈ 𝐼 ) → ( ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) = ( 𝑌 ‘ 𝑧 ) ↔ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) = ( 𝑘 ‘ 𝑧 ) ) )
71		eqcom	⊢ ( ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) = ( 𝑘 ‘ 𝑧 ) ↔ ( 𝑘 ‘ 𝑧 ) = ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) )
72	70 71	bitrdi	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) ∧ 𝑧 ∈ 𝐼 ) → ( ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) = ( 𝑌 ‘ 𝑧 ) ↔ ( 𝑘 ‘ 𝑧 ) = ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ) )
73	72	ralbidva	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ∀ 𝑧 ∈ 𝐼 ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) = ( 𝑌 ‘ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝐼 ( 𝑘 ‘ 𝑧 ) = ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ) )
74		mpteqb	⊢ ( ∀ 𝑧 ∈ 𝐼 ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ∈ V → ( ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝐼 ↦ ( 𝑌 ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐼 ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) = ( 𝑌 ‘ 𝑧 ) ) )
75		ovexd	⊢ ( 𝑧 ∈ 𝐼 → ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ∈ V )
76	74 75	mprg	⊢ ( ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝐼 ↦ ( 𝑌 ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐼 ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) = ( 𝑌 ‘ 𝑧 ) )
77		mpteqb	⊢ ( ∀ 𝑧 ∈ 𝐼 ( 𝑘 ‘ 𝑧 ) ∈ V → ( ( 𝑧 ∈ 𝐼 ↦ ( 𝑘 ‘ 𝑧 ) ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ) ↔ ∀ 𝑧 ∈ 𝐼 ( 𝑘 ‘ 𝑧 ) = ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ) )
78		fvexd	⊢ ( 𝑧 ∈ 𝐼 → ( 𝑘 ‘ 𝑧 ) ∈ V )
79	77 78	mprg	⊢ ( ( 𝑧 ∈ 𝐼 ↦ ( 𝑘 ‘ 𝑧 ) ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ) ↔ ∀ 𝑧 ∈ 𝐼 ( 𝑘 ‘ 𝑧 ) = ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) )
80	73 76 79	3bitr4g	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝐼 ↦ ( 𝑌 ‘ 𝑧 ) ) ↔ ( 𝑧 ∈ 𝐼 ↦ ( 𝑘 ‘ 𝑧 ) ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ) ) )
81	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝐼 ∈ 𝑊 )
82	53	feqmptd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑘 = ( 𝑧 ∈ 𝐼 ↦ ( 𝑘 ‘ 𝑧 ) ) )
83	57	feqmptd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑋 = ( 𝑧 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑧 ) ) )
84	83	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑋 = ( 𝑧 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑧 ) ) )
85	81 54 59 82 84	offval2	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑋 ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ) )
86	62	feqmptd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑌 = ( 𝑧 ∈ 𝐼 ↦ ( 𝑌 ‘ 𝑧 ) ) )
87	86	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑌 = ( 𝑧 ∈ 𝐼 ↦ ( 𝑌 ‘ 𝑧 ) ) )
88	85 87	eqeq12d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 ↔ ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝐼 ↦ ( 𝑌 ‘ 𝑧 ) ) ) )
89	6	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝐼 ∈ 𝑊 )
90	89 58 63 83 86	offval2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑋 ∘f + 𝑌 ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ) )
91	90	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑋 ∘f + 𝑌 ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ) )
92	82 91	eqeq12d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) ↔ ( 𝑧 ∈ 𝐼 ↦ ( 𝑘 ‘ 𝑧 ) ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ) ) )
93	80 88 92	3bitr4d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 ↔ 𝑘 = ( 𝑋 ∘f + 𝑌 ) ) )
94	93	ifbid	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → if ( ( 𝑘 ∘f − 𝑋 ) = 𝑌 , 1 , 0 ) = if ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) )
95	44 51 94	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑋 ) ) ) = if ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) )
96	94 49	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → if ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
97	95 96	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑋 ) ) ) ∈ ( Base ‘ 𝑅 ) )
98		fveq2	⊢ ( 𝑗 = 𝑋 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) = ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑋 ) )
99		oveq2	⊢ ( 𝑗 = 𝑋 → ( 𝑘 ∘f − 𝑗 ) = ( 𝑘 ∘f − 𝑋 ) )
100	99	fveq2d	⊢ ( 𝑗 = 𝑋 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) = ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑋 ) ) )
101	98 100	oveq12d	⊢ ( 𝑗 = 𝑋 → ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) = ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑋 ) ) ) )
102	45 101	gsumsn	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑋 ∈ 𝐷 ∧ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑋 ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑅 Σg ( 𝑗 ∈ { 𝑋 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ) = ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑋 ) ) ) )
103	24 25 97 102	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑅 Σg ( 𝑗 ∈ { 𝑋 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ) = ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑋 ) ) ) )
104	21 103 95	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑅 Σg ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ↾ { 𝑋 } ) ) = if ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) )
105	3	gsum0	⊢ ( 𝑅 Σg ∅ ) = 0
106		disjsn	⊢ ( ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∩ { 𝑋 } ) = ∅ ↔ ¬ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } )
107	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑅 ∈ Ring )
108	1 45 2 5 12	mplelf	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
109	108	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
110		simpr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } )
111	31 110	sselid	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑗 ∈ 𝐷 )
112	109 111	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
113	1 45 2 5 13	mplelf	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
114	113	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
115		simplr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → 𝑘 ∈ 𝐷 )
116	5 33	psrbagconcl	⊢ ( ( 𝑘 ∈ 𝐷 ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑗 ) ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } )
117	115 110 116	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑗 ) ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } )
118	31 117	sselid	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑗 ) ∈ 𝐷 )
119	114 118	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) )
120	45 11	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ∈ ( Base ‘ 𝑅 ) )
121	107 112 119 120	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ∈ ( Base ‘ 𝑅 ) )
122	121	fmpttd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) : { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ⟶ ( Base ‘ 𝑅 ) )
123		ffn	⊢ ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) : { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ⟶ ( Base ‘ 𝑅 ) → ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) Fn { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } )
124		fnresdisj	⊢ ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) Fn { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } → ( ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∩ { 𝑋 } ) = ∅ ↔ ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ↾ { 𝑋 } ) = ∅ ) )
125	122 123 124	3syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∩ { 𝑋 } ) = ∅ ↔ ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ↾ { 𝑋 } ) = ∅ ) )
126	125	biimpa	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∩ { 𝑋 } ) = ∅ ) → ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ↾ { 𝑋 } ) = ∅ )
127	106 126	sylan2br	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ ¬ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ↾ { 𝑋 } ) = ∅ )
128	127	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ ¬ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑅 Σg ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ↾ { 𝑋 } ) ) = ( 𝑅 Σg ∅ ) )
129		breq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∘r ≤ ( 𝑋 ∘f + 𝑌 ) ↔ 𝑋 ∘r ≤ ( 𝑋 ∘f + 𝑌 ) ) )
130	58	nn0red	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑧 ) ∈ ℝ )
131		nn0addge1	⊢ ( ( ( 𝑋 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝑌 ‘ 𝑧 ) ∈ ℕ0 ) → ( 𝑋 ‘ 𝑧 ) ≤ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) )
132	130 63 131	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑧 ) ≤ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) )
133	132	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ∀ 𝑧 ∈ 𝐼 ( 𝑋 ‘ 𝑧 ) ≤ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) )
134		ovexd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ∈ V )
135	89 58 134 83 90	ofrfval2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑋 ∘r ≤ ( 𝑋 ∘f + 𝑌 ) ↔ ∀ 𝑧 ∈ 𝐼 ( 𝑋 ‘ 𝑧 ) ≤ ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ) )
136	133 135	mpbird	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑋 ∘r ≤ ( 𝑋 ∘f + 𝑌 ) )
137	129 55 136	elrabd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝑋 ∘f + 𝑌 ) } )
138		breq2	⊢ ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) → ( 𝑥 ∘r ≤ 𝑘 ↔ 𝑥 ∘r ≤ ( 𝑋 ∘f + 𝑌 ) ) )
139	138	rabbidv	⊢ ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) → { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } = { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝑋 ∘f + 𝑌 ) } )
140	139	eleq2d	⊢ ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) → ( 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↔ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝑋 ∘f + 𝑌 ) } ) )
141	137 140	syl5ibrcom	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) → 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) )
142	141	con3dimp	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ ¬ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ¬ 𝑘 = ( 𝑋 ∘f + 𝑌 ) )
143	142	iffalsed	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ ¬ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → if ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) = 0 )
144	105 128 143	3eqtr4a	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ ¬ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 𝑅 Σg ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ↾ { 𝑋 } ) ) = if ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) )
145	104 144	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑅 Σg ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ↾ { 𝑋 } ) ) = if ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) )
146	7	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑅 ∈ Ring )
147		ringcmn	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
148	146 147	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝑅 ∈ CMnd )
149	5	psrbaglefi	⊢ ( 𝑘 ∈ 𝐷 → { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∈ Fin )
150	149	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∈ Fin )
151		ssdif	⊢ ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ⊆ 𝐷 → ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∖ { 𝑋 } ) ⊆ ( 𝐷 ∖ { 𝑋 } ) )
152	31 151	ax-mp	⊢ ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∖ { 𝑋 } ) ⊆ ( 𝐷 ∖ { 𝑋 } )
153	152	sseli	⊢ ( 𝑗 ∈ ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∖ { 𝑋 } ) → 𝑗 ∈ ( 𝐷 ∖ { 𝑋 } ) )
154	108	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
155		eldifsni	⊢ ( 𝑦 ∈ ( 𝐷 ∖ { 𝑋 } ) → 𝑦 ≠ 𝑋 )
156	155	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐷 ∖ { 𝑋 } ) ) → 𝑦 ≠ 𝑋 )
157	156	neneqd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐷 ∖ { 𝑋 } ) ) → ¬ 𝑦 = 𝑋 )
158	157	iffalsed	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑦 ∈ ( 𝐷 ∖ { 𝑋 } ) ) → if ( 𝑦 = 𝑋 , 1 , 0 ) = 0 )
159		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
160	5 159	rabex2	⊢ 𝐷 ∈ V
161	160	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 𝐷 ∈ V )
162	158 161	suppss2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) supp 0 ) ⊆ { 𝑋 } )
163	40	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → 0 ∈ V )
164	154 162 161 163	suppssr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ ( 𝐷 ∖ { 𝑋 } ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) = 0 )
165	153 164	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∖ { 𝑋 } ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) = 0 )
166	165	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∖ { 𝑋 } ) ) → ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) = ( 0 ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) )
167		eldifi	⊢ ( 𝑗 ∈ ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∖ { 𝑋 } ) → 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } )
168	45 11 3	ringlz	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( 0 ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) = 0 )
169	107 119 168	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ) → ( 0 ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) = 0 )
170	167 169	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∖ { 𝑋 } ) ) → ( 0 ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) = 0 )
171	166 170	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) ∧ 𝑗 ∈ ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∖ { 𝑋 } ) ) → ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) = 0 )
172	160	rabex	⊢ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∈ V
173	172	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ∈ V )
174	171 173	suppss2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) supp 0 ) ⊆ { 𝑋 } )
175	160	mptrabex	⊢ ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ∈ V
176		funmpt	⊢ Fun ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) )
177	175 176 40	3pm3.2i	⊢ ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ∈ V ∧ Fun ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ∧ 0 ∈ V )
178	177	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ∈ V ∧ Fun ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ∧ 0 ∈ V ) )
179		snfi	⊢ { 𝑋 } ∈ Fin
180	179	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → { 𝑋 } ∈ Fin )
181		suppssfifsupp	⊢ ( ( ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ∈ V ∧ Fun ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ∧ 0 ∈ V ) ∧ ( { 𝑋 } ∈ Fin ∧ ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) supp 0 ) ⊆ { 𝑋 } ) ) → ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) finSupp 0 )
182	178 180 174 181	syl12anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) finSupp 0 )
183	45 3 148 150 122 174 182	gsumres	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → ( 𝑅 Σg ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ↾ { 𝑋 } ) ) = ( 𝑅 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ) )
184	145 183	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ) → if ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) = ( 𝑅 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ) )
185	184	mpteq2dva	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 ↦ if ( 𝑘 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ) ) )
186	17 185	eqtrid	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) ) = ( 𝑘 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑘 } ↦ ( ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) ‘ 𝑗 ) ( .r ‘ 𝑅 ) ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ‘ ( 𝑘 ∘f − 𝑗 ) ) ) ) ) ) )
187	14 186	eqtr4d	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑋 , 1 , 0 ) ) · ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑋 ∘f + 𝑌 ) , 1 , 0 ) ) )