Theorem mplmonmul 19285

Description: The product of two monomials adds the exponent vectors together. For example, the product of (𝑥↑2)(𝑦↑2) with (𝑦↑1)(𝑧↑3) is (𝑥↑2)(𝑦↑3)(𝑧↑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.)

Hypotheses

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

Assertion

Ref	Expression
mplmonmul	⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 )) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑋 ∘𝑓 + 𝑌), 1 , 0 )))

Distinct variable groups:   𝑦,𝐷   𝑓,𝐼   𝜑,𝑦   𝑦,𝑓,𝑋   𝑦, 0   𝑦, 1   𝑦,𝑅   𝑓,𝑌,𝑦

Allowed substitution hints:   𝜑(𝑓)   𝐵(𝑦,𝑓)   𝐷(𝑓)   𝑃(𝑦,𝑓)   𝑅(𝑓)   · (𝑦,𝑓)   1 (𝑓)   𝐼(𝑦)   𝑊(𝑦,𝑓)   0 (𝑓)

Proof of Theorem mplmonmul

Dummy variables 𝑗 𝑘 𝑥 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mplmon.s	. . 3 ⊢ 𝑃 = (𝐼 mPoly 𝑅)
2		mplmon.b	. . 3 ⊢ 𝐵 = (Base‘𝑃)
3		eqid 2610	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
4		mplmonmul.t	. . 3 ⊢ · = (.r‘𝑃)
5		mplmon.d	. . 3 ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}
6		mplmon.z	. . . 4 ⊢ 0 = (0g‘𝑅)
7		mplmon.o	. . . 4 ⊢ 1 = (1r‘𝑅)
8		mplmon.i	. . . 4 ⊢ (𝜑 → 𝐼 ∈ 𝑊)
9		mplmon.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ Ring)
10		mplmon.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝐷)
11	1, 2, 6, 7, 5, 8, 9, 10	mplmon 19284	. . 3 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 )) ∈ 𝐵)
12		mplmonmul.x	. . . 4 ⊢ (𝜑 → 𝑌 ∈ 𝐷)
13	1, 2, 6, 7, 5, 8, 9, 12	mplmon 19284	. . 3 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 )) ∈ 𝐵)
14	1, 2, 3, 4, 5, 11, 13	mplmul 19264	. 2 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 )) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))))))
15		eqeq1 2614	. . . . 5 ⊢ (𝑦 = 𝑘 → (𝑦 = (𝑋 ∘𝑓 + 𝑌) ↔ 𝑘 = (𝑋 ∘𝑓 + 𝑌)))
16	15	ifbid 4058	. . . 4 ⊢ (𝑦 = 𝑘 → if(𝑦 = (𝑋 ∘𝑓 + 𝑌), 1 , 0 ) = if(𝑘 = (𝑋 ∘𝑓 + 𝑌), 1 , 0 ))
17	16	cbvmptv 4678	. . 3 ⊢ (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑋 ∘𝑓 + 𝑌), 1 , 0 )) = (𝑘 ∈ 𝐷 ↦ if(𝑘 = (𝑋 ∘𝑓 + 𝑌), 1 , 0 ))
18		simpr 476	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘})
19	18	snssd 4281	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → {𝑋} ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘})
20	19	resmptd 5371	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) ↾ {𝑋}) = (𝑗 ∈ {𝑋} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))))
21	20	oveq2d 6565	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → (𝑅 Σg ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) ↾ {𝑋})) = (𝑅 Σg (𝑗 ∈ {𝑋} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗))))))
22	9	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → 𝑅 ∈ Ring)
23		ringmnd 18379	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
24	22, 23	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → 𝑅 ∈ Mnd)
25	10	ad2antrr 758	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → 𝑋 ∈ 𝐷)
26		iftrue 4042	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑋 → if(𝑦 = 𝑋, 1 , 0 ) = 1 )
27		eqid 2610	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))
28		fvex 6113	. . . . . . . . . . . . . 14 ⊢ (1r‘𝑅) ∈ V
29	7, 28	eqeltri 2684	. . . . . . . . . . . . 13 ⊢ 1 ∈ V
30	26, 27, 29	fvmpt 6191	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ 𝐷 → ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑋) = 1 )
31	25, 30	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑋) = 1 )
32		ssrab2 3650	. . . . . . . . . . . . 13 ⊢ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ⊆ 𝐷
33	8	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → 𝐼 ∈ 𝑊)
34		simplr 788	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → 𝑘 ∈ 𝐷)
35		eqid 2610	. . . . . . . . . . . . . . 15 ⊢ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} = {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}
36	5, 35	psrbagconcl 19194	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑘 ∈ 𝐷 ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → (𝑘 ∘𝑓 − 𝑋) ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘})
37	33, 34, 18, 36	syl3anc 1318	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → (𝑘 ∘𝑓 − 𝑋) ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘})
38	32, 37	sseldi 3566	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → (𝑘 ∘𝑓 − 𝑋) ∈ 𝐷)
39		eqeq1 2614	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑘 ∘𝑓 − 𝑋) → (𝑦 = 𝑌 ↔ (𝑘 ∘𝑓 − 𝑋) = 𝑌))
40	39	ifbid 4058	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑘 ∘𝑓 − 𝑋) → if(𝑦 = 𝑌, 1 , 0 ) = if((𝑘 ∘𝑓 − 𝑋) = 𝑌, 1 , 0 ))
41		eqid 2610	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 )) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))
42		fvex 6113	. . . . . . . . . . . . . . 15 ⊢ (0g‘𝑅) ∈ V
43	6, 42	eqeltri 2684	. . . . . . . . . . . . . 14 ⊢ 0 ∈ V
44	29, 43	ifex 4106	. . . . . . . . . . . . 13 ⊢ if((𝑘 ∘𝑓 − 𝑋) = 𝑌, 1 , 0 ) ∈ V
45	40, 41, 44	fvmpt 6191	. . . . . . . . . . . 12 ⊢ ((𝑘 ∘𝑓 − 𝑋) ∈ 𝐷 → ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑋)) = if((𝑘 ∘𝑓 − 𝑋) = 𝑌, 1 , 0 ))
46	38, 45	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑋)) = if((𝑘 ∘𝑓 − 𝑋) = 𝑌, 1 , 0 ))
47	31, 46	oveq12d 6567	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑋)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑋))) = ( 1 (.r‘𝑅)if((𝑘 ∘𝑓 − 𝑋) = 𝑌, 1 , 0 )))
48		eqid 2610	. . . . . . . . . . . . . 14 ⊢ (Base‘𝑅) = (Base‘𝑅)
49	48, 7	ringidcl 18391	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ Ring → 1 ∈ (Base‘𝑅))
50	48, 6	ring0cl 18392	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ Ring → 0 ∈ (Base‘𝑅))
51	49, 50	ifcld 4081	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ Ring → if((𝑘 ∘𝑓 − 𝑋) = 𝑌, 1 , 0 ) ∈ (Base‘𝑅))
52	22, 51	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → if((𝑘 ∘𝑓 − 𝑋) = 𝑌, 1 , 0 ) ∈ (Base‘𝑅))
53	48, 3, 7	ringlidm 18394	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Ring ∧ if((𝑘 ∘𝑓 − 𝑋) = 𝑌, 1 , 0 ) ∈ (Base‘𝑅)) → ( 1 (.r‘𝑅)if((𝑘 ∘𝑓 − 𝑋) = 𝑌, 1 , 0 )) = if((𝑘 ∘𝑓 − 𝑋) = 𝑌, 1 , 0 ))
54	22, 52, 53	syl2anc 691	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → ( 1 (.r‘𝑅)if((𝑘 ∘𝑓 − 𝑋) = 𝑌, 1 , 0 )) = if((𝑘 ∘𝑓 − 𝑋) = 𝑌, 1 , 0 ))
55	5	psrbagf 19186	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑘 ∈ 𝐷) → 𝑘:𝐼⟶ℕ0)
56	33, 34, 55	syl2anc 691	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → 𝑘:𝐼⟶ℕ0)
57	56	ffvelrnda 6267	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) ∧ 𝑧 ∈ 𝐼) → (𝑘‘𝑧) ∈ ℕ0)
58	8	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝐼 ∈ 𝑊)
59	10	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑋 ∈ 𝐷)
60	5	psrbagf 19186	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐷) → 𝑋:𝐼⟶ℕ0)
61	58, 59, 60	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑋:𝐼⟶ℕ0)
62	61	ffvelrnda 6267	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑧 ∈ 𝐼) → (𝑋‘𝑧) ∈ ℕ0)
63	62	adantlr 747	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) ∧ 𝑧 ∈ 𝐼) → (𝑋‘𝑧) ∈ ℕ0)
64	5	psrbagf 19186	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑌 ∈ 𝐷) → 𝑌:𝐼⟶ℕ0)
65	8, 12, 64	syl2anc 691	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑌:𝐼⟶ℕ0)
66	65	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑌:𝐼⟶ℕ0)
67	66	ffvelrnda 6267	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑧 ∈ 𝐼) → (𝑌‘𝑧) ∈ ℕ0)
68	67	adantlr 747	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) ∧ 𝑧 ∈ 𝐼) → (𝑌‘𝑧) ∈ ℕ0)
69		nn0cn 11179	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘‘𝑧) ∈ ℕ0 → (𝑘‘𝑧) ∈ ℂ)
70		nn0cn 11179	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋‘𝑧) ∈ ℕ0 → (𝑋‘𝑧) ∈ ℂ)
71		nn0cn 11179	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑌‘𝑧) ∈ ℕ0 → (𝑌‘𝑧) ∈ ℂ)
72		subadd 10163	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘‘𝑧) ∈ ℂ ∧ (𝑋‘𝑧) ∈ ℂ ∧ (𝑌‘𝑧) ∈ ℂ) → (((𝑘‘𝑧) − (𝑋‘𝑧)) = (𝑌‘𝑧) ↔ ((𝑋‘𝑧) + (𝑌‘𝑧)) = (𝑘‘𝑧)))
73	69, 70, 71, 72	syl3an 1360	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘‘𝑧) ∈ ℕ0 ∧ (𝑋‘𝑧) ∈ ℕ0 ∧ (𝑌‘𝑧) ∈ ℕ0) → (((𝑘‘𝑧) − (𝑋‘𝑧)) = (𝑌‘𝑧) ↔ ((𝑋‘𝑧) + (𝑌‘𝑧)) = (𝑘‘𝑧)))
74	57, 63, 68, 73	syl3anc 1318	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) ∧ 𝑧 ∈ 𝐼) → (((𝑘‘𝑧) − (𝑋‘𝑧)) = (𝑌‘𝑧) ↔ ((𝑋‘𝑧) + (𝑌‘𝑧)) = (𝑘‘𝑧)))
75		eqcom 2617	. . . . . . . . . . . . . . 15 ⊢ (((𝑋‘𝑧) + (𝑌‘𝑧)) = (𝑘‘𝑧) ↔ (𝑘‘𝑧) = ((𝑋‘𝑧) + (𝑌‘𝑧)))
76	74, 75	syl6bb 275	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) ∧ 𝑧 ∈ 𝐼) → (((𝑘‘𝑧) − (𝑋‘𝑧)) = (𝑌‘𝑧) ↔ (𝑘‘𝑧) = ((𝑋‘𝑧) + (𝑌‘𝑧))))
77	76	ralbidva 2968	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → (∀𝑧 ∈ 𝐼 ((𝑘‘𝑧) − (𝑋‘𝑧)) = (𝑌‘𝑧) ↔ ∀𝑧 ∈ 𝐼 (𝑘‘𝑧) = ((𝑋‘𝑧) + (𝑌‘𝑧))))
78		mpteqb 6207	. . . . . . . . . . . . . 14 ⊢ (∀𝑧 ∈ 𝐼 ((𝑘‘𝑧) − (𝑋‘𝑧)) ∈ V → ((𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧) − (𝑋‘𝑧))) = (𝑧 ∈ 𝐼 ↦ (𝑌‘𝑧)) ↔ ∀𝑧 ∈ 𝐼 ((𝑘‘𝑧) − (𝑋‘𝑧)) = (𝑌‘𝑧)))
79		ovex 6577	. . . . . . . . . . . . . . 15 ⊢ ((𝑘‘𝑧) − (𝑋‘𝑧)) ∈ V
80	79	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ 𝐼 → ((𝑘‘𝑧) − (𝑋‘𝑧)) ∈ V)
81	78, 80	mprg 2910	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧) − (𝑋‘𝑧))) = (𝑧 ∈ 𝐼 ↦ (𝑌‘𝑧)) ↔ ∀𝑧 ∈ 𝐼 ((𝑘‘𝑧) − (𝑋‘𝑧)) = (𝑌‘𝑧))
82		mpteqb 6207	. . . . . . . . . . . . . 14 ⊢ (∀𝑧 ∈ 𝐼 (𝑘‘𝑧) ∈ V → ((𝑧 ∈ 𝐼 ↦ (𝑘‘𝑧)) = (𝑧 ∈ 𝐼 ↦ ((𝑋‘𝑧) + (𝑌‘𝑧))) ↔ ∀𝑧 ∈ 𝐼 (𝑘‘𝑧) = ((𝑋‘𝑧) + (𝑌‘𝑧))))
83		fvex 6113	. . . . . . . . . . . . . . 15 ⊢ (𝑘‘𝑧) ∈ V
84	83	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ 𝐼 → (𝑘‘𝑧) ∈ V)
85	82, 84	mprg 2910	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ 𝐼 ↦ (𝑘‘𝑧)) = (𝑧 ∈ 𝐼 ↦ ((𝑋‘𝑧) + (𝑌‘𝑧))) ↔ ∀𝑧 ∈ 𝐼 (𝑘‘𝑧) = ((𝑋‘𝑧) + (𝑌‘𝑧)))
86	77, 81, 85	3bitr4g 302	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → ((𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧) − (𝑋‘𝑧))) = (𝑧 ∈ 𝐼 ↦ (𝑌‘𝑧)) ↔ (𝑧 ∈ 𝐼 ↦ (𝑘‘𝑧)) = (𝑧 ∈ 𝐼 ↦ ((𝑋‘𝑧) + (𝑌‘𝑧)))))
87	56	feqmptd 6159	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → 𝑘 = (𝑧 ∈ 𝐼 ↦ (𝑘‘𝑧)))
88	61	feqmptd 6159	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑋 = (𝑧 ∈ 𝐼 ↦ (𝑋‘𝑧)))
89	88	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → 𝑋 = (𝑧 ∈ 𝐼 ↦ (𝑋‘𝑧)))
90	33, 57, 63, 87, 89	offval2 6812	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → (𝑘 ∘𝑓 − 𝑋) = (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧) − (𝑋‘𝑧))))
91	66	feqmptd 6159	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑌 = (𝑧 ∈ 𝐼 ↦ (𝑌‘𝑧)))
92	91	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → 𝑌 = (𝑧 ∈ 𝐼 ↦ (𝑌‘𝑧)))
93	90, 92	eqeq12d 2625	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → ((𝑘 ∘𝑓 − 𝑋) = 𝑌 ↔ (𝑧 ∈ 𝐼 ↦ ((𝑘‘𝑧) − (𝑋‘𝑧))) = (𝑧 ∈ 𝐼 ↦ (𝑌‘𝑧))))
94	58, 62, 67, 88, 91	offval2 6812	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑋 ∘𝑓 + 𝑌) = (𝑧 ∈ 𝐼 ↦ ((𝑋‘𝑧) + (𝑌‘𝑧))))
95	94	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → (𝑋 ∘𝑓 + 𝑌) = (𝑧 ∈ 𝐼 ↦ ((𝑋‘𝑧) + (𝑌‘𝑧))))
96	87, 95	eqeq12d 2625	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → (𝑘 = (𝑋 ∘𝑓 + 𝑌) ↔ (𝑧 ∈ 𝐼 ↦ (𝑘‘𝑧)) = (𝑧 ∈ 𝐼 ↦ ((𝑋‘𝑧) + (𝑌‘𝑧)))))
97	86, 93, 96	3bitr4d 299	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → ((𝑘 ∘𝑓 − 𝑋) = 𝑌 ↔ 𝑘 = (𝑋 ∘𝑓 + 𝑌)))
98	97	ifbid 4058	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → if((𝑘 ∘𝑓 − 𝑋) = 𝑌, 1 , 0 ) = if(𝑘 = (𝑋 ∘𝑓 + 𝑌), 1 , 0 ))
99	47, 54, 98	3eqtrd 2648	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑋)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑋))) = if(𝑘 = (𝑋 ∘𝑓 + 𝑌), 1 , 0 ))
100	98, 52	eqeltrrd 2689	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → if(𝑘 = (𝑋 ∘𝑓 + 𝑌), 1 , 0 ) ∈ (Base‘𝑅))
101	99, 100	eqeltrd 2688	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑋)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑋))) ∈ (Base‘𝑅))
102		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑗 = 𝑋 → ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗) = ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑋))
103		oveq2 6557	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑋 → (𝑘 ∘𝑓 − 𝑗) = (𝑘 ∘𝑓 − 𝑋))
104	103	fveq2d 6107	. . . . . . . . . 10 ⊢ (𝑗 = 𝑋 → ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)) = ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑋)))
105	102, 104	oveq12d 6567	. . . . . . . . 9 ⊢ (𝑗 = 𝑋 → (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗))) = (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑋)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑋))))
106	48, 105	gsumsn 18177	. . . . . . . 8 ⊢ ((𝑅 ∈ Mnd ∧ 𝑋 ∈ 𝐷 ∧ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑋)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑋))) ∈ (Base‘𝑅)) → (𝑅 Σg (𝑗 ∈ {𝑋} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗))))) = (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑋)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑋))))
107	24, 25, 101, 106	syl3anc 1318	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → (𝑅 Σg (𝑗 ∈ {𝑋} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗))))) = (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑋)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑋))))
108	21, 107, 99	3eqtrd 2648	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → (𝑅 Σg ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) ↾ {𝑋})) = if(𝑘 = (𝑋 ∘𝑓 + 𝑌), 1 , 0 ))
109	6	gsum0 17101	. . . . . . 7 ⊢ (𝑅 Σg ∅) = 0
110		disjsn 4192	. . . . . . . . 9 ⊢ (({𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ∩ {𝑋}) = ∅ ↔ ¬ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘})
111	9	ad2antrr 758	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → 𝑅 ∈ Ring)
112	1, 48, 2, 5, 11	mplelf 19254	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 )):𝐷⟶(Base‘𝑅))
113	112	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 )):𝐷⟶(Base‘𝑅))
114		simpr 476	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘})
115	32, 114	sseldi 3566	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → 𝑗 ∈ 𝐷)
116	113, 115	ffvelrnd 6268	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗) ∈ (Base‘𝑅))
117	1, 48, 2, 5, 13	mplelf 19254	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 )):𝐷⟶(Base‘𝑅))
118	117	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 )):𝐷⟶(Base‘𝑅))
119	8	ad2antrr 758	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → 𝐼 ∈ 𝑊)
120		simplr 788	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → 𝑘 ∈ 𝐷)
121	5, 35	psrbagconcl 19194	. . . . . . . . . . . . . . . 16 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑘 ∈ 𝐷 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → (𝑘 ∘𝑓 − 𝑗) ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘})
122	119, 120, 114, 121	syl3anc 1318	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → (𝑘 ∘𝑓 − 𝑗) ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘})
123	32, 122	sseldi 3566	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → (𝑘 ∘𝑓 − 𝑗) ∈ 𝐷)
124	118, 123	ffvelrnd 6268	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)) ∈ (Base‘𝑅))
125	48, 3	ringcl 18384	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Ring ∧ ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗) ∈ (Base‘𝑅) ∧ ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)) ∈ (Base‘𝑅)) → (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗))) ∈ (Base‘𝑅))
126	111, 116, 124, 125	syl3anc 1318	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗))) ∈ (Base‘𝑅))
127		eqid 2610	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) = (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗))))
128	126, 127	fmptd 6292	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}⟶(Base‘𝑅))
129		ffn 5958	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}⟶(Base‘𝑅) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) Fn {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘})
130		fnresdisj 5915	. . . . . . . . . . 11 ⊢ ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) Fn {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} → (({𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ∩ {𝑋}) = ∅ ↔ ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) ↾ {𝑋}) = ∅))
131	128, 129, 130	3syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (({𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ∩ {𝑋}) = ∅ ↔ ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) ↾ {𝑋}) = ∅))
132	131	biimpa 500	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ∩ {𝑋}) = ∅) → ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) ↾ {𝑋}) = ∅)
133	110, 132	sylan2br 492	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ ¬ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) ↾ {𝑋}) = ∅)
134	133	oveq2d 6565	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ ¬ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → (𝑅 Σg ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) ↾ {𝑋})) = (𝑅 Σg ∅))
135	62	nn0red 11229	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑧 ∈ 𝐼) → (𝑋‘𝑧) ∈ ℝ)
136		nn0addge1 11216	. . . . . . . . . . . . . 14 ⊢ (((𝑋‘𝑧) ∈ ℝ ∧ (𝑌‘𝑧) ∈ ℕ0) → (𝑋‘𝑧) ≤ ((𝑋‘𝑧) + (𝑌‘𝑧)))
137	135, 67, 136	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑧 ∈ 𝐼) → (𝑋‘𝑧) ≤ ((𝑋‘𝑧) + (𝑌‘𝑧)))
138	137	ralrimiva 2949	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ∀𝑧 ∈ 𝐼 (𝑋‘𝑧) ≤ ((𝑋‘𝑧) + (𝑌‘𝑧)))
139		ovex 6577	. . . . . . . . . . . . . 14 ⊢ ((𝑋‘𝑧) + (𝑌‘𝑧)) ∈ V
140	139	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑧 ∈ 𝐼) → ((𝑋‘𝑧) + (𝑌‘𝑧)) ∈ V)
141	58, 62, 140, 88, 94	ofrfval2 6813	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑋 ∘𝑟 ≤ (𝑋 ∘𝑓 + 𝑌) ↔ ∀𝑧 ∈ 𝐼 (𝑋‘𝑧) ≤ ((𝑋‘𝑧) + (𝑌‘𝑧))))
142	138, 141	mpbird 246	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑋 ∘𝑟 ≤ (𝑋 ∘𝑓 + 𝑌))
143		breq1 4586	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → (𝑥 ∘𝑟 ≤ (𝑋 ∘𝑓 + 𝑌) ↔ 𝑋 ∘𝑟 ≤ (𝑋 ∘𝑓 + 𝑌)))
144	143	elrab 3331	. . . . . . . . . . 11 ⊢ (𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝑋 ∘𝑓 + 𝑌)} ↔ (𝑋 ∈ 𝐷 ∧ 𝑋 ∘𝑟 ≤ (𝑋 ∘𝑓 + 𝑌)))
145	59, 142, 144	sylanbrc 695	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝑋 ∘𝑓 + 𝑌)})
146		breq2 4587	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑋 ∘𝑓 + 𝑌) → (𝑥 ∘𝑟 ≤ 𝑘 ↔ 𝑥 ∘𝑟 ≤ (𝑋 ∘𝑓 + 𝑌)))
147	146	rabbidv 3164	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑋 ∘𝑓 + 𝑌) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} = {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝑋 ∘𝑓 + 𝑌)})
148	147	eleq2d 2673	. . . . . . . . . 10 ⊢ (𝑘 = (𝑋 ∘𝑓 + 𝑌) → (𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↔ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝑋 ∘𝑓 + 𝑌)}))
149	145, 148	syl5ibrcom 236	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑘 = (𝑋 ∘𝑓 + 𝑌) → 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}))
150	149	con3dimp 456	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ ¬ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → ¬ 𝑘 = (𝑋 ∘𝑓 + 𝑌))
151	150	iffalsed 4047	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ ¬ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → if(𝑘 = (𝑋 ∘𝑓 + 𝑌), 1 , 0 ) = 0 )
152	109, 134, 151	3eqtr4a 2670	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ ¬ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → (𝑅 Σg ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) ↾ {𝑋})) = if(𝑘 = (𝑋 ∘𝑓 + 𝑌), 1 , 0 ))
153	108, 152	pm2.61dan 828	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) ↾ {𝑋})) = if(𝑘 = (𝑋 ∘𝑓 + 𝑌), 1 , 0 ))
154	9	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 ∈ Ring)
155		ringcmn 18404	. . . . . . 7 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
156	154, 155	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝑅 ∈ CMnd)
157	5	psrbaglefi 19193	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑘 ∈ 𝐷) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ∈ Fin)
158	8, 157	sylan 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ∈ Fin)
159		ssdif 3707	. . . . . . . . . . . 12 ⊢ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ⊆ 𝐷 → ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ∖ {𝑋}) ⊆ (𝐷 ∖ {𝑋}))
160	32, 159	ax-mp 5	. . . . . . . . . . 11 ⊢ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ∖ {𝑋}) ⊆ (𝐷 ∖ {𝑋})
161	160	sseli 3564	. . . . . . . . . 10 ⊢ (𝑗 ∈ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ∖ {𝑋}) → 𝑗 ∈ (𝐷 ∖ {𝑋}))
162	112	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 )):𝐷⟶(Base‘𝑅))
163		eldifsni 4261	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝐷 ∖ {𝑋}) → 𝑦 ≠ 𝑋)
164	163	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑦 ∈ (𝐷 ∖ {𝑋})) → 𝑦 ≠ 𝑋)
165	164	neneqd 2787	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑦 ∈ (𝐷 ∖ {𝑋})) → ¬ 𝑦 = 𝑋)
166	165	iffalsed 4047	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑦 ∈ (𝐷 ∖ {𝑋})) → if(𝑦 = 𝑋, 1 , 0 ) = 0 )
167		ovex 6577	. . . . . . . . . . . . . 14 ⊢ (ℕ0 ↑𝑚 𝐼) ∈ V
168	5, 167	rabex2 4742	. . . . . . . . . . . . 13 ⊢ 𝐷 ∈ V
169	168	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 𝐷 ∈ V)
170	166, 169	suppss2 7216	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 )) supp 0 ) ⊆ {𝑋})
171	43	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → 0 ∈ V)
172	162, 170, 169, 171	suppssr 7213	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑗 ∈ (𝐷 ∖ {𝑋})) → ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗) = 0 )
173	161, 172	sylan2 490	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑗 ∈ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ∖ {𝑋})) → ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗) = 0 )
174	173	oveq1d 6564	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑗 ∈ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ∖ {𝑋})) → (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗))) = ( 0 (.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗))))
175		eldifi 3694	. . . . . . . . 9 ⊢ (𝑗 ∈ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ∖ {𝑋}) → 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘})
176	48, 3, 6	ringlz 18410	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Ring ∧ ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)) ∈ (Base‘𝑅)) → ( 0 (.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗))) = 0 )
177	111, 124, 176	syl2anc 691	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘}) → ( 0 (.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗))) = 0 )
178	175, 177	sylan2 490	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑗 ∈ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ∖ {𝑋})) → ( 0 (.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗))) = 0 )
179	174, 178	eqtrd 2644	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐷) ∧ 𝑗 ∈ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ∖ {𝑋})) → (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗))) = 0 )
180	168	rabex 4740	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ∈ V
181	180	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ∈ V)
182	179, 181	suppss2 7216	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) supp 0 ) ⊆ {𝑋})
183	168	mptrabex 6392	. . . . . . . . 9 ⊢ (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) ∈ V
184		funmpt 5840	. . . . . . . . 9 ⊢ Fun (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗))))
185	183, 184, 43	3pm3.2i 1232	. . . . . . . 8 ⊢ ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) ∈ V ∧ Fun (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) ∧ 0 ∈ V)
186	185	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) ∈ V ∧ Fun (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) ∧ 0 ∈ V))
187		snfi 7923	. . . . . . . 8 ⊢ {𝑋} ∈ Fin
188	187	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → {𝑋} ∈ Fin)
189		suppssfifsupp 8173	. . . . . . 7 ⊢ ((((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) ∈ V ∧ Fun (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) ∧ 0 ∈ V) ∧ ({𝑋} ∈ Fin ∧ ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) supp 0 ) ⊆ {𝑋})) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) finSupp 0 )
190	186, 188, 182, 189	syl12anc 1316	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) finSupp 0 )
191	48, 6, 156, 158, 128, 182, 190	gsumres 18137	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → (𝑅 Σg ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))) ↾ {𝑋})) = (𝑅 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗))))))
192	153, 191	eqtr3d 2646	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐷) → if(𝑘 = (𝑋 ∘𝑓 + 𝑌), 1 , 0 ) = (𝑅 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗))))))
193	192	mpteq2dva 4672	. . 3 ⊢ (𝜑 → (𝑘 ∈ 𝐷 ↦ if(𝑘 = (𝑋 ∘𝑓 + 𝑌), 1 , 0 )) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))))))
194	17, 193	syl5eq 2656	. 2 ⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑋 ∘𝑓 + 𝑌), 1 , 0 )) = (𝑘 ∈ 𝐷 ↦ (𝑅 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑘} ↦ (((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 ))‘𝑗)(.r‘𝑅)((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))‘(𝑘 ∘𝑓 − 𝑗)))))))
195	14, 194	eqtr4d 2647	1 ⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑋, 1 , 0 )) · (𝑦 ∈ 𝐷 ↦ if(𝑦 = 𝑌, 1 , 0 ))) = (𝑦 ∈ 𝐷 ↦ if(𝑦 = (𝑋 ∘𝑓 + 𝑌), 1 , 0 )))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  {crab 2900  Vcvv 3173   ∖ cdif 3537   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  ifcif 4036  {csn 4125   class class class wbr 4583   ↦ cmpt 4643  ^◡ccnv 5037   ↾ cres 5040   “ cima 5041  Fun wfun 5798   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ∘_𝑓 cof 6793   ∘_𝑟 cofr 6794   supp csupp 7182   ↑_𝑚 cmap 7744  Fincfn 7841   finSupp cfsupp 8158  ℂcc 9813  ℝcr 9814   + caddc 9818   ≤ cle 9954   − cmin 10145  ℕcn 10897  ℕ₀cn0 11169  Basecbs 15695  ._rcmulr 15769  0_gc0g 15923   Σ_g cgsu 15924  Mndcmnd 17117  CMndccmn 18016  1_rcur 18324  Ringcrg 18370   mPoly cmpl 19174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-ofr 6796  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-seq 12664  df-hash 12980  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-sca 15784  df-vsca 15785  df-tset 15787  df-0g 15925  df-gsum 15926  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-grp 17248  df-minusg 17249  df-mulg 17364  df-cntz 17573  df-cmn 18018  df-abl 18019  df-mgp 18313  df-ur 18325  df-ring 18372  df-psr 19177  df-mpl 19179

This theorem is referenced by:  mplcoe3  19287  mplcoe5  19289  mplmon2mul  19322