Theorem psrmonmul

Description: The product of two power series 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 Thierry Arnoux, 16-Mar-2026)

	Ref	Expression
Hypotheses	psrmon.s	$$⊢S=I\mathrm{mPwSer}R$$
	psrmon.b	$$⊢B={\mathrm{Base}}_S$$
	psrmon.z	$$⊢\underset{\dot{}}{0}=0_R$$
	psrmon.o	$$⊢\underset{\dot{}}{1}=1_R$$
	psrmon.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
	psrmon.i	$$⊢\phi \to I\in W$$
	psrmon.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	psrmon.x	$$⊢\phi \to X\in D$$
	psrmonmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
	psrmonmul.y	$$⊢\phi \to Y\in D$$
Assertion	psrmonmul	$$⊢\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		psrmon.s	$$⊢S=I\mathrm{mPwSer}R$$
2		psrmon.b	$$⊢B={\mathrm{Base}}_S$$
3		psrmon.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		psrmon.o	$$⊢\underset{\dot{}}{1}=1_R$$
5		psrmon.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
6		psrmon.i	$$⊢\phi \to I\in W$$
7		psrmon.r	$$⊢\phi \to R\in \mathrm{Ring}$$
8		psrmon.x	$$⊢\phi \to X\in D$$
9		psrmonmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_S$$
10		psrmonmul.y	$$⊢\phi \to Y\in D$$
11		eqid	$$⊢{\cdot }_R={\cdot }_R$$
12	5	psrbasfsupp	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
13	1 2 3 4 5 6 7 8	psrmon	$$⊢\phi \to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in B$$
14	1 2 3 4 5 6 7 10	psrmon	$$⊢\phi \to \left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\in B$$
15	1 2 11 9 12 13 14	psrmulfval	$$⊢\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)$$
16		eqeq1	$$⊢y=k\to \left(y=X{+}_{f}Y\leftrightarrow k=X{+}_{f}Y\right)$$
17	16	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)$$
18	17	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)$$
19		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\}$$
20	19	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\}$$
21	20	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)$$
22	21	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)$$
23	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}$$
24		ringmnd	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Mnd}$$
25	23 24	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}$$
26	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$$
27		iftrue	$$⊢y=X\to if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=\underset{\dot{}}{1}$$
28		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)$$
29	4	fvexi	$$⊢\underset{\dot{}}{1}\in \mathrm{V}$$
30	27 28 29	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}$$
31	26 30	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}$$
32		ssrab2	$$⊢\left\{x\in D|x{\le }_{f}k\right\}\subseteq D$$
33		eqid	$$⊢\left\{x\in D|x{\le }_{f}k\right\}=\left\{x\in D|x{\le }_{f}k\right\}$$
34	12 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	34	adantll	$$⊢\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	32 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	29 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	31 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	23 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 23 49	ringlidmd	$$⊢\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)$$
51	12	psrbagf	$$⊢k\in D\to k:I⟶{\mathbb{N}}_0$$
52	51	ad2antlr	$$⊢\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$$
53	52	ffvelcdmda	$$⊢\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$$
54	8	adantr	$$⊢\left(\phi \wedge k\in D\right)\to X\in D$$
55	12	psrbagf	$$⊢X\in D\to X:I⟶{\mathbb{N}}_0$$
56	54 55	syl	$$⊢\left(\phi \wedge k\in D\right)\to X:I⟶{\mathbb{N}}_0$$
57	56	ffvelcdmda	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge z\in I\right)\to X\left(z\right)\in {\mathbb{N}}_0$$
58	57	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$$
59	12	psrbagf	$$⊢Y\in D\to Y:I⟶{\mathbb{N}}_0$$
60	10 59	syl	$$⊢\phi \to Y:I⟶{\mathbb{N}}_0$$
61	60	adantr	$$⊢\left(\phi \wedge k\in D\right)\to Y:I⟶{\mathbb{N}}_0$$
62	61	ffvelcdmda	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge z\in I\right)\to Y\left(z\right)\in {\mathbb{N}}_0$$
63	62	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$$
64		nn0cn	$$⊢k\left(z\right)\in {\mathbb{N}}_0\to k\left(z\right)\in ℂ$$
65		nn0cn	$$⊢X\left(z\right)\in {\mathbb{N}}_0\to X\left(z\right)\in ℂ$$
66		nn0cn	$$⊢Y\left(z\right)\in {\mathbb{N}}_0\to Y\left(z\right)\in ℂ$$
67		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)$$
68	64 65 66 67	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)$$
69	53 58 63 68	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)$$
70		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)$$
71	69 70	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)$$
72	71	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)$$
73		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)$$
74		ovexd	$$⊢z\in I\to k\left(z\right)-X\left(z\right)\in \mathrm{V}$$
75	73 74	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)$$
76		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)$$
77		fvexd	$$⊢z\in I\to k\left(z\right)\in \mathrm{V}$$
78	76 77	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)$$
79	72 75 78	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)$$
80	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$$
81	52	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)$$
82	56	feqmptd	$$⊢\left(\phi \wedge k\in D\right)\to X=\left(z\in I⟼X\left(z\right)\right)$$
83	82	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)$$
84	80 53 58 81 83	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)$$
85	61	feqmptd	$$⊢\left(\phi \wedge k\in D\right)\to Y=\left(z\in I⟼Y\left(z\right)\right)$$
86	85	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)$$
87	84 86	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)$$
88	6	adantr	$$⊢\left(\phi \wedge k\in D\right)\to I\in W$$
89	88 57 62 82 85	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)$$
90	89	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)$$
91	81 90	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)$$
92	79 87 91	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)$$
93	92	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)$$
94	44 50 93	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)$$
95	93 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$$
96	94 95	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$$
97		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)$$
98		oveq2	$$⊢j=X\to k{-}_{f}j=k{-}_{f}X$$
99	98	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)$$
100	97 99	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)$$
101	45 100	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)$$
102	25 26 96 101	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)$$
103	22 102 94	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)$$
104	3	gsum0	$$⊢{\sum }_R\varnothing =\underset{\dot{}}{0}$$
105		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\}$$
106	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}$$
107	1 45 12 2 13	psrelbas	$$⊢\phi \to \left(y\in D⟼if\left(y=X,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right):D⟶{\mathrm{Base}}_R$$
108	107	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$$
109		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\}$$
110	32 109	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$$
111	108 110	ffvelcdmd	$$⊢\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$$
112	1 45 12 2 14	psrelbas	$$⊢\phi \to \left(y\in D⟼if\left(y=Y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right):D⟶{\mathrm{Base}}_R$$
113	112	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$$
114	12 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\}$$
115	114	adantll	$$⊢\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\}$$
116	32 115	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$$
117	113 116	ffvelcdmd	$$⊢\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$$
118	45 11 106 111 117	ringcld	$$⊢\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$$
119	118	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$$
120		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\}$$
121		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)$$
122	119 120 121	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)$$
123	122	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$$
124	105 123	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$$
125	124	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$$
126		breq1	$$⊢x=X\to \left(x{\le }_f\left(X{+}_{f}Y\right)\leftrightarrow X{\le }_f\left(X{+}_{f}Y\right)\right)$$
127	57	nn0red	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge z\in I\right)\to X\left(z\right)\in ℝ$$
128		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)$$
129	127 62 128	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)$$
130	129	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)$$
131		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}$$
132	88 57 131 82 89	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)$$
133	130 132	mpbird	$$⊢\left(\phi \wedge k\in D\right)\to X{\le }_f\left(X{+}_{f}Y\right)$$
134	126 54 133	elrabd	$$⊢\left(\phi \wedge k\in D\right)\to X\in \left\{x\in D|x{\le }_f\left(X{+}_{f}Y\right)\right\}$$
135		breq2	$$⊢k=X{+}_{f}Y\to \left(x{\le }_{f}k\leftrightarrow x{\le }_f\left(X{+}_{f}Y\right)\right)$$
136	135	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\}$$
137	136	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)$$
138	134 137	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)$$
139	138	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$$
140	139	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}$$
141	104 125 140	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)$$
142	103 141	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)$$
143	7	adantr	$$⊢\left(\phi \wedge k\in D\right)\to R\in \mathrm{Ring}$$
144	143	ringcmnd	$$⊢\left(\phi \wedge k\in D\right)\to R\in \mathrm{CMnd}$$
145	12	psrbaglefi	$$⊢k\in D\to \left\{x\in D|x{\le }_{f}k\right\}\in \mathrm{Fin}$$
146	145	adantl	$$⊢\left(\phi \wedge k\in D\right)\to \left\{x\in D|x{\le }_{f}k\right\}\in \mathrm{Fin}$$
147		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\}$$
148	32 147	ax-mp	$$⊢\left\{x\in D|x{\le }_{f}k\right\}\setminus \left\{X\right\}\subseteq D\setminus \left\{X\right\}$$
149	148	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)$$
150	107	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$$
151		eldifsni	$$⊢y\in \left(D\setminus \left\{X\right\}\right)\to y\ne X$$
152	151	adantl	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge y\in \left(D\setminus \left\{X\right\}\right)\right)\to y\ne X$$
153	152	neneqd	$$⊢\left(\left(\phi \wedge k\in D\right)\wedge y\in \left(D\setminus \left\{X\right\}\right)\right)\to \neg y=X$$
154	153	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}$$
155		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
156	5 155	rabex2	$$⊢D\in \mathrm{V}$$
157	156	a1i	$$⊢\left(\phi \wedge k\in D\right)\to D\in \mathrm{V}$$
158	154 157	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\}$$
159	40	a1i	$$⊢\left(\phi \wedge k\in D\right)\to \underset{\dot{}}{0}\in \mathrm{V}$$
160	150 158 157 159	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}$$
161	149 160	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}$$
162	161	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)$$
163		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\}$$
164	45 11 3 106 117	ringlzd	$$⊢\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}$$
165	163 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 \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}$$
166	162 165	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}$$
167	156	rabex	$$⊢\left\{x\in D|x{\le }_{f}k\right\}\in \mathrm{V}$$
168	167	a1i	$$⊢\left(\phi \wedge k\in D\right)\to \left\{x\in D|x{\le }_{f}k\right\}\in \mathrm{V}$$
169	166 168	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\}$$
170	156	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}$$
171		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)$$
172	170 171 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)$$
173	172	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)$$
174		snfi	$$⊢\left\{X\right\}\in \mathrm{Fin}$$
175	174	a1i	$$⊢\left(\phi \wedge k\in D\right)\to \left\{X\right\}\in \mathrm{Fin}$$
176		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)$$
177	173 175 169 176	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)$$
178	45 3 144 146 119 169 177	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)$$
179	142 178	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)$$
180	179	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)$$
181	18 180	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)$$
182	15 181	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)$$