Metamath Proof Explorer

Theorem rngunsnply1chr2lem3

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 rngunsnply1chr2lem3 ( 𝜑 → ( ( 𝐷 ‘ 𝐻 ) ≤ 1 ∧ ( ( 𝑄 ‘ 𝐻 ) ‘ 𝑋 ) = ( ( 𝑄 ‘ 𝐹 ) ‘ 𝑋 ) ) )

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 20 fveq2i ⊢ ( 𝐷 ‘ 𝐻 ) = ( 𝐷 ‘ ( 𝐹 𝐸 𝐺 ) )
23 eqid ⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
24 23 subrgring ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑅 ↾s 𝑆 ) ∈ Ring )
25 7 24 syl ⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ Ring )
26 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 rngunsnply1chr2lem2 ⊢ ( 𝜑 → 𝐺 ∈ ( Unic1p ‘ ( 𝑅 ↾s 𝑆 ) ) )
27 eqid ⊢ ( Unic1p ‘ ( 𝑅 ↾s 𝑆 ) ) = ( Unic1p ‘ ( 𝑅 ↾s 𝑆 ) )
28 18 2 3 27 r1pcl ⊢ ( ( ( 𝑅 ↾s 𝑆 ) ∈ Ring ∧ 𝐹 ∈ 𝑈 ∧ 𝐺 ∈ ( Unic1p ‘ ( 𝑅 ↾s 𝑆 ) ) ) → ( 𝐹 𝐸 𝐺 ) ∈ 𝑈 )
29 25 21 26 28 syl3anc ⊢ ( 𝜑 → ( 𝐹 𝐸 𝐺 ) ∈ 𝑈 )
30 23 17 2 3 29 7 ressdeg1 ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐹 𝐸 𝐺 ) ) = ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) )
31 22 30 eqtrid ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐻 ) = ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) )
32 simpr ⊢ ( ( 𝜑 ∧ ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ℕ0 ) → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ℕ0 )
33 1nn0 ⊢ 1 ∈ ℕ0
34 33 a1i ⊢ ( ( 𝜑 ∧ ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ℕ0 ) → 1 ∈ ℕ0 )
35 eqid ⊢ ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) = ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) )
36 18 2 3 27 35 r1pdeglt ⊢ ( ( ( 𝑅 ↾s 𝑆 ) ∈ Ring ∧ 𝐹 ∈ 𝑈 ∧ 𝐺 ∈ ( Unic1p ‘ ( 𝑅 ↾s 𝑆 ) ) ) → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) < ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ 𝐺 ) )
37 25 21 26 36 syl3anc ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) < ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ 𝐺 ) )
38 37 adantr ⊢ ( ( 𝜑 ∧ ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ℕ0 ) → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) < ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ 𝐺 ) )
39 1p1e2 ⊢ ( 1 + 1 ) = 2
40 2 3 27 uc1pcl ⊢ ( 𝐺 ∈ ( Unic1p ‘ ( 𝑅 ↾s 𝑆 ) ) → 𝐺 ∈ 𝑈 )
41 26 40 syl ⊢ ( 𝜑 → 𝐺 ∈ 𝑈 )
42 23 17 2 3 41 7 ressdeg1 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) = ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ 𝐺 ) )
43 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 rngunsnply1chr2lem1 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) = 2 )
44 42 43 eqtr3d ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ 𝐺 ) = 2 )
45 39 44 eqtr4id ⊢ ( 𝜑 → ( 1 + 1 ) = ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ 𝐺 ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ℕ0 ) → ( 1 + 1 ) = ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ 𝐺 ) )
47 38 46 breqtrrd ⊢ ( ( 𝜑 ∧ ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ℕ0 ) → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) < ( 1 + 1 ) )
48 nn0leltp1 ⊢ ( ( ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ℕ0 ∧ 1 ∈ ℕ0 ) → ( ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ≤ 1 ↔ ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) < ( 1 + 1 ) ) )
49 48 biimpar ⊢ ( ( ( ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) < ( 1 + 1 ) ) → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ≤ 1 )
50 32 34 47 49 syl21anc ⊢ ( ( 𝜑 ∧ ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ℕ0 ) → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ≤ 1 )
51 simpr ⊢ ( ( 𝜑 ∧ ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) = -∞ ) → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) = -∞ )
52 1xr ⊢ 1 ∈ ℝ*
53 mnfle ⊢ ( 1 ∈ ℝ* → -∞ ≤ 1 )
54 52 53 ax-mp ⊢ -∞ ≤ 1
55 51 54 eqbrtrdi ⊢ ( ( 𝜑 ∧ ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) = -∞ ) → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ≤ 1 )
56 35 2 3 deg1cl ⊢ ( ( 𝐹 𝐸 𝐺 ) ∈ 𝑈 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ( ℕ0 ∪ { -∞ } ) )
57 29 56 syl ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ( ℕ0 ∪ { -∞ } ) )
58 fvex ⊢ ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ V
59 elunsn ⊢ ( ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ V → ( ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ( ℕ0 ∪ { -∞ } ) ↔ ( ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ℕ0 ∨ ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) = -∞ ) ) )
60 58 59 ax-mp ⊢ ( ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ( ℕ0 ∪ { -∞ } ) ↔ ( ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ℕ0 ∨ ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) = -∞ ) )
61 57 60 sylib ⊢ ( 𝜑 → ( ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ∈ ℕ0 ∨ ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) = -∞ ) )
62 50 55 61 mpjaodan ⊢ ( 𝜑 → ( ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) ) ‘ ( 𝐹 𝐸 𝐺 ) ) ≤ 1 )
63 31 62 eqbrtrd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐻 ) ≤ 1 )
64 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
65 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
66 2 ply1ring ⊢ ( ( 𝑅 ↾s 𝑆 ) ∈ Ring → 𝑃 ∈ Ring )
67 25 66 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
68 eqid ⊢ ( quot1p ‘ ( 𝑅 ↾s 𝑆 ) ) = ( quot1p ‘ ( 𝑅 ↾s 𝑆 ) )
69 68 2 3 27 q1pcl ⊢ ( ( ( 𝑅 ↾s 𝑆 ) ∈ Ring ∧ 𝐹 ∈ 𝑈 ∧ 𝐺 ∈ ( Unic1p ‘ ( 𝑅 ↾s 𝑆 ) ) ) → ( 𝐹 ( quot1p ‘ ( 𝑅 ↾s 𝑆 ) ) 𝐺 ) ∈ 𝑈 )
70 25 21 26 69 syl3anc ⊢ ( 𝜑 → ( 𝐹 ( quot1p ‘ ( 𝑅 ↾s 𝑆 ) ) 𝐺 ) ∈ 𝑈 )
71 3 65 67 70 41 ringcld ⊢ ( 𝜑 → ( ( 𝐹 ( quot1p ‘ ( 𝑅 ↾s 𝑆 ) ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ∈ 𝑈 )
72 4 1 2 23 3 64 11 5 7 71 29 8 evls1addd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( ( ( 𝐹 ( quot1p ‘ ( 𝑅 ↾s 𝑆 ) ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ( +g ‘ 𝑃 ) ( 𝐹 𝐸 𝐺 ) ) ) ‘ 𝑋 ) = ( ( ( 𝑄 ‘ ( ( 𝐹 ( quot1p ‘ ( 𝑅 ↾s 𝑆 ) ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) ‘ 𝑋 ) + ( ( 𝑄 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 𝑋 ) ) )
73 4 1 2 23 3 65 12 5 7 70 41 8 evls1muld ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( ( 𝐹 ( quot1p ‘ ( 𝑅 ↾s 𝑆 ) ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) ‘ 𝑋 ) = ( ( ( 𝑄 ‘ ( 𝐹 ( quot1p ‘ ( 𝑅 ↾s 𝑆 ) ) 𝐺 ) ) ‘ 𝑋 ) · ( ( 𝑄 ‘ 𝐺 ) ‘ 𝑋 ) ) )
74 19 fveq2i ⊢ ( 𝑄 ‘ 𝐺 ) = ( 𝑄 ‘ ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) )
75 74 fveq1i ⊢ ( ( 𝑄 ‘ 𝐺 ) ‘ 𝑋 ) = ( ( 𝑄 ‘ ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ‘ 𝑋 )
76 75 a1i ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐺 ) ‘ 𝑋 ) = ( ( 𝑄 ‘ ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ‘ 𝑋 ) )
77 eqid ⊢ ( -g ‘ 𝑃 ) = ( -g ‘ 𝑃 )
78 eqid ⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
79 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
80 79 3 mgpbas ⊢ 𝑈 = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
81 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
82 79 ringmgp ⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
83 67 82 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
84 2nn0 ⊢ 2 ∈ ℕ0
85 84 a1i ⊢ ( 𝜑 → 2 ∈ ℕ0 )
86 eqid ⊢ ( var1 ‘ 𝑅 ) = ( var1 ‘ 𝑅 )
87 86 7 23 2 3 subrgvr1cl ⊢ ( 𝜑 → ( var1 ‘ 𝑅 ) ∈ 𝑈 )
88 80 81 83 85 87 mulgnn0cld ⊢ ( 𝜑 → ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ 𝑈 )
89 67 ringgrpd ⊢ ( 𝜑 → 𝑃 ∈ Grp )
90 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
91 eqid ⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
92 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
93 2 ply1lmod ⊢ ( ( 𝑅 ↾s 𝑆 ) ∈ Ring → 𝑃 ∈ LMod )
94 25 93 syl ⊢ ( 𝜑 → 𝑃 ∈ LMod )
95 23 subrgbas ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 = ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
96 7 95 syl ⊢ ( 𝜑 → 𝑆 = ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
97 ovex ⊢ ( 𝑅 ↾s 𝑆 ) ∈ V
98 2 ply1sca ⊢ ( ( 𝑅 ↾s 𝑆 ) ∈ V → ( 𝑅 ↾s 𝑆 ) = ( Scalar ‘ 𝑃 ) )
99 97 98 ax-mp ⊢ ( 𝑅 ↾s 𝑆 ) = ( Scalar ‘ 𝑃 )
100 99 fveq2i ⊢ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
101 96 100 eqtrdi ⊢ ( 𝜑 → 𝑆 = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
102 14 101 eleqtrd ⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
103 3 90 91 92 94 102 87 lmodvscld ⊢ ( 𝜑 → ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ∈ 𝑈 )
104 eqid ⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
105 2 23 104 3 5 7 15 ressasclcl ⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ∈ 𝑈 )
106 3 64 89 103 105 grpcld ⊢ ( 𝜑 → ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ∈ 𝑈 )
107 4 1 2 23 3 77 78 5 7 88 106 8 evls1subd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ‘ 𝑋 ) = ( ( ( 𝑄 ‘ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ‘ 𝑋 ) ( -g ‘ 𝑅 ) ( ( 𝑄 ‘ ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ‘ 𝑋 ) ) )
108 4 1 2 23 3 5 7 81 13 85 87 8 evls1expd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ‘ 𝑋 ) = ( 2 ↑ ( ( 𝑄 ‘ ( var1 ‘ 𝑅 ) ) ‘ 𝑋 ) ) )
109 86 7 23 subrgvr1 ⊢ ( 𝜑 → ( var1 ‘ 𝑅 ) = ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) )
110 109 fveq2d ⊢ ( 𝜑 → ( 𝑄 ‘ ( var1 ‘ 𝑅 ) ) = ( 𝑄 ‘ ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) )
111 110 fveq1d ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( var1 ‘ 𝑅 ) ) ‘ 𝑋 ) = ( ( 𝑄 ‘ ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ‘ 𝑋 ) )
112 eqid ⊢ ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) = ( var1 ‘ ( 𝑅 ↾s 𝑆 ) )
113 4 112 23 1 5 7 evls1var ⊢ ( 𝜑 → ( 𝑄 ‘ ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) = ( I ↾ 𝑉 ) )
114 113 fveq1d ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ‘ 𝑋 ) = ( ( I ↾ 𝑉 ) ‘ 𝑋 ) )
115 fvresi ⊢ ( 𝑋 ∈ 𝑉 → ( ( I ↾ 𝑉 ) ‘ 𝑋 ) = 𝑋 )
116 8 115 syl ⊢ ( 𝜑 → ( ( I ↾ 𝑉 ) ‘ 𝑋 ) = 𝑋 )
117 111 114 116 3eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( var1 ‘ 𝑅 ) ) ‘ 𝑋 ) = 𝑋 )
118 117 oveq2d ⊢ ( 𝜑 → ( 2 ↑ ( ( 𝑄 ‘ ( var1 ‘ 𝑅 ) ) ‘ 𝑋 ) ) = ( 2 ↑ 𝑋 ) )
119 108 118 eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ‘ 𝑋 ) = ( 2 ↑ 𝑋 ) )
120 4 1 2 23 3 64 11 5 7 103 105 8 evls1addd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ‘ 𝑋 ) = ( ( ( 𝑄 ‘ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) ‘ 𝑋 ) + ( ( 𝑄 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ‘ 𝑋 ) ) )
121 4 1 2 23 3 91 12 5 7 14 87 8 evls1vsca ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) ‘ 𝑋 ) = ( 𝐴 · ( ( 𝑄 ‘ ( var1 ‘ 𝑅 ) ) ‘ 𝑋 ) ) )
122 117 oveq2d ⊢ ( 𝜑 → ( 𝐴 · ( ( 𝑄 ‘ ( var1 ‘ 𝑅 ) ) ‘ 𝑋 ) ) = ( 𝐴 · 𝑋 ) )
123 121 122 eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) ‘ 𝑋 ) = ( 𝐴 · 𝑋 ) )
124 4 2 23 1 104 5 7 15 8 evls1scafv ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ‘ 𝑋 ) = 𝐵 )
125 123 124 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) ‘ 𝑋 ) + ( ( 𝑄 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ‘ 𝑋 ) ) = ( ( 𝐴 · 𝑋 ) + 𝐵 ) )
126 120 125 eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ‘ 𝑋 ) = ( ( 𝐴 · 𝑋 ) + 𝐵 ) )
127 119 126 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ‘ 𝑋 ) ( -g ‘ 𝑅 ) ( ( 𝑄 ‘ ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ‘ 𝑋 ) ) = ( ( 2 ↑ 𝑋 ) ( -g ‘ 𝑅 ) ( ( 𝐴 · 𝑋 ) + 𝐵 ) ) )
128 5 crnggrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
129 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
130 129 1 mgpbas ⊢ 𝑉 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
131 5 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
132 129 ringmgp ⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
133 131 132 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
134 130 13 133 85 8 mulgnn0cld ⊢ ( 𝜑 → ( 2 ↑ 𝑋 ) ∈ 𝑉 )
135 16 134 eqeltrrd ⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) + 𝐵 ) ∈ 𝑉 )
136 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
137 1 136 78 grpsubeq0 ⊢ ( ( 𝑅 ∈ Grp ∧ ( 2 ↑ 𝑋 ) ∈ 𝑉 ∧ ( ( 𝐴 · 𝑋 ) + 𝐵 ) ∈ 𝑉 ) → ( ( ( 2 ↑ 𝑋 ) ( -g ‘ 𝑅 ) ( ( 𝐴 · 𝑋 ) + 𝐵 ) ) = ( 0g ‘ 𝑅 ) ↔ ( 2 ↑ 𝑋 ) = ( ( 𝐴 · 𝑋 ) + 𝐵 ) ) )
138 137 biimpar ⊢ ( ( ( 𝑅 ∈ Grp ∧ ( 2 ↑ 𝑋 ) ∈ 𝑉 ∧ ( ( 𝐴 · 𝑋 ) + 𝐵 ) ∈ 𝑉 ) ∧ ( 2 ↑ 𝑋 ) = ( ( 𝐴 · 𝑋 ) + 𝐵 ) ) → ( ( 2 ↑ 𝑋 ) ( -g ‘ 𝑅 ) ( ( 𝐴 · 𝑋 ) + 𝐵 ) ) = ( 0g ‘ 𝑅 ) )
139 128 134 135 16 138 syl31anc ⊢ ( 𝜑 → ( ( 2 ↑ 𝑋 ) ( -g ‘ 𝑅 ) ( ( 𝐴 · 𝑋 ) + 𝐵 ) ) = ( 0g ‘ 𝑅 ) )
140 127 139 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ‘ 𝑋 ) ( -g ‘ 𝑅 ) ( ( 𝑄 ‘ ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ‘ 𝑋 ) ) = ( 0g ‘ 𝑅 ) )
141 76 107 140 3eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐺 ) ‘ 𝑋 ) = ( 0g ‘ 𝑅 ) )
142 141 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ ( 𝐹 ( quot1p ‘ ( 𝑅 ↾s 𝑆 ) ) 𝐺 ) ) ‘ 𝑋 ) · ( ( 𝑄 ‘ 𝐺 ) ‘ 𝑋 ) ) = ( ( ( 𝑄 ‘ ( 𝐹 ( quot1p ‘ ( 𝑅 ↾s 𝑆 ) ) 𝐺 ) ) ‘ 𝑋 ) · ( 0g ‘ 𝑅 ) ) )
143 4 2 1 3 5 7 8 70 evls1fvcl ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐹 ( quot1p ‘ ( 𝑅 ↾s 𝑆 ) ) 𝐺 ) ) ‘ 𝑋 ) ∈ 𝑉 )
144 1 12 136 131 143 ringrzd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ ( 𝐹 ( quot1p ‘ ( 𝑅 ↾s 𝑆 ) ) 𝐺 ) ) ‘ 𝑋 ) · ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
145 73 142 144 3eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( ( 𝐹 ( quot1p ‘ ( 𝑅 ↾s 𝑆 ) ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) ‘ 𝑋 ) = ( 0g ‘ 𝑅 ) )
146 145 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ ( ( 𝐹 ( quot1p ‘ ( 𝑅 ↾s 𝑆 ) ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ) ‘ 𝑋 ) + ( ( 𝑄 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 𝑋 ) ) = ( ( 0g ‘ 𝑅 ) + ( ( 𝑄 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 𝑋 ) ) )
147 4 2 1 3 5 7 8 29 evls1fvcl ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 𝑋 ) ∈ 𝑉 )
148 1 11 136 128 147 grplidd ⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) + ( ( 𝑄 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 𝑋 ) ) = ( ( 𝑄 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 𝑋 ) )
149 72 146 148 3eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( ( ( 𝐹 ( quot1p ‘ ( 𝑅 ↾s 𝑆 ) ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ( +g ‘ 𝑃 ) ( 𝐹 𝐸 𝐺 ) ) ) ‘ 𝑋 ) = ( ( 𝑄 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 𝑋 ) )
150 2 3 27 68 18 65 64 r1pid ⊢ ( ( ( 𝑅 ↾s 𝑆 ) ∈ Ring ∧ 𝐹 ∈ 𝑈 ∧ 𝐺 ∈ ( Unic1p ‘ ( 𝑅 ↾s 𝑆 ) ) ) → 𝐹 = ( ( ( 𝐹 ( quot1p ‘ ( 𝑅 ↾s 𝑆 ) ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ( +g ‘ 𝑃 ) ( 𝐹 𝐸 𝐺 ) ) )
151 25 21 26 150 syl3anc ⊢ ( 𝜑 → 𝐹 = ( ( ( 𝐹 ( quot1p ‘ ( 𝑅 ↾s 𝑆 ) ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ( +g ‘ 𝑃 ) ( 𝐹 𝐸 𝐺 ) ) )
152 151 fveq2d ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐹 ) = ( 𝑄 ‘ ( ( ( 𝐹 ( quot1p ‘ ( 𝑅 ↾s 𝑆 ) ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ( +g ‘ 𝑃 ) ( 𝐹 𝐸 𝐺 ) ) ) )
153 152 fveq1d ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝑋 ) = ( ( 𝑄 ‘ ( ( ( 𝐹 ( quot1p ‘ ( 𝑅 ↾s 𝑆 ) ) 𝐺 ) ( .r ‘ 𝑃 ) 𝐺 ) ( +g ‘ 𝑃 ) ( 𝐹 𝐸 𝐺 ) ) ) ‘ 𝑋 ) )
154 20 fveq2i ⊢ ( 𝑄 ‘ 𝐻 ) = ( 𝑄 ‘ ( 𝐹 𝐸 𝐺 ) )
155 154 fveq1i ⊢ ( ( 𝑄 ‘ 𝐻 ) ‘ 𝑋 ) = ( ( 𝑄 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 𝑋 )
156 155 a1i ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐻 ) ‘ 𝑋 ) = ( ( 𝑄 ‘ ( 𝐹 𝐸 𝐺 ) ) ‘ 𝑋 ) )
157 149 153 156 3eqtr4rd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐻 ) ‘ 𝑋 ) = ( ( 𝑄 ‘ 𝐹 ) ‘ 𝑋 ) )
158 63 157 jca ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐻 ) ≤ 1 ∧ ( ( 𝑄 ‘ 𝐻 ) ‘ 𝑋 ) = ( ( 𝑄 ‘ 𝐹 ) ‘ 𝑋 ) ) )