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	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$$
33		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$$
34		eqid	$$⊢\left\{x\in D|x{\le }_{f}k\right\}=\left\{x\in D|x{\le }_{f}k\right\}$$
35	5 34	psrbagconcl	$$⊢\left(I\in W\wedge 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\}$$
36	32 33 18 35	syl3anc	$$⊢\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\}$$
37	31 36	sseldi	$$⊢\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$$
38		eqeq1	$$⊢y=k{-}_{f}X\to \left(y=Y\leftrightarrow k{-}_{f}X=Y\right)$$
39	38	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)$$
40		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)$$
41	3	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
42	28 41	ifex	$$⊢if\left(k{-}_{f}X=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in \mathrm{V}$$
43	39 40 42	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)$$
44	37 43	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)$$
45	30 44	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)$$
46		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
47	46 4	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
48	46 3	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
49	47 48	ifcld	$$⊢R\in \mathrm{Ring}\to if\left(k{-}_{f}X=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_R$$
50	22 49	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$$
51	46 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)$$
52	22 50 51	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)$$
53	5	psrbagf	$$⊢\left(I\in W\wedge k\in D\right)\to k:I⟶{\mathbb{N}}_0$$
54	32 33 53	syl2anc	$$⊢\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$$
55	54	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$$
56	6	adantr	$$⊢\left(\phi \wedge k\in D\right)\to I\in W$$
57	8	adantr	$$⊢\left(\phi \wedge k\in D\right)\to X\in D$$
58	5	psrbagf	$$⊢\left(I\in W\wedge X\in D\right)\to X:I⟶{\mathbb{N}}_0$$
59	56 57 58	syl2anc	$$⊢\left(\phi \wedge k\in D\right)\to X:I⟶{\mathbb{N}}_0$$
60	59	ffvelrnda	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge z\in I\right)\to X\left(z\right)\in {\mathbb{N}}_0$$
61	60	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$$
62	5	psrbagf	$$⊢\left(I\in W\wedge Y\in D\right)\to Y:I⟶{\mathbb{N}}_0$$
63	6 10 62	syl2anc	$$⊢\phi \to Y:I⟶{\mathbb{N}}_0$$
64	63	adantr	$$⊢\left(\phi \wedge k\in D\right)\to Y:I⟶{\mathbb{N}}_0$$
65	64	ffvelrnda	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge z\in I\right)\to Y\left(z\right)\in {\mathbb{N}}_0$$
66	65	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$$
67		nn0cn	$$⊢k\left(z\right)\in {\mathbb{N}}_0\to k\left(z\right)\in ℂ$$
68		nn0cn	$$⊢X\left(z\right)\in {\mathbb{N}}_0\to X\left(z\right)\in ℂ$$
69		nn0cn	$$⊢Y\left(z\right)\in {\mathbb{N}}_0\to Y\left(z\right)\in ℂ$$
70		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)$$
71	67 68 69 70	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)$$
72	55 61 66 71	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)$$
73		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)$$
74	72 73	syl6bb	$$⊢\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)$$
75	74	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)$$
76		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)$$
77		ovexd	$$⊢z\in I\to k\left(z\right)-X\left(z\right)\in \mathrm{V}$$
78	76 77	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)$$
79		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)$$
80		fvexd	$$⊢z\in I\to k\left(z\right)\in \mathrm{V}$$
81	79 80	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)$$
82	75 78 81	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)$$
83	54	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)$$
84	59	feqmptd	$$⊢\left(\phi \wedge k\in D\right)\to X=\left(z\in I⟼X\left(z\right)\right)$$
85	84	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)$$
86	32 55 61 83 85	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)$$
87	64	feqmptd	$$⊢\left(\phi \wedge k\in D\right)\to Y=\left(z\in I⟼Y\left(z\right)\right)$$
88	87	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)$$
89	86 88	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)$$
90	56 60 65 84 87	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	83 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	82 89 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	45 52 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 50	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	46 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 46 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	sseldi	$$⊢\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 46 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	6	ad2antrr	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge j\in \left\{x\in D|x{\le }_{f}k\right\}\right)\to I\in W$$
116		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$$
117	5 34	psrbagconcl	$$⊢\left(I\in W\wedge 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\}$$
118	115 116 110 117	syl3anc	$$⊢\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\}$$
119	31 118	sseldi	$$⊢\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$$
120	114 119	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$$
121	46 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$$
122	107 112 120 121	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$$
123	122	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$$
124		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\}$$
125		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)$$
126	123 124 125	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)$$
127	126	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$$
128	106 127	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$$
129	128	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$$
130		breq1	$$⊢x=X\to \left(x{\le }_f\left(X{+}_{f}Y\right)\leftrightarrow X{\le }_f\left(X{+}_{f}Y\right)\right)$$
131	60	nn0red	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge z\in I\right)\to X\left(z\right)\in ℝ$$
132		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)$$
133	131 65 132	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)$$
134	133	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)$$
135		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}$$
136	56 60 135 84 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)$$
137	134 136	mpbird	$$⊢\left(\phi \wedge k\in D\right)\to X{\le }_f\left(X{+}_{f}Y\right)$$
138	130 57 137	elrabd	$$⊢\left(\phi \wedge k\in D\right)\to X\in \left\{x\in D|x{\le }_f\left(X{+}_{f}Y\right)\right\}$$
139		breq2	$$⊢k=X{+}_{f}Y\to \left(x{\le }_{f}k\leftrightarrow x{\le }_f\left(X{+}_{f}Y\right)\right)$$
140	139	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\}$$
141	140	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)$$
142	138 141	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)$$
143	142	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$$
144	143	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}$$
145	105 129 144	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)$$
146	104 145	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)$$
147	7	adantr	$$⊢\left(\phi \wedge k\in D\right)\to R\in \mathrm{Ring}$$
148		ringcmn	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{CMnd}$$
149	147 148	syl	$$⊢\left(\phi \wedge k\in D\right)\to R\in \mathrm{CMnd}$$
150	5	psrbaglefi	$$⊢\left(I\in W\wedge k\in D\right)\to \left\{x\in D|x{\le }_{f}k\right\}\in \mathrm{Fin}$$
151	6 150	sylan	$$⊢\left(\phi \wedge k\in D\right)\to \left\{x\in D|x{\le }_{f}k\right\}\in \mathrm{Fin}$$
152		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\}$$
153	31 152	ax-mp	$$⊢\left\{x\in D|x{\le }_{f}k\right\}\setminus \left\{X\right\}\subseteq D\setminus \left\{X\right\}$$
154	153	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)$$
155	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$$
156		eldifsni	$$⊢y\in \left(D\setminus \left\{X\right\}\right)\to y\ne X$$
157	156	adantl	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge y\in \left(D\setminus \left\{X\right\}\right)\right)\to y\ne X$$
158	157	neneqd	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge y\in \left(D\setminus \left\{X\right\}\right)\right)\to \neg y=X$$
159	158	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}$$
160		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
161	5 160	rabex2	$$⊢D\in \mathrm{V}$$
162	161	a1i	$$⊢\left(\phi \wedge k\in D\right)\to D\in \mathrm{V}$$
163	159 162	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\}$$
164	41	a1i	$$⊢\left(\phi \wedge k\in D\right)\to \underset{\dot{}}{0}\in \mathrm{V}$$
165	155 163 162 164	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}$$
166	154 165	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}$$
167	166	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)$$
168		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\}$$
169	46 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}$$
170	107 120 169	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}$$
171	168 170	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}$$
172	167 171	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}$$
173	161	rabex	$$⊢\left\{x\in D|x{\le }_{f}k\right\}\in \mathrm{V}$$
174	173	a1i	$$⊢\left(\phi \wedge k\in D\right)\to \left\{x\in D|x{\le }_{f}k\right\}\in \mathrm{V}$$
175	172 174	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\}$$
176	161	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}$$
177		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)$$
178	176 177 41	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)$$
179	178	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)$$
180		snfi	$$⊢\left\{X\right\}\in \mathrm{Fin}$$
181	180	a1i	$$⊢\left(\phi \wedge k\in D\right)\to \left\{X\right\}\in \mathrm{Fin}$$
182		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)$$
183	179 181 175 182	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)$$
184	46 3 149 151 123 175 183	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)$$
185	146 184	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)$$
186	185	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)$$
187	17 186	syl5eq	$$⊢\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)$$
188	14 187	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)$$