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