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	ffvelrnd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑁 ) ∈ 𝐵 )
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	ffvelrnd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐺 ) ∈ ( 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 } ) = { 𝑁 } ) )