Theorem mdegaddle

Description: The degree of a sum is at most the maximum of the degrees of the factors. (Contributed by Stefan O'Rear, 26-Mar-2015)

	Ref	Expression
Hypotheses	mdegaddle.y	$$⊢Y=I\mathrm{mPoly}R$$
	mdegaddle.d	$$⊢D=I\mathrm{mDeg}R$$
	mdegaddle.i	$$⊢\phi \to I\in V$$
	mdegaddle.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	mdegaddle.b	$$⊢B={\mathrm{Base}}_Y$$
	mdegaddle.p	$$⊢\underset{\dot{}}{+}={+}_Y$$
	mdegaddle.f	$$⊢\phi \to F\in B$$
	mdegaddle.g	$$⊢\phi \to G\in B$$
Assertion	mdegaddle	$$⊢\phi \to D\left(F\underset{\dot{}}{+}G\right)\le if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mdegaddle.y	$$⊢Y=I\mathrm{mPoly}R$$
2		mdegaddle.d	$$⊢D=I\mathrm{mDeg}R$$
3		mdegaddle.i	$$⊢\phi \to I\in V$$
4		mdegaddle.r	$$⊢\phi \to R\in \mathrm{Ring}$$
5		mdegaddle.b	$$⊢B={\mathrm{Base}}_Y$$
6		mdegaddle.p	$$⊢\underset{\dot{}}{+}={+}_Y$$
7		mdegaddle.f	$$⊢\phi \to F\in B$$
8		mdegaddle.g	$$⊢\phi \to G\in B$$
9		eqid	$$⊢{+}_R={+}_R$$
10	1 5 9 6 7 8	mpladd	$$⊢\phi \to F\underset{\dot{}}{+}G=F{{+}_R}_{f}G$$
11	10	fveq1d	$$⊢\phi \to \left(F\underset{\dot{}}{+}G\right)\left(c\right)=\left(F{{+}_R}_{f}G\right)\left(c\right)$$
12	11	adantr	$$⊢\left(\phi \wedge c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(F\underset{\dot{}}{+}G\right)\left(c\right)=\left(F{{+}_R}_{f}G\right)\left(c\right)$$
13		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
14		eqid	$$⊢\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
15	1 13 5 14 7	mplelf	$$⊢\phi \to F:\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
16	15	ffnd	$$⊢\phi \to FFn\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
17	16	adantr	$$⊢\left(\phi \wedge c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to FFn\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
18	1 13 5 14 8	mplelf	$$⊢\phi \to G:\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathrm{Base}}_R$$
19	18	ffnd	$$⊢\phi \to GFn\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
20	19	adantr	$$⊢\left(\phi \wedge c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to GFn\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
21		ovex	$$⊢{{\mathbb{N}}_0}^I\in \mathrm{V}$$
22	21	rabex	$$⊢\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
23	22	a1i	$$⊢\left(\phi \wedge c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}$$
24		simpr	$$⊢\left(\phi \wedge c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
25		fnfvof	$$⊢\left(\left(FFn\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge GFn\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\wedge \left(\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\in \mathrm{V}\wedge c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\right)\to \left(F{{+}_R}_{f}G\right)\left(c\right)=F\left(c\right){+}_{R}G\left(c\right)$$
26	17 20 23 24 25	syl22anc	$$⊢\left(\phi \wedge c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(F{{+}_R}_{f}G\right)\left(c\right)=F\left(c\right){+}_{R}G\left(c\right)$$
27	12 26	eqtrd	$$⊢\left(\phi \wedge c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(F\underset{\dot{}}{+}G\right)\left(c\right)=F\left(c\right){+}_{R}G\left(c\right)$$
28	27	adantrr	$$⊢\left(\phi \wedge \left(c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)\right)\to \left(F\underset{\dot{}}{+}G\right)\left(c\right)=F\left(c\right){+}_{R}G\left(c\right)$$
29		eqid	$$⊢0_R=0_R$$
30		eqid	$$⊢\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)=\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)$$
31	7	adantr	$$⊢\left(\phi \wedge \left(c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)\right)\to F\in B$$
32		simprl	$$⊢\left(\phi \wedge \left(c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)\right)\to c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
33	2 1 5	mdegxrcl	$$⊢F\in B\to D\left(F\right)\in {ℝ}^{*}$$
34	7 33	syl	$$⊢\phi \to D\left(F\right)\in {ℝ}^{*}$$
35	34	adantr	$$⊢\left(\phi \wedge c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to D\left(F\right)\in {ℝ}^{*}$$
36	2 1 5	mdegxrcl	$$⊢G\in B\to D\left(G\right)\in {ℝ}^{*}$$
37	8 36	syl	$$⊢\phi \to D\left(G\right)\in {ℝ}^{*}$$
38	37 34	ifcld	$$⊢\phi \to if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\in {ℝ}^{*}$$
39	38	adantr	$$⊢\left(\phi \wedge c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\in {ℝ}^{*}$$
40		nn0ssre	$$⊢{\mathbb{N}}_0\subseteq ℝ$$
41		ressxr	$$⊢ℝ\subseteq {ℝ}^{*}$$
42	40 41	sstri	$$⊢{\mathbb{N}}_0\subseteq {ℝ}^{*}$$
43	14 30	tdeglem1	$$⊢I\in V\to \left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right):\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathbb{N}}_0$$
44	3 43	syl	$$⊢\phi \to \left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right):\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathbb{N}}_0$$
45	44	ffvelrnda	$$⊢\left(\phi \wedge c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\in {\mathbb{N}}_0$$
46	42 45	sseldi	$$⊢\left(\phi \wedge c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\in {ℝ}^{*}$$
47	35 39 46	3jca	$$⊢\left(\phi \wedge c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(D\left(F\right)\in {ℝ}^{*}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\in {ℝ}^{*}\wedge \left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\in {ℝ}^{*}\right)$$
48	47	adantrr	$$⊢\left(\phi \wedge \left(c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)\right)\to \left(D\left(F\right)\in {ℝ}^{*}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\in {ℝ}^{*}\wedge \left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\in {ℝ}^{*}\right)$$
49		xrmax1	$$⊢\left(D\left(F\right)\in {ℝ}^{*}\wedge D\left(G\right)\in {ℝ}^{*}\right)\to D\left(F\right)\le if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)$$
50	34 37 49	syl2anc	$$⊢\phi \to D\left(F\right)\le if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)$$
51	50	adantr	$$⊢\left(\phi \wedge \left(c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)\right)\to D\left(F\right)\le if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)$$
52		simprr	$$⊢\left(\phi \wedge \left(c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)\right)\to if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)$$
53	51 52	jca	$$⊢\left(\phi \wedge \left(c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)\right)\to \left(D\left(F\right)\le if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)$$
54		xrlelttr	$$⊢\left(D\left(F\right)\in {ℝ}^{*}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\in {ℝ}^{*}\wedge \left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\in {ℝ}^{*}\right)\to \left(\left(D\left(F\right)\le if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)\to D\left(F\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)$$
55	48 53 54	sylc	$$⊢\left(\phi \wedge \left(c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)\right)\to D\left(F\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)$$
56	2 1 5 29 14 30 31 32 55	mdeglt	$$⊢\left(\phi \wedge \left(c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)\right)\to F\left(c\right)=0_R$$
57	8	adantr	$$⊢\left(\phi \wedge \left(c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)\right)\to G\in B$$
58	37	adantr	$$⊢\left(\phi \wedge c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to D\left(G\right)\in {ℝ}^{*}$$
59	58 39 46	3jca	$$⊢\left(\phi \wedge c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(D\left(G\right)\in {ℝ}^{*}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\in {ℝ}^{*}\wedge \left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\in {ℝ}^{*}\right)$$
60	59	adantrr	$$⊢\left(\phi \wedge \left(c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)\right)\to \left(D\left(G\right)\in {ℝ}^{*}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\in {ℝ}^{*}\wedge \left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\in {ℝ}^{*}\right)$$
61		xrmax2	$$⊢\left(D\left(F\right)\in {ℝ}^{*}\wedge D\left(G\right)\in {ℝ}^{*}\right)\to D\left(G\right)\le if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)$$
62	34 37 61	syl2anc	$$⊢\phi \to D\left(G\right)\le if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)$$
63	62	adantr	$$⊢\left(\phi \wedge \left(c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)\right)\to D\left(G\right)\le if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)$$
64	63 52	jca	$$⊢\left(\phi \wedge \left(c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)\right)\to \left(D\left(G\right)\le if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)$$
65		xrlelttr	$$⊢\left(D\left(G\right)\in {ℝ}^{*}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\in {ℝ}^{*}\wedge \left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\in {ℝ}^{*}\right)\to \left(\left(D\left(G\right)\le if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)\to D\left(G\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)$$
66	60 64 65	sylc	$$⊢\left(\phi \wedge \left(c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)\right)\to D\left(G\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)$$
67	2 1 5 29 14 30 57 32 66	mdeglt	$$⊢\left(\phi \wedge \left(c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)\right)\to G\left(c\right)=0_R$$
68	56 67	oveq12d	$$⊢\left(\phi \wedge \left(c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)\right)\to F\left(c\right){+}_{R}G\left(c\right)=0_R{+}_R{0}_R$$
69		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
70	4 69	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
71	13 29	ring0cl	$$⊢R\in \mathrm{Ring}\to 0_R\in {\mathrm{Base}}_R$$
72	4 71	syl	$$⊢\phi \to 0_R\in {\mathrm{Base}}_R$$
73	13 9 29	grplid	$$⊢\left(R\in \mathrm{Grp}\wedge 0_R\in {\mathrm{Base}}_R\right)\to 0_R{+}_R{0}_R=0_R$$
74	70 72 73	syl2anc	$$⊢\phi \to 0_R{+}_R{0}_R=0_R$$
75	74	adantr	$$⊢\left(\phi \wedge \left(c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)\right)\to 0_R{+}_R{0}_R=0_R$$
76	68 75	eqtrd	$$⊢\left(\phi \wedge \left(c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)\right)\to F\left(c\right){+}_{R}G\left(c\right)=0_R$$
77	28 76	eqtrd	$$⊢\left(\phi \wedge \left(c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\right)\right)\to \left(F\underset{\dot{}}{+}G\right)\left(c\right)=0_R$$
78	77	expr	$$⊢\left(\phi \wedge c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\to \left(F\underset{\dot{}}{+}G\right)\left(c\right)=0_R\right)$$
79	78	ralrimiva	$$⊢\phi \to \forall c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\to \left(F\underset{\dot{}}{+}G\right)\left(c\right)=0_R\right)$$
80	1	mplring	$$⊢\left(I\in V\wedge R\in \mathrm{Ring}\right)\to Y\in \mathrm{Ring}$$
81	3 4 80	syl2anc	$$⊢\phi \to Y\in \mathrm{Ring}$$
82	5 6	ringacl	$$⊢\left(Y\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to F\underset{\dot{}}{+}G\in B$$
83	81 7 8 82	syl3anc	$$⊢\phi \to F\underset{\dot{}}{+}G\in B$$
84	2 1 5 29 14 30	mdegleb	$$⊢\left(F\underset{\dot{}}{+}G\in B\wedge if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\in {ℝ}^{*}\right)\to \left(D\left(F\underset{\dot{}}{+}G\right)\le if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\leftrightarrow \forall c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\to \left(F\underset{\dot{}}{+}G\right)\left(c\right)=0_R\right)\right)$$
85	83 38 84	syl2anc	$$⊢\phi \to \left(D\left(F\underset{\dot{}}{+}G\right)\le if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\leftrightarrow \forall c\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)<\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left(c\right)\to \left(F\underset{\dot{}}{+}G\right)\left(c\right)=0_R\right)\right)$$
86	79 85	mpbird	$$⊢\phi \to D\left(F\underset{\dot{}}{+}G\right)\le if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)$$