ply1divex

Description: Lemma for ply1divalg : existence part. (Contributed by Stefan O'Rear, 27-Mar-2015)

	Ref	Expression
Hypotheses	ply1divalg.p	$⊢ P = {Poly}_{1} (R)$
	ply1divalg.d	$⊢ D = \deg_{1} (R)$
	ply1divalg.b	$⊢ B = {Base}_{P}$
	ply1divalg.m	$⊢ \underset{˙}{-} = -_{P}$
	ply1divalg.z	$⊢ \underset{˙}{0} = 0_{P}$
	ply1divalg.t	$⊢ \underset{˙}{∙} = \cdot_{P}$
	ply1divalg.r1	$⊢ φ \to R \in Ring$
	ply1divalg.f	$⊢ φ \to F \in B$
	ply1divalg.g1	$⊢ φ \to G \in B$
	ply1divalg.g2	$⊢ φ \to G \neq \underset{˙}{0}$
	ply1divex.o	$⊢ \underset{˙}{1} = 1_{R}$
	ply1divex.k	$⊢ K = {Base}_{R}$
	ply1divex.u	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	ply1divex.i	$⊢ φ \to I \in K$
	ply1divex.g3	$⊢ φ \to {coe}_{1} (G) (D (G)) \underset{˙}{\cdot} I = \underset{˙}{1}$
Assertion	ply1divex	$⊢ φ \to \exists q \in B D (F \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)$

Proof

Step	Hyp	Ref	Expression
1		ply1divalg.p	$⊢ P = {Poly}_{1} (R)$
2		ply1divalg.d	$⊢ D = \deg_{1} (R)$
3		ply1divalg.b	$⊢ B = {Base}_{P}$
4		ply1divalg.m	$⊢ \underset{˙}{-} = -_{P}$
5		ply1divalg.z	$⊢ \underset{˙}{0} = 0_{P}$
6		ply1divalg.t	$⊢ \underset{˙}{∙} = \cdot_{P}$
7		ply1divalg.r1	$⊢ φ \to R \in Ring$
8		ply1divalg.f	$⊢ φ \to F \in B$
9		ply1divalg.g1	$⊢ φ \to G \in B$
10		ply1divalg.g2	$⊢ φ \to G \neq \underset{˙}{0}$
11		ply1divex.o	$⊢ \underset{˙}{1} = 1_{R}$
12		ply1divex.k	$⊢ K = {Base}_{R}$
13		ply1divex.u	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
14		ply1divex.i	$⊢ φ \to I \in K$
15		ply1divex.g3	$⊢ φ \to {coe}_{1} (G) (D (G)) \underset{˙}{\cdot} I = \underset{˙}{1}$
16		fveq2	$⊢ F = \underset{˙}{0} \to D (F) = D (\underset{˙}{0})$
17	16	breq1d	$⊢ F = \underset{˙}{0} \to (D (F) < D (G) + d \leftrightarrow D (\underset{˙}{0}) < D (G) + d)$
18	17	rexbidv	$⊢ F = \underset{˙}{0} \to (\exists d \in ℕ_{0} D (F) < D (G) + d \leftrightarrow \exists d \in ℕ_{0} D (\underset{˙}{0}) < D (G) + d)$
19		nnssnn0	$⊢ ℕ \subseteq ℕ_{0}$
20	7	adantr	$⊢ (φ \land F \neq \underset{˙}{0}) \to R \in Ring$
21	8	adantr	$⊢ (φ \land F \neq \underset{˙}{0}) \to F \in B$
22		simpr	$⊢ (φ \land F \neq \underset{˙}{0}) \to F \neq \underset{˙}{0}$
23	2 1 5 3	deg1nn0cl	$⊢ (R \in Ring \land F \in B \land F \neq \underset{˙}{0}) \to D (F) \in ℕ_{0}$
24	20 21 22 23	syl3anc	$⊢ (φ \land F \neq \underset{˙}{0}) \to D (F) \in ℕ_{0}$
25	24	nn0red	$⊢ (φ \land F \neq \underset{˙}{0}) \to D (F) \in ℝ$
26	2 1 5 3	deg1nn0cl	$⊢ (R \in Ring \land G \in B \land G \neq \underset{˙}{0}) \to D (G) \in ℕ_{0}$
27	7 9 10 26	syl3anc	$⊢ φ \to D (G) \in ℕ_{0}$
28	27	nn0red	$⊢ φ \to D (G) \in ℝ$
29	28	adantr	$⊢ (φ \land F \neq \underset{˙}{0}) \to D (G) \in ℝ$
30	25 29	resubcld	$⊢ (φ \land F \neq \underset{˙}{0}) \to D (F) - D (G) \in ℝ$
31		arch	$⊢ D (F) - D (G) \in ℝ \to \exists d \in ℕ D (F) - D (G) < d$
32	30 31	syl	$⊢ (φ \land F \neq \underset{˙}{0}) \to \exists d \in ℕ D (F) - D (G) < d$
33		ssrexv	$⊢ ℕ \subseteq ℕ_{0} \to (\exists d \in ℕ D (F) - D (G) < d \to \exists d \in ℕ_{0} D (F) - D (G) < d)$
34	19 32 33	mpsyl	$⊢ (φ \land F \neq \underset{˙}{0}) \to \exists d \in ℕ_{0} D (F) - D (G) < d$
35	25	adantr	$⊢ ((φ \land F \neq \underset{˙}{0}) \land d \in ℕ_{0}) \to D (F) \in ℝ$
36	28	ad2antrr	$⊢ ((φ \land F \neq \underset{˙}{0}) \land d \in ℕ_{0}) \to D (G) \in ℝ$
37		nn0re	$⊢ d \in ℕ_{0} \to d \in ℝ$
38	37	adantl	$⊢ ((φ \land F \neq \underset{˙}{0}) \land d \in ℕ_{0}) \to d \in ℝ$
39	35 36 38	ltsubadd2d	$⊢ ((φ \land F \neq \underset{˙}{0}) \land d \in ℕ_{0}) \to (D (F) - D (G) < d \leftrightarrow D (F) < D (G) + d)$
40	39	biimpd	$⊢ ((φ \land F \neq \underset{˙}{0}) \land d \in ℕ_{0}) \to (D (F) - D (G) < d \to D (F) < D (G) + d)$
41	40	reximdva	$⊢ (φ \land F \neq \underset{˙}{0}) \to (\exists d \in ℕ_{0} D (F) - D (G) < d \to \exists d \in ℕ_{0} D (F) < D (G) + d)$
42	34 41	mpd	$⊢ (φ \land F \neq \underset{˙}{0}) \to \exists d \in ℕ_{0} D (F) < D (G) + d$
43		0nn0	$⊢ 0 \in ℕ_{0}$
44	2 1 5	deg1z	$⊢ R \in Ring \to D (\underset{˙}{0}) = −∞$
45	7 44	syl	$⊢ φ \to D (\underset{˙}{0}) = −∞$
46		0re	$⊢ 0 \in ℝ$
47		readdcl	$⊢ (D (G) \in ℝ \land 0 \in ℝ) \to D (G) + 0 \in ℝ$
48	28 46 47	sylancl	$⊢ φ \to D (G) + 0 \in ℝ$
49	48	mnfltd	$⊢ φ \to −∞ < D (G) + 0$
50	45 49	eqbrtrd	$⊢ φ \to D (\underset{˙}{0}) < D (G) + 0$
51		oveq2	$⊢ d = 0 \to D (G) + d = D (G) + 0$
52	51	breq2d	$⊢ d = 0 \to (D (\underset{˙}{0}) < D (G) + d \leftrightarrow D (\underset{˙}{0}) < D (G) + 0)$
53	52	rspcev	$⊢ (0 \in ℕ_{0} \land D (\underset{˙}{0}) < D (G) + 0) \to \exists d \in ℕ_{0} D (\underset{˙}{0}) < D (G) + d$
54	43 50 53	sylancr	$⊢ φ \to \exists d \in ℕ_{0} D (\underset{˙}{0}) < D (G) + d$
55	18 42 54	pm2.61ne	$⊢ φ \to \exists d \in ℕ_{0} D (F) < D (G) + d$
56		fveq2	$⊢ f = F \to D (f) = D (F)$
57	56	breq1d	$⊢ f = F \to (D (f) < D (G) + d \leftrightarrow D (F) < D (G) + d)$
58		fvoveq1	$⊢ f = F \to D (f \underset{˙}{-} (G \underset{˙}{∙} q)) = D (F \underset{˙}{-} (G \underset{˙}{∙} q))$
59	58	breq1d	$⊢ f = F \to (D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \leftrightarrow D (F \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))$
60	59	rexbidv	$⊢ f = F \to (\exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \leftrightarrow \exists q \in B D (F \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))$
61	57 60	imbi12d	$⊢ f = F \to ((D (f) < D (G) + d \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)) \leftrightarrow (D (F) < D (G) + d \to \exists q \in B D (F \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)))$
62		oveq2	$⊢ a = 0 \to D (G) + a = D (G) + 0$
63	62	breq2d	$⊢ a = 0 \to (D (f) < D (G) + a \leftrightarrow D (f) < D (G) + 0)$
64	63	imbi1d	$⊢ a = 0 \to ((D (f) < D (G) + a \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)) \leftrightarrow (D (f) < D (G) + 0 \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)))$
65	64	ralbidv	$⊢ a = 0 \to (\forall f \in B (D (f) < D (G) + a \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)) \leftrightarrow \forall f \in B (D (f) < D (G) + 0 \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)))$
66	65	imbi2d	$⊢ a = 0 \to ((φ \to \forall f \in B (D (f) < D (G) + a \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))) \leftrightarrow (φ \to \forall f \in B (D (f) < D (G) + 0 \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))))$
67		oveq2	$⊢ a = d \to D (G) + a = D (G) + d$
68	67	breq2d	$⊢ a = d \to (D (f) < D (G) + a \leftrightarrow D (f) < D (G) + d)$
69	68	imbi1d	$⊢ a = d \to ((D (f) < D (G) + a \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)) \leftrightarrow (D (f) < D (G) + d \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)))$
70	69	ralbidv	$⊢ a = d \to (\forall f \in B (D (f) < D (G) + a \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)) \leftrightarrow \forall f \in B (D (f) < D (G) + d \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)))$
71	70	imbi2d	$⊢ a = d \to ((φ \to \forall f \in B (D (f) < D (G) + a \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))) \leftrightarrow (φ \to \forall f \in B (D (f) < D (G) + d \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))))$
72		oveq2	$⊢ a = d + 1 \to D (G) + a = D (G) + d + 1$
73	72	breq2d	$⊢ a = d + 1 \to (D (f) < D (G) + a \leftrightarrow D (f) < D (G) + d + 1)$
74	73	imbi1d	$⊢ a = d + 1 \to ((D (f) < D (G) + a \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)) \leftrightarrow (D (f) < D (G) + d + 1 \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)))$
75	74	ralbidv	$⊢ a = d + 1 \to (\forall f \in B (D (f) < D (G) + a \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)) \leftrightarrow \forall f \in B (D (f) < D (G) + d + 1 \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)))$
76	75	imbi2d	$⊢ a = d + 1 \to ((φ \to \forall f \in B (D (f) < D (G) + a \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))) \leftrightarrow (φ \to \forall f \in B (D (f) < D (G) + d + 1 \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))))$
77	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
78	7 77	syl	$⊢ φ \to P \in Ring$
79	3 5	ring0cl	$⊢ P \in Ring \to \underset{˙}{0} \in B$
80	78 79	syl	$⊢ φ \to \underset{˙}{0} \in B$
81	80	ad2antrr	$⊢ ((φ \land f \in B) \land D (f) < D (G) + 0) \to \underset{˙}{0} \in B$
82	3 6 5	ringrz	$⊢ (P \in Ring \land G \in B) \to G \underset{˙}{∙} \underset{˙}{0} = \underset{˙}{0}$
83	78 9 82	syl2anc	$⊢ φ \to G \underset{˙}{∙} \underset{˙}{0} = \underset{˙}{0}$
84	83	oveq2d	$⊢ φ \to f \underset{˙}{-} (G \underset{˙}{∙} \underset{˙}{0}) = f \underset{˙}{-} \underset{˙}{0}$
85	84	adantr	$⊢ (φ \land f \in B) \to f \underset{˙}{-} (G \underset{˙}{∙} \underset{˙}{0}) = f \underset{˙}{-} \underset{˙}{0}$
86		ringgrp	$⊢ P \in Ring \to P \in Grp$
87	78 86	syl	$⊢ φ \to P \in Grp$
88	3 5 4	grpsubid1	$⊢ (P \in Grp \land f \in B) \to f \underset{˙}{-} \underset{˙}{0} = f$
89	87 88	sylan	$⊢ (φ \land f \in B) \to f \underset{˙}{-} \underset{˙}{0} = f$
90	85 89	eqtr2d	$⊢ (φ \land f \in B) \to f = f \underset{˙}{-} (G \underset{˙}{∙} \underset{˙}{0})$
91	90	fveq2d	$⊢ (φ \land f \in B) \to D (f) = D (f \underset{˙}{-} (G \underset{˙}{∙} \underset{˙}{0}))$
92	27	nn0cnd	$⊢ φ \to D (G) \in ℂ$
93	92	addridd	$⊢ φ \to D (G) + 0 = D (G)$
94	93	adantr	$⊢ (φ \land f \in B) \to D (G) + 0 = D (G)$
95	91 94	breq12d	$⊢ (φ \land f \in B) \to (D (f) < D (G) + 0 \leftrightarrow D (f \underset{˙}{-} (G \underset{˙}{∙} \underset{˙}{0})) < D (G))$
96	95	biimpa	$⊢ ((φ \land f \in B) \land D (f) < D (G) + 0) \to D (f \underset{˙}{-} (G \underset{˙}{∙} \underset{˙}{0})) < D (G)$
97		oveq2	$⊢ q = \underset{˙}{0} \to G \underset{˙}{∙} q = G \underset{˙}{∙} \underset{˙}{0}$
98	97	oveq2d	$⊢ q = \underset{˙}{0} \to f \underset{˙}{-} (G \underset{˙}{∙} q) = f \underset{˙}{-} (G \underset{˙}{∙} \underset{˙}{0})$
99	98	fveq2d	$⊢ q = \underset{˙}{0} \to D (f \underset{˙}{-} (G \underset{˙}{∙} q)) = D (f \underset{˙}{-} (G \underset{˙}{∙} \underset{˙}{0}))$
100	99	breq1d	$⊢ q = \underset{˙}{0} \to (D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \leftrightarrow D (f \underset{˙}{-} (G \underset{˙}{∙} \underset{˙}{0})) < D (G))$
101	100	rspcev	$⊢ (\underset{˙}{0} \in B \land D (f \underset{˙}{-} (G \underset{˙}{∙} \underset{˙}{0})) < D (G)) \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)$
102	81 96 101	syl2anc	$⊢ ((φ \land f \in B) \land D (f) < D (G) + 0) \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)$
103	102	ex	$⊢ (φ \land f \in B) \to (D (f) < D (G) + 0 \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))$
104	103	ralrimiva	$⊢ φ \to \forall f \in B (D (f) < D (G) + 0 \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))$
105		nn0addcl	$⊢ (D (G) \in ℕ_{0} \land d \in ℕ_{0}) \to D (G) + d \in ℕ_{0}$
106	27 105	sylan	$⊢ (φ \land d \in ℕ_{0}) \to D (G) + d \in ℕ_{0}$
107	106	adantr	$⊢ ((φ \land d \in ℕ_{0}) \land (g \in B \land D (g) < D (G) + d + 1)) \to D (G) + d \in ℕ_{0}$
108	7	ad2antrr	$⊢ ((φ \land d \in ℕ_{0}) \land (g \in B \land D (g) < D (G) + d + 1)) \to R \in Ring$
109		simprl	$⊢ ((φ \land d \in ℕ_{0}) \land (g \in B \land D (g) < D (G) + d + 1)) \to g \in B$
110	2 1 3	deg1cl	$⊢ g \in B \to D (g) \in (ℕ_{0} \cup \{−∞\})$
111	27	ad2antrr	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to D (G) \in ℕ_{0}$
112		peano2nn0	$⊢ d \in ℕ_{0} \to d + 1 \in ℕ_{0}$
113	112	ad2antlr	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to d + 1 \in ℕ_{0}$
114	111 113	nn0addcld	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to D (G) + d + 1 \in ℕ_{0}$
115	114	nn0zd	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to D (G) + d + 1 \in ℤ$
116		degltlem1	$⊢ (D (g) \in (ℕ_{0} \cup \{−∞\}) \land D (G) + d + 1 \in ℤ) \to (D (g) < D (G) + d + 1 \leftrightarrow D (g) \leq D (G) + (d + 1) - 1)$
117	110 115 116	syl2an2	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to (D (g) < D (G) + d + 1 \leftrightarrow D (g) \leq D (G) + (d + 1) - 1)$
118	117	biimpd	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to (D (g) < D (G) + d + 1 \to D (g) \leq D (G) + (d + 1) - 1)$
119	118	impr	$⊢ ((φ \land d \in ℕ_{0}) \land (g \in B \land D (g) < D (G) + d + 1)) \to D (g) \leq D (G) + (d + 1) - 1$
120	27	adantr	$⊢ (φ \land d \in ℕ_{0}) \to D (G) \in ℕ_{0}$
121	120	nn0cnd	$⊢ (φ \land d \in ℕ_{0}) \to D (G) \in ℂ$
122		nn0cn	$⊢ d \in ℕ_{0} \to d \in ℂ$
123	122	adantl	$⊢ (φ \land d \in ℕ_{0}) \to d \in ℂ$
124		peano2cn	$⊢ d \in ℂ \to d + 1 \in ℂ$
125	123 124	syl	$⊢ (φ \land d \in ℕ_{0}) \to d + 1 \in ℂ$
126		1cnd	$⊢ (φ \land d \in ℕ_{0}) \to 1 \in ℂ$
127	121 125 126	addsubassd	$⊢ (φ \land d \in ℕ_{0}) \to D (G) + (d + 1) - 1 = D (G) + (d + 1) - 1$
128		ax-1cn	$⊢ 1 \in ℂ$
129		pncan	$⊢ (d \in ℂ \land 1 \in ℂ) \to d + 1 - 1 = d$
130	123 128 129	sylancl	$⊢ (φ \land d \in ℕ_{0}) \to d + 1 - 1 = d$
131	130	oveq2d	$⊢ (φ \land d \in ℕ_{0}) \to D (G) + (d + 1) - 1 = D (G) + d$
132	127 131	eqtrd	$⊢ (φ \land d \in ℕ_{0}) \to D (G) + (d + 1) - 1 = D (G) + d$
133	132	adantr	$⊢ ((φ \land d \in ℕ_{0}) \land (g \in B \land D (g) < D (G) + d + 1)) \to D (G) + (d + 1) - 1 = D (G) + d$
134	119 133	breqtrd	$⊢ ((φ \land d \in ℕ_{0}) \land (g \in B \land D (g) < D (G) + d + 1)) \to D (g) \leq D (G) + d$
135	78	ad2antrr	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to P \in Ring$
136	9	ad2antrr	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to G \in B$
137	7	ad2antrr	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to R \in Ring$
138	14	ad2antrr	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to I \in K$
139		eqid	$⊢ {coe}_{1} (g) = {coe}_{1} (g)$
140	139 3 1 12	coe1f	$⊢ g \in B \to {coe}_{1} (g) : ℕ_{0} ⟶ K$
141	140	adantl	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to {coe}_{1} (g) : ℕ_{0} ⟶ K$
142		simplr	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to d \in ℕ_{0}$
143	111 142	nn0addcld	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to D (G) + d \in ℕ_{0}$
144	141 143	ffvelcdmd	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to {coe}_{1} (g) (D (G) + d) \in K$
145	12 13	ringcl	$⊢ (R \in Ring \land I \in K \land {coe}_{1} (g) (D (G) + d) \in K) \to I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d) \in K$
146	137 138 144 145	syl3anc	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d) \in K$
147		eqid	$⊢ {var}_{1} (R) = {var}_{1} (R)$
148		eqid	$⊢ \cdot_{P} = \cdot_{P}$
149		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
150		eqid	$⊢ \cdot_{{mulGrp}_{P}} = \cdot_{{mulGrp}_{P}}$
151	12 1 147 148 149 150 3	ply1tmcl	$⊢ (R \in Ring \land I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d) \in K \land d \in ℕ_{0}) \to (I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \in B$
152	137 146 142 151	syl3anc	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to (I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \in B$
153	3 6	ringcl	$⊢ (P \in Ring \land G \in B \land (I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \in B) \to G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))) \in B$
154	135 136 152 153	syl3anc	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))) \in B$
155	154	adantrr	$⊢ ((φ \land d \in ℕ_{0}) \land (g \in B \land D (g) < D (G) + d + 1)) \to G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))) \in B$
156	111	nn0red	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to D (G) \in ℝ$
157	156	leidd	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to D (G) \leq D (G)$
158	2 12 1 147 148 149 150	deg1tmle	$⊢ (R \in Ring \land I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d) \in K \land d \in ℕ_{0}) \to D ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))) \leq d$
159	137 146 142 158	syl3anc	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to D ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))) \leq d$
160	1 2 137 3 6 136 152 111 142 157 159	deg1mulle2	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to D (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) \leq D (G) + d$
161	160	adantrr	$⊢ ((φ \land d \in ℕ_{0}) \land (g \in B \land D (g) < D (G) + d + 1)) \to D (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) \leq D (G) + d$
162		eqid	$⊢ {coe}_{1} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) = {coe}_{1} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))$
163		eqid	$⊢ 0_{R} = 0_{R}$
164	163 12 1 147 148 149 150 3 6 13 136 137 146 142 111	coe1tmmul2fv	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to {coe}_{1} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) (d + D (G)) = {coe}_{1} (G) (D (G)) \underset{˙}{\cdot} (I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d))$
165	111	nn0cnd	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to D (G) \in ℂ$
166	122	ad2antlr	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to d \in ℂ$
167	165 166	addcomd	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to D (G) + d = d + D (G)$
168	167	fveq2d	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to {coe}_{1} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) (D (G) + d) = {coe}_{1} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) (d + D (G))$
169	15	oveq1d	$⊢ φ \to ({coe}_{1} (G) (D (G)) \underset{˙}{\cdot} I) \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d) = \underset{˙}{1} \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)$
170	169	ad2antrr	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to ({coe}_{1} (G) (D (G)) \underset{˙}{\cdot} I) \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d) = \underset{˙}{1} \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)$
171		eqid	$⊢ {coe}_{1} (G) = {coe}_{1} (G)$
172	171 3 1 12	coe1f	$⊢ G \in B \to {coe}_{1} (G) : ℕ_{0} ⟶ K$
173	9 172	syl	$⊢ φ \to {coe}_{1} (G) : ℕ_{0} ⟶ K$
174	173	ad2antrr	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to {coe}_{1} (G) : ℕ_{0} ⟶ K$
175	174 111	ffvelcdmd	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to {coe}_{1} (G) (D (G)) \in K$
176	12 13	ringass	$⊢ (R \in Ring \land ({coe}_{1} (G) (D (G)) \in K \land I \in K \land {coe}_{1} (g) (D (G) + d) \in K)) \to ({coe}_{1} (G) (D (G)) \underset{˙}{\cdot} I) \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d) = {coe}_{1} (G) (D (G)) \underset{˙}{\cdot} (I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d))$
177	137 175 138 144 176	syl13anc	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to ({coe}_{1} (G) (D (G)) \underset{˙}{\cdot} I) \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d) = {coe}_{1} (G) (D (G)) \underset{˙}{\cdot} (I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d))$
178	12 13 11	ringlidm	$⊢ (R \in Ring \land {coe}_{1} (g) (D (G) + d) \in K) \to \underset{˙}{1} \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d) = {coe}_{1} (g) (D (G) + d)$
179	137 144 178	syl2anc	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to \underset{˙}{1} \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d) = {coe}_{1} (g) (D (G) + d)$
180	170 177 179	3eqtr3rd	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to {coe}_{1} (g) (D (G) + d) = {coe}_{1} (G) (D (G)) \underset{˙}{\cdot} (I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d))$
181	164 168 180	3eqtr4rd	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to {coe}_{1} (g) (D (G) + d) = {coe}_{1} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) (D (G) + d)$
182	181	adantrr	$⊢ ((φ \land d \in ℕ_{0}) \land (g \in B \land D (g) < D (G) + d + 1)) \to {coe}_{1} (g) (D (G) + d) = {coe}_{1} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) (D (G) + d)$
183	2 1 3 4 107 108 109 134 155 161 139 162 182	deg1sublt	$⊢ ((φ \land d \in ℕ_{0}) \land (g \in B \land D (g) < D (G) + d + 1)) \to D (g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))) < D (G) + d$
184	183	adantlrr	$⊢ ((φ \land (d \in ℕ_{0} \land \forall f \in B (D (f) < D (G) + d \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)))) \land (g \in B \land D (g) < D (G) + d + 1)) \to D (g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))) < D (G) + d$
185		fveq2	$⊢ f = g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) \to D (f) = D (g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))))$
186	185	breq1d	$⊢ f = g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) \to (D (f) < D (G) + d \leftrightarrow D (g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))) < D (G) + d)$
187		fvoveq1	$⊢ f = g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) \to D (f \underset{˙}{-} (G \underset{˙}{∙} q)) = D ((g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))) \underset{˙}{-} (G \underset{˙}{∙} q))$
188	187	breq1d	$⊢ f = g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) \to (D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \leftrightarrow D ((g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))) \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))$
189	188	rexbidv	$⊢ f = g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) \to (\exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \leftrightarrow \exists q \in B D ((g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))) \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))$
190	186 189	imbi12d	$⊢ f = g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) \to ((D (f) < D (G) + d \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)) \leftrightarrow (D (g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))) < D (G) + d \to \exists q \in B D ((g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))) \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)))$
191		simplrr	$⊢ ((φ \land (d \in ℕ_{0} \land \forall f \in B (D (f) < D (G) + d \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)))) \land (g \in B \land D (g) < D (G) + d + 1)) \to \forall f \in B (D (f) < D (G) + d \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))$
192	87	ad2antrr	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to P \in Grp$
193		simpr	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to g \in B$
194	3 4	grpsubcl	$⊢ (P \in Grp \land g \in B \land G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))) \in B) \to g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) \in B$
195	192 193 154 194	syl3anc	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) \in B$
196	195	adantrr	$⊢ ((φ \land d \in ℕ_{0}) \land (g \in B \land D (g) < D (G) + d + 1)) \to g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) \in B$
197	196	adantlrr	$⊢ ((φ \land (d \in ℕ_{0} \land \forall f \in B (D (f) < D (G) + d \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)))) \land (g \in B \land D (g) < D (G) + d + 1)) \to g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) \in B$
198	190 191 197	rspcdva	$⊢ ((φ \land (d \in ℕ_{0} \land \forall f \in B (D (f) < D (G) + d \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)))) \land (g \in B \land D (g) < D (G) + d + 1)) \to (D (g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))) < D (G) + d \to \exists q \in B D ((g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))) \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))$
199	184 198	mpd	$⊢ ((φ \land (d \in ℕ_{0} \land \forall f \in B (D (f) < D (G) + d \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)))) \land (g \in B \land D (g) < D (G) + d + 1)) \to \exists q \in B D ((g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))) \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)$
200	78	ad3antrrr	$⊢ (((φ \land d \in ℕ_{0}) \land g \in B) \land q \in B) \to P \in Ring$
201		simpr	$⊢ (((φ \land d \in ℕ_{0}) \land g \in B) \land q \in B) \to q \in B$
202	152	adantr	$⊢ (((φ \land d \in ℕ_{0}) \land g \in B) \land q \in B) \to (I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \in B$
203		eqid	$⊢ +_{P} = +_{P}$
204	3 203	ringacl	$⊢ (P \in Ring \land q \in B \land (I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \in B) \to q +_{P} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))) \in B$
205	200 201 202 204	syl3anc	$⊢ (((φ \land d \in ℕ_{0}) \land g \in B) \land q \in B) \to q +_{P} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))) \in B$
206	87	ad3antrrr	$⊢ (((φ \land d \in ℕ_{0}) \land g \in B) \land q \in B) \to P \in Grp$
207		simplr	$⊢ (((φ \land d \in ℕ_{0}) \land g \in B) \land q \in B) \to g \in B$
208	154	adantr	$⊢ (((φ \land d \in ℕ_{0}) \land g \in B) \land q \in B) \to G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))) \in B$
209	9	ad3antrrr	$⊢ (((φ \land d \in ℕ_{0}) \land g \in B) \land q \in B) \to G \in B$
210	3 6	ringcl	$⊢ (P \in Ring \land G \in B \land q \in B) \to G \underset{˙}{∙} q \in B$
211	200 209 201 210	syl3anc	$⊢ (((φ \land d \in ℕ_{0}) \land g \in B) \land q \in B) \to G \underset{˙}{∙} q \in B$
212	3 203 4	grpsubsub4	$⊢ (P \in Grp \land (g \in B \land G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))) \in B \land G \underset{˙}{∙} q \in B)) \to (g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))) \underset{˙}{-} (G \underset{˙}{∙} q) = g \underset{˙}{-} ((G \underset{˙}{∙} q) +_{P} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))))$
213	206 207 208 211 212	syl13anc	$⊢ (((φ \land d \in ℕ_{0}) \land g \in B) \land q \in B) \to (g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))) \underset{˙}{-} (G \underset{˙}{∙} q) = g \underset{˙}{-} ((G \underset{˙}{∙} q) +_{P} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))))$
214	3 203 6	ringdi	$⊢ (P \in Ring \land (G \in B \land q \in B \land (I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)) \in B)) \to G \underset{˙}{∙} (q +_{P} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) = (G \underset{˙}{∙} q) +_{P} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))$
215	200 209 201 202 214	syl13anc	$⊢ (((φ \land d \in ℕ_{0}) \land g \in B) \land q \in B) \to G \underset{˙}{∙} (q +_{P} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))) = (G \underset{˙}{∙} q) +_{P} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))$
216	215	oveq2d	$⊢ (((φ \land d \in ℕ_{0}) \land g \in B) \land q \in B) \to g \underset{˙}{-} (G \underset{˙}{∙} (q +_{P} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))) = g \underset{˙}{-} ((G \underset{˙}{∙} q) +_{P} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))))$
217	213 216	eqtr4d	$⊢ (((φ \land d \in ℕ_{0}) \land g \in B) \land q \in B) \to (g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))) \underset{˙}{-} (G \underset{˙}{∙} q) = g \underset{˙}{-} (G \underset{˙}{∙} (q +_{P} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))))$
218	217	fveq2d	$⊢ (((φ \land d \in ℕ_{0}) \land g \in B) \land q \in B) \to D ((g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))) \underset{˙}{-} (G \underset{˙}{∙} q)) = D (g \underset{˙}{-} (G \underset{˙}{∙} (q +_{P} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))))$
219	218	breq1d	$⊢ (((φ \land d \in ℕ_{0}) \land g \in B) \land q \in B) \to (D ((g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))) \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \leftrightarrow D (g \underset{˙}{-} (G \underset{˙}{∙} (q +_{P} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))))) < D (G))$
220	219	biimpd	$⊢ (((φ \land d \in ℕ_{0}) \land g \in B) \land q \in B) \to (D ((g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))) \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \to D (g \underset{˙}{-} (G \underset{˙}{∙} (q +_{P} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))))) < D (G))$
221		oveq2	$⊢ r = q +_{P} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))) \to G \underset{˙}{∙} r = G \underset{˙}{∙} (q +_{P} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))$
222	221	oveq2d	$⊢ r = q +_{P} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))) \to g \underset{˙}{-} (G \underset{˙}{∙} r) = g \underset{˙}{-} (G \underset{˙}{∙} (q +_{P} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))))$
223	222	fveq2d	$⊢ r = q +_{P} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))) \to D (g \underset{˙}{-} (G \underset{˙}{∙} r)) = D (g \underset{˙}{-} (G \underset{˙}{∙} (q +_{P} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))))$
224	223	breq1d	$⊢ r = q +_{P} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))) \to (D (g \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G) \leftrightarrow D (g \underset{˙}{-} (G \underset{˙}{∙} (q +_{P} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))))) < D (G))$
225	224	rspcev	$⊢ (q +_{P} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))) \in B \land D (g \underset{˙}{-} (G \underset{˙}{∙} (q +_{P} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R)))))) < D (G)) \to \exists r \in B D (g \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G)$
226	205 220 225	syl6an	$⊢ (((φ \land d \in ℕ_{0}) \land g \in B) \land q \in B) \to (D ((g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))) \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \to \exists r \in B D (g \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G))$
227	226	rexlimdva	$⊢ ((φ \land d \in ℕ_{0}) \land g \in B) \to (\exists q \in B D ((g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))) \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \to \exists r \in B D (g \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G))$
228	227	adantrr	$⊢ ((φ \land d \in ℕ_{0}) \land (g \in B \land D (g) < D (G) + d + 1)) \to (\exists q \in B D ((g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))) \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \to \exists r \in B D (g \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G))$
229	228	adantlrr	$⊢ ((φ \land (d \in ℕ_{0} \land \forall f \in B (D (f) < D (G) + d \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)))) \land (g \in B \land D (g) < D (G) + d + 1)) \to (\exists q \in B D ((g \underset{˙}{-} (G \underset{˙}{∙} ((I \underset{˙}{\cdot} {coe}_{1} (g) (D (G) + d)) \cdot_{P} (d \cdot_{{mulGrp}_{P}} {var}_{1} (R))))) \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G) \to \exists r \in B D (g \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G))$
230	199 229	mpd	$⊢ ((φ \land (d \in ℕ_{0} \land \forall f \in B (D (f) < D (G) + d \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)))) \land (g \in B \land D (g) < D (G) + d + 1)) \to \exists r \in B D (g \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G)$
231	230	expr	$⊢ ((φ \land (d \in ℕ_{0} \land \forall f \in B (D (f) < D (G) + d \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)))) \land g \in B) \to (D (g) < D (G) + d + 1 \to \exists r \in B D (g \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G))$
232	231	ralrimiva	$⊢ (φ \land (d \in ℕ_{0} \land \forall f \in B (D (f) < D (G) + d \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)))) \to \forall g \in B (D (g) < D (G) + d + 1 \to \exists r \in B D (g \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G))$
233		fveq2	$⊢ g = f \to D (g) = D (f)$
234	233	breq1d	$⊢ g = f \to (D (g) < D (G) + d + 1 \leftrightarrow D (f) < D (G) + d + 1)$
235		fvoveq1	$⊢ g = f \to D (g \underset{˙}{-} (G \underset{˙}{∙} r)) = D (f \underset{˙}{-} (G \underset{˙}{∙} r))$
236	235	breq1d	$⊢ g = f \to (D (g \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G) \leftrightarrow D (f \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G))$
237	236	rexbidv	$⊢ g = f \to (\exists r \in B D (g \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G) \leftrightarrow \exists r \in B D (f \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G))$
238		oveq2	$⊢ r = q \to G \underset{˙}{∙} r = G \underset{˙}{∙} q$
239	238	oveq2d	$⊢ r = q \to f \underset{˙}{-} (G \underset{˙}{∙} r) = f \underset{˙}{-} (G \underset{˙}{∙} q)$
240	239	fveq2d	$⊢ r = q \to D (f \underset{˙}{-} (G \underset{˙}{∙} r)) = D (f \underset{˙}{-} (G \underset{˙}{∙} q))$
241	240	breq1d	$⊢ r = q \to (D (f \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G) \leftrightarrow D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))$
242	241	cbvrexvw	$⊢ \exists r \in B D (f \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G) \leftrightarrow \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)$
243	237 242	bitrdi	$⊢ g = f \to (\exists r \in B D (g \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G) \leftrightarrow \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))$
244	234 243	imbi12d	$⊢ g = f \to ((D (g) < D (G) + d + 1 \to \exists r \in B D (g \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G)) \leftrightarrow (D (f) < D (G) + d + 1 \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)))$
245	244	cbvralvw	$⊢ \forall g \in B (D (g) < D (G) + d + 1 \to \exists r \in B D (g \underset{˙}{-} (G \underset{˙}{∙} r)) < D (G)) \leftrightarrow \forall f \in B (D (f) < D (G) + d + 1 \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))$
246	232 245	sylib	$⊢ (φ \land (d \in ℕ_{0} \land \forall f \in B (D (f) < D (G) + d \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)))) \to \forall f \in B (D (f) < D (G) + d + 1 \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))$
247	246	exp32	$⊢ φ \to (d \in ℕ_{0} \to (\forall f \in B (D (f) < D (G) + d \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)) \to \forall f \in B (D (f) < D (G) + d + 1 \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))))$
248	247	com12	$⊢ d \in ℕ_{0} \to (φ \to (\forall f \in B (D (f) < D (G) + d \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)) \to \forall f \in B (D (f) < D (G) + d + 1 \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))))$
249	248	a2d	$⊢ d \in ℕ_{0} \to ((φ \to \forall f \in B (D (f) < D (G) + d \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))) \to (φ \to \forall f \in B (D (f) < D (G) + d + 1 \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))))$
250	66 71 76 71 104 249	nn0ind	$⊢ d \in ℕ_{0} \to (φ \to \forall f \in B (D (f) < D (G) + d \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)))$
251	250	impcom	$⊢ (φ \land d \in ℕ_{0}) \to \forall f \in B (D (f) < D (G) + d \to \exists q \in B D (f \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))$
252	8	adantr	$⊢ (φ \land d \in ℕ_{0}) \to F \in B$
253	61 251 252	rspcdva	$⊢ (φ \land d \in ℕ_{0}) \to (D (F) < D (G) + d \to \exists q \in B D (F \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))$
254	253	rexlimdva	$⊢ φ \to (\exists d \in ℕ_{0} D (F) < D (G) + d \to \exists q \in B D (F \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G))$
255	55 254	mpd	$⊢ φ \to \exists q \in B D (F \underset{˙}{-} (G \underset{˙}{∙} q)) < D (G)$

Metamath Proof Explorer

Theorem ply1divex

Proof