Theorem elirng

Description: Property for an element X of a field R to be integral over a subring S . (Contributed by Thierry Arnoux, 28-Jan-2025)

	Ref	Expression
Hypotheses	irngval.o	⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
	irngval.u	⊢ 𝑈 = ( 𝑅 ↾s 𝑆 )
	irngval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	irngval.0	⊢ 0 = ( 0g ‘ 𝑅 )
	elirng.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	elirng.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
Assertion	elirng	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑅 IntgRing 𝑆 ) ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑋 ) = 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		irngval.o	⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
2		irngval.u	⊢ 𝑈 = ( 𝑅 ↾s 𝑆 )
3		irngval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		irngval.0	⊢ 0 = ( 0g ‘ 𝑅 )
5		elirng.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
6		elirng.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
7	5	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
8	3	subrgss	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ⊆ 𝐵 )
9	6 8	syl	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
10	1 2 3 4 7 9	irngval	⊢ ( 𝜑 → ( 𝑅 IntgRing 𝑆 ) = ∪ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 0 } ) )
11	10	eleq2d	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑅 IntgRing 𝑆 ) ↔ 𝑋 ∈ ∪ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 0 } ) ) )
12		eliun	⊢ ( 𝑋 ∈ ∪ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 0 } ) ↔ ∃ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) 𝑋 ∈ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 0 } ) )
13	11 12	bitrdi	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑅 IntgRing 𝑆 ) ↔ ∃ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) 𝑋 ∈ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 0 } ) ) )
14		eqid	⊢ ( 𝑅 ↑s 𝐵 ) = ( 𝑅 ↑s 𝐵 )
15		eqid	⊢ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) = ( Base ‘ ( 𝑅 ↑s 𝐵 ) )
16	7	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ) → 𝑅 ∈ Ring )
17	3	fvexi	⊢ 𝐵 ∈ V
18	17	a1i	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ) → 𝐵 ∈ V )
19		eqid	⊢ ( Poly1 ‘ 𝑈 ) = ( Poly1 ‘ 𝑈 )
20	1 3 14 2 19	evls1rhm	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑂 ∈ ( ( Poly1 ‘ 𝑈 ) RingHom ( 𝑅 ↑s 𝐵 ) ) )
21	5 6 20	syl2anc	⊢ ( 𝜑 → 𝑂 ∈ ( ( Poly1 ‘ 𝑈 ) RingHom ( 𝑅 ↑s 𝐵 ) ) )
22		eqid	⊢ ( Base ‘ ( Poly1 ‘ 𝑈 ) ) = ( Base ‘ ( Poly1 ‘ 𝑈 ) )
23	22 15	rhmf	⊢ ( 𝑂 ∈ ( ( Poly1 ‘ 𝑈 ) RingHom ( 𝑅 ↑s 𝐵 ) ) → 𝑂 : ( Base ‘ ( Poly1 ‘ 𝑈 ) ) ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
24	21 23	syl	⊢ ( 𝜑 → 𝑂 : ( Base ‘ ( Poly1 ‘ 𝑈 ) ) ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ) → 𝑂 : ( Base ‘ ( Poly1 ‘ 𝑈 ) ) ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
26		eqid	⊢ ( Monic1p ‘ 𝑈 ) = ( Monic1p ‘ 𝑈 )
27	19 22 26	mon1pcl	⊢ ( 𝑓 ∈ ( Monic1p ‘ 𝑈 ) → 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝑈 ) ) )
28	27	adantl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ) → 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝑈 ) ) )
29	25 28	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ) → ( 𝑂 ‘ 𝑓 ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
30	14 3 15 16 18 29	pwselbas	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ) → ( 𝑂 ‘ 𝑓 ) : 𝐵 ⟶ 𝐵 )
31		ffn	⊢ ( ( 𝑂 ‘ 𝑓 ) : 𝐵 ⟶ 𝐵 → ( 𝑂 ‘ 𝑓 ) Fn 𝐵 )
32		fniniseg	⊢ ( ( 𝑂 ‘ 𝑓 ) Fn 𝐵 → ( 𝑋 ∈ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 0 } ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑋 ) = 0 ) ) )
33	30 31 32	3syl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ) → ( 𝑋 ∈ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 0 } ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑋 ) = 0 ) ) )
34	33	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) 𝑋 ∈ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 0 } ) ↔ ∃ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ( 𝑋 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑋 ) = 0 ) ) )
35	13 34	bitrd	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑅 IntgRing 𝑆 ) ↔ ∃ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ( 𝑋 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑋 ) = 0 ) ) )
36		r19.42v	⊢ ( ∃ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ( 𝑋 ∈ 𝐵 ∧ ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑋 ) = 0 ) ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑋 ) = 0 ) )
37	35 36	bitrdi	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑅 IntgRing 𝑆 ) ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ( ( 𝑂 ‘ 𝑓 ) ‘ 𝑋 ) = 0 ) ) )