Theorem rngunsnply1chr2lem2

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

	Ref	Expression
Hypotheses	rngunsnply1chr2.v	|- V = ( Base ` R )
	rngunsnply1chr2.p	|- P = ( Poly1 ` ( R |`s S ) )
	rngunsnply1chr2.u	|- U = ( Base ` P )
	rngunsnply1chr2.q	|- Q = ( R evalSub1 S )
	rngunsnply1chr2.r	|- ( ph -> R e. CRing )
	rngunsnply1chr2.1	|- ( ph -> R e. NzRing )
	rngunsnply1chr2.s	|- ( ph -> S e. ( SubRing ` R ) )
	rngunsnply1chr2.x	|- ( ph -> X e. V )
	rngunsnply1chr2.y	|- ( ph -> Y e. ( N ` ( S u. { X } ) ) )
	rngunsnply1chr2.n	|- N = ( RingSpan ` R )
	rngunsnply1chr2.2	|- .+ = ( +g ` R )
	rngunsnply1chr2.3	|- .x. = ( .r ` R )
	rngunsnply1chr2.4	|- .^ = ( .g ` ( mulGrp ` R ) )
	rngunsnply1chr2.a	|- ( ph -> A e. S )
	rngunsnply1chr2.b	|- ( ph -> B e. S )
	rngunsnply1chr2.5	|- ( ph -> ( 2 .^ X ) = ( ( A .x. X ) .+ B ) )
	rngunsnply1chr2lem.d	|- D = ( deg1 ` R )
	rngunsnply1chr2lem.e	|- E = ( rem1p ` ( R |`s S ) )
	rngunsnply1chr2lem.g	|- G = ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) )
	rngunsnply1chr2lem.h	|- H = ( F E G )
	rngunsnply1chr2lem.f	|- ( ph -> F e. U )
Assertion	rngunsnply1chr2lem2	|- ( ph -> G e. ( Unic1p ` ( R |`s S ) ) )

Proof

Step	Hyp	Ref	Expression
1		rngunsnply1chr2.v	|- V = ( Base ` R )
2		rngunsnply1chr2.p	|- P = ( Poly1 ` ( R |`s S ) )
3		rngunsnply1chr2.u	|- U = ( Base ` P )
4		rngunsnply1chr2.q	|- Q = ( R evalSub1 S )
5		rngunsnply1chr2.r	|- ( ph -> R e. CRing )
6		rngunsnply1chr2.1	|- ( ph -> R e. NzRing )
7		rngunsnply1chr2.s	|- ( ph -> S e. ( SubRing ` R ) )
8		rngunsnply1chr2.x	|- ( ph -> X e. V )
9		rngunsnply1chr2.y	|- ( ph -> Y e. ( N ` ( S u. { X } ) ) )
10		rngunsnply1chr2.n	|- N = ( RingSpan ` R )
11		rngunsnply1chr2.2	|- .+ = ( +g ` R )
12		rngunsnply1chr2.3	|- .x. = ( .r ` R )
13		rngunsnply1chr2.4	|- .^ = ( .g ` ( mulGrp ` R ) )
14		rngunsnply1chr2.a	|- ( ph -> A e. S )
15		rngunsnply1chr2.b	|- ( ph -> B e. S )
16		rngunsnply1chr2.5	|- ( ph -> ( 2 .^ X ) = ( ( A .x. X ) .+ B ) )
17		rngunsnply1chr2lem.d	|- D = ( deg1 ` R )
18		rngunsnply1chr2lem.e	|- E = ( rem1p ` ( R |`s S ) )
19		rngunsnply1chr2lem.g	|- G = ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) )
20		rngunsnply1chr2lem.h	|- H = ( F E G )
21		rngunsnply1chr2lem.f	|- ( ph -> F e. U )
22		eqid	|- ( R |`s S ) = ( R |`s S )
23	22	subrgring	|- ( S e. ( SubRing ` R ) -> ( R |`s S ) e. Ring )
24	7 23	syl	|- ( ph -> ( R |`s S ) e. Ring )
25		eqid	|- ( -g ` P ) = ( -g ` P )
26	2	ply1ring	|- ( ( R |`s S ) e. Ring -> P e. Ring )
27	24 26	syl	|- ( ph -> P e. Ring )
28	27	ringgrpd	|- ( ph -> P e. Grp )
29		eqid	|- ( mulGrp ` P ) = ( mulGrp ` P )
30	29 3	mgpbas	|- U = ( Base ` ( mulGrp ` P ) )
31		eqid	|- ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
32	29	ringmgp	|- ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
33	27 32	syl	|- ( ph -> ( mulGrp ` P ) e. Mnd )
34		2nn0	|- 2 e. NN0
35	34	a1i	|- ( ph -> 2 e. NN0 )
36		eqid	|- ( var1 ` R ) = ( var1 ` R )
37	36 7 22 2 3	subrgvr1cl	|- ( ph -> ( var1 ` R ) e. U )
38	30 31 33 35 37	mulgnn0cld	|- ( ph -> ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. U )
39		eqid	|- ( +g ` P ) = ( +g ` P )
40		eqid	|- ( Scalar ` P ) = ( Scalar ` P )
41		eqid	|- ( .s ` P ) = ( .s ` P )
42		eqid	|- ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
43	2	ply1lmod	|- ( ( R |`s S ) e. Ring -> P e. LMod )
44	24 43	syl	|- ( ph -> P e. LMod )
45	22	subrgbas	|- ( S e. ( SubRing ` R ) -> S = ( Base ` ( R |`s S ) ) )
46	7 45	syl	|- ( ph -> S = ( Base ` ( R |`s S ) ) )
47		ovex	|- ( R |`s S ) e. _V
48	2	ply1sca	|- ( ( R |`s S ) e. _V -> ( R |`s S ) = ( Scalar ` P ) )
49	47 48	ax-mp	|- ( R |`s S ) = ( Scalar ` P )
50	49	fveq2i	|- ( Base ` ( R |`s S ) ) = ( Base ` ( Scalar ` P ) )
51	46 50	eqtrdi	|- ( ph -> S = ( Base ` ( Scalar ` P ) ) )
52	14 51	eleqtrd	|- ( ph -> A e. ( Base ` ( Scalar ` P ) ) )
53	3 40 41 42 44 52 37	lmodvscld	|- ( ph -> ( A ( .s ` P ) ( var1 ` R ) ) e. U )
54		eqid	|- ( algSc ` P ) = ( algSc ` P )
55	2 22 54 3 5 7 15	ressasclcl	|- ( ph -> ( ( algSc ` P ) ` B ) e. U )
56	3 39 28 53 55	grpcld	|- ( ph -> ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) e. U )
57	3 25 28 38 56	grpsubcld	|- ( ph -> ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) e. U )
58	19 57	eqeltrid	|- ( ph -> G e. U )
59		eqid	|- ( Poly1 ` R ) = ( Poly1 ` R )
60		eqid	|- ( PwSer1 ` ( R |`s S ) ) = ( PwSer1 ` ( R |`s S ) )
61		eqid	|- ( Base ` ( PwSer1 ` ( R |`s S ) ) ) = ( Base ` ( PwSer1 ` ( R |`s S ) ) )
62		eqid	|- ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
63	59 22 2 3 7 60 61 62	ressply1bas2	|- ( ph -> U = ( ( Base ` ( PwSer1 ` ( R |`s S ) ) ) i^i ( Base ` ( Poly1 ` R ) ) ) )
64	58 63	eleqtrd	|- ( ph -> G e. ( ( Base ` ( PwSer1 ` ( R |`s S ) ) ) i^i ( Base ` ( Poly1 ` R ) ) ) )
65	64	elin2d	|- ( ph -> G e. ( Base ` ( Poly1 ` R ) ) )
66	5	crngringd	|- ( ph -> R e. Ring )
67	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21	rngunsnply1chr2lem1	|- ( ph -> ( D ` G ) = 2 )
68	67 34	eqeltrdi	|- ( ph -> ( D ` G ) e. NN0 )
69		eqid	|- ( 0g ` ( Poly1 ` R ) ) = ( 0g ` ( Poly1 ` R ) )
70	17 59 69 62	deg1nn0clb	|- ( ( R e. Ring /\ G e. ( Base ` ( Poly1 ` R ) ) ) -> ( G =/= ( 0g ` ( Poly1 ` R ) ) <-> ( D ` G ) e. NN0 ) )
71	70	biimpar	|- ( ( ( R e. Ring /\ G e. ( Base ` ( Poly1 ` R ) ) ) /\ ( D ` G ) e. NN0 ) -> G =/= ( 0g ` ( Poly1 ` R ) ) )
72	66 65 68 71	syl21anc	|- ( ph -> G =/= ( 0g ` ( Poly1 ` R ) ) )
73	19	fveq2i	|- ( coe1 ` G ) = ( coe1 ` ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) )
74	73	a1i	|- ( ph -> ( coe1 ` G ) = ( coe1 ` ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) )
75	74 67	fveq12d	|- ( ph -> ( ( coe1 ` G ) ` ( D ` G ) ) = ( ( coe1 ` ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ` 2 ) )
76		eqid	|- ( -g ` ( R |`s S ) ) = ( -g ` ( R |`s S ) )
77	2 3 25 76	coe1subfv	|- ( ( ( ( R |`s S ) e. Ring /\ ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. U /\ ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) e. U ) /\ 2 e. NN0 ) -> ( ( coe1 ` ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ` 2 ) = ( ( ( coe1 ` ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ` 2 ) ( -g ` ( R |`s S ) ) ( ( coe1 ` ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ` 2 ) ) )
78	24 38 56 35 77	syl31anc	|- ( ph -> ( ( coe1 ` ( ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ( -g ` P ) ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ) ` 2 ) = ( ( ( coe1 ` ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ` 2 ) ( -g ` ( R |`s S ) ) ( ( coe1 ` ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ` 2 ) ) )
79	36 7 22	subrgvr1	|- ( ph -> ( var1 ` R ) = ( var1 ` ( R |`s S ) ) )
80	79 37	eqeltrrd	|- ( ph -> ( var1 ` ( R |`s S ) ) e. U )
81	30 31 33 35 80	mulgnn0cld	|- ( ph -> ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) e. U )
82		eqid	|- ( 1r ` ( Scalar ` P ) ) = ( 1r ` ( Scalar ` P ) )
83	3 40 41 82	lmodvs1	|- ( ( P e. LMod /\ ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) e. U ) -> ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) ) = ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) )
84	44 81 83	syl2anc	|- ( ph -> ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) ) = ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) )
85		eqid	|- ( 1r ` R ) = ( 1r ` R )
86	22 85	subrg1	|- ( S e. ( SubRing ` R ) -> ( 1r ` R ) = ( 1r ` ( R |`s S ) ) )
87	7 86	syl	|- ( ph -> ( 1r ` R ) = ( 1r ` ( R |`s S ) ) )
88	49	fveq2i	|- ( 1r ` ( R |`s S ) ) = ( 1r ` ( Scalar ` P ) )
89	87 88	eqtrdi	|- ( ph -> ( 1r ` R ) = ( 1r ` ( Scalar ` P ) ) )
90	89	oveq1d	|- ( ph -> ( ( 1r ` R ) ( .s ` P ) ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) ) = ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) ) )
91	79	oveq2d	|- ( ph -> ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) )
92	84 90 91	3eqtr4d	|- ( ph -> ( ( 1r ` R ) ( .s ` P ) ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) ) = ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) )
93	92	fveq2d	|- ( ph -> ( coe1 ` ( ( 1r ` R ) ( .s ` P ) ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) ) ) = ( coe1 ` ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
94	93	fveq1d	|- ( ph -> ( ( coe1 ` ( ( 1r ` R ) ( .s ` P ) ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) ) ) ` 2 ) = ( ( coe1 ` ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ` 2 ) )
95	85	subrg1cl	|- ( S e. ( SubRing ` R ) -> ( 1r ` R ) e. S )
96	7 95	syl	|- ( ph -> ( 1r ` R ) e. S )
97	96 46	eleqtrd	|- ( ph -> ( 1r ` R ) e. ( Base ` ( R |`s S ) ) )
98		eqid	|- ( 0g ` ( R |`s S ) ) = ( 0g ` ( R |`s S ) )
99		eqid	|- ( Base ` ( R |`s S ) ) = ( Base ` ( R |`s S ) )
100		eqid	|- ( var1 ` ( R |`s S ) ) = ( var1 ` ( R |`s S ) )
101	98 99 2 100 41 29 31	coe1tmfv1	|- ( ( ( R |`s S ) e. Ring /\ ( 1r ` R ) e. ( Base ` ( R |`s S ) ) /\ 2 e. NN0 ) -> ( ( coe1 ` ( ( 1r ` R ) ( .s ` P ) ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) ) ) ` 2 ) = ( 1r ` R ) )
102	24 97 35 101	syl3anc	|- ( ph -> ( ( coe1 ` ( ( 1r ` R ) ( .s ` P ) ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) ) ) ` 2 ) = ( 1r ` R ) )
103	94 102	eqtr3d	|- ( ph -> ( ( coe1 ` ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ` 2 ) = ( 1r ` R ) )
104		eqid	|- ( +g ` ( R |`s S ) ) = ( +g ` ( R |`s S ) )
105	2 3 39 104	coe1addfv	|- ( ( ( ( R |`s S ) e. Ring /\ ( A ( .s ` P ) ( var1 ` R ) ) e. U /\ ( ( algSc ` P ) ` B ) e. U ) /\ 2 e. NN0 ) -> ( ( coe1 ` ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ` 2 ) = ( ( ( coe1 ` ( A ( .s ` P ) ( var1 ` R ) ) ) ` 2 ) ( +g ` ( R |`s S ) ) ( ( coe1 ` ( ( algSc ` P ) ` B ) ) ` 2 ) ) )
106	24 53 55 35 105	syl31anc	|- ( ph -> ( ( coe1 ` ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ` 2 ) = ( ( ( coe1 ` ( A ( .s ` P ) ( var1 ` R ) ) ) ` 2 ) ( +g ` ( R |`s S ) ) ( ( coe1 ` ( ( algSc ` P ) ` B ) ) ` 2 ) ) )
107	66	ringgrpd	|- ( ph -> R e. Grp )
108	107	grpmndd	|- ( ph -> R e. Mnd )
109		subrgsubg	|- ( S e. ( SubRing ` R ) -> S e. ( SubGrp ` R ) )
110	7 109	syl	|- ( ph -> S e. ( SubGrp ` R ) )
111		eqid	|- ( 0g ` R ) = ( 0g ` R )
112	111	subg0cl	|- ( S e. ( SubGrp ` R ) -> ( 0g ` R ) e. S )
113	110 112	syl	|- ( ph -> ( 0g ` R ) e. S )
114	1	subrgss	|- ( S e. ( SubRing ` R ) -> S C_ V )
115	7 114	syl	|- ( ph -> S C_ V )
116	22 1 111	ress0g	|- ( ( R e. Mnd /\ ( 0g ` R ) e. S /\ S C_ V ) -> ( 0g ` R ) = ( 0g ` ( R |`s S ) ) )
117	108 113 115 116	syl3anc	|- ( ph -> ( 0g ` R ) = ( 0g ` ( R |`s S ) ) )
118	14 46	eleqtrd	|- ( ph -> A e. ( Base ` ( R |`s S ) ) )
119		1nn0	|- 1 e. NN0
120	119	a1i	|- ( ph -> 1 e. NN0 )
121		1ne2	|- 1 =/= 2
122	121	a1i	|- ( ph -> 1 =/= 2 )
123	98 99 2 100 41 29 31 24 118 120 35 122	coe1tmfv2	|- ( ph -> ( ( coe1 ` ( A ( .s ` P ) ( 1 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) ) ) ` 2 ) = ( 0g ` ( R |`s S ) ) )
124	30 31	mulg1	|- ( ( var1 ` ( R |`s S ) ) e. U -> ( 1 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) = ( var1 ` ( R |`s S ) ) )
125	80 124	syl	|- ( ph -> ( 1 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) = ( var1 ` ( R |`s S ) ) )
126	125 79	eqtr4d	|- ( ph -> ( 1 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) = ( var1 ` R ) )
127	126	oveq2d	|- ( ph -> ( A ( .s ` P ) ( 1 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) ) = ( A ( .s ` P ) ( var1 ` R ) ) )
128	127	fveq2d	|- ( ph -> ( coe1 ` ( A ( .s ` P ) ( 1 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) ) ) = ( coe1 ` ( A ( .s ` P ) ( var1 ` R ) ) ) )
129	128	fveq1d	|- ( ph -> ( ( coe1 ` ( A ( .s ` P ) ( 1 ( .g ` ( mulGrp ` P ) ) ( var1 ` ( R |`s S ) ) ) ) ) ` 2 ) = ( ( coe1 ` ( A ( .s ` P ) ( var1 ` R ) ) ) ` 2 ) )
130	117 123 129	3eqtr2rd	|- ( ph -> ( ( coe1 ` ( A ( .s ` P ) ( var1 ` R ) ) ) ` 2 ) = ( 0g ` R ) )
131	15 46	eleqtrd	|- ( ph -> B e. ( Base ` ( R |`s S ) ) )
132	2 54 99 98	coe1scl	|- ( ( ( R |`s S ) e. Ring /\ B e. ( Base ` ( R |`s S ) ) ) -> ( coe1 ` ( ( algSc ` P ) ` B ) ) = ( i e. NN0 |-> if ( i = 0 , B , ( 0g ` ( R |`s S ) ) ) ) )
133	24 131 132	syl2anc	|- ( ph -> ( coe1 ` ( ( algSc ` P ) ` B ) ) = ( i e. NN0 |-> if ( i = 0 , B , ( 0g ` ( R |`s S ) ) ) ) )
134		simpr	|- ( ( ph /\ i = 2 ) -> i = 2 )
135		2ne0	|- 2 =/= 0
136	135	a1i	|- ( ( ph /\ i = 2 ) -> 2 =/= 0 )
137	134 136	eqnetrd	|- ( ( ph /\ i = 2 ) -> i =/= 0 )
138	137	neneqd	|- ( ( ph /\ i = 2 ) -> -. i = 0 )
139	138	iffalsed	|- ( ( ph /\ i = 2 ) -> if ( i = 0 , B , ( 0g ` ( R |`s S ) ) ) = ( 0g ` ( R |`s S ) ) )
140	117	adantr	|- ( ( ph /\ i = 2 ) -> ( 0g ` R ) = ( 0g ` ( R |`s S ) ) )
141	139 140	eqtr4d	|- ( ( ph /\ i = 2 ) -> if ( i = 0 , B , ( 0g ` ( R |`s S ) ) ) = ( 0g ` R ) )
142		fvexd	|- ( ph -> ( 0g ` R ) e. _V )
143	133 141 35 142	fvmptd	|- ( ph -> ( ( coe1 ` ( ( algSc ` P ) ` B ) ) ` 2 ) = ( 0g ` R ) )
144	130 143	oveq12d	|- ( ph -> ( ( ( coe1 ` ( A ( .s ` P ) ( var1 ` R ) ) ) ` 2 ) ( +g ` ( R |`s S ) ) ( ( coe1 ` ( ( algSc ` P ) ` B ) ) ` 2 ) ) = ( ( 0g ` R ) ( +g ` ( R |`s S ) ) ( 0g ` R ) ) )
145	22 11	ressplusg	|- ( S e. ( SubRing ` R ) -> .+ = ( +g ` ( R |`s S ) ) )
146	7 145	syl	|- ( ph -> .+ = ( +g ` ( R |`s S ) ) )
147	146	oveqd	|- ( ph -> ( ( 0g ` R ) .+ ( 0g ` R ) ) = ( ( 0g ` R ) ( +g ` ( R |`s S ) ) ( 0g ` R ) ) )
148	1 111 107	grpidcld	|- ( ph -> ( 0g ` R ) e. V )
149	1 11 111 107 148	grplidd	|- ( ph -> ( ( 0g ` R ) .+ ( 0g ` R ) ) = ( 0g ` R ) )
150	147 149	eqtr3d	|- ( ph -> ( ( 0g ` R ) ( +g ` ( R |`s S ) ) ( 0g ` R ) ) = ( 0g ` R ) )
151	106 144 150	3eqtrd	|- ( ph -> ( ( coe1 ` ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ` 2 ) = ( 0g ` R ) )
152	103 151	oveq12d	|- ( ph -> ( ( ( coe1 ` ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ` 2 ) ( -g ` ( R |`s S ) ) ( ( coe1 ` ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ` 2 ) ) = ( ( 1r ` R ) ( -g ` ( R |`s S ) ) ( 0g ` R ) ) )
153		eqid	|- ( -g ` R ) = ( -g ` R )
154	153 22 76	subgsub	|- ( ( S e. ( SubGrp ` R ) /\ ( 1r ` R ) e. S /\ ( 0g ` R ) e. S ) -> ( ( 1r ` R ) ( -g ` R ) ( 0g ` R ) ) = ( ( 1r ` R ) ( -g ` ( R |`s S ) ) ( 0g ` R ) ) )
155	110 96 113 154	syl3anc	|- ( ph -> ( ( 1r ` R ) ( -g ` R ) ( 0g ` R ) ) = ( ( 1r ` R ) ( -g ` ( R |`s S ) ) ( 0g ` R ) ) )
156	1 85 66	ringidcld	|- ( ph -> ( 1r ` R ) e. V )
157	1 111 153	grpsubid1	|- ( ( R e. Grp /\ ( 1r ` R ) e. V ) -> ( ( 1r ` R ) ( -g ` R ) ( 0g ` R ) ) = ( 1r ` R ) )
158	107 156 157	syl2anc	|- ( ph -> ( ( 1r ` R ) ( -g ` R ) ( 0g ` R ) ) = ( 1r ` R ) )
159	152 155 158	3eqtr2d	|- ( ph -> ( ( ( coe1 ` ( 2 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ` 2 ) ( -g ` ( R |`s S ) ) ( ( coe1 ` ( ( A ( .s ` P ) ( var1 ` R ) ) ( +g ` P ) ( ( algSc ` P ) ` B ) ) ) ` 2 ) ) = ( 1r ` R ) )
160	75 78 159	3eqtrd	|- ( ph -> ( ( coe1 ` G ) ` ( D ` G ) ) = ( 1r ` R ) )
161		eqid	|- ( Monic1p ` R ) = ( Monic1p ` R )
162	59 62 69 17 161 85	ismon1p	|- ( G e. ( Monic1p ` R ) <-> ( G e. ( Base ` ( Poly1 ` R ) ) /\ G =/= ( 0g ` ( Poly1 ` R ) ) /\ ( ( coe1 ` G ) ` ( D ` G ) ) = ( 1r ` R ) ) )
163	65 72 160 162	syl3anbrc	|- ( ph -> G e. ( Monic1p ` R ) )
164	58 163	elind	|- ( ph -> G e. ( U i^i ( Monic1p ` R ) ) )
165		eqid	|- ( Monic1p ` ( R |`s S ) ) = ( Monic1p ` ( R |`s S ) )
166	59 22 2 3 7 161 165	ressply1mon1p	|- ( ph -> ( Monic1p ` ( R |`s S ) ) = ( U i^i ( Monic1p ` R ) ) )
167	164 166	eleqtrrd	|- ( ph -> G e. ( Monic1p ` ( R |`s S ) ) )
168		eqid	|- ( Unic1p ` ( R |`s S ) ) = ( Unic1p ` ( R |`s S ) )
169	168 165	mon1puc1p	|- ( ( ( R |`s S ) e. Ring /\ G e. ( Monic1p ` ( R |`s S ) ) ) -> G e. ( Unic1p ` ( R |`s S ) ) )
170	24 167 169	syl2anc	|- ( ph -> G e. ( Unic1p ` ( R |`s S ) ) )