This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )