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	⊢ 𝑂 = ( 𝑅 evalSub₁ 𝑆 )
	irngval.u	⊢ 𝑈 = ( 𝑅 ↾_s 𝑆 )
	irngval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	irngval.0	⊢ 0 = ( 0_g ‘ 𝑅 )
	elirng.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	elirng.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
	irngss.1	⊢ ( 𝜑 → 𝑅 ∈ NzRing )
Assertion	irngss	⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑅 IntgRing 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		irngval.o	⊢ 𝑂 = ( 𝑅 evalSub₁ 𝑆 )
2		irngval.u	⊢ 𝑈 = ( 𝑅 ↾_s 𝑆 )
3		irngval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		irngval.0	⊢ 0 = ( 0_g ‘ 𝑅 )
5		elirng.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
6		elirng.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
7		irngss.1	⊢ ( 𝜑 → 𝑅 ∈ NzRing )
8		simpl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝜑 )
9	3	subrgss	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ⊆ 𝐵 )
10	6 9	syl	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
11	10	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝐵 )
12		eqid	⊢ ( Poly₁ ‘ 𝑅 ) = ( Poly₁ ‘ 𝑅 )
13		eqid	⊢ ( Poly₁ ‘ 𝑈 ) = ( Poly₁ ‘ 𝑈 )
14		eqid	⊢ ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) = ( Base ‘ ( Poly₁ ‘ 𝑈 ) )
15	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
16		eqid	⊢ ( ( Poly₁ ‘ 𝑅 ) ↾_s ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) ) = ( ( Poly₁ ‘ 𝑅 ) ↾_s ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) )
17		eqid	⊢ ( var₁ ‘ 𝑅 ) = ( var₁ ‘ 𝑅 )
18	17 15 2 13 14	subrgvr1cl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( var₁ ‘ 𝑅 ) ∈ ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) )
19		eqid	⊢ ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) = ( algSc ‘ ( Poly₁ ‘ 𝑅 ) )
20		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
21	19 2 12 13 14 15 20	asclply1subcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ∈ ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) )
22	12 2 13 14 15 16 18 21	ressply1sub	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑈 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) = ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( ( Poly₁ ‘ 𝑅 ) ↾_s ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) )
23	12 2 13 14	subrgply1	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) ∈ ( SubRing ‘ ( Poly₁ ‘ 𝑅 ) ) )
24		subrgsubg	⊢ ( ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) ∈ ( SubRing ‘ ( Poly₁ ‘ 𝑅 ) ) → ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) ∈ ( SubGrp ‘ ( Poly₁ ‘ 𝑅 ) ) )
25	6 23 24	3syl	⊢ ( 𝜑 → ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) ∈ ( SubGrp ‘ ( Poly₁ ‘ 𝑅 ) ) )
26	25	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) ∈ ( SubGrp ‘ ( Poly₁ ‘ 𝑅 ) ) )
27		eqid	⊢ ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) = ( -_g ‘ ( Poly₁ ‘ 𝑅 ) )
28		eqid	⊢ ( -_g ‘ ( ( Poly₁ ‘ 𝑅 ) ↾_s ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) ) ) = ( -_g ‘ ( ( Poly₁ ‘ 𝑅 ) ↾_s ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) ) )
29	27 16 28	subgsub	⊢ ( ( ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) ∈ ( SubGrp ‘ ( Poly₁ ‘ 𝑅 ) ) ∧ ( var₁ ‘ 𝑅 ) ∈ ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) ∧ ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ∈ ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) ) → ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) = ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( ( Poly₁ ‘ 𝑅 ) ↾_s ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) )
30	26 18 21 29	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) = ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( ( Poly₁ ‘ 𝑅 ) ↾_s ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) )
31	22 30	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑈 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) = ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) )
32	2	subrgcrng	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑈 ∈ CRing )
33	5 6 32	syl2anc	⊢ ( 𝜑 → 𝑈 ∈ CRing )
34	13	ply1crng	⊢ ( 𝑈 ∈ CRing → ( Poly₁ ‘ 𝑈 ) ∈ CRing )
35	33 34	syl	⊢ ( 𝜑 → ( Poly₁ ‘ 𝑈 ) ∈ CRing )
36	35	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( Poly₁ ‘ 𝑈 ) ∈ CRing )
37	36	crnggrpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( Poly₁ ‘ 𝑈 ) ∈ Grp )
38		eqid	⊢ ( -_g ‘ ( Poly₁ ‘ 𝑈 ) ) = ( -_g ‘ ( Poly₁ ‘ 𝑈 ) )
39	14 38	grpsubcl	⊢ ( ( ( Poly₁ ‘ 𝑈 ) ∈ Grp ∧ ( var₁ ‘ 𝑅 ) ∈ ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) ∧ ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ∈ ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) ) → ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑈 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ∈ ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) )
40	37 18 21 39	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑈 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ∈ ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) )
41	31 40	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ∈ ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) )
42		eqid	⊢ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) = ( Base ‘ ( Poly₁ ‘ 𝑅 ) )
43		eqid	⊢ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) = ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) )
44		eqid	⊢ ( eval₁ ‘ 𝑅 ) = ( eval₁ ‘ 𝑅 )
45	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑅 ∈ NzRing )
46	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑅 ∈ CRing )
47		eqid	⊢ ( Monic_1p ‘ 𝑅 ) = ( Monic_1p ‘ 𝑅 )
48		eqid	⊢ ( deg₁ ‘ 𝑅 ) = ( deg₁ ‘ 𝑅 )
49	12 42 3 17 27 19 43 44 45 46 11 47 48 4	ply1remlem	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ∈ ( Monic_1p ‘ 𝑅 ) ∧ ( ( deg₁ ‘ 𝑅 ) ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) = 1 ∧ ( ^◡ ( ( eval₁ ‘ 𝑅 ) ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) “ { 0 } ) = { 𝑥 } ) )
50	49	simp1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ∈ ( Monic_1p ‘ 𝑅 ) )
51	41 50	elind	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ∈ ( ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) ∩ ( Monic_1p ‘ 𝑅 ) ) )
52		eqid	⊢ ( Monic_1p ‘ 𝑈 ) = ( Monic_1p ‘ 𝑈 )
53	12 2 13 14 6 47 52	ressply1mon1p	⊢ ( 𝜑 → ( Monic_1p ‘ 𝑈 ) = ( ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) ∩ ( Monic_1p ‘ 𝑅 ) ) )
54	53	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( Monic_1p ‘ 𝑈 ) = ( ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) ∩ ( Monic_1p ‘ 𝑅 ) ) )
55	51 54	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ∈ ( Monic_1p ‘ 𝑈 ) )
56		fveq2	⊢ ( 𝑓 = ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) → ( 𝑂 ‘ 𝑓 ) = ( 𝑂 ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) )
57	56	fveq1d	⊢ ( 𝑓 = ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) → ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑥 ) = ( ( 𝑂 ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) ‘ 𝑥 ) )
58	57	eqeq1d	⊢ ( 𝑓 = ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) → ( ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑥 ) = 0 ↔ ( ( 𝑂 ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) ‘ 𝑥 ) = 0 ) )
59	58	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑓 = ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) → ( ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑥 ) = 0 ↔ ( ( 𝑂 ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) ‘ 𝑥 ) = 0 ) )
60	1 3 13 2 14 44 46 15	ressply1evl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑂 = ( ( eval₁ ‘ 𝑅 ) ↾ ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) ) )
61	60	fveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑂 ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) = ( ( ( eval₁ ‘ 𝑅 ) ↾ ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) ) ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) )
62	41	fvresd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( ( eval₁ ‘ 𝑅 ) ↾ ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) ) ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) = ( ( eval₁ ‘ 𝑅 ) ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) )
63	61 62	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑂 ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) = ( ( eval₁ ‘ 𝑅 ) ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) )
64	63	fveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑂 ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) ‘ 𝑥 ) = ( ( ( eval₁ ‘ 𝑅 ) ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) ‘ 𝑥 ) )
65		eqid	⊢ ( 𝑅 ↑_s 𝐵 ) = ( 𝑅 ↑_s 𝐵 )
66		eqid	⊢ ( Base ‘ ( 𝑅 ↑_s 𝐵 ) ) = ( Base ‘ ( 𝑅 ↑_s 𝐵 ) )
67	3	fvexi	⊢ 𝐵 ∈ V
68	67	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ V )
69	44 12 65 3	evl1rhm	⊢ ( 𝑅 ∈ CRing → ( eval₁ ‘ 𝑅 ) ∈ ( ( Poly₁ ‘ 𝑅 ) RingHom ( 𝑅 ↑_s 𝐵 ) ) )
70	42 66	rhmf	⊢ ( ( eval₁ ‘ 𝑅 ) ∈ ( ( Poly₁ ‘ 𝑅 ) RingHom ( 𝑅 ↑_s 𝐵 ) ) → ( eval₁ ‘ 𝑅 ) : ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ⟶ ( Base ‘ ( 𝑅 ↑_s 𝐵 ) ) )
71	5 69 70	3syl	⊢ ( 𝜑 → ( eval₁ ‘ 𝑅 ) : ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ⟶ ( Base ‘ ( 𝑅 ↑_s 𝐵 ) ) )
72	71	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( eval₁ ‘ 𝑅 ) : ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ⟶ ( Base ‘ ( 𝑅 ↑_s 𝐵 ) ) )
73		eqid	⊢ ( PwSer₁ ‘ 𝑈 ) = ( PwSer₁ ‘ 𝑈 )
74		eqid	⊢ ( Base ‘ ( PwSer₁ ‘ 𝑈 ) ) = ( Base ‘ ( PwSer₁ ‘ 𝑈 ) )
75	12 2 13 14 6 73 74 42	ressply1bas2	⊢ ( 𝜑 → ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) = ( ( Base ‘ ( PwSer₁ ‘ 𝑈 ) ) ∩ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) )
76	75	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( Base ‘ ( Poly₁ ‘ 𝑈 ) ) = ( ( Base ‘ ( PwSer₁ ‘ 𝑈 ) ) ∩ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) )
77	41 76	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ∈ ( ( Base ‘ ( PwSer₁ ‘ 𝑈 ) ) ∩ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) ) )
78	77	elin2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ∈ ( Base ‘ ( Poly₁ ‘ 𝑅 ) ) )
79	72 78	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( eval₁ ‘ 𝑅 ) ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) ∈ ( Base ‘ ( 𝑅 ↑_s 𝐵 ) ) )
80	65 3 66 45 68 79	pwselbas	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( eval₁ ‘ 𝑅 ) ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) : 𝐵 ⟶ 𝐵 )
81	80	ffnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( eval₁ ‘ 𝑅 ) ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) Fn 𝐵 )
82		vsnid	⊢ 𝑥 ∈ { 𝑥 }
83	49	simp3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ^◡ ( ( eval₁ ‘ 𝑅 ) ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) “ { 0 } ) = { 𝑥 } )
84	82 83	eleqtrrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( ^◡ ( ( eval₁ ‘ 𝑅 ) ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) “ { 0 } ) )
85		fniniseg	⊢ ( ( ( eval₁ ‘ 𝑅 ) ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) Fn 𝐵 → ( 𝑥 ∈ ( ^◡ ( ( eval₁ ‘ 𝑅 ) ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) “ { 0 } ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( ( ( eval₁ ‘ 𝑅 ) ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) ‘ 𝑥 ) = 0 ) ) )
86	85	simplbda	⊢ ( ( ( ( eval₁ ‘ 𝑅 ) ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) Fn 𝐵 ∧ 𝑥 ∈ ( ^◡ ( ( eval₁ ‘ 𝑅 ) ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) “ { 0 } ) ) → ( ( ( eval₁ ‘ 𝑅 ) ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) ‘ 𝑥 ) = 0 )
87	81 84 86	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( ( eval₁ ‘ 𝑅 ) ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) ‘ 𝑥 ) = 0 )
88	64 87	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑂 ‘ ( ( var₁ ‘ 𝑅 ) ( -_g ‘ ( Poly₁ ‘ 𝑅 ) ) ( ( algSc ‘ ( Poly₁ ‘ 𝑅 ) ) ‘ 𝑥 ) ) ) ‘ 𝑥 ) = 0 )
89	55 59 88	rspcedvd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ∃ 𝑓 ∈ ( Monic_1p ‘ 𝑈 ) ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑥 ) = 0 )
90	1 2 3 4 5 6	elirng	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑅 IntgRing 𝑆 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑓 ∈ ( Monic_1p ‘ 𝑈 ) ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑥 ) = 0 ) ) )
91	90	biimpar	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑓 ∈ ( Monic_1p ‘ 𝑈 ) ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑥 ) = 0 ) ) → 𝑥 ∈ ( 𝑅 IntgRing 𝑆 ) )
92	8 11 89 91	syl12anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( 𝑅 IntgRing 𝑆 ) )
93	92	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 → 𝑥 ∈ ( 𝑅 IntgRing 𝑆 ) ) )
94	93	ssrdv	⊢ ( 𝜑 → 𝑆 ⊆ ( 𝑅 IntgRing 𝑆 ) )

Metamath Proof Explorer

Theorem irngss

Proof