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 {evalSub}_{1} S$
	irngval.u	$⊢ U = R ↾_{𝑠} S$
	irngval.b	$⊢ B = {Base}_{R}$
	irngval.0	$⊢ \underset{˙}{0} = 0_{R}$
	elirng.r	$⊢ φ \to R \in CRing$
	elirng.s	$⊢ φ \to S \in SubRing (R)$
	irngss.1	$⊢ φ \to R \in NzRing$
Assertion	irngss	$⊢ φ \to S \subseteq R IntgRing S$

Proof

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

Metamath Proof Explorer

Theorem irngss

Proof