Metamath Proof Explorer

Theorem irngnzply1

Description: In the case of a field E , the roots of nonzero polynomials p with coefficients in a subfield F are exactly the integral elements over F . Roots of nonzero polynomials are called algebraic numbers, so this shows that in the case of a field, elements integral over F are exactly the algebraic numbers. In this formula, dom O represents the polynomials, and Z the zero polynomial. (Contributed by Thierry Arnoux, 5-Feb-2025)

Ref Expression
Hypotheses irngnzply1.o ⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
irngnzply1.z ⊢ 𝑍 = ( 0g ‘ ( Poly1 ‘ 𝐸 ) )
irngnzply1.1 ⊢ 0 = ( 0g ‘ 𝐸 )
irngnzply1.e ⊢ ( 𝜑 → 𝐸 ∈ Field )
irngnzply1.f ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
Assertion irngnzply1 ( 𝜑 → ( 𝐸 IntgRing 𝐹 ) = ∪ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) )

Proof

Step Hyp Ref Expression
1 irngnzply1.o ⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
2 irngnzply1.z ⊢ 𝑍 = ( 0g ‘ ( Poly1 ‘ 𝐸 ) )
3 irngnzply1.1 ⊢ 0 = ( 0g ‘ 𝐸 )
4 irngnzply1.e ⊢ ( 𝜑 → 𝐸 ∈ Field )
5 irngnzply1.f ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
6 eqid ⊢ ( 𝐸 ↾s 𝐹 ) = ( 𝐸 ↾s 𝐹 )
7 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
8 4 fldcrngd ⊢ ( 𝜑 → 𝐸 ∈ CRing )
9 issdrg ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) ↔ ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s 𝐹 ) ∈ DivRing ) )
10 5 9 sylib ⊢ ( 𝜑 → ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s 𝐹 ) ∈ DivRing ) )
11 10 simp2d ⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
12 1 6 7 3 8 11 elirng ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ ∃ 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) )
13 12 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) → ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ ∃ 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) )
14 13 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) → ∃ 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 )
15 eqid ⊢ ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
16 eqid ⊢ ( Base ‘ ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) ) = ( Base ‘ ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) )
17 eqid ⊢ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) = ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) )
18 15 16 17 mon1pcl ⊢ ( 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) → 𝑝 ∈ ( Base ‘ ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) ) )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) ) → 𝑝 ∈ ( Base ‘ ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) ) )
20 eqid ⊢ ( 𝐸 ↑s ( Base ‘ 𝐸 ) ) = ( 𝐸 ↑s ( Base ‘ 𝐸 ) )
21 1 7 20 6 15 evls1rhm ⊢ ( ( 𝐸 ∈ CRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ) → 𝑂 ∈ ( ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) RingHom ( 𝐸 ↑s ( Base ‘ 𝐸 ) ) ) )
22 8 11 21 syl2anc ⊢ ( 𝜑 → 𝑂 ∈ ( ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) RingHom ( 𝐸 ↑s ( Base ‘ 𝐸 ) ) ) )
23 eqid ⊢ ( Base ‘ ( 𝐸 ↑s ( Base ‘ 𝐸 ) ) ) = ( Base ‘ ( 𝐸 ↑s ( Base ‘ 𝐸 ) ) )
24 16 23 rhmf ⊢ ( 𝑂 ∈ ( ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) RingHom ( 𝐸 ↑s ( Base ‘ 𝐸 ) ) ) → 𝑂 : ( Base ‘ ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) ) ⟶ ( Base ‘ ( 𝐸 ↑s ( Base ‘ 𝐸 ) ) ) )
25 22 24 syl ⊢ ( 𝜑 → 𝑂 : ( Base ‘ ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) ) ⟶ ( Base ‘ ( 𝐸 ↑s ( Base ‘ 𝐸 ) ) ) )
26 25 fdmd ⊢ ( 𝜑 → dom 𝑂 = ( Base ‘ ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) ) → dom 𝑂 = ( Base ‘ ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) ) )
28 19 27 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) ) → 𝑝 ∈ dom 𝑂 )
29 eqid ⊢ ( 0g ‘ ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) ) = ( 0g ‘ ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) )
30 15 29 17 mon1pn0 ⊢ ( 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) → 𝑝 ≠ ( 0g ‘ ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) ) )
31 30 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) ) → 𝑝 ≠ ( 0g ‘ ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) ) )
32 eqid ⊢ ( Poly1 ‘ 𝐸 ) = ( Poly1 ‘ 𝐸 )
33 32 6 15 16 11 2 ressply10g ⊢ ( 𝜑 → 𝑍 = ( 0g ‘ ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) ) )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) ) → 𝑍 = ( 0g ‘ ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) ) )
35 31 34 neeqtrrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) ) → 𝑝 ≠ 𝑍 )
36 eldifsn ⊢ ( 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ↔ ( 𝑝 ∈ dom 𝑂 ∧ 𝑝 ≠ 𝑍 ) )
37 28 35 36 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) ) → 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) )
38 37 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) ∧ ( 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) → 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) )
39 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) ∧ ( 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) → 𝐸 ∈ Field )
40 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) ∧ ( 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) → ( Base ‘ 𝐸 ) ∈ V )
41 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) ∧ ( 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) → 𝑂 : ( Base ‘ ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) ) ⟶ ( Base ‘ ( 𝐸 ↑s ( Base ‘ 𝐸 ) ) ) )
42 18 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) ∧ ( 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) → 𝑝 ∈ ( Base ‘ ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) ) )
43 41 42 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) ∧ ( 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) → ( 𝑂 ‘ 𝑝 ) ∈ ( Base ‘ ( 𝐸 ↑s ( Base ‘ 𝐸 ) ) ) )
44 20 7 23 39 40 43 pwselbas ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) ∧ ( 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) → ( 𝑂 ‘ 𝑝 ) : ( Base ‘ 𝐸 ) ⟶ ( Base ‘ 𝐸 ) )
45 44 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) ∧ ( 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) → ( 𝑂 ‘ 𝑝 ) Fn ( Base ‘ 𝐸 ) )
46 13 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) → 𝑥 ∈ ( Base ‘ 𝐸 ) )
47 46 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) ∧ ( 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) → 𝑥 ∈ ( Base ‘ 𝐸 ) )
48 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) ∧ ( 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 )
49 fniniseg ⊢ ( ( 𝑂 ‘ 𝑝 ) Fn ( Base ‘ 𝐸 ) → ( 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) )
50 49 biimpar ⊢ ( ( ( 𝑂 ‘ 𝑝 ) Fn ( Base ‘ 𝐸 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) → 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) )
51 45 47 48 50 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) ∧ ( 𝑝 ∈ ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) → 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) )
52 14 38 51 reximssdv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) → ∃ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) )
53 eliun ⊢ ( 𝑥 ∈ ∪ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) ↔ ∃ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) )
54 52 53 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) → 𝑥 ∈ ∪ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) )
55 nfv ⊢ Ⅎ 𝑝 𝜑
56 nfiu1 ⊢ Ⅎ 𝑝 ∪ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } )
57 56 nfcri ⊢ Ⅎ 𝑝 𝑥 ∈ ∪ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } )
58 55 57 nfan ⊢ Ⅎ 𝑝 ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) )
59 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ) ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) ) → 𝐸 ∈ Field )
60 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ) ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) ) → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
61 eldifi ⊢ ( 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) → 𝑝 ∈ dom 𝑂 )
62 61 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ) → 𝑝 ∈ dom 𝑂 )
63 62 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ) ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) ) → 𝑝 ∈ dom 𝑂 )
64 eldifsni ⊢ ( 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) → 𝑝 ≠ 𝑍 )
65 64 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ) → 𝑝 ≠ 𝑍 )
66 65 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ) ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) ) → 𝑝 ≠ 𝑍 )
67 4 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ) → 𝐸 ∈ Field )
68 fvexd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ) → ( Base ‘ 𝐸 ) ∈ V )
69 25 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ) → 𝑂 : ( Base ‘ ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) ) ⟶ ( Base ‘ ( 𝐸 ↑s ( Base ‘ 𝐸 ) ) ) )
70 26 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ) → dom 𝑂 = ( Base ‘ ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) ) )
71 62 70 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ) → 𝑝 ∈ ( Base ‘ ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) ) ) )
72 69 71 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ) → ( 𝑂 ‘ 𝑝 ) ∈ ( Base ‘ ( 𝐸 ↑s ( Base ‘ 𝐸 ) ) ) )
73 20 7 23 67 68 72 pwselbas ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ) → ( 𝑂 ‘ 𝑝 ) : ( Base ‘ 𝐸 ) ⟶ ( Base ‘ 𝐸 ) )
74 73 ffnd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ) → ( 𝑂 ‘ 𝑝 ) Fn ( Base ‘ 𝐸 ) )
75 49 biimpa ⊢ ( ( ( 𝑂 ‘ 𝑝 ) Fn ( Base ‘ 𝐸 ) ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) ) → ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) )
76 74 75 sylan ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ) ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) ) → ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) )
77 76 simprd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ) ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) ) → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 )
78 76 simpld ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ) ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) ) → 𝑥 ∈ ( Base ‘ 𝐸 ) )
79 1 2 3 59 60 7 63 66 77 78 irngnzply1lem ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ) ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) ) → 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) )
80 79 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) ) ∧ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ) ∧ 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) ) → 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) )
81 53 biimpi ⊢ ( 𝑥 ∈ ∪ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) → ∃ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) )
82 81 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) ) → ∃ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) 𝑥 ∈ ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) )
83 58 80 82 r19.29af ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) ) → 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) )
84 54 83 impbida ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ↔ 𝑥 ∈ ∪ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) ) )
85 84 eqrdv ⊢ ( 𝜑 → ( 𝐸 IntgRing 𝐹 ) = ∪ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ( ◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) )