Theorem rngunsnply1chr2lem2

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

	Ref	Expression
Hypotheses	rngunsnply1chr2.v	$$⊢V={\mathrm{Base}}_R$$
	rngunsnply1chr2.p	$$⊢P={\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)$$
	rngunsnply1chr2.u	$$⊢U={\mathrm{Base}}_P$$
	rngunsnply1chr2.q	$$⊢Q=R{\mathrm{evalSub}}_{1}S$$
	rngunsnply1chr2.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	rngunsnply1chr2.1	$$⊢\phi \to R\in \mathrm{NzRing}$$
	rngunsnply1chr2.s	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
	rngunsnply1chr2.x	$$⊢\phi \to X\in V$$
	rngunsnply1chr2.y	$$⊢\phi \to Y\in N\left(S\cup \left\{X\right\}\right)$$
	rngunsnply1chr2.n	$$⊢N=\mathrm{RingSpan}\left(R\right)$$
	rngunsnply1chr2.2	$$⊢\underset{\dot{}}{+}={+}_R$$
	rngunsnply1chr2.3	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	rngunsnply1chr2.4	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_R}$$
	rngunsnply1chr2.a	$$⊢\phi \to A\in S$$
	rngunsnply1chr2.b	$$⊢\phi \to B\in S$$
	rngunsnply1chr2.5	$$⊢\phi \to 2\underset{\dot{}}{\times }X=\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}B$$
	rngunsnply1chr2lem.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	rngunsnply1chr2lem.e	$$⊢E={rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)$$
	rngunsnply1chr2lem.g	$$⊢G=\left(2{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right){-}_P\left(\left(A{\cdot }_P{\mathrm{var}}_1\left(R\right)\right){+}_P\mathrm{algSc}\left(P\right)\left(B\right)\right)$$
	rngunsnply1chr2lem.h	$$⊢H=FEG$$
	rngunsnply1chr2lem.f	$$⊢\phi \to F\in U$$
Assertion	rngunsnply1chr2lem2	$$⊢\phi \to G\in {Unic}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)$$

Proof

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