Theorem rngunsnply1chr2

Description: When adjoining an element X with characteristic polynomial of degree 2 to a subring S , the elements Y of the generated subring can be written as a linear form. (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$$
Assertion	rngunsnply1chr2	$$⊢\phi \to \exists a\in S\exists b\in SY=\left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}b$$

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		oveq1	$$⊢a={\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(1\right)\to a\underset{\dot{}}{·}X={\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(1\right)\underset{\dot{}}{·}X$$
18	17	oveq1d	$$⊢a={\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(1\right)\to \left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}b=\left({\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(1\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}b$$
19	18	eqeq2d	$$⊢a={\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(1\right)\to \left(Y=\left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}b\leftrightarrow Y=\left({\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(1\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}b\right)$$
20		oveq2	$$⊢b={\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(0\right)\to \left({\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(1\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}b=\left({\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(1\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}{\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(0\right)$$
21	20	eqeq2d	$$⊢b={\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(0\right)\to \left(Y=\left({\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(1\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}b\leftrightarrow Y=\left({\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(1\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}{\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(0\right)\right)$$
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	24	adantr	$$⊢\left(\phi \wedge p\in U\right)\to R{\upharpoonright }_{𝑠}S\in \mathrm{Ring}$$
26		simpr	$$⊢\left(\phi \wedge p\in U\right)\to p\in U$$
27	5	adantr	$$⊢\left(\phi \wedge p\in U\right)\to R\in \mathrm{CRing}$$
28	6	adantr	$$⊢\left(\phi \wedge p\in U\right)\to R\in \mathrm{NzRing}$$
29	7	adantr	$$⊢\left(\phi \wedge p\in U\right)\to S\in \mathrm{SubRing}\left(R\right)$$
30	8	adantr	$$⊢\left(\phi \wedge p\in U\right)\to X\in V$$
31	9	adantr	$$⊢\left(\phi \wedge p\in U\right)\to Y\in N\left(S\cup \left\{X\right\}\right)$$
32	14	adantr	$$⊢\left(\phi \wedge p\in U\right)\to A\in S$$
33	15	adantr	$$⊢\left(\phi \wedge p\in U\right)\to B\in S$$
34	16	adantr	$$⊢\left(\phi \wedge p\in U\right)\to 2\underset{\dot{}}{\times }X=\left(A\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}B$$
35		eqid	$$⊢{\mathrm{deg}}_1\left(R\right)={\mathrm{deg}}_1\left(R\right)$$
36		eqid	$$⊢{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)={rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)$$
37		eqid	$$⊢\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)=\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)$$
38		eqid	$$⊢p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)=p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)$$
39	1 2 3 4 27 28 29 30 31 10 11 12 13 32 33 34 35 36 37 38 26	rngunsnply1chr2lem2	$$⊢\left(\phi \wedge p\in U\right)\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 {Unic}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)$$
40		eqid	$$⊢{Unic}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)={Unic}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)$$
41	36 2 3 40	r1pcl	$$⊢\left(R{\upharpoonright }_{𝑠}S\in \mathrm{Ring}\wedge p\in U\wedge \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 {Unic}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\right)\to p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\in U$$
42	25 26 39 41	syl3anc	$$⊢\left(\phi \wedge p\in U\right)\to p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\in U$$
43		1nn0	$$⊢1\in {\mathbb{N}}_0$$
44		eqid	$$⊢{\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)={\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)$$
45		eqid	$$⊢{\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}={\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
46	44 3 2 45	coe1fvalcl	$$⊢\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\in U\wedge 1\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(1\right)\in {\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
47	42 43 46	sylancl	$$⊢\left(\phi \wedge p\in U\right)\to {\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(1\right)\in {\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
48	22	subrgbas	$$⊢S\in \mathrm{SubRing}\left(R\right)\to S={\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
49	29 48	syl	$$⊢\left(\phi \wedge p\in U\right)\to S={\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
50	47 49	eleqtrrd	$$⊢\left(\phi \wedge p\in U\right)\to {\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(1\right)\in S$$
51	50	adantr	$$⊢\left(\left(\phi \wedge p\in U\right)\wedge Y=Q\left(p\right)\left(X\right)\right)\to {\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(1\right)\in S$$
52		0nn0	$$⊢0\in {\mathbb{N}}_0$$
53	44 3 2 45	coe1fvalcl	$$⊢\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\in U\wedge 0\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(0\right)\in {\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
54	42 52 53	sylancl	$$⊢\left(\phi \wedge p\in U\right)\to {\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(0\right)\in {\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}S\right)}$$
55	54 49	eleqtrrd	$$⊢\left(\phi \wedge p\in U\right)\to {\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(0\right)\in S$$
56	55	adantr	$$⊢\left(\left(\phi \wedge p\in U\right)\wedge Y=Q\left(p\right)\left(X\right)\right)\to {\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(0\right)\in S$$
57		simpr	$$⊢\left(\left(\phi \wedge p\in U\right)\wedge Y=Q\left(p\right)\left(X\right)\right)\to Y=Q\left(p\right)\left(X\right)$$
58	1 2 3 4 27 28 29 30 31 10 11 12 13 32 33 34 35 36 37 38 26	rngunsnply1chr2lem3	$$⊢\left(\phi \wedge p\in U\right)\to \left({\mathrm{deg}}_1\left(R\right)\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\le 1\wedge Q\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(X\right)=Q\left(p\right)\left(X\right)\right)$$
59	58	simprd	$$⊢\left(\phi \wedge p\in U\right)\to Q\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(X\right)=Q\left(p\right)\left(X\right)$$
60	59	adantr	$$⊢\left(\left(\phi \wedge p\in U\right)\wedge Y=Q\left(p\right)\left(X\right)\right)\to Q\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(X\right)=Q\left(p\right)\left(X\right)$$
61		eqid	$$⊢{\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(1\right)={\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(1\right)$$
62		eqid	$$⊢{\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(0\right)={\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(0\right)$$
63	58	simpld	$$⊢\left(\phi \wedge p\in U\right)\to {\mathrm{deg}}_1\left(R\right)\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\le 1$$
64	2 4 1 3 12 11 44 35 61 62 27 29 42 63 30	evls1degle1	$$⊢\left(\phi \wedge p\in U\right)\to Q\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(X\right)=\left({\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(1\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}{\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(0\right)$$
65	64	adantr	$$⊢\left(\left(\phi \wedge p\in U\right)\wedge Y=Q\left(p\right)\left(X\right)\right)\to Q\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(X\right)=\left({\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(1\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}{\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(0\right)$$
66	57 60 65	3eqtr2d	$$⊢\left(\left(\phi \wedge p\in U\right)\wedge Y=Q\left(p\right)\left(X\right)\right)\to Y=\left({\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(1\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}{\mathrm{coe}}_1\left(p{rem}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\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)\right)\left(0\right)$$
67	19 21 51 56 66	2rspcedvdw	$$⊢\left(\left(\phi \wedge p\in U\right)\wedge Y=Q\left(p\right)\left(X\right)\right)\to \exists a\in S\exists b\in SY=\left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}b$$
68	1 2 3 4 5 7 8 10	rngunsnply1	$$⊢\phi \to \left(Y\in N\left(S\cup \left\{X\right\}\right)\leftrightarrow \exists p\in UY=Q\left(p\right)\left(X\right)\right)$$
69	9 68	mpbid	$$⊢\phi \to \exists p\in UY=Q\left(p\right)\left(X\right)$$
70	67 69	r19.29a	$$⊢\phi \to \exists a\in S\exists b\in SY=\left(a\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}b$$