Metamath Proof Explorer

Definition df-irng

Description: Define the subring of elements of r integral over s in a ring. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Assertion df-irng ⊢ IntgRing = r ∈ V , s ∈ V ⟼ ⋃ f ∈ Monic 1p ⁡ r ↾ 𝑠 s f -1 0 r

Detailed syntax breakdown

Step Hyp Ref Expression
0 citr class IntgRing
1 vr setvar r
2 cvv class V
3 vs setvar s
4 vf setvar f
5 cmn1 class Monic 1p
6 1 cv setvar r
7 cress class ↾ 𝑠
8 3 cv setvar s
9 6 8 7 co class r ↾ 𝑠 s
10 9 5 cfv class Monic 1p ⁡ r ↾ 𝑠 s
11 4 cv setvar f
12 11 ccnv class f -1
13 c0g class 0 𝑔
14 6 13 cfv class 0 r
15 14 csn class 0 r
16 12 15 cima class f -1 0 r
17 4 10 16 ciun class ⋃ f ∈ Monic 1p ⁡ r ↾ 𝑠 s f -1 0 r
18 1 3 2 2 17 cmpo class r ∈ V , s ∈ V ⟼ ⋃ f ∈ Monic 1p ⁡ r ↾ 𝑠 s f -1 0 r
19 0 18 wceq wff IntgRing = r ∈ V , s ∈ V ⟼ ⋃ f ∈ Monic 1p ⁡ r ↾ 𝑠 s f -1 0 r