Theorem rngunsnply1chr2lem2

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	rngunsnply1chr2lem2	⊢ ( 𝜑 → 𝐺 ∈ ( Unic1p ‘ ( 𝑅 ↾s 𝑆 ) ) )

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		eqid	⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
23	22	subrgring	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑅 ↾s 𝑆 ) ∈ Ring )
24	7 23	syl	⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ Ring )
25		eqid	⊢ ( -g ‘ 𝑃 ) = ( -g ‘ 𝑃 )
26	2	ply1ring	⊢ ( ( 𝑅 ↾s 𝑆 ) ∈ Ring → 𝑃 ∈ Ring )
27	24 26	syl	⊢ ( 𝜑 → 𝑃 ∈ Ring )
28	27	ringgrpd	⊢ ( 𝜑 → 𝑃 ∈ Grp )
29		eqid	⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
30	29 3	mgpbas	⊢ 𝑈 = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
31		eqid	⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
32	29	ringmgp	⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
33	27 32	syl	⊢ ( 𝜑 → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
34		2nn0	⊢ 2 ∈ ℕ0
35	34	a1i	⊢ ( 𝜑 → 2 ∈ ℕ0 )
36		eqid	⊢ ( var1 ‘ 𝑅 ) = ( var1 ‘ 𝑅 )
37	36 7 22 2 3	subrgvr1cl	⊢ ( 𝜑 → ( var1 ‘ 𝑅 ) ∈ 𝑈 )
38	30 31 33 35 37	mulgnn0cld	⊢ ( 𝜑 → ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ 𝑈 )
39		eqid	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
40		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
41		eqid	⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
42		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
43	2	ply1lmod	⊢ ( ( 𝑅 ↾s 𝑆 ) ∈ Ring → 𝑃 ∈ LMod )
44	24 43	syl	⊢ ( 𝜑 → 𝑃 ∈ LMod )
45	22	subrgbas	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 = ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
46	7 45	syl	⊢ ( 𝜑 → 𝑆 = ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
47		ovex	⊢ ( 𝑅 ↾s 𝑆 ) ∈ V
48	2	ply1sca	⊢ ( ( 𝑅 ↾s 𝑆 ) ∈ V → ( 𝑅 ↾s 𝑆 ) = ( Scalar ‘ 𝑃 ) )
49	47 48	ax-mp	⊢ ( 𝑅 ↾s 𝑆 ) = ( Scalar ‘ 𝑃 )
50	49	fveq2i	⊢ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
51	46 50	eqtrdi	⊢ ( 𝜑 → 𝑆 = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
52	14 51	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
53	3 40 41 42 44 52 37	lmodvscld	⊢ ( 𝜑 → ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ∈ 𝑈 )
54		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
55	2 22 54 3 5 7 15	ressasclcl	⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ∈ 𝑈 )
56	3 39 28 53 55	grpcld	⊢ ( 𝜑 → ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ∈ 𝑈 )
57	3 25 28 38 56	grpsubcld	⊢ ( 𝜑 → ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ∈ 𝑈 )
58	19 57	eqeltrid	⊢ ( 𝜑 → 𝐺 ∈ 𝑈 )
59		eqid	⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
60		eqid	⊢ ( PwSer1 ‘ ( 𝑅 ↾s 𝑆 ) ) = ( PwSer1 ‘ ( 𝑅 ↾s 𝑆 ) )
61		eqid	⊢ ( Base ‘ ( PwSer1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) = ( Base ‘ ( PwSer1 ‘ ( 𝑅 ↾s 𝑆 ) ) )
62		eqid	⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
63	59 22 2 3 7 60 61 62	ressply1bas2	⊢ ( 𝜑 → 𝑈 = ( ( Base ‘ ( PwSer1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) )
64	58 63	eleqtrd	⊢ ( 𝜑 → 𝐺 ∈ ( ( Base ‘ ( PwSer1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) )
65	64	elin2d	⊢ ( 𝜑 → 𝐺 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
66	5	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
67	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21	rngunsnply1chr2lem1	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) = 2 )
68	67 34	eqeltrdi	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 )
69		eqid	⊢ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) = ( 0g ‘ ( Poly1 ‘ 𝑅 ) )
70	17 59 69 62	deg1nn0clb	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( 𝐺 ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) ↔ ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 ) )
71	70	biimpar	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) ∧ ( 𝐷 ‘ 𝐺 ) ∈ ℕ0 ) → 𝐺 ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) )
72	66 65 68 71	syl21anc	⊢ ( 𝜑 → 𝐺 ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) )
73	19	fveq2i	⊢ ( coe1 ‘ 𝐺 ) = ( coe1 ‘ ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) )
74	73	a1i	⊢ ( 𝜑 → ( coe1 ‘ 𝐺 ) = ( coe1 ‘ ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) )
75	74 67	fveq12d	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) = ( ( coe1 ‘ ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ‘ 2 ) )
76		eqid	⊢ ( -g ‘ ( 𝑅 ↾s 𝑆 ) ) = ( -g ‘ ( 𝑅 ↾s 𝑆 ) )
77	2 3 25 76	coe1subfv	⊢ ( ( ( ( 𝑅 ↾s 𝑆 ) ∈ Ring ∧ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ 𝑈 ∧ ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ∈ 𝑈 ) ∧ 2 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ‘ 2 ) = ( ( ( coe1 ‘ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ‘ 2 ) ( -g ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( coe1 ‘ ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ‘ 2 ) ) )
78	24 38 56 35 77	syl31anc	⊢ ( 𝜑 → ( ( coe1 ‘ ( ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ) ‘ 2 ) = ( ( ( coe1 ‘ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ‘ 2 ) ( -g ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( coe1 ‘ ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ‘ 2 ) ) )
79	36 7 22	subrgvr1	⊢ ( 𝜑 → ( var1 ‘ 𝑅 ) = ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) )
80	79 37	eqeltrrd	⊢ ( 𝜑 → ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ∈ 𝑈 )
81	30 31 33 35 80	mulgnn0cld	⊢ ( 𝜑 → ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∈ 𝑈 )
82		eqid	⊢ ( 1r ‘ ( Scalar ‘ 𝑃 ) ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) )
83	3 40 41 82	lmodvs1	⊢ ( ( 𝑃 ∈ LMod ∧ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∈ 𝑈 ) → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) = ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) )
84	44 81 83	syl2anc	⊢ ( 𝜑 → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) = ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) )
85		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
86	22 85	subrg1	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) )
87	7 86	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) )
88	49	fveq2i	⊢ ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) )
89	87 88	eqtrdi	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) ) )
90	89	oveq1d	⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) = ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) )
91	79	oveq2d	⊢ ( 𝜑 → ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) = ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) )
92	84 90 91	3eqtr4d	⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) = ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) )
93	92	fveq2d	⊢ ( 𝜑 → ( coe1 ‘ ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) ) = ( coe1 ‘ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
94	93	fveq1d	⊢ ( 𝜑 → ( ( coe1 ‘ ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) ) ‘ 2 ) = ( ( coe1 ‘ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ‘ 2 ) )
95	85	subrg1cl	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
96	7 95	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
97	96 46	eleqtrd	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
98		eqid	⊢ ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) )
99		eqid	⊢ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) = ( Base ‘ ( 𝑅 ↾s 𝑆 ) )
100		eqid	⊢ ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) = ( var1 ‘ ( 𝑅 ↾s 𝑆 ) )
101	98 99 2 100 41 29 31	coe1tmfv1	⊢ ( ( ( 𝑅 ↾s 𝑆 ) ∈ Ring ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ∧ 2 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) ) ‘ 2 ) = ( 1r ‘ 𝑅 ) )
102	24 97 35 101	syl3anc	⊢ ( 𝜑 → ( ( coe1 ‘ ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) ) ‘ 2 ) = ( 1r ‘ 𝑅 ) )
103	94 102	eqtr3d	⊢ ( 𝜑 → ( ( coe1 ‘ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ‘ 2 ) = ( 1r ‘ 𝑅 ) )
104		eqid	⊢ ( +g ‘ ( 𝑅 ↾s 𝑆 ) ) = ( +g ‘ ( 𝑅 ↾s 𝑆 ) )
105	2 3 39 104	coe1addfv	⊢ ( ( ( ( 𝑅 ↾s 𝑆 ) ∈ Ring ∧ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ∈ 𝑈 ∧ ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ∈ 𝑈 ) ∧ 2 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ‘ 2 ) = ( ( ( coe1 ‘ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) ‘ 2 ) ( +g ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( coe1 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ‘ 2 ) ) )
106	24 53 55 35 105	syl31anc	⊢ ( 𝜑 → ( ( coe1 ‘ ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ‘ 2 ) = ( ( ( coe1 ‘ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) ‘ 2 ) ( +g ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( coe1 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ‘ 2 ) ) )
107	66	ringgrpd	⊢ ( 𝜑 → 𝑅 ∈ Grp )
108	107	grpmndd	⊢ ( 𝜑 → 𝑅 ∈ Mnd )
109		subrgsubg	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
110	7 109	syl	⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝑅 ) )
111		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
112	111	subg0cl	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) → ( 0g ‘ 𝑅 ) ∈ 𝑆 )
113	110 112	syl	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ 𝑆 )
114	1	subrgss	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ⊆ 𝑉 )
115	7 114	syl	⊢ ( 𝜑 → 𝑆 ⊆ 𝑉 )
116	22 1 111	ress0g	⊢ ( ( 𝑅 ∈ Mnd ∧ ( 0g ‘ 𝑅 ) ∈ 𝑆 ∧ 𝑆 ⊆ 𝑉 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) )
117	108 113 115 116	syl3anc	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) )
118	14 46	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
119		1nn0	⊢ 1 ∈ ℕ0
120	119	a1i	⊢ ( 𝜑 → 1 ∈ ℕ0 )
121		1ne2	⊢ 1 ≠ 2
122	121	a1i	⊢ ( 𝜑 → 1 ≠ 2 )
123	98 99 2 100 41 29 31 24 118 120 35 122	coe1tmfv2	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) ) ‘ 2 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) )
124	30 31	mulg1	⊢ ( ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ∈ 𝑈 → ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) = ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) )
125	80 124	syl	⊢ ( 𝜑 → ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) = ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) )
126	125 79	eqtr4d	⊢ ( 𝜑 → ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) = ( var1 ‘ 𝑅 ) )
127	126	oveq2d	⊢ ( 𝜑 → ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) = ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) )
128	127	fveq2d	⊢ ( 𝜑 → ( coe1 ‘ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) ) = ( coe1 ‘ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) )
129	128	fveq1d	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( 1 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) ) ‘ 2 ) = ( ( coe1 ‘ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) ‘ 2 ) )
130	117 123 129	3eqtr2rd	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) ‘ 2 ) = ( 0g ‘ 𝑅 ) )
131	15 46	eleqtrd	⊢ ( 𝜑 → 𝐵 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) )
132	2 54 99 98	coe1scl	⊢ ( ( ( 𝑅 ↾s 𝑆 ) ∈ Ring ∧ 𝐵 ∈ ( Base ‘ ( 𝑅 ↾s 𝑆 ) ) ) → ( coe1 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) = ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , 𝐵 , ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) )
133	24 131 132	syl2anc	⊢ ( 𝜑 → ( coe1 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) = ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , 𝐵 , ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) )
134		simpr	⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → 𝑖 = 2 )
135		2ne0	⊢ 2 ≠ 0
136	135	a1i	⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → 2 ≠ 0 )
137	134 136	eqnetrd	⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → 𝑖 ≠ 0 )
138	137	neneqd	⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → ¬ 𝑖 = 0 )
139	138	iffalsed	⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → if ( 𝑖 = 0 , 𝐵 , ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) )
140	117	adantr	⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) )
141	139 140	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑖 = 2 ) → if ( 𝑖 = 0 , 𝐵 , ( 0g ‘ ( 𝑅 ↾s 𝑆 ) ) ) = ( 0g ‘ 𝑅 ) )
142		fvexd	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ V )
143	133 141 35 142	fvmptd	⊢ ( 𝜑 → ( ( coe1 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ‘ 2 ) = ( 0g ‘ 𝑅 ) )
144	130 143	oveq12d	⊢ ( 𝜑 → ( ( ( coe1 ‘ ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ) ‘ 2 ) ( +g ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( coe1 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ‘ 2 ) ) = ( ( 0g ‘ 𝑅 ) ( +g ‘ ( 𝑅 ↾s 𝑆 ) ) ( 0g ‘ 𝑅 ) ) )
145	22 11	ressplusg	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → + = ( +g ‘ ( 𝑅 ↾s 𝑆 ) ) )
146	7 145	syl	⊢ ( 𝜑 → + = ( +g ‘ ( 𝑅 ↾s 𝑆 ) ) )
147	146	oveqd	⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) + ( 0g ‘ 𝑅 ) ) = ( ( 0g ‘ 𝑅 ) ( +g ‘ ( 𝑅 ↾s 𝑆 ) ) ( 0g ‘ 𝑅 ) ) )
148	1 111 107	grpidcld	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ 𝑉 )
149	1 11 111 107 148	grplidd	⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) + ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
150	147 149	eqtr3d	⊢ ( 𝜑 → ( ( 0g ‘ 𝑅 ) ( +g ‘ ( 𝑅 ↾s 𝑆 ) ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
151	106 144 150	3eqtrd	⊢ ( 𝜑 → ( ( coe1 ‘ ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ‘ 2 ) = ( 0g ‘ 𝑅 ) )
152	103 151	oveq12d	⊢ ( 𝜑 → ( ( ( coe1 ‘ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ‘ 2 ) ( -g ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( coe1 ‘ ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ‘ 2 ) ) = ( ( 1r ‘ 𝑅 ) ( -g ‘ ( 𝑅 ↾s 𝑆 ) ) ( 0g ‘ 𝑅 ) ) )
153		eqid	⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
154	153 22 76	subgsub	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝑆 ∧ ( 0g ‘ 𝑅 ) ∈ 𝑆 ) → ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( ( 1r ‘ 𝑅 ) ( -g ‘ ( 𝑅 ↾s 𝑆 ) ) ( 0g ‘ 𝑅 ) ) )
155	110 96 113 154	syl3anc	⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( ( 1r ‘ 𝑅 ) ( -g ‘ ( 𝑅 ↾s 𝑆 ) ) ( 0g ‘ 𝑅 ) ) )
156	1 85 66	ringidcld	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝑉 )
157	1 111 153	grpsubid1	⊢ ( ( 𝑅 ∈ Grp ∧ ( 1r ‘ 𝑅 ) ∈ 𝑉 ) → ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
158	107 156 157	syl2anc	⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) ( -g ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
159	152 155 158	3eqtr2d	⊢ ( 𝜑 → ( ( ( coe1 ‘ ( 2 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ‘ 2 ) ( -g ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( coe1 ‘ ( ( 𝐴 ( ·𝑠 ‘ 𝑃 ) ( var1 ‘ 𝑅 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ 𝐵 ) ) ) ‘ 2 ) ) = ( 1r ‘ 𝑅 ) )
160	75 78 159	3eqtrd	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) = ( 1r ‘ 𝑅 ) )
161		eqid	⊢ ( Monic1p ‘ 𝑅 ) = ( Monic1p ‘ 𝑅 )
162	59 62 69 17 161 85	ismon1p	⊢ ( 𝐺 ∈ ( Monic1p ‘ 𝑅 ) ↔ ( 𝐺 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ 𝐺 ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) ∧ ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) = ( 1r ‘ 𝑅 ) ) )
163	65 72 160 162	syl3anbrc	⊢ ( 𝜑 → 𝐺 ∈ ( Monic1p ‘ 𝑅 ) )
164	58 163	elind	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑈 ∩ ( Monic1p ‘ 𝑅 ) ) )
165		eqid	⊢ ( Monic1p ‘ ( 𝑅 ↾s 𝑆 ) ) = ( Monic1p ‘ ( 𝑅 ↾s 𝑆 ) )
166	59 22 2 3 7 161 165	ressply1mon1p	⊢ ( 𝜑 → ( Monic1p ‘ ( 𝑅 ↾s 𝑆 ) ) = ( 𝑈 ∩ ( Monic1p ‘ 𝑅 ) ) )
167	164 166	eleqtrrd	⊢ ( 𝜑 → 𝐺 ∈ ( Monic1p ‘ ( 𝑅 ↾s 𝑆 ) ) )
168		eqid	⊢ ( Unic1p ‘ ( 𝑅 ↾s 𝑆 ) ) = ( Unic1p ‘ ( 𝑅 ↾s 𝑆 ) )
169	168 165	mon1puc1p	⊢ ( ( ( 𝑅 ↾s 𝑆 ) ∈ Ring ∧ 𝐺 ∈ ( Monic1p ‘ ( 𝑅 ↾s 𝑆 ) ) ) → 𝐺 ∈ ( Unic1p ‘ ( 𝑅 ↾s 𝑆 ) ) )
170	24 167 169	syl2anc	⊢ ( 𝜑 → 𝐺 ∈ ( Unic1p ‘ ( 𝑅 ↾s 𝑆 ) ) )