This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ply1remlem

Description: A term of the form x - N is linear, monic, and has exactly one zero. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses ply1rem.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
ply1rem.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
ply1rem.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
ply1rem.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
ply1rem.m ⊢ − = ( -g ‘ 𝑃 )
ply1rem.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
ply1rem.g ⊢ 𝐺 = ( 𝑋 − ( 𝐴 ‘ 𝑁 ) )
ply1rem.o ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
ply1rem.1 ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
ply1rem.2 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
ply1rem.3 ⊢ ( 𝜑 → 𝑁 ∈ 𝐾 )
ply1rem.u ⊢ 𝑈 = ( Monic1p ‘ 𝑅 )
ply1rem.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
ply1rem.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion ply1remlem ( 𝜑 → ( 𝐺 ∈ 𝑈 ∧ ( 𝐷 ‘ 𝐺 ) = 1 ∧ ( ◡ ( 𝑂 ‘ 𝐺 ) “ { 0 } ) = { 𝑁 } ) )

Proof

Step Hyp Ref Expression
1 ply1rem.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 ply1rem.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 ply1rem.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
4 ply1rem.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
5 ply1rem.m ⊢ − = ( -g ‘ 𝑃 )
6 ply1rem.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
7 ply1rem.g ⊢ 𝐺 = ( 𝑋 − ( 𝐴 ‘ 𝑁 ) )
8 ply1rem.o ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
9 ply1rem.1 ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
10 ply1rem.2 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
11 ply1rem.3 ⊢ ( 𝜑 → 𝑁 ∈ 𝐾 )
12 ply1rem.u ⊢ 𝑈 = ( Monic1p ‘ 𝑅 )
13 ply1rem.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
14 ply1rem.z ⊢ 0 = ( 0g ‘ 𝑅 )
15 nzrring ⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
16 9 15 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
17 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
18 16 17 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
19 ringgrp ⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ Grp )
20 18 19 syl ⊢ ( 𝜑 → 𝑃 ∈ Grp )
21 4 1 2 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )
22 16 21 syl ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
23 1 6 3 2 ply1sclf ⊢ ( 𝑅 ∈ Ring → 𝐴 : 𝐾 ⟶ 𝐵 )
24 16 23 syl ⊢ ( 𝜑 → 𝐴 : 𝐾 ⟶ 𝐵 )
25 24 11 ffvelcdmd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑁 ) ∈ 𝐵 )
26 2 5 grpsubcl ⊢ ( ( 𝑃 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐴 ‘ 𝑁 ) ∈ 𝐵 ) → ( 𝑋 − ( 𝐴 ‘ 𝑁 ) ) ∈ 𝐵 )
27 20 22 25 26 syl3anc ⊢ ( 𝜑 → ( 𝑋 − ( 𝐴 ‘ 𝑁 ) ) ∈ 𝐵 )
28 7 27 eqeltrid ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
29 7 fveq2i ⊢ ( 𝐷 ‘ 𝐺 ) = ( 𝐷 ‘ ( 𝑋 − ( 𝐴 ‘ 𝑁 ) ) )
30 13 1 2 deg1xrcl ⊢ ( ( 𝐴 ‘ 𝑁 ) ∈ 𝐵 → ( 𝐷 ‘ ( 𝐴 ‘ 𝑁 ) ) ∈ ℝ* )
31 25 30 syl ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐴 ‘ 𝑁 ) ) ∈ ℝ* )
32 0xr ⊢ 0 ∈ ℝ*
33 32 a1i ⊢ ( 𝜑 → 0 ∈ ℝ* )
34 1re ⊢ 1 ∈ ℝ
35 rexr ⊢ ( 1 ∈ ℝ → 1 ∈ ℝ* )
36 34 35 mp1i ⊢ ( 𝜑 → 1 ∈ ℝ* )
37 13 1 3 6 deg1sclle ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ 𝐾 ) → ( 𝐷 ‘ ( 𝐴 ‘ 𝑁 ) ) ≤ 0 )
38 16 11 37 syl2anc ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐴 ‘ 𝑁 ) ) ≤ 0 )
39 0lt1 ⊢ 0 < 1
40 39 a1i ⊢ ( 𝜑 → 0 < 1 )
41 31 33 36 38 40 xrlelttrd ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐴 ‘ 𝑁 ) ) < 1 )
42 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
43 42 2 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
44 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
45 43 44 mulg1 ⊢ ( 𝑋 ∈ 𝐵 → ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) = 𝑋 )
46 22 45 syl ⊢ ( 𝜑 → ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) = 𝑋 )
47 46 fveq2d ⊢ ( 𝜑 → ( 𝐷 ‘ ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) = ( 𝐷 ‘ 𝑋 ) )
48 1nn0 ⊢ 1 ∈ ℕ0
49 13 1 4 42 44 deg1pw ⊢ ( ( 𝑅 ∈ NzRing ∧ 1 ∈ ℕ0 ) → ( 𝐷 ‘ ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) = 1 )
50 9 48 49 sylancl ⊢ ( 𝜑 → ( 𝐷 ‘ ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) = 1 )
51 47 50 eqtr3d ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑋 ) = 1 )
52 41 51 breqtrrd ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐴 ‘ 𝑁 ) ) < ( 𝐷 ‘ 𝑋 ) )
53 1 13 16 2 5 22 25 52 deg1sub ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑋 − ( 𝐴 ‘ 𝑁 ) ) ) = ( 𝐷 ‘ 𝑋 ) )
54 29 53 eqtrid ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) = ( 𝐷 ‘ 𝑋 ) )
55 54 51 eqtrd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) = 1 )
56 55 48 eqeltrdi ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 )
57 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
58 13 1 57 2 deg1nn0clb ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ) → ( 𝐺 ≠ ( 0g ‘ 𝑃 ) ↔ ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 ) )
59 16 28 58 syl2anc ⊢ ( 𝜑 → ( 𝐺 ≠ ( 0g ‘ 𝑃 ) ↔ ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 ) )
60 56 59 mpbird ⊢ ( 𝜑 → 𝐺 ≠ ( 0g ‘ 𝑃 ) )
61 55 fveq2d ⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) = ( ( coe1 ‘ 𝐺 ) ‘ 1 ) )
62 7 fveq2i ⊢ ( coe1 ‘ 𝐺 ) = ( coe1 ‘ ( 𝑋 − ( 𝐴 ‘ 𝑁 ) ) )
63 62 fveq1i ⊢ ( ( coe1 ‘ 𝐺 ) ‘ 1 ) = ( ( coe1 ‘ ( 𝑋 − ( 𝐴 ‘ 𝑁 ) ) ) ‘ 1 )
64 48 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
65 eqid ⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
66 1 2 5 65 coe1subfv ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐴 ‘ 𝑁 ) ∈ 𝐵 ) ∧ 1 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑋 − ( 𝐴 ‘ 𝑁 ) ) ) ‘ 1 ) = ( ( ( coe1 ‘ 𝑋 ) ‘ 1 ) ( -g ‘ 𝑅 ) ( ( coe1 ‘ ( 𝐴 ‘ 𝑁 ) ) ‘ 1 ) ) )
67 16 22 25 64 66 syl31anc ⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑋 − ( 𝐴 ‘ 𝑁 ) ) ) ‘ 1 ) = ( ( ( coe1 ‘ 𝑋 ) ‘ 1 ) ( -g ‘ 𝑅 ) ( ( coe1 ‘ ( 𝐴 ‘ 𝑁 ) ) ‘ 1 ) ) )
68 63 67 eqtrid ⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ 1 ) = ( ( ( coe1 ‘ 𝑋 ) ‘ 1 ) ( -g ‘ 𝑅 ) ( ( coe1 ‘ ( 𝐴 ‘ 𝑁 ) ) ‘ 1 ) ) )
69 46 oveq2d ⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) = ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) 𝑋 ) )
70 1 ply1sca ⊢ ( 𝑅 ∈ NzRing → 𝑅 = ( Scalar ‘ 𝑃 ) )
71 9 70 syl ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
72 71 fveq2d ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) ) )
73 72 oveq1d ⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) 𝑋 ) = ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) 𝑋 ) )
74 1 ply1lmod ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
75 16 74 syl ⊢ ( 𝜑 → 𝑃 ∈ LMod )
76 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
77 eqid ⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
78 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑃 ) ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) )
79 2 76 77 78 lmodvs1 ⊢ ( ( 𝑃 ∈ LMod ∧ 𝑋 ∈ 𝐵 ) → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) 𝑋 ) = 𝑋 )
80 75 22 79 syl2anc ⊢ ( 𝜑 → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) 𝑋 ) = 𝑋 )
81 69 73 80 3eqtrd ⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) = 𝑋 )
82 81 fveq2d ⊢ ( 𝜑 → ( coe1 ‘ ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) ) = ( coe1 ‘ 𝑋 ) )
83 82 fveq1d ⊢ ( 𝜑 → ( ( coe1 ‘ ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) ) ‘ 1 ) = ( ( coe1 ‘ 𝑋 ) ‘ 1 ) )
84 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
85 3 84 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐾 )
86 16 85 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝐾 )
87 14 3 1 4 77 42 44 coe1tmfv1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ∈ 𝐾 ∧ 1 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) ) ‘ 1 ) = ( 1r ‘ 𝑅 ) )
88 16 86 64 87 syl3anc ⊢ ( 𝜑 → ( ( coe1 ‘ ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) 𝑋 ) ) ) ‘ 1 ) = ( 1r ‘ 𝑅 ) )
89 83 88 eqtr3d ⊢ ( 𝜑 → ( ( coe1 ‘ 𝑋 ) ‘ 1 ) = ( 1r ‘ 𝑅 ) )
90 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
91 1 6 3 90 coe1scl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ 𝐾 ) → ( coe1 ‘ ( 𝐴 ‘ 𝑁 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑁 , ( 0g ‘ 𝑅 ) ) ) )
92 16 11 91 syl2anc ⊢ ( 𝜑 → ( coe1 ‘ ( 𝐴 ‘ 𝑁 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑁 , ( 0g ‘ 𝑅 ) ) ) )
93 92 fveq1d ⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝐴 ‘ 𝑁 ) ) ‘ 1 ) = ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑁 , ( 0g ‘ 𝑅 ) ) ) ‘ 1 ) )
94 ax-1ne0 ⊢ 1 ≠ 0
95 neeq1 ⊢ ( 𝑥 = 1 → ( 𝑥 ≠ 0 ↔ 1 ≠ 0 ) )
96 94 95 mpbiri ⊢ ( 𝑥 = 1 → 𝑥 ≠ 0 )
97 ifnefalse ⊢ ( 𝑥 ≠ 0 → if ( 𝑥 = 0 , 𝑁 , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
98 96 97 syl ⊢ ( 𝑥 = 1 → if ( 𝑥 = 0 , 𝑁 , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
99 eqid ⊢ ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑁 , ( 0g ‘ 𝑅 ) ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑁 , ( 0g ‘ 𝑅 ) ) )
100 fvex ⊢ ( 0g ‘ 𝑅 ) ∈ V
101 98 99 100 fvmpt ⊢ ( 1 ∈ ℕ0 → ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑁 , ( 0g ‘ 𝑅 ) ) ) ‘ 1 ) = ( 0g ‘ 𝑅 ) )
102 48 101 ax-mp ⊢ ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑁 , ( 0g ‘ 𝑅 ) ) ) ‘ 1 ) = ( 0g ‘ 𝑅 )
103 93 102 eqtrdi ⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝐴 ‘ 𝑁 ) ) ‘ 1 ) = ( 0g ‘ 𝑅 ) )
104 89 103 oveq12d ⊢ ( 𝜑 → ( ( ( coe1 ‘ 𝑋 ) ‘ 1 ) ( -g ‘ 𝑅 ) ( ( coe1 ‘ ( 𝐴 ‘ 𝑁 ) ) ‘ 1 ) ) = ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
105 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
106 16 105 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
107 3 90 65 grpsubid1 ⊢ ( ( 𝑅 ∈ Grp ∧ ( 1r ‘ 𝑅 ) ∈ 𝐾 ) → ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
108 106 86 107 syl2anc ⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
109 104 108 eqtrd ⊢ ( 𝜑 → ( ( ( coe1 ‘ 𝑋 ) ‘ 1 ) ( -g ‘ 𝑅 ) ( ( coe1 ‘ ( 𝐴 ‘ 𝑁 ) ) ‘ 1 ) ) = ( 1r ‘ 𝑅 ) )
110 61 68 109 3eqtrd ⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) = ( 1r ‘ 𝑅 ) )
111 1 2 57 13 12 84 ismon1p ⊢ ( 𝐺 ∈ 𝑈 ↔ ( 𝐺 ∈ 𝐵 ∧ 𝐺 ≠ ( 0g ‘ 𝑃 ) ∧ ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) = ( 1r ‘ 𝑅 ) ) )
112 28 60 110 111 syl3anbrc ⊢ ( 𝜑 → 𝐺 ∈ 𝑈 )
113 7 fveq2i ⊢ ( 𝑂 ‘ 𝐺 ) = ( 𝑂 ‘ ( 𝑋 − ( 𝐴 ‘ 𝑁 ) ) )
114 113 fveq1i ⊢ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = ( ( 𝑂 ‘ ( 𝑋 − ( 𝐴 ‘ 𝑁 ) ) ) ‘ 𝑥 )
115 10 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → 𝑅 ∈ CRing )
116 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → 𝑥 ∈ 𝐾 )
117 8 4 3 1 2 115 116 evl1vard ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( 𝑋 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑋 ) ‘ 𝑥 ) = 𝑥 ) )
118 11 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → 𝑁 ∈ 𝐾 )
119 8 1 3 6 2 115 118 116 evl1scad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( ( 𝐴 ‘ 𝑁 ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝐴 ‘ 𝑁 ) ) ‘ 𝑥 ) = 𝑁 ) )
120 8 1 3 2 115 116 117 119 5 65 evl1subd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( ( 𝑋 − ( 𝐴 ‘ 𝑁 ) ) ∈ 𝐵 ∧ ( ( 𝑂 ‘ ( 𝑋 − ( 𝐴 ‘ 𝑁 ) ) ) ‘ 𝑥 ) = ( 𝑥 ( -g ‘ 𝑅 ) 𝑁 ) ) )
121 120 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( ( 𝑂 ‘ ( 𝑋 − ( 𝐴 ‘ 𝑁 ) ) ) ‘ 𝑥 ) = ( 𝑥 ( -g ‘ 𝑅 ) 𝑁 ) )
122 114 121 eqtrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = ( 𝑥 ( -g ‘ 𝑅 ) 𝑁 ) )
123 122 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 0 ↔ ( 𝑥 ( -g ‘ 𝑅 ) 𝑁 ) = 0 ) )
124 106 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → 𝑅 ∈ Grp )
125 3 14 65 grpsubeq0 ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑥 ∈ 𝐾 ∧ 𝑁 ∈ 𝐾 ) → ( ( 𝑥 ( -g ‘ 𝑅 ) 𝑁 ) = 0 ↔ 𝑥 = 𝑁 ) )
126 124 116 118 125 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( ( 𝑥 ( -g ‘ 𝑅 ) 𝑁 ) = 0 ↔ 𝑥 = 𝑁 ) )
127 123 126 bitrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 0 ↔ 𝑥 = 𝑁 ) )
128 velsn ⊢ ( 𝑥 ∈ { 𝑁 } ↔ 𝑥 = 𝑁 )
129 127 128 bitr4di ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 0 ↔ 𝑥 ∈ { 𝑁 } ) )
130 129 pm5.32da ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 0 ) ↔ ( 𝑥 ∈ 𝐾 ∧ 𝑥 ∈ { 𝑁 } ) ) )
131 eqid ⊢ ( 𝑅 ↑s 𝐾 ) = ( 𝑅 ↑s 𝐾 )
132 eqid ⊢ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) = ( Base ‘ ( 𝑅 ↑s 𝐾 ) )
133 3 fvexi ⊢ 𝐾 ∈ V
134 133 a1i ⊢ ( 𝜑 → 𝐾 ∈ V )
135 8 1 131 3 evl1rhm ⊢ ( 𝑅 ∈ CRing → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐾 ) ) )
136 10 135 syl ⊢ ( 𝜑 → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐾 ) ) )
137 2 132 rhmf ⊢ ( 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐾 ) ) → 𝑂 : 𝐵 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
138 136 137 syl ⊢ ( 𝜑 → 𝑂 : 𝐵 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
139 138 28 ffvelcdmd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐺 ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐾 ) ) )
140 131 3 132 9 134 139 pwselbas ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐺 ) : 𝐾 ⟶ 𝐾 )
141 140 ffnd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐺 ) Fn 𝐾 )
142 fniniseg ⊢ ( ( 𝑂 ‘ 𝐺 ) Fn 𝐾 → ( 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐺 ) “ { 0 } ) ↔ ( 𝑥 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 0 ) ) )
143 141 142 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐺 ) “ { 0 } ) ↔ ( 𝑥 ∈ 𝐾 ∧ ( ( 𝑂 ‘ 𝐺 ) ‘ 𝑥 ) = 0 ) ) )
144 11 snssd ⊢ ( 𝜑 → { 𝑁 } ⊆ 𝐾 )
145 144 sseld ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑁 } → 𝑥 ∈ 𝐾 ) )
146 145 pm4.71rd ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑁 } ↔ ( 𝑥 ∈ 𝐾 ∧ 𝑥 ∈ { 𝑁 } ) ) )
147 130 143 146 3bitr4d ⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝐺 ) “ { 0 } ) ↔ 𝑥 ∈ { 𝑁 } ) )
148 147 eqrdv ⊢ ( 𝜑 → ( ◡ ( 𝑂 ‘ 𝐺 ) “ { 0 } ) = { 𝑁 } )
149 112 55 148 3jca ⊢ ( 𝜑 → ( 𝐺 ∈ 𝑈 ∧ ( 𝐷 ‘ 𝐺 ) = 1 ∧ ( ◡ ( 𝑂 ‘ 𝐺 ) “ { 0 } ) = { 𝑁 } ) )