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	$⊢ O = R {evalSub}_{1} S$
	irngval.u	$⊢ U = R ↾_{𝑠} S$
	irngval.b	$⊢ B = {Base}_{R}$
	irngval.0	$⊢ \underset{˙}{0} = 0_{R}$
	irngval.r	$⊢ φ \to R \in Ring$
	irngval.s	$⊢ φ \to S \subseteq B$
Assertion	irngval	$⊢ φ \to R IntgRing S = ⋃_{f \in {Monic}_{1p} (U)} {O (f)}^{-1} [\{\underset{˙}{0}\}]$

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		irngval.r	$⊢ φ \to R \in Ring$
6		irngval.s	$⊢ φ \to S \subseteq B$
7	5	elexd	$⊢ φ \to R \in V$
8	3	fvexi	$⊢ B \in V$
9	8	a1i	$⊢ φ \to B \in V$
10	9 6	ssexd	$⊢ φ \to S \in V$
11		fvexd	$⊢ φ \to {Monic}_{1p} (U) \in V$
12		fvex	$⊢ O (f) \in V$
13	12	cnvex	$⊢ {O (f)}^{-1} \in V$
14	13	imaex	$⊢ {O (f)}^{-1} [\{\underset{˙}{0}\}] \in V$
15	14	rgenw	$⊢ \forall f \in {Monic}_{1p} (U) {O (f)}^{-1} [\{\underset{˙}{0}\}] \in V$
16		iunexg	$⊢ ({Monic}_{1p} (U) \in V \land \forall f \in {Monic}_{1p} (U) {O (f)}^{-1} [\{\underset{˙}{0}\}] \in V) \to ⋃_{f \in {Monic}_{1p} (U)} {O (f)}^{-1} [\{\underset{˙}{0}\}] \in V$
17	11 15 16	sylancl	$⊢ φ \to ⋃_{f \in {Monic}_{1p} (U)} {O (f)}^{-1} [\{\underset{˙}{0}\}] \in V$
18		oveq12	$⊢ (r = R \land s = S) \to r ↾_{𝑠} s = R ↾_{𝑠} S$
19	18 2	eqtr4di	$⊢ (r = R \land s = S) \to r ↾_{𝑠} s = U$
20	19	fveq2d	$⊢ (r = R \land s = S) \to {Monic}_{1p} (r ↾_{𝑠} s) = {Monic}_{1p} (U)$
21		oveq12	$⊢ (r = R \land s = S) \to r {evalSub}_{1} s = R {evalSub}_{1} S$
22	21 1	eqtr4di	$⊢ (r = R \land s = S) \to r {evalSub}_{1} s = O$
23	22	fveq1d	$⊢ (r = R \land s = S) \to (r {evalSub}_{1} s) (f) = O (f)$
24	23	cnveqd	$⊢ (r = R \land s = S) \to {(r {evalSub}_{1} s) (f)}^{-1} = {O (f)}^{-1}$
25		simpl	$⊢ (r = R \land s = S) \to r = R$
26	25	fveq2d	$⊢ (r = R \land s = S) \to 0_{r} = 0_{R}$
27	26 4	eqtr4di	$⊢ (r = R \land s = S) \to 0_{r} = \underset{˙}{0}$
28	27	sneqd	$⊢ (r = R \land s = S) \to \{0_{r}\} = \{\underset{˙}{0}\}$
29	24 28	imaeq12d	$⊢ (r = R \land s = S) \to {(r {evalSub}_{1} s) (f)}^{-1} [\{0_{r}\}] = {O (f)}^{-1} [\{\underset{˙}{0}\}]$
30	20 29	iuneq12d	$⊢ (r = R \land s = S) \to ⋃_{f \in {Monic}_{1p} (r ↾_{𝑠} s)} {(r {evalSub}_{1} s) (f)}^{-1} [\{0_{r}\}] = ⋃_{f \in {Monic}_{1p} (U)} {O (f)}^{-1} [\{\underset{˙}{0}\}]$
31		df-irng	$⊢ IntgRing = (r \in V, s \in V ⟼ ⋃_{f \in {Monic}_{1p} (r ↾_{𝑠} s)} {(r {evalSub}_{1} s) (f)}^{-1} [\{0_{r}\}])$
32	30 31	ovmpoga	$⊢ (R \in V \land S \in V \land ⋃_{f \in {Monic}_{1p} (U)} {O (f)}^{-1} [\{\underset{˙}{0}\}] \in V) \to R IntgRing S = ⋃_{f \in {Monic}_{1p} (U)} {O (f)}^{-1} [\{\underset{˙}{0}\}]$
33	7 10 17 32	syl3anc	$⊢ φ \to R IntgRing S = ⋃_{f \in {Monic}_{1p} (U)} {O (f)}^{-1} [\{\underset{˙}{0}\}]$

Metamath Proof Explorer

Theorem irngval

Proof