Metamath Proof Explorer

Theorem rngunsnply1chr2lem1

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

Ref Expression
Hypotheses rngunsnply1chr2.v ⊢ 𝑉 = ( Base ‘ 𝑅 )
rngunsnply1chr2.p ⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
rngunsnply1chr2.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
rngunsnply1chr2.q ⊢ 𝑄 = ( 𝑅 evalSub1 𝑆 )
rngunsnply1chr2.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
rngunsnply1chr2.1 ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
rngunsnply1chr2.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
rngunsnply1chr2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
rngunsnply1chr2.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) )
rngunsnply1chr2.n ⊢ 𝑁 = ( RingSpan ‘ 𝑅 )
rngunsnply1chr2.2 ⊢ + = ( +g ‘ 𝑅 )
rngunsnply1chr2.3 ⊢ · = ( .r ‘ 𝑅 )
rngunsnply1chr2.4 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
rngunsnply1chr2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
rngunsnply1chr2.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
rngunsnply1chr2.5 ⊢ ( 𝜑 → ( 2 ↑ 𝑋 ) = ( ( 𝐴 · 𝑋 ) + 𝐵 ) )
rngunsnply1chr2lem.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
rngunsnply1chr2lem.e ⊢ 𝐸 = ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) )
rngunsnply1chr2lem.g ⊢ 𝐺 = ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) )
rngunsnply1chr2lem.h ⊢ 𝐻 = ( 𝐹 𝐸 𝐺 )
rngunsnply1chr2lem.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑈 )
Assertion rngunsnply1chr2lem1 ( 𝜑 → ( 𝐷 ‘ 𝐺 ) = 2 )

Proof

Step Hyp Ref Expression
1 rngunsnply1chr2.v ⊢ 𝑉 = ( Base ‘ 𝑅 )
2 rngunsnply1chr2.p ⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
3 rngunsnply1chr2.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
4 rngunsnply1chr2.q ⊢ 𝑄 = ( 𝑅 evalSub1 𝑆 )
5 rngunsnply1chr2.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
6 rngunsnply1chr2.1 ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
7 rngunsnply1chr2.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
8 rngunsnply1chr2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
9 rngunsnply1chr2.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) )
10 rngunsnply1chr2.n ⊢ 𝑁 = ( RingSpan ‘ 𝑅 )
11 rngunsnply1chr2.2 ⊢ + = ( +g ‘ 𝑅 )
12 rngunsnply1chr2.3 ⊢ · = ( .r ‘ 𝑅 )
13 rngunsnply1chr2.4 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑅 ) )
14 rngunsnply1chr2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
15 rngunsnply1chr2.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
16 rngunsnply1chr2.5 ⊢ ( 𝜑 → ( 2 ↑ 𝑋 ) = ( ( 𝐴 · 𝑋 ) + 𝐵 ) )
17 rngunsnply1chr2lem.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
18 rngunsnply1chr2lem.e ⊢ 𝐸 = ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) )
19 rngunsnply1chr2lem.g ⊢ 𝐺 = ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) )
20 rngunsnply1chr2lem.h ⊢ 𝐻 = ( 𝐹 𝐸 𝐺 )
21 rngunsnply1chr2lem.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑈 )
22 eqid ⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
23 eqid ⊢ ( -g ‘ 𝑃 ) = ( -g ‘ 𝑃 )
24 22 subrgring ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑅 ↾s 𝑆 ) ∈ Ring )
25 7 24 syl ⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ Ring )
26 2 ply1ring ⊢ ( ( 𝑅 ↾s 𝑆 ) ∈ Ring → 𝑃 ∈ Ring )
27 25 26 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
28 27 ringgrpd ⊢ ( 𝜑 → 𝑃 ∈ Grp )
29 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
30 29 3 mgpbas ⊢ 𝑈 = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
31 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
32 29 ringmgp ⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
33 27 32 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
34 2nn0 ⊢ 2 ∈ ℕ0
35 34 a1i ⊢ ( 𝜑 → 2 ∈ ℕ0 )
36 eqid ⊢ ( var1 ‘ 𝑅 ) = ( var1 ‘ 𝑅 )
37 36 7 22 2 3 subrgvr1cl ⊢ ( 𝜑 → ( var1 ‘ 𝑅 ) ∈ 𝑈 )
38 30 31 33 35 37 mulgnn0cld ⊢ ( 𝜑 → ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ 𝑈 )
39 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
40 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
41 eqid ⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
42 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
43 2 ply1lmod ⊢ ( ( 𝑅 ↾s 𝑆 ) ∈ Ring → 𝑃 ∈ LMod )
44 25 43 syl ⊢ ( 𝜑 → 𝑃 ∈ LMod )
45 22 subrgbas ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 = ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
46 7 45 syl ⊢ ( 𝜑 → 𝑆 = ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
47 ovex ⊢ ( 𝑅 ↾s 𝑆 ) ∈ V
48 2 ply1sca ⊢ ( ( 𝑅 ↾s 𝑆 ) ∈ V → ( 𝑅 ↾s 𝑆 ) = ( Scalar ‘ 𝑃 ) )
49 47 48 ax-mp ⊢ ( 𝑅 ↾s 𝑆 ) = ( Scalar ‘ 𝑃 )
50 49 fveq2i ⊢ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
51 46 50 eqtrdi ⊢ ( 𝜑 → 𝑆 = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
52 14 51 eleqtrd ⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
53 3 40 41 42 44 52 37 lmodvscld ⊢ ( 𝜑 → ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ∈ 𝑈 )
54 eqid ⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
55 2 22 54 3 5 7 15 ressasclcl ⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ∈ 𝑈 )
56 3 39 28 53 55 grpcld ⊢ ( 𝜑 → ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ∈ 𝑈 )
57 3 23 28 38 56 grpsubcld ⊢ ( 𝜑 → ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ∈ 𝑈 )
58 19 57 eqeltrid ⊢ ( 𝜑 → 𝐺 ∈ 𝑈 )
59 22 17 2 3 58 7 ressdeg1 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) = ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ 𝐺 ) )
60 19 fveq2i ⊢ ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ 𝐺 ) = ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) )
61 60 a1i ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ 𝐺 ) = ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) )
62 eqid ⊢ ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) = ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) )
63 62 2 3 deg1xrcl ⊢ ( ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ∈ 𝑈 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ∈ ℝ* )
64 56 63 syl ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ∈ ℝ* )
65 1xr ⊢ 1 ∈ ℝ*
66 65 a1i ⊢ ( 𝜑 → 1 ∈ ℝ* )
67 62 2 3 deg1xrcl ⊢ ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ 𝑈 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ ℝ* )
68 38 67 syl ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∈ ℝ* )
69 36 7 22 subrgvr1 ⊢ ( 𝜑 → ( var1 ‘ 𝑅 ) = ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) )
70 69 37 eqeltrrd ⊢ ( 𝜑 → ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ∈ 𝑈 )
71 30 31 mulg1 ⊢ ( ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ∈ 𝑈 → ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) = ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) )
72 70 71 syl ⊢ ( 𝜑 → ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) = ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) )
73 72 69 eqtr4d ⊢ ( 𝜑 → ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) = ( var1 ‘ 𝑅 ) )
74 73 oveq2d ⊢ ( 𝜑 → ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) = ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) )
75 74 fveq2d ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) ) = ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) )
76 14 46 eleqtrd ⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
77 1nn0 ⊢ 1 ∈ ℕ0
78 77 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
79 eqid ⊢ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) = ( Base ‘ ( 𝑅 ↾s 𝑆 ) )
80 eqid ⊢ ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) = ( var1 ‘ ( 𝑅 ↾s 𝑆 ) )
81 62 79 2 80 41 29 31 deg1tmle ⊢ ( ( ( 𝑅 ↾s 𝑆 ) ∈ Ring ∧ 𝐴 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ∧ 1 ∈ ℕ0 ) → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) ) ≤ 1 )
82 25 76 78 81 syl3anc ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) ) ≤ 1 )
83 75 82 eqbrtrrd ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) ≤ 1 )
84 62 2 3 deg1xrcl ⊢ ( ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ∈ 𝑈 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ∈ ℝ* )
85 55 84 syl ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ∈ ℝ* )
86 0xr ⊢ 0 ∈ ℝ*
87 86 a1i ⊢ ( 𝜑 → 0 ∈ ℝ* )
88 15 46 eleqtrd ⊢ ( 𝜑 → 𝐵 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
89 62 2 79 54 deg1sclle ⊢ ( ( ( 𝑅 ↾s 𝑆 ) ∈ Ring ∧ 𝐵 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ≤ 0 )
90 25 88 89 syl2anc ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ≤ 0 )
91 0lt1 ⊢ 0 < 1
92 91 a1i ⊢ ( 𝜑 → 0 < 1 )
93 85 87 66 90 92 xrlelttrd ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) < 1 )
94 85 66 93 xrltled ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ≤ 1 )
95 2 62 25 3 39 53 55 66 83 94 deg1addle2 ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ≤ 1 )
96 1lt2 ⊢ 1 < 2
97 69 oveq2d ⊢ ( 𝜑 → ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) = ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) )
98 97 fveq2d ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) )
99 22 subrgnzr ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ) → ( 𝑅 ↾s 𝑆 ) ∈ NzRing )
100 6 7 99 syl2anc ⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ NzRing )
101 62 2 80 29 31 deg1pw ⊢ ( ( ( 𝑅 ↾s 𝑆 ) ∈ NzRing ∧ 2 ∈ ℕ0 ) → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) = 2 )
102 100 35 101 syl2anc ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) = 2 )
103 98 102 eqtrd ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) = 2 )
104 96 103 breqtrrid ⊢ ( 𝜑 → 1 < ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
105 64 66 68 95 104 xrlelttrd ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) < ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
106 2 62 25 3 23 38 56 105 deg1sub ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) = ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
107 106 103 eqtrd ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) = 2 )
108 59 61 107 3eqtrd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) = 2 )