Metamath Proof Explorer

Theorem rngunsnply1chr2

Description: When adjoining an element X with characteristic polynomial of degree 2 to a subring S , the elements Y of the generated subring can be written as a linear form. (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 ↑ 𝑋 ) = ( ( 𝐴 · 𝑋 ) + 𝐵 ) )
Assertion rngunsnply1chr2 ( 𝜑 → ∃ 𝑎 ∈ 𝑆 ∃ 𝑏 ∈ 𝑆 𝑌 = ( ( 𝑎 · 𝑋 ) + 𝑏 ) )

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 oveq1 ⊢ ( 𝑎 = ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 1 ) → ( 𝑎 · 𝑋 ) = ( ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 1 ) · 𝑋 ) )
18 17 oveq1d ⊢ ( 𝑎 = ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 1 ) → ( ( 𝑎 · 𝑋 ) + 𝑏 ) = ( ( ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 1 ) · 𝑋 ) + 𝑏 ) )
19 18 eqeq2d ⊢ ( 𝑎 = ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 1 ) → ( 𝑌 = ( ( 𝑎 · 𝑋 ) + 𝑏 ) ↔ 𝑌 = ( ( ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 1 ) · 𝑋 ) + 𝑏 ) ) )
20 oveq2 ⊢ ( 𝑏 = ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 0 ) → ( ( ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 1 ) · 𝑋 ) + 𝑏 ) = ( ( ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 1 ) · 𝑋 ) + ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 0 ) ) )
21 20 eqeq2d ⊢ ( 𝑏 = ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 0 ) → ( 𝑌 = ( ( ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 1 ) · 𝑋 ) + 𝑏 ) ↔ 𝑌 = ( ( ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 1 ) · 𝑋 ) + ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 0 ) ) ) )
22 eqid ⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
23 22 subrgring ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑅 ↾s 𝑆 ) ∈ Ring )
24 7 23 syl ⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ Ring )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( 𝑅 ↾s 𝑆 ) ∈ Ring )
26 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑝 ∈ 𝑈 )
27 5 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑅 ∈ CRing )
28 6 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑅 ∈ NzRing )
29 7 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
30 8 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑋 ∈ 𝑉 )
31 9 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) )
32 14 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝐴 ∈ 𝑆 )
33 15 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝐵 ∈ 𝑆 )
34 16 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( 2 ↑ 𝑋 ) = ( ( 𝐴 · 𝑋 ) + 𝐵 ) )
35 eqid ⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 )
36 eqid ⊢ ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) = ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) )
37 eqid ⊢ ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) = ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) )
38 eqid ⊢ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) = ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) )
39 1 2 3 4 27 28 29 30 31 10 11 12 13 32 33 34 35 36 37 38 26 rngunsnply1chr2lem2 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ∈ ( Unic1p ‘ ( 𝑅 ↾s 𝑆 ) ) )
40 eqid ⊢ ( Unic1p ‘ ( 𝑅 ↾s 𝑆 ) ) = ( Unic1p ‘ ( 𝑅 ↾s 𝑆 ) )
41 36 2 3 40 r1pcl ⊢ ( ( ( 𝑅 ↾s 𝑆 ) ∈ Ring ∧ 𝑝 ∈ 𝑈 ∧ ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ∈ ( Unic1p ‘ ( 𝑅 ↾s 𝑆 ) ) ) → ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ∈ 𝑈 )
42 25 26 39 41 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ∈ 𝑈 )
43 1nn0 ⊢ 1 ∈ ℕ0
44 eqid ⊢ ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) = ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) )
45 eqid ⊢ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) = ( Base ‘ ( 𝑅 ↾s 𝑆 ) )
46 44 3 2 45 coe1fvalcl ⊢ ( ( ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ∈ 𝑈 ∧ 1 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 1 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
47 42 43 46 sylancl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 1 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
48 22 subrgbas ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 = ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
49 29 48 syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑆 = ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
50 47 49 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 1 ) ∈ 𝑆 )
51 50 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑌 = ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) → ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 1 ) ∈ 𝑆 )
52 0nn0 ⊢ 0 ∈ ℕ0
53 44 3 2 45 coe1fvalcl ⊢ ( ( ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ∈ 𝑈 ∧ 0 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 0 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
54 42 52 53 sylancl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 0 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
55 54 49 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 0 ) ∈ 𝑆 )
56 55 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑌 = ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) → ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 0 ) ∈ 𝑆 )
57 simpr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑌 = ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) → 𝑌 = ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) )
58 1 2 3 4 27 28 29 30 31 10 11 12 13 32 33 34 35 36 37 38 26 rngunsnply1chr2lem3 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( ( deg1 ‘ 𝑅 ) ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ≤ 1 ∧ ( ( 𝑄 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 𝑋 ) = ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) )
59 58 simprd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( 𝑄 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 𝑋 ) = ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) )
60 59 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑌 = ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) → ( ( 𝑄 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 𝑋 ) = ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) )
61 eqid ⊢ ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 1 ) = ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 1 )
62 eqid ⊢ ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 0 ) = ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 0 )
63 58 simpld ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( deg1 ‘ 𝑅 ) ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ≤ 1 )
64 2 4 1 3 12 11 44 35 61 62 27 29 42 63 30 evls1degle1 ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( 𝑄 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 𝑋 ) = ( ( ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 1 ) · 𝑋 ) + ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 0 ) ) )
65 64 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑌 = ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) → ( ( 𝑄 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 𝑋 ) = ( ( ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 1 ) · 𝑋 ) + ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 0 ) ) )
66 57 60 65 3eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑌 = ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) → 𝑌 = ( ( ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 1 ) · 𝑋 ) + ( ( coe1 ‘ ( 𝑝 ( rem1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ) ‘ 0 ) ) )
67 19 21 51 56 66 2rspcedvdw ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) ∧ 𝑌 = ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) → ∃ 𝑎 ∈ 𝑆 ∃ 𝑏 ∈ 𝑆 𝑌 = ( ( 𝑎 · 𝑋 ) + 𝑏 ) )
68 1 2 3 4 5 7 8 10 rngunsnply1 ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∪ { 𝑋 } ) ) ↔ ∃ 𝑝 ∈ 𝑈 𝑌 = ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) ) )
69 9 68 mpbid ⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝑈 𝑌 = ( ( 𝑄 ‘ 𝑝 ) ‘ 𝑋 ) )
70 67 69 r19.29a ⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝑆 ∃ 𝑏 ∈ 𝑆 𝑌 = ( ( 𝑎 · 𝑋 ) + 𝑏 ) )