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

Metamath Proof Explorer

Theorem irngval

Description: The elements of a field R integral over a subset S . In the case of a subfield, those are the algebraic numbers over the field S within the field R . That is, the numbers X which are roots of monic polynomials P ( X ) with coefficients in S . (Contributed by Thierry Arnoux, 28-Jan-2025)

Ref Expression
Hypotheses irngval.o ⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
irngval.u ⊢ 𝑈 = ( 𝑅 ↾s 𝑆 )
irngval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
irngval.0 ⊢ 0 = ( 0g ‘ 𝑅 )
irngval.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
irngval.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
Assertion irngval ( 𝜑 → ( 𝑅 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 irngval.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 irngval.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
7 5 elexd ⊢ ( 𝜑 → 𝑅 ∈ V )
8 3 fvexi ⊢ 𝐵 ∈ V
9 8 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
10 9 6 ssexd ⊢ ( 𝜑 → 𝑆 ∈ V )
11 fvexd ⊢ ( 𝜑 → ( Monic1p ‘ 𝑈 ) ∈ V )
12 fvex ⊢ ( 𝑂 ‘ 𝑓 ) ∈ V
13 12 cnvex ⊢ ◡ ( 𝑂 ‘ 𝑓 ) ∈ V
14 13 imaex ⊢ ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 0 } ) ∈ V
15 14 rgenw ⊢ ∀ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 0 } ) ∈ V
16 iunexg ⊢ ( ( ( Monic1p ‘ 𝑈 ) ∈ V ∧ ∀ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 0 } ) ∈ V ) → ∪ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 0 } ) ∈ V )
17 11 15 16 sylancl ⊢ ( 𝜑 → ∪ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 0 } ) ∈ V )
18 oveq12 ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 𝑟 ↾s 𝑠 ) = ( 𝑅 ↾s 𝑆 ) )
19 18 2 eqtr4di ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 𝑟 ↾s 𝑠 ) = 𝑈 )
20 19 fveq2d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( Monic1p ‘ ( 𝑟 ↾s 𝑠 ) ) = ( Monic1p ‘ 𝑈 ) )
21 oveq12 ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 𝑟 evalSub1 𝑠 ) = ( 𝑅 evalSub1 𝑆 ) )
22 21 1 eqtr4di ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 𝑟 evalSub1 𝑠 ) = 𝑂 )
23 22 fveq1d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ( 𝑟 evalSub1 𝑠 ) ‘ 𝑓 ) = ( 𝑂 ‘ 𝑓 ) )
24 23 cnveqd ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ◡ ( ( 𝑟 evalSub1 𝑠 ) ‘ 𝑓 ) = ◡ ( 𝑂 ‘ 𝑓 ) )
25 simpl ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → 𝑟 = 𝑅 )
26 25 fveq2d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
27 26 4 eqtr4di ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 0g ‘ 𝑟 ) = 0 )
28 27 sneqd ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → { ( 0g ‘ 𝑟 ) } = { 0 } )
29 24 28 imaeq12d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ◡ ( ( 𝑟 evalSub1 𝑠 ) ‘ 𝑓 ) “ { ( 0g ‘ 𝑟 ) } ) = ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 0 } ) )
30 20 29 iuneq12d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ∪ 𝑓 ∈ ( Monic1p ‘ ( 𝑟 ↾s 𝑠 ) ) ( ◡ ( ( 𝑟 evalSub1 𝑠 ) ‘ 𝑓 ) “ { ( 0g ‘ 𝑟 ) } ) = ∪ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 0 } ) )
31 df-irng ⊢ IntgRing = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ∪ 𝑓 ∈ ( Monic1p ‘ ( 𝑟 ↾s 𝑠 ) ) ( ◡ ( ( 𝑟 evalSub1 𝑠 ) ‘ 𝑓 ) “ { ( 0g ‘ 𝑟 ) } ) )
32 30 31 ovmpoga ⊢ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ∧ ∪ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 0 } ) ∈ V ) → ( 𝑅 IntgRing 𝑆 ) = ∪ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 0 } ) )
33 7 10 17 32 syl3anc ⊢ ( 𝜑 → ( 𝑅 IntgRing 𝑆 ) = ∪ 𝑓 ∈ ( Monic1p ‘ 𝑈 ) ( ◡ ( 𝑂 ‘ 𝑓 ) “ { 0 } ) )