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

Metamath Proof Explorer

Definition df-irng

Description: Define the subring of elements of a ring r integral over a subset s . (Contributed by Mario Carneiro, 2-Dec-2014) (Revised by Thierry Arnoux, 28-Jan-2025)

Ref Expression
Assertion df-irng IntgRing = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ∪ 𝑓 ∈ ( Monic1p ‘ ( 𝑟 ↾s 𝑠 ) ) ( ◡ ( ( 𝑟 evalSub1 𝑠 ) ‘ 𝑓 ) “ { ( 0g ‘ 𝑟 ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cirng ⊢ IntgRing
1 vr ⊢ 𝑟
2 cvv ⊢ V
3 vs ⊢ 𝑠
4 vf ⊢ 𝑓
5 cmn1 ⊢ Monic1p
6 1 cv ⊢ 𝑟
7 cress ⊢ ↾s
8 3 cv ⊢ 𝑠
9 6 8 7 co ⊢ ( 𝑟 ↾s 𝑠 )
10 9 5 cfv ⊢ ( Monic1p ‘ ( 𝑟 ↾s 𝑠 ) )
11 ces1 ⊢ evalSub1
12 6 8 11 co ⊢ ( 𝑟 evalSub1 𝑠 )
13 4 cv ⊢ 𝑓
14 13 12 cfv ⊢ ( ( 𝑟 evalSub1 𝑠 ) ‘ 𝑓 )
15 14 ccnv ⊢ ◡ ( ( 𝑟 evalSub1 𝑠 ) ‘ 𝑓 )
16 c0g ⊢ 0g
17 6 16 cfv ⊢ ( 0g ‘ 𝑟 )
18 17 csn ⊢ { ( 0g ‘ 𝑟 ) }
19 15 18 cima ⊢ ( ◡ ( ( 𝑟 evalSub1 𝑠 ) ‘ 𝑓 ) “ { ( 0g ‘ 𝑟 ) } )
20 4 10 19 ciun ⊢ ∪ 𝑓 ∈ ( Monic1p ‘ ( 𝑟 ↾s 𝑠 ) ) ( ◡ ( ( 𝑟 evalSub1 𝑠 ) ‘ 𝑓 ) “ { ( 0g ‘ 𝑟 ) } )
21 1 3 2 2 20 cmpo ⊢ ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ∪ 𝑓 ∈ ( Monic1p ‘ ( 𝑟 ↾s 𝑠 ) ) ( ◡ ( ( 𝑟 evalSub1 𝑠 ) ‘ 𝑓 ) “ { ( 0g ‘ 𝑟 ) } ) )
22 0 21 wceq ⊢ IntgRing = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ∪ 𝑓 ∈ ( Monic1p ‘ ( 𝑟 ↾s 𝑠 ) ) ( ◡ ( ( 𝑟 evalSub1 𝑠 ) ‘ 𝑓 ) “ { ( 0g ‘ 𝑟 ) } ) )