Theorem irngss

Description: All elements of a subring S are integral over S . This is only true in the case of a nonzero ring, since there are no integral elements in a zero ring (see 0ringirng ). (Contributed by Thierry Arnoux, 28-Jan-2025)

	Ref	Expression
Hypotheses	irngval.o	$$⊢O=R{\mathrm{evalSub}}_{1}S$$
	irngval.u	$$⊢U=R{\upharpoonright }_{𝑠}S$$
	irngval.b	$$⊢B={\mathrm{Base}}_R$$
	irngval.0	$$⊢\underset{\dot{}}{0}=0_R$$
	elirng.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	elirng.s	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
	irngss.1	$$⊢\phi \to R\in \mathrm{NzRing}$$
Assertion	irngss	$$⊢\phi \to S\subseteq R\mathrm{IntgRing}S$$

Proof

Step	Hyp	Ref	Expression
1		irngval.o	$$⊢O=R{\mathrm{evalSub}}_{1}S$$
2		irngval.u	$$⊢U=R{\upharpoonright }_{𝑠}S$$
3		irngval.b	$$⊢B={\mathrm{Base}}_R$$
4		irngval.0	$$⊢\underset{\dot{}}{0}=0_R$$
5		elirng.r	$$⊢\phi \to R\in \mathrm{CRing}$$
6		elirng.s	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
7		irngss.1	$$⊢\phi \to R\in \mathrm{NzRing}$$
8		simpl	$$⊢\left(\phi \wedge x\in S\right)\to \phi$$
9	3	subrgss	$$⊢S\in \mathrm{SubRing}\left(R\right)\to S\subseteq B$$
10	6 9	syl	$$⊢\phi \to S\subseteq B$$
11	10	sselda	$$⊢\left(\phi \wedge x\in S\right)\to x\in B$$
12		eqid	$$⊢{\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(R\right)$$
13		eqid	$$⊢{\mathrm{Poly}}_1\left(U\right)={\mathrm{Poly}}_1\left(U\right)$$
14		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}$$
15	6	adantr	$$⊢\left(\phi \wedge x\in S\right)\to S\in \mathrm{SubRing}\left(R\right)$$
16		eqid	$$⊢{\mathrm{Poly}}_1\left(R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}={\mathrm{Poly}}_1\left(R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}$$
17		eqid	$$⊢{\mathrm{var}}_1\left(R\right)={\mathrm{var}}_1\left(R\right)$$
18	17 15 2 13 14	subrgvr1cl	$$⊢\left(\phi \wedge x\in S\right)\to {\mathrm{var}}_1\left(R\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}$$
19		eqid	$$⊢\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)=\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)$$
20		simpr	$$⊢\left(\phi \wedge x\in S\right)\to x\in S$$
21	19 2 12 13 14 15 20	asclply1subcl	$$⊢\left(\phi \wedge x\in S\right)\to \mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}$$
22	12 2 13 14 15 16 18 21	ressply1sub	$$⊢\left(\phi \wedge x\in S\right)\to {\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(U\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)={\mathrm{var}}_1\left(R\right){-}_{\left({\mathrm{Poly}}_1\left(R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)$$
23	12 2 13 14	subrgply1	$$⊢S\in \mathrm{SubRing}\left(R\right)\to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}\in \mathrm{SubRing}\left({\mathrm{Poly}}_1\left(R\right)\right)$$
24		subrgsubg	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}\in \mathrm{SubRing}\left({\mathrm{Poly}}_1\left(R\right)\right)\to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}\in \mathrm{SubGrp}\left({\mathrm{Poly}}_1\left(R\right)\right)$$
25	6 23 24	3syl	$$⊢\phi \to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}\in \mathrm{SubGrp}\left({\mathrm{Poly}}_1\left(R\right)\right)$$
26	25	adantr	$$⊢\left(\phi \wedge x\in S\right)\to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}\in \mathrm{SubGrp}\left({\mathrm{Poly}}_1\left(R\right)\right)$$
27		eqid	$$⊢{-}_{{\mathrm{Poly}}_1\left(R\right)}={-}_{{\mathrm{Poly}}_1\left(R\right)}$$
28		eqid	$$⊢{-}_{\left({\mathrm{Poly}}_1\left(R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}\right)}={-}_{\left({\mathrm{Poly}}_1\left(R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}\right)}$$
29	27 16 28	subgsub	$$⊢\left({\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}\in \mathrm{SubGrp}\left({\mathrm{Poly}}_1\left(R\right)\right)\wedge {\mathrm{var}}_1\left(R\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}\wedge \mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}\right)\to {\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)={\mathrm{var}}_1\left(R\right){-}_{\left({\mathrm{Poly}}_1\left(R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)$$
30	26 18 21 29	syl3anc	$$⊢\left(\phi \wedge x\in S\right)\to {\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)={\mathrm{var}}_1\left(R\right){-}_{\left({\mathrm{Poly}}_1\left(R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)$$
31	22 30	eqtr4d	$$⊢\left(\phi \wedge x\in S\right)\to {\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(U\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)={\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)$$
32	2	subrgcrng	$$⊢\left(R\in \mathrm{CRing}\wedge S\in \mathrm{SubRing}\left(R\right)\right)\to U\in \mathrm{CRing}$$
33	5 6 32	syl2anc	$$⊢\phi \to U\in \mathrm{CRing}$$
34	13	ply1crng	$$⊢U\in \mathrm{CRing}\to {\mathrm{Poly}}_1\left(U\right)\in \mathrm{CRing}$$
35	33 34	syl	$$⊢\phi \to {\mathrm{Poly}}_1\left(U\right)\in \mathrm{CRing}$$
36	35	adantr	$$⊢\left(\phi \wedge x\in S\right)\to {\mathrm{Poly}}_1\left(U\right)\in \mathrm{CRing}$$
37	36	crnggrpd	$$⊢\left(\phi \wedge x\in S\right)\to {\mathrm{Poly}}_1\left(U\right)\in \mathrm{Grp}$$
38		eqid	$$⊢{-}_{{\mathrm{Poly}}_1\left(U\right)}={-}_{{\mathrm{Poly}}_1\left(U\right)}$$
39	14 38	grpsubcl	$$⊢\left({\mathrm{Poly}}_1\left(U\right)\in \mathrm{Grp}\wedge {\mathrm{var}}_1\left(R\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}\wedge \mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}\right)\to {\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(U\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}$$
40	37 18 21 39	syl3anc	$$⊢\left(\phi \wedge x\in S\right)\to {\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(U\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}$$
41	31 40	eqeltrrd	$$⊢\left(\phi \wedge x\in S\right)\to {\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}$$
42		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
43		eqid	$$⊢{\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)={\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)$$
44		eqid	$$⊢{\mathrm{eval}}_1\left(R\right)={\mathrm{eval}}_1\left(R\right)$$
45	7	adantr	$$⊢\left(\phi \wedge x\in S\right)\to R\in \mathrm{NzRing}$$
46	5	adantr	$$⊢\left(\phi \wedge x\in S\right)\to R\in \mathrm{CRing}$$
47		eqid	$$⊢{Monic}_{\mathrm{1p}}\left(R\right)={Monic}_{\mathrm{1p}}\left(R\right)$$
48		eqid	$$⊢{\mathrm{deg}}_1\left(R\right)={\mathrm{deg}}_1\left(R\right)$$
49	12 42 3 17 27 19 43 44 45 46 11 47 48 4	ply1remlem	$$⊢\left(\phi \wedge x\in S\right)\to \left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\in {Monic}_{\mathrm{1p}}\left(R\right)\wedge {\mathrm{deg}}_1\left(R\right)\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)=1\wedge {{\mathrm{eval}}_1\left(R\right)\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]=\left\{x\right\}\right)$$
50	49	simp1d	$$⊢\left(\phi \wedge x\in S\right)\to {\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\in {Monic}_{\mathrm{1p}}\left(R\right)$$
51	41 50	elind	$$⊢\left(\phi \wedge x\in S\right)\to {\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\in \left({\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}\cap {Monic}_{\mathrm{1p}}\left(R\right)\right)$$
52		eqid	$$⊢{Monic}_{\mathrm{1p}}\left(U\right)={Monic}_{\mathrm{1p}}\left(U\right)$$
53	12 2 13 14 6 47 52	ressply1mon1p	$$⊢\phi \to {Monic}_{\mathrm{1p}}\left(U\right)={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}\cap {Monic}_{\mathrm{1p}}\left(R\right)$$
54	53	adantr	$$⊢\left(\phi \wedge x\in S\right)\to {Monic}_{\mathrm{1p}}\left(U\right)={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}\cap {Monic}_{\mathrm{1p}}\left(R\right)$$
55	51 54	eleqtrrd	$$⊢\left(\phi \wedge x\in S\right)\to {\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\in {Monic}_{\mathrm{1p}}\left(U\right)$$
56		fveq2	$$⊢f={\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\to O\left(f\right)=O\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)$$
57	56	fveq1d	$$⊢f={\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\to O\left(f\right)\left(x\right)=O\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)\left(x\right)$$
58	57	eqeq1d	$$⊢f={\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\to \left(O\left(f\right)\left(x\right)=\underset{\dot{}}{0}\leftrightarrow O\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)\left(x\right)=\underset{\dot{}}{0}\right)$$
59	58	adantl	$$⊢\left(\left(\phi \wedge x\in S\right)\wedge f={\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)\to \left(O\left(f\right)\left(x\right)=\underset{\dot{}}{0}\leftrightarrow O\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)\left(x\right)=\underset{\dot{}}{0}\right)$$
60	1 3 13 2 14 44 46 15	ressply1evl	$$⊢\left(\phi \wedge x\in S\right)\to O={{\mathrm{eval}}_1\left(R\right)\upharpoonright }_{{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}}$$
61	60	fveq1d	$$⊢\left(\phi \wedge x\in S\right)\to O\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)=\left({{\mathrm{eval}}_1\left(R\right)\upharpoonright }_{{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}}\right)\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)$$
62	41	fvresd	$$⊢\left(\phi \wedge x\in S\right)\to \left({{\mathrm{eval}}_1\left(R\right)\upharpoonright }_{{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}}\right)\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)={\mathrm{eval}}_1\left(R\right)\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)$$
63	61 62	eqtrd	$$⊢\left(\phi \wedge x\in S\right)\to O\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)={\mathrm{eval}}_1\left(R\right)\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)$$
64	63	fveq1d	$$⊢\left(\phi \wedge x\in S\right)\to O\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)\left(x\right)={\mathrm{eval}}_1\left(R\right)\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)\left(x\right)$$
65		eqid	$$⊢R{\uparrow }_{𝑠}B=R{\uparrow }_{𝑠}B$$
66		eqid	$$⊢{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}={\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
67	3	fvexi	$$⊢B\in \mathrm{V}$$
68	67	a1i	$$⊢\left(\phi \wedge x\in S\right)\to B\in \mathrm{V}$$
69	44 12 65 3	evl1rhm	$$⊢R\in \mathrm{CRing}\to {\mathrm{eval}}_1\left(R\right)\in \left({\mathrm{Poly}}_1\left(R\right)\mathrm{RingHom}\left(R{\uparrow }_{𝑠}B\right)\right)$$
70	42 66	rhmf	$$⊢{\mathrm{eval}}_1\left(R\right)\in \left({\mathrm{Poly}}_1\left(R\right)\mathrm{RingHom}\left(R{\uparrow }_{𝑠}B\right)\right)\to {\mathrm{eval}}_1\left(R\right):{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}⟶{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
71	5 69 70	3syl	$$⊢\phi \to {\mathrm{eval}}_1\left(R\right):{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}⟶{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
72	71	adantr	$$⊢\left(\phi \wedge x\in S\right)\to {\mathrm{eval}}_1\left(R\right):{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}⟶{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
73		eqid	$$⊢{\mathrm{PwSer}}_1\left(U\right)={\mathrm{PwSer}}_1\left(U\right)$$
74		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(U\right)}={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(U\right)}$$
75	12 2 13 14 6 73 74 42	ressply1bas2	$$⊢\phi \to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(U\right)}\cap {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
76	75	adantr	$$⊢\left(\phi \wedge x\in S\right)\to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(U\right)}\cap {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
77	41 76	eleqtrd	$$⊢\left(\phi \wedge x\in S\right)\to {\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\in \left({\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(U\right)}\cap {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\right)$$
78	77	elin2d	$$⊢\left(\phi \wedge x\in S\right)\to {\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
79	72 78	ffvelcdmd	$$⊢\left(\phi \wedge x\in S\right)\to {\mathrm{eval}}_1\left(R\right)\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)\in {\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
80	65 3 66 45 68 79	pwselbas	$$⊢\left(\phi \wedge x\in S\right)\to {\mathrm{eval}}_1\left(R\right)\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right):B⟶B$$
81	80	ffnd	$$⊢\left(\phi \wedge x\in S\right)\to {\mathrm{eval}}_1\left(R\right)\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)FnB$$
82		vsnid	$$⊢x\in \left\{x\right\}$$
83	49	simp3d	$$⊢\left(\phi \wedge x\in S\right)\to {{\mathrm{eval}}_1\left(R\right)\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]=\left\{x\right\}$$
84	82 83	eleqtrrid	$$⊢\left(\phi \wedge x\in S\right)\to x\in {{\mathrm{eval}}_1\left(R\right)\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$
85		fniniseg	$$⊢{\mathrm{eval}}_1\left(R\right)\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)FnB\to \left(x\in {{\mathrm{eval}}_1\left(R\right)\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\leftrightarrow \left(x\in B\wedge {\mathrm{eval}}_1\left(R\right)\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)\left(x\right)=\underset{\dot{}}{0}\right)\right)$$
86	85	simplbda	$$⊢\left({\mathrm{eval}}_1\left(R\right)\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)FnB\wedge x\in {{\mathrm{eval}}_1\left(R\right)\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\right)\to {\mathrm{eval}}_1\left(R\right)\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)\left(x\right)=\underset{\dot{}}{0}$$
87	81 84 86	syl2anc	$$⊢\left(\phi \wedge x\in S\right)\to {\mathrm{eval}}_1\left(R\right)\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)\left(x\right)=\underset{\dot{}}{0}$$
88	64 87	eqtrd	$$⊢\left(\phi \wedge x\in S\right)\to O\left({\mathrm{var}}_1\left(R\right){-}_{{\mathrm{Poly}}_1\left(R\right)}\mathrm{algSc}\left({\mathrm{Poly}}_1\left(R\right)\right)\left(x\right)\right)\left(x\right)=\underset{\dot{}}{0}$$
89	55 59 88	rspcedvd	$$⊢\left(\phi \wedge x\in S\right)\to \exists f\in {Monic}_{\mathrm{1p}}\left(U\right)O\left(f\right)\left(x\right)=\underset{\dot{}}{0}$$
90	1 2 3 4 5 6	elirng	$$⊢\phi \to \left(x\in \left(R\mathrm{IntgRing}S\right)\leftrightarrow \left(x\in B\wedge \exists f\in {Monic}_{\mathrm{1p}}\left(U\right)O\left(f\right)\left(x\right)=\underset{\dot{}}{0}\right)\right)$$
91	90	biimpar	$$⊢\left(\phi \wedge \left(x\in B\wedge \exists f\in {Monic}_{\mathrm{1p}}\left(U\right)O\left(f\right)\left(x\right)=\underset{\dot{}}{0}\right)\right)\to x\in \left(R\mathrm{IntgRing}S\right)$$
92	8 11 89 91	syl12anc	$$⊢\left(\phi \wedge x\in S\right)\to x\in \left(R\mathrm{IntgRing}S\right)$$
93	92	ex	$$⊢\phi \to \left(x\in S\to x\in \left(R\mathrm{IntgRing}S\right)\right)$$
94	93	ssrdv	$$⊢\phi \to S\subseteq R\mathrm{IntgRing}S$$