Theorem rngunsnply1chr2lem1

Description: Lemma for rngunsnply1chr2 . (Contributed by Thierry Arnoux, 8-Nov-2026)

	Ref	Expression
Hypotheses	rngunsnply1chr2.v	$$⊢V={\mathrm{Base}}_R$$
	rngunsnply1chr2.p	$$⊢P={\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)$$
	rngunsnply1chr2.u	$$⊢U={\mathrm{Base}}_P$$
	rngunsnply1chr2.q	$$⊢Q=R{\mathrm{evalSub}}_{1}S$$
	rngunsnply1chr2.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	rngunsnply1chr2.1	$$⊢\phi \to R\in \mathrm{NzRing}$$
	rngunsnply1chr2.s	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
	rngunsnply1chr2.x	$$⊢\phi \to X\in V$$
	rngunsnply1chr2.y	$$⊢\phi \to Y\in N\left(S\cup \left\{X\right\}\right)$$
	rngunsnply1chr2.n	$$⊢N=\mathrm{RingSpan}\left(R\right)$$
	rngunsnply1chr2.2	$$⊢\underset{\dot{}}{+}={+}_R$$
	rngunsnply1chr2.3	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	rngunsnply1chr2.4	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_R}$$
	rngunsnply1chr2.a	$$⊢\phi \to A\in S$$
	rngunsnply1chr2.b	$$⊢\phi \to B\in S$$
	rngunsnply1chr2.5	$$⊢\phi \to 2\underset{\dot{}}{\times }X=\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}B$$
	rngunsnply1chr2lem.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	rngunsnply1chr2lem.e	$$⊢E={rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)$$
	rngunsnply1chr2lem.g	$$⊢G=\left(2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right){-}_P\left(\left(A{\cdot }_P{\mathrm{var}}_1\left(R\right)\right){+}_P\mathrm{algSc}\left(P\right)\left(B\right)\right)$$
	rngunsnply1chr2lem.h	$$⊢H=FEG$$
	rngunsnply1chr2lem.f	$$⊢\phi \to F\in U$$
Assertion	rngunsnply1chr2lem1	$$⊢\phi \to D\left(G\right)=2$$

Proof

Step	Hyp	Ref	Expression
1		rngunsnply1chr2.v	$$⊢V={\mathrm{Base}}_R$$
2		rngunsnply1chr2.p	$$⊢P={\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)$$
3		rngunsnply1chr2.u	$$⊢U={\mathrm{Base}}_P$$
4		rngunsnply1chr2.q	$$⊢Q=R{\mathrm{evalSub}}_{1}S$$
5		rngunsnply1chr2.r	$$⊢\phi \to R\in \mathrm{CRing}$$
6		rngunsnply1chr2.1	$$⊢\phi \to R\in \mathrm{NzRing}$$
7		rngunsnply1chr2.s	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
8		rngunsnply1chr2.x	$$⊢\phi \to X\in V$$
9		rngunsnply1chr2.y	$$⊢\phi \to Y\in N\left(S\cup \left\{X\right\}\right)$$
10		rngunsnply1chr2.n	$$⊢N=\mathrm{RingSpan}\left(R\right)$$
11		rngunsnply1chr2.2	$$⊢\underset{\dot{}}{+}={+}_R$$
12		rngunsnply1chr2.3	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
13		rngunsnply1chr2.4	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_R}$$
14		rngunsnply1chr2.a	$$⊢\phi \to A\in S$$
15		rngunsnply1chr2.b	$$⊢\phi \to B\in S$$
16		rngunsnply1chr2.5	$$⊢\phi \to 2\underset{\dot{}}{\times }X=\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}B$$
17		rngunsnply1chr2lem.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
18		rngunsnply1chr2lem.e	$$⊢E={rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)$$
19		rngunsnply1chr2lem.g	$$⊢G=\left(2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right){-}_P\left(\left(A{\cdot }_P{\mathrm{var}}_1\left(R\right)\right){+}_P\mathrm{algSc}\left(P\right)\left(B\right)\right)$$
20		rngunsnply1chr2lem.h	$$⊢H=FEG$$
21		rngunsnply1chr2lem.f	$$⊢\phi \to F\in U$$
22		eqid	$$⊢R{\upharpoonright }_{𝑠}S=R{\upharpoonright }_{𝑠}S$$
23		eqid	$$⊢{-}_P={-}_P$$
24	22	subrgring	$$⊢S\in \mathrm{SubRing}\left(R\right)\to R{\upharpoonright }_{𝑠}S\in \mathrm{Ring}$$
25	7 24	syl	$$⊢\phi \to R{\upharpoonright }_{𝑠}S\in \mathrm{Ring}$$
26	2	ply1ring	$$⊢R{\upharpoonright }_{𝑠}S\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
27	25 26	syl	$$⊢\phi \to P\in \mathrm{Ring}$$
28	27	ringgrpd	$$⊢\phi \to P\in \mathrm{Grp}$$
29		eqid	$$⊢{\mathrm{mulGrp}}_P={\mathrm{mulGrp}}_P$$
30	29 3	mgpbas	$$⊢U={\mathrm{Base}}_{{\mathrm{mulGrp}}_P}$$
31		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_P}={\cdot }_{{\mathrm{mulGrp}}_P}$$
32	29	ringmgp	$$⊢P\in \mathrm{Ring}\to {\mathrm{mulGrp}}_P\in \mathrm{Mnd}$$
33	27 32	syl	$$⊢\phi \to {\mathrm{mulGrp}}_P\in \mathrm{Mnd}$$
34		2nn0	$$⊢2\in {\mathbb{N}}_0$$
35	34	a1i	$$⊢\phi \to 2\in {\mathbb{N}}_0$$
36		eqid	$$⊢{\mathrm{var}}_1\left(R\right)={\mathrm{var}}_1\left(R\right)$$
37	36 7 22 2 3	subrgvr1cl	$$⊢\phi \to {\mathrm{var}}_1\left(R\right)\in U$$
38	30 31 33 35 37	mulgnn0cld	$$⊢\phi \to 2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\in U$$
39		eqid	$$⊢{+}_P={+}_P$$
40		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
41		eqid	$$⊢{\cdot }_P={\cdot }_P$$
42		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
43	2	ply1lmod	$$⊢R{\upharpoonright }_{𝑠}S\in \mathrm{Ring}\to P\in \mathrm{LMod}$$
44	25 43	syl	$$⊢\phi \to P\in \mathrm{LMod}$$
45	22	subrgbas	$$⊢S\in \mathrm{SubRing}\left(R\right)\to S={\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
46	7 45	syl	$$⊢\phi \to S={\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
47		ovex	$$⊢R{\upharpoonright }_{𝑠}S\in \mathrm{V}$$
48	2	ply1sca	$$⊢R{\upharpoonright }_{𝑠}S\in \mathrm{V}\to R{\upharpoonright }_{𝑠}S=\mathrm{Scalar}\left(P\right)$$
49	47 48	ax-mp	$$⊢R{\upharpoonright }_{𝑠}S=\mathrm{Scalar}\left(P\right)$$
50	49	fveq2i	$$⊢{\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
51	46 50	eqtrdi	$$⊢\phi \to S={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
52	14 51	eleqtrd	$$⊢\phi \to A\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
53	3 40 41 42 44 52 37	lmodvscld	$$⊢\phi \to A{\cdot }_P{\mathrm{var}}_1\left(R\right)\in U$$
54		eqid	$$⊢\mathrm{algSc}\left(P\right)=\mathrm{algSc}\left(P\right)$$
55	2 22 54 3 5 7 15	ressasclcl	$$⊢\phi \to \mathrm{algSc}\left(P\right)\left(B\right)\in U$$
56	3 39 28 53 55	grpcld	$$⊢\phi \to \left(A{\cdot }_P{\mathrm{var}}_1\left(R\right)\right){+}_P\mathrm{algSc}\left(P\right)\left(B\right)\in U$$
57	3 23 28 38 56	grpsubcld	$$⊢\phi \to \left(2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right){-}_P\left(\left(A{\cdot }_P{\mathrm{var}}_1\left(R\right)\right){+}_P\mathrm{algSc}\left(P\right)\left(B\right)\right)\in U$$
58	19 57	eqeltrid	$$⊢\phi \to G\in U$$
59	22 17 2 3 58 7	ressdeg1	$$⊢\phi \to D\left(G\right)={\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(G\right)$$
60	19	fveq2i	$$⊢{\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(G\right)={\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(\left(2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right){-}_P\left(\left(A{\cdot }_P{\mathrm{var}}_1\left(R\right)\right){+}_P\mathrm{algSc}\left(P\right)\left(B\right)\right)\right)$$
61	60	a1i	$$⊢\phi \to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(G\right)={\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(\left(2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right){-}_P\left(\left(A{\cdot }_P{\mathrm{var}}_1\left(R\right)\right){+}_P\mathrm{algSc}\left(P\right)\left(B\right)\right)\right)$$
62		eqid	$$⊢{\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)={\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)$$
63	62 2 3	deg1xrcl	$$⊢\left(A{\cdot }_P{\mathrm{var}}_1\left(R\right)\right){+}_P\mathrm{algSc}\left(P\right)\left(B\right)\in U\to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(\left(A{\cdot }_P{\mathrm{var}}_1\left(R\right)\right){+}_P\mathrm{algSc}\left(P\right)\left(B\right)\right)\in {ℝ}^{*}$$
64	56 63	syl	$$⊢\phi \to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(\left(A{\cdot }_P{\mathrm{var}}_1\left(R\right)\right){+}_P\mathrm{algSc}\left(P\right)\left(B\right)\right)\in {ℝ}^{*}$$
65		1xr	$$⊢1\in {ℝ}^{*}$$
66	65	a1i	$$⊢\phi \to 1\in {ℝ}^{*}$$
67	62 2 3	deg1xrcl	$$⊢2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\in U\to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)\in {ℝ}^{*}$$
68	38 67	syl	$$⊢\phi \to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)\in {ℝ}^{*}$$
69	36 7 22	subrgvr1	$$⊢\phi \to {\mathrm{var}}_1\left(R\right)={\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}S\right)$$
70	69 37	eqeltrrd	$$⊢\phi \to {\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}S\right)\in U$$
71	30 31	mulg1	$$⊢{\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}S\right)\in U\to 1{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}S\right)={\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}S\right)$$
72	70 71	syl	$$⊢\phi \to 1{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}S\right)={\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}S\right)$$
73	72 69	eqtr4d	$$⊢\phi \to 1{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}S\right)={\mathrm{var}}_1\left(R\right)$$
74	73	oveq2d	$$⊢\phi \to A{\cdot }_P\left(1{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}S\right)\right)=A{\cdot }_P{\mathrm{var}}_1\left(R\right)$$
75	74	fveq2d	$$⊢\phi \to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(A{\cdot }_P\left(1{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}S\right)\right)\right)={\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(A{\cdot }_P{\mathrm{var}}_1\left(R\right)\right)$$
76	14 46	eleqtrd	$$⊢\phi \to A\in {\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
77		1nn0	$$⊢1\in {\mathbb{N}}_0$$
78	77	a1i	$$⊢\phi \to 1\in {\mathbb{N}}_0$$
79		eqid	$$⊢{\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}={\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
80		eqid	$$⊢{\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}S\right)={\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}S\right)$$
81	62 79 2 80 41 29 31	deg1tmle	$$⊢\left(R{\upharpoonright }_{𝑠}S\in \mathrm{Ring}\wedge A\in {\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}\wedge 1\in {\mathbb{N}}_0\right)\to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(A{\cdot }_P\left(1{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}S\right)\right)\right)\le 1$$
82	25 76 78 81	syl3anc	$$⊢\phi \to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(A{\cdot }_P\left(1{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}S\right)\right)\right)\le 1$$
83	75 82	eqbrtrrd	$$⊢\phi \to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(A{\cdot }_P{\mathrm{var}}_1\left(R\right)\right)\le 1$$
84	62 2 3	deg1xrcl	$$⊢\mathrm{algSc}\left(P\right)\left(B\right)\in U\to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(\mathrm{algSc}\left(P\right)\left(B\right)\right)\in {ℝ}^{*}$$
85	55 84	syl	$$⊢\phi \to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(\mathrm{algSc}\left(P\right)\left(B\right)\right)\in {ℝ}^{*}$$
86		0xr	$$⊢0\in {ℝ}^{*}$$
87	86	a1i	$$⊢\phi \to 0\in {ℝ}^{*}$$
88	15 46	eleqtrd	$$⊢\phi \to B\in {\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
89	62 2 79 54	deg1sclle	$$⊢\left(R{\upharpoonright }_{𝑠}S\in \mathrm{Ring}\wedge B\in {\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}\right)\to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(\mathrm{algSc}\left(P\right)\left(B\right)\right)\le 0$$
90	25 88 89	syl2anc	$$⊢\phi \to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(\mathrm{algSc}\left(P\right)\left(B\right)\right)\le 0$$
91		0lt1	$$⊢0<1$$
92	91	a1i	$$⊢\phi \to 0<1$$
93	85 87 66 90 92	xrlelttrd	$$⊢\phi \to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(\mathrm{algSc}\left(P\right)\left(B\right)\right)<1$$
94	85 66 93	xrltled	$$⊢\phi \to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(\mathrm{algSc}\left(P\right)\left(B\right)\right)\le 1$$
95	2 62 25 3 39 53 55 66 83 94	deg1addle2	$$⊢\phi \to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(\left(A{\cdot }_P{\mathrm{var}}_1\left(R\right)\right){+}_P\mathrm{algSc}\left(P\right)\left(B\right)\right)\le 1$$
96		1lt2	$$⊢1<2$$
97	69	oveq2d	$$⊢\phi \to 2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)=2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}S\right)$$
98	97	fveq2d	$$⊢\phi \to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)={\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}S\right)\right)$$
99	22	subrgnzr	$$⊢\left(R\in \mathrm{NzRing}\wedge S\in \mathrm{SubRing}\left(R\right)\right)\to R{\upharpoonright }_{𝑠}S\in \mathrm{NzRing}$$
100	6 7 99	syl2anc	$$⊢\phi \to R{\upharpoonright }_{𝑠}S\in \mathrm{NzRing}$$
101	62 2 80 29 31	deg1pw	$$⊢\left(R{\upharpoonright }_{𝑠}S\in \mathrm{NzRing}\wedge 2\in {\mathbb{N}}_0\right)\to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}S\right)\right)=2$$
102	100 35 101	syl2anc	$$⊢\phi \to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R{\upharpoonright }_{𝑠}S\right)\right)=2$$
103	98 102	eqtrd	$$⊢\phi \to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)=2$$
104	96 103	breqtrrid	$$⊢\phi \to 1<{\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)$$
105	64 66 68 95 104	xrlelttrd	$$⊢\phi \to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(\left(A{\cdot }_P{\mathrm{var}}_1\left(R\right)\right){+}_P\mathrm{algSc}\left(P\right)\left(B\right)\right)<{\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)$$
106	2 62 25 3 23 38 56 105	deg1sub	$$⊢\phi \to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(\left(2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right){-}_P\left(\left(A{\cdot }_P{\mathrm{var}}_1\left(R\right)\right){+}_P\mathrm{algSc}\left(P\right)\left(B\right)\right)\right)={\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)$$
107	106 103	eqtrd	$$⊢\phi \to {\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)\left(\left(2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right){-}_P\left(\left(A{\cdot }_P{\mathrm{var}}_1\left(R\right)\right){+}_P\mathrm{algSc}\left(P\right)\left(B\right)\right)\right)=2$$
108	59 61 107	3eqtrd	$$⊢\phi \to D\left(G\right)=2$$