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	$$⊢P=I\mathrm{mPoly}R$$
	mplmon.b	$$⊢B={\mathrm{Base}}_P$$
	mplmon.z	$$⊢\underset{\dot{}}{0}=0_R$$
	mplmon.o	$$⊢\underset{\dot{}}{1}=1_R$$
	mplmon.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	mplmon.i	$$⊢\phi \to I\in W$$
	mplmon.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	mplmon.x	$$⊢\phi \to X\in D$$
	mplmonmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
	mplmonmul.x	$$⊢\phi \to Y\in D$$
Assertion	mplmonmul	$$⊢\phi \to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=X{+}_{f}Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mplmon.s	$$⊢P=I\mathrm{mPoly}R$$
2		mplmon.b	$$⊢B={\mathrm{Base}}_P$$
3		mplmon.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		mplmon.o	$$⊢\underset{\dot{}}{1}=1_R$$
5		mplmon.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
6		mplmon.i	$$⊢\phi \to I\in W$$
7		mplmon.r	$$⊢\phi \to R\in \mathrm{Ring}$$
8		mplmon.x	$$⊢\phi \to X\in D$$
9		mplmonmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
10		mplmonmul.x	$$⊢\phi \to Y\in D$$
11		eqid	$$⊢{\cdot }_R={\cdot }_R$$
12	1 2 3 4 5 6 7 8	mplmon	$$⊢\phi \to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in B$$
13	1 2 3 4 5 6 7 10	mplmon	$$⊢\phi \to \left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in B$$
14	1 2 11 9 5 12 13	mplmul	$$⊢\phi \to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(k\in D⟼\underset{j\in \left\{x\in D|x{\le }_{f}k\right\}}{{\sum }_R}\left(\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\right)$$
15		eqeq1	$$⊢y=k\to \left(y=X{+}_{f}Y\leftrightarrow k=X{+}_{f}Y\right)$$
16	15	ifbid	$$⊢y=k\to if\left(y=X{+}_{f}Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(k=X{+}_{f}Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
17	16	cbvmptv	$$⊢\left(y\in D⟼if\left(y=X{+}_{f}Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(k\in D⟼if\left(k=X{+}_{f}Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
18		simpr	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to X\in \left\{x\in D|x{\le }_{f}k\right\}$$
19	18	snssd	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to \left\{X\right\}\subseteq \left\{x\in D|x{\le }_{f}k\right\}$$
20	19	resmptd	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to {\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\upharpoonright }_{\left\{X\right\}}=\left(j\in \left\{X\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)$$
21	20	oveq2d	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to {\sum }_R\left({\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\upharpoonright }_{\left\{X\right\}}\right)=\underset{j\in \left\{X\right\}}{{\sum }_R}\left(\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)$$
22	7	ad2antrr	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to R\in \mathrm{Ring}$$
23		ringmnd	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Mnd}$$
24	22 23	syl	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to R\in \mathrm{Mnd}$$
25	8	ad2antrr	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to X\in D$$
26		iftrue	$$⊢y=X\to if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=\underset{\dot{}}{1}$$
27		eqid	$$⊢\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
28	4	fvexi	$$⊢\underset{\dot{}}{1}\in \mathrm{V}$$
29	26 27 28	fvmpt	$$⊢X\in D\to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(X\right)=\underset{\dot{}}{1}$$
30	25 29	syl	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(X\right)=\underset{\dot{}}{1}$$
31		ssrab2	$$⊢\left\{x\in D|x{\le }_{f}k\right\}\subseteq D$$
32		simplr	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to k\in D$$
33		eqid	$$⊢\left\{x\in D|x{\le }_{f}k\right\}=\left\{x\in D|x{\le }_{f}k\right\}$$
34	5 33	psrbagconcl	$$⊢\left(k\in D\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to k{-}_{f}X\in \left\{x\in D|x{\le }_{f}k\right\}$$
35	32 18 34	syl2anc	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to k{-}_{f}X\in \left\{x\in D|x{\le }_{f}k\right\}$$
36	31 35	sselid	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to k{-}_{f}X\in D$$
37		eqeq1	$$⊢y=k{-}_{f}X\to \left(y=Y\leftrightarrow k{-}_{f}X=Y\right)$$
38	37	ifbid	$$⊢y=k{-}_{f}X\to if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(k{-}_{f}X=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
39		eqid	$$⊢\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
40	3	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
41	28 40	ifex	$$⊢if\left(k{-}_{f}X=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in \mathrm{V}$$
42	38 39 41	fvmpt	$$⊢k{-}_{f}X\in D\to \left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}X\right)=if\left(k{-}_{f}X=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
43	36 42	syl	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to \left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}X\right)=if\left(k{-}_{f}X=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
44	30 43	oveq12d	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(X\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}X\right)=\underset{\dot{}}{1}{\cdot }_{R}if\left(k{-}_{f}X=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
45		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
46	45 4	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
47	45 3	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
48	46 47	ifcld	$$⊢R\in \mathrm{Ring}\to if\left(k{-}_{f}X=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R$$
49	22 48	syl	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to if\left(k{-}_{f}X=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R$$
50	45 11 4	ringlidm	$$⊢\left(R\in \mathrm{Ring}\wedge if\left(k{-}_{f}X=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R\right)\to \underset{\dot{}}{1}{\cdot }_{R}if\left(k{-}_{f}X=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(k{-}_{f}X=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
51	22 49 50	syl2anc	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to \underset{\dot{}}{1}{\cdot }_{R}if\left(k{-}_{f}X=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(k{-}_{f}X=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
52	5	psrbagf	$$⊢k\in D\to k:I⟶{\mathbb{N}}_0$$
53	32 52	syl	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to k:I⟶{\mathbb{N}}_0$$
54	53	ffvelrnda	$$⊢\left(\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\wedge z\in I\right)\to k\left(z\right)\in {\mathbb{N}}_0$$
55	8	adantr	$$⊢\left(\phi \wedge k\in D\right)\to X\in D$$
56	5	psrbagf	$$⊢X\in D\to X:I⟶{\mathbb{N}}_0$$
57	55 56	syl	$$⊢\left(\phi \wedge k\in D\right)\to X:I⟶{\mathbb{N}}_0$$
58	57	ffvelrnda	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge z\in I\right)\to X\left(z\right)\in {\mathbb{N}}_0$$
59	58	adantlr	$$⊢\left(\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\wedge z\in I\right)\to X\left(z\right)\in {\mathbb{N}}_0$$
60	5	psrbagf	$$⊢Y\in D\to Y:I⟶{\mathbb{N}}_0$$
61	10 60	syl	$$⊢\phi \to Y:I⟶{\mathbb{N}}_0$$
62	61	adantr	$$⊢\left(\phi \wedge k\in D\right)\to Y:I⟶{\mathbb{N}}_0$$
63	62	ffvelrnda	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge z\in I\right)\to Y\left(z\right)\in {\mathbb{N}}_0$$
64	63	adantlr	$$⊢\left(\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\wedge z\in I\right)\to Y\left(z\right)\in {\mathbb{N}}_0$$
65		nn0cn	$$⊢k\left(z\right)\in {\mathbb{N}}_0\to k\left(z\right)\in ℂ$$
66		nn0cn	$$⊢X\left(z\right)\in {\mathbb{N}}_0\to X\left(z\right)\in ℂ$$
67		nn0cn	$$⊢Y\left(z\right)\in {\mathbb{N}}_0\to Y\left(z\right)\in ℂ$$
68		subadd	$$⊢\left(k\left(z\right)\in ℂ\wedge X\left(z\right)\in ℂ\wedge Y\left(z\right)\in ℂ\right)\to \left(k\left(z\right)-X\left(z\right)=Y\left(z\right)\leftrightarrow X\left(z\right)+Y\left(z\right)=k\left(z\right)\right)$$
69	65 66 67 68	syl3an	$$⊢\left(k\left(z\right)\in {\mathbb{N}}_0\wedge X\left(z\right)\in {\mathbb{N}}_0\wedge Y\left(z\right)\in {\mathbb{N}}_0\right)\to \left(k\left(z\right)-X\left(z\right)=Y\left(z\right)\leftrightarrow X\left(z\right)+Y\left(z\right)=k\left(z\right)\right)$$
70	54 59 64 69	syl3anc	$$⊢\left(\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\wedge z\in I\right)\to \left(k\left(z\right)-X\left(z\right)=Y\left(z\right)\leftrightarrow X\left(z\right)+Y\left(z\right)=k\left(z\right)\right)$$
71		eqcom	$$⊢X\left(z\right)+Y\left(z\right)=k\left(z\right)\leftrightarrow k\left(z\right)=X\left(z\right)+Y\left(z\right)$$
72	70 71	bitrdi	$$⊢\left(\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\wedge z\in I\right)\to \left(k\left(z\right)-X\left(z\right)=Y\left(z\right)\leftrightarrow k\left(z\right)=X\left(z\right)+Y\left(z\right)\right)$$
73	72	ralbidva	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to \left(\forall z\in Ik\left(z\right)-X\left(z\right)=Y\left(z\right)\leftrightarrow \forall z\in Ik\left(z\right)=X\left(z\right)+Y\left(z\right)\right)$$
74		mpteqb	$$⊢\forall z\in Ik\left(z\right)-X\left(z\right)\in \mathrm{V}\to \left(\left(z\in I⟼k\left(z\right)-X\left(z\right)\right)=\left(z\in I⟼Y\left(z\right)\right)\leftrightarrow \forall z\in Ik\left(z\right)-X\left(z\right)=Y\left(z\right)\right)$$
75		ovexd	$$⊢z\in I\to k\left(z\right)-X\left(z\right)\in \mathrm{V}$$
76	74 75	mprg	$$⊢\left(z\in I⟼k\left(z\right)-X\left(z\right)\right)=\left(z\in I⟼Y\left(z\right)\right)\leftrightarrow \forall z\in Ik\left(z\right)-X\left(z\right)=Y\left(z\right)$$
77		mpteqb	$$⊢\forall z\in Ik\left(z\right)\in \mathrm{V}\to \left(\left(z\in I⟼k\left(z\right)\right)=\left(z\in I⟼X\left(z\right)+Y\left(z\right)\right)\leftrightarrow \forall z\in Ik\left(z\right)=X\left(z\right)+Y\left(z\right)\right)$$
78		fvexd	$$⊢z\in I\to k\left(z\right)\in \mathrm{V}$$
79	77 78	mprg	$$⊢\left(z\in I⟼k\left(z\right)\right)=\left(z\in I⟼X\left(z\right)+Y\left(z\right)\right)\leftrightarrow \forall z\in Ik\left(z\right)=X\left(z\right)+Y\left(z\right)$$
80	73 76 79	3bitr4g	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to \left(\left(z\in I⟼k\left(z\right)-X\left(z\right)\right)=\left(z\in I⟼Y\left(z\right)\right)\leftrightarrow \left(z\in I⟼k\left(z\right)\right)=\left(z\in I⟼X\left(z\right)+Y\left(z\right)\right)\right)$$
81	6	ad2antrr	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to I\in W$$
82	53	feqmptd	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to k=\left(z\in I⟼k\left(z\right)\right)$$
83	57	feqmptd	$$⊢\left(\phi \wedge k\in D\right)\to X=\left(z\in I⟼X\left(z\right)\right)$$
84	83	adantr	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to X=\left(z\in I⟼X\left(z\right)\right)$$
85	81 54 59 82 84	offval2	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to k{-}_{f}X=\left(z\in I⟼k\left(z\right)-X\left(z\right)\right)$$
86	62	feqmptd	$$⊢\left(\phi \wedge k\in D\right)\to Y=\left(z\in I⟼Y\left(z\right)\right)$$
87	86	adantr	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to Y=\left(z\in I⟼Y\left(z\right)\right)$$
88	85 87	eqeq12d	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to \left(k{-}_{f}X=Y\leftrightarrow \left(z\in I⟼k\left(z\right)-X\left(z\right)\right)=\left(z\in I⟼Y\left(z\right)\right)\right)$$
89	6	adantr	$$⊢\left(\phi \wedge k\in D\right)\to I\in W$$
90	89 58 63 83 86	offval2	$$⊢\left(\phi \wedge k\in D\right)\to X{+}_{f}Y=\left(z\in I⟼X\left(z\right)+Y\left(z\right)\right)$$
91	90	adantr	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to X{+}_{f}Y=\left(z\in I⟼X\left(z\right)+Y\left(z\right)\right)$$
92	82 91	eqeq12d	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to \left(k=X{+}_{f}Y\leftrightarrow \left(z\in I⟼k\left(z\right)\right)=\left(z\in I⟼X\left(z\right)+Y\left(z\right)\right)\right)$$
93	80 88 92	3bitr4d	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to \left(k{-}_{f}X=Y\leftrightarrow k=X{+}_{f}Y\right)$$
94	93	ifbid	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to if\left(k{-}_{f}X=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(k=X{+}_{f}Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
95	44 51 94	3eqtrd	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(X\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}X\right)=if\left(k=X{+}_{f}Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
96	94 49	eqeltrrd	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to if\left(k=X{+}_{f}Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R$$
97	95 96	eqeltrd	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(X\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}X\right)\in {\mathrm{Base}}_R$$
98		fveq2	$$⊢j=X\to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right)=\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(X\right)$$
99		oveq2	$$⊢j=X\to k{-}_{f}j=k{-}_{f}X$$
100	99	fveq2d	$$⊢j=X\to \left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)=\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}X\right)$$
101	98 100	oveq12d	$$⊢j=X\to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)=\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(X\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}X\right)$$
102	45 101	gsumsn	$$⊢\left(R\in \mathrm{Mnd}\wedge X\in D\wedge \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(X\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}X\right)\in {\mathrm{Base}}_R\right)\to \underset{j\in \left\{X\right\}}{{\sum }_R}\left(\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)=\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(X\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}X\right)$$
103	24 25 97 102	syl3anc	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to \underset{j\in \left\{X\right\}}{{\sum }_R}\left(\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)=\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(X\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}X\right)$$
104	21 103 95	3eqtrd	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to {\sum }_R\left({\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\upharpoonright }_{\left\{X\right\}}\right)=if\left(k=X{+}_{f}Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
105	3	gsum0	$$⊢{\sum }_R\varnothing =\underset{\dot{}}{0}$$
106		disjsn	$$⊢\left\{x\in D|x{\le }_{f}k\right\}\cap \left\{X\right\}=\varnothing \leftrightarrow \neg X\in \left\{x\in D|x{\le }_{f}k\right\}$$
107	7	ad2antrr	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge j\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to R\in \mathrm{Ring}$$
108	1 45 2 5 12	mplelf	$$⊢\phi \to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right):D⟶{\mathrm{Base}}_R$$
109	108	ad2antrr	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge j\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right):D⟶{\mathrm{Base}}_R$$
110		simpr	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge j\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to j\in \left\{x\in D|x{\le }_{f}k\right\}$$
111	31 110	sselid	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge j\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to j\in D$$
112	109 111	ffvelrnd	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge j\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right)\in {\mathrm{Base}}_R$$
113	1 45 2 5 13	mplelf	$$⊢\phi \to \left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right):D⟶{\mathrm{Base}}_R$$
114	113	ad2antrr	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge j\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to \left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right):D⟶{\mathrm{Base}}_R$$
115		simplr	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge j\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to k\in D$$
116	5 33	psrbagconcl	$$⊢\left(k\in D\wedge j\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to k{-}_{f}j\in \left\{x\in D|x{\le }_{f}k\right\}$$
117	115 110 116	syl2anc	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge j\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to k{-}_{f}j\in \left\{x\in D|x{\le }_{f}k\right\}$$
118	31 117	sselid	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge j\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to k{-}_{f}j\in D$$
119	114 118	ffvelrnd	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge j\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to \left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\in {\mathrm{Base}}_R$$
120	45 11	ringcl	$$⊢\left(R\in \mathrm{Ring}\wedge \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right)\in {\mathrm{Base}}_R\wedge \left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\in {\mathrm{Base}}_R\right)\to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\in {\mathrm{Base}}_R$$
121	107 112 119 120	syl3anc	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge j\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\in {\mathrm{Base}}_R$$
122	121	fmpttd	$$⊢\left(\phi \wedge k\in D\right)\to \left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right):\left\{x\in D|x{\le }_{f}k\right\}⟶{\mathrm{Base}}_R$$
123		ffn	$$⊢\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right):\left\{x\in D|x{\le }_{f}k\right\}⟶{\mathrm{Base}}_R\to \left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)Fn\left\{x\in D|x{\le }_{f}k\right\}$$
124		fnresdisj	$$⊢\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)Fn\left\{x\in D|x{\le }_{f}k\right\}\to \left(\left\{x\in D|x{\le }_{f}k\right\}\cap \left\{X\right\}=\varnothing \leftrightarrow {\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\upharpoonright }_{\left\{X\right\}}=\varnothing \right)$$
125	122 123 124	3syl	$$⊢\left(\phi \wedge k\in D\right)\to \left(\left\{x\in D|x{\le }_{f}k\right\}\cap \left\{X\right\}=\varnothing \leftrightarrow {\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\upharpoonright }_{\left\{X\right\}}=\varnothing \right)$$
126	125	biimpa	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge \left\{x\in D|x{\le }_{f}k\right\}\cap \left\{X\right\}=\varnothing \right)\to {\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\upharpoonright }_{\left\{X\right\}}=\varnothing$$
127	106 126	sylan2br	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge \neg X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to {\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\upharpoonright }_{\left\{X\right\}}=\varnothing$$
128	127	oveq2d	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge \neg X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to {\sum }_R\left({\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\upharpoonright }_{\left\{X\right\}}\right)={\sum }_R\varnothing$$
129		breq1	$$⊢x=X\to \left(x{\le }_f\left(X{+}_{f}Y\right)\leftrightarrow X{\le }_f\left(X{+}_{f}Y\right)\right)$$
130	58	nn0red	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge z\in I\right)\to X\left(z\right)\in ℝ$$
131		nn0addge1	$$⊢\left(X\left(z\right)\in ℝ\wedge Y\left(z\right)\in {\mathbb{N}}_0\right)\to X\left(z\right)\le X\left(z\right)+Y\left(z\right)$$
132	130 63 131	syl2anc	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge z\in I\right)\to X\left(z\right)\le X\left(z\right)+Y\left(z\right)$$
133	132	ralrimiva	$$⊢\left(\phi \wedge k\in D\right)\to \forall z\in IX\left(z\right)\le X\left(z\right)+Y\left(z\right)$$
134		ovexd	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge z\in I\right)\to X\left(z\right)+Y\left(z\right)\in \mathrm{V}$$
135	89 58 134 83 90	ofrfval2	$$⊢\left(\phi \wedge k\in D\right)\to \left(X{\le }_f\left(X{+}_{f}Y\right)\leftrightarrow \forall z\in IX\left(z\right)\le X\left(z\right)+Y\left(z\right)\right)$$
136	133 135	mpbird	$$⊢\left(\phi \wedge k\in D\right)\to X{\le }_f\left(X{+}_{f}Y\right)$$
137	129 55 136	elrabd	$$⊢\left(\phi \wedge k\in D\right)\to X\in \left\{x\in D|x{\le }_f\left(X{+}_{f}Y\right)\right\}$$
138		breq2	$$⊢k=X{+}_{f}Y\to \left(x{\le }_{f}k\leftrightarrow x{\le }_f\left(X{+}_{f}Y\right)\right)$$
139	138	rabbidv	$$⊢k=X{+}_{f}Y\to \left\{x\in D|x{\le }_{f}k\right\}=\left\{x\in D|x{\le }_f\left(X{+}_{f}Y\right)\right\}$$
140	139	eleq2d	$$⊢k=X{+}_{f}Y\to \left(X\in \left\{x\in D|x{\le }_{f}k\right\}\leftrightarrow X\in \left\{x\in D|x{\le }_f\left(X{+}_{f}Y\right)\right\}\right)$$
141	137 140	syl5ibrcom	$$⊢\left(\phi \wedge k\in D\right)\to \left(k=X{+}_{f}Y\to X\in \left\{x\in D|x{\le }_{f}k\right\}\right)$$
142	141	con3dimp	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge \neg X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to \neg k=X{+}_{f}Y$$
143	142	iffalsed	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge \neg X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to if\left(k=X{+}_{f}Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
144	105 128 143	3eqtr4a	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge \neg X\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to {\sum }_R\left({\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\upharpoonright }_{\left\{X\right\}}\right)=if\left(k=X{+}_{f}Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
145	104 144	pm2.61dan	$$⊢\left(\phi \wedge k\in D\right)\to {\sum }_R\left({\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\upharpoonright }_{\left\{X\right\}}\right)=if\left(k=X{+}_{f}Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
146	7	adantr	$$⊢\left(\phi \wedge k\in D\right)\to R\in \mathrm{Ring}$$
147		ringcmn	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{CMnd}$$
148	146 147	syl	$$⊢\left(\phi \wedge k\in D\right)\to R\in \mathrm{CMnd}$$
149	5	psrbaglefi	$$⊢k\in D\to \left\{x\in D|x{\le }_{f}k\right\}\in \mathrm{Fin}$$
150	149	adantl	$$⊢\left(\phi \wedge k\in D\right)\to \left\{x\in D|x{\le }_{f}k\right\}\in \mathrm{Fin}$$
151		ssdif	$$⊢\left\{x\in D|x{\le }_{f}k\right\}\subseteq D\to \left\{x\in D|x{\le }_{f}k\right\}\setminus \left\{X\right\}\subseteq D\setminus \left\{X\right\}$$
152	31 151	ax-mp	$$⊢\left\{x\in D|x{\le }_{f}k\right\}\setminus \left\{X\right\}\subseteq D\setminus \left\{X\right\}$$
153	152	sseli	$$⊢j\in \left(\left\{x\in D|x{\le }_{f}k\right\}\setminus \left\{X\right\}\right)\to j\in \left(D\setminus \left\{X\right\}\right)$$
154	108	adantr	$$⊢\left(\phi \wedge k\in D\right)\to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right):D⟶{\mathrm{Base}}_R$$
155		eldifsni	$$⊢y\in \left(D\setminus \left\{X\right\}\right)\to y\ne X$$
156	155	adantl	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge y\in \left(D\setminus \left\{X\right\}\right)\right)\to y\ne X$$
157	156	neneqd	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge y\in \left(D\setminus \left\{X\right\}\right)\right)\to \neg y=X$$
158	157	iffalsed	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge y\in \left(D\setminus \left\{X\right\}\right)\right)\to if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
159		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
160	5 159	rabex2	$$⊢D\in \mathrm{V}$$
161	160	a1i	$$⊢\left(\phi \wedge k\in D\right)\to D\in \mathrm{V}$$
162	158 161	suppss2	$$⊢\left(\phi \wedge k\in D\right)\to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{X\right\}$$
163	40	a1i	$$⊢\left(\phi \wedge k\in D\right)\to \underset{\dot{}}{0}\in \mathrm{V}$$
164	154 162 161 163	suppssr	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge j\in \left(D\setminus \left\{X\right\}\right)\right)\to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right)=\underset{\dot{}}{0}$$
165	153 164	sylan2	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge j\in \left(\left\{x\in D|x{\le }_{f}k\right\}\setminus \left\{X\right\}\right)\right)\to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right)=\underset{\dot{}}{0}$$
166	165	oveq1d	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge j\in \left(\left\{x\in D|x{\le }_{f}k\right\}\setminus \left\{X\right\}\right)\right)\to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)=\underset{\dot{}}{0}{\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)$$
167		eldifi	$$⊢j\in \left(\left\{x\in D|x{\le }_{f}k\right\}\setminus \left\{X\right\}\right)\to j\in \left\{x\in D|x{\le }_{f}k\right\}$$
168	45 11 3	ringlz	$$⊢\left(R\in \mathrm{Ring}\wedge \left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\in {\mathrm{Base}}_R\right)\to \underset{\dot{}}{0}{\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)=\underset{\dot{}}{0}$$
169	107 119 168	syl2anc	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge j\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to \underset{\dot{}}{0}{\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)=\underset{\dot{}}{0}$$
170	167 169	sylan2	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge j\in \left(\left\{x\in D|x{\le }_{f}k\right\}\setminus \left\{X\right\}\right)\right)\to \underset{\dot{}}{0}{\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)=\underset{\dot{}}{0}$$
171	166 170	eqtrd	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge j\in \left(\left\{x\in D|x{\le }_{f}k\right\}\setminus \left\{X\right\}\right)\right)\to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)=\underset{\dot{}}{0}$$
172	160	rabex	$$⊢\left\{x\in D|x{\le }_{f}k\right\}\in \mathrm{V}$$
173	172	a1i	$$⊢\left(\phi \wedge k\in D\right)\to \left\{x\in D|x{\le }_{f}k\right\}\in \mathrm{V}$$
174	171 173	suppss2	$$⊢\left(\phi \wedge k\in D\right)\to \left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{X\right\}$$
175	160	mptrabex	$$⊢\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\in \mathrm{V}$$
176		funmpt	$$⊢\mathrm{Fun}\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)$$
177	175 176 40	3pm3.2i	$$⊢\left(\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)$$
178	177	a1i	$$⊢\left(\phi \wedge k\in D\right)\to \left(\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)$$
179		snfi	$$⊢\left\{X\right\}\in \mathrm{Fin}$$
180	179	a1i	$$⊢\left(\phi \wedge k\in D\right)\to \left\{X\right\}\in \mathrm{Fin}$$
181		suppssfifsupp	$$⊢\left(\left(\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)\wedge \left(\left\{X\right\}\in \mathrm{Fin}\wedge \left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq \left\{X\right\}\right)\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\right)$$
182	178 180 174 181	syl12anc	$$⊢\left(\phi \wedge k\in D\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\right)$$
183	45 3 148 150 122 174 182	gsumres	$$⊢\left(\phi \wedge k\in D\right)\to {\sum }_R\left({\left(j\in \left\{x\in D|x{\le }_{f}k\right\}⟼\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\upharpoonright }_{\left\{X\right\}}\right)=\underset{j\in \left\{x\in D|x{\le }_{f}k\right\}}{{\sum }_R}\left(\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)$$
184	145 183	eqtr3d	$$⊢\left(\phi \wedge k\in D\right)\to if\left(k=X{+}_{f}Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=\underset{j\in \left\{x\in D|x{\le }_{f}k\right\}}{{\sum }_R}\left(\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)$$
185	184	mpteq2dva	$$⊢\phi \to \left(k\in D⟼if\left(k=X{+}_{f}Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(k\in D⟼\underset{j\in \left\{x\in D|x{\le }_{f}k\right\}}{{\sum }_R}\left(\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\right)$$
186	17 185	eqtrid	$$⊢\phi \to \left(y\in D⟼if\left(y=X{+}_{f}Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(k\in D⟼\underset{j\in \left\{x\in D|x{\le }_{f}k\right\}}{{\sum }_R}\left(\left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(j\right){\cdot }_R\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(k{-}_{f}j\right)\right)\right)$$
187	14 186	eqtr4d	$$⊢\phi \to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\underset{\dot{}}{·}\left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(y\in D⟼if\left(y=X{+}_{f}Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$