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	⊢ 𝑂 = ( 𝐸 evalSub₁ 𝐹 )
	irngnzply1.z	⊢ 𝑍 = ( 0_g ‘ ( Poly₁ ‘ 𝐸 ) )
	irngnzply1.1	⊢ 0 = ( 0_g ‘ 𝐸 )
	irngnzply1.e	⊢ ( 𝜑 → 𝐸 ∈ Field )
	irngnzply1.f	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
Assertion	irngnzply1	⊢ ( 𝜑 → ( 𝐸 IntgRing 𝐹 ) = ∪ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ( ^◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		irngnzply1.o	⊢ 𝑂 = ( 𝐸 evalSub₁ 𝐹 )
2		irngnzply1.z	⊢ 𝑍 = ( 0_g ‘ ( Poly₁ ‘ 𝐸 ) )
3		irngnzply1.1	⊢ 0 = ( 0_g ‘ 𝐸 )
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 ‘ 𝐸 ) ∧ ∃ 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) )
13	12	biimpa	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) → ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ ∃ 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) )
14	13	simprd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) → ∃ 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 )
15		eqid	⊢ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) = ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) )
16		eqid	⊢ ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) = ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) )
17		eqid	⊢ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) = ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) )
18	15 16 17	mon1pcl	⊢ ( 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) → 𝑝 ∈ ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
19	18	adantl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ) → 𝑝 ∈ ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
20		eqid	⊢ ( 𝐸 ↑_s ( Base ‘ 𝐸 ) ) = ( 𝐸 ↑_s ( Base ‘ 𝐸 ) )
21	1 7 20 6 15	evls1rhm	⊢ ( ( 𝐸 ∈ CRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ) → 𝑂 ∈ ( ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) RingHom ( 𝐸 ↑_s ( Base ‘ 𝐸 ) ) ) )
22	8 11 21	syl2anc	⊢ ( 𝜑 → 𝑂 ∈ ( ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) RingHom ( 𝐸 ↑_s ( Base ‘ 𝐸 ) ) ) )
23		eqid	⊢ ( Base ‘ ( 𝐸 ↑_s ( Base ‘ 𝐸 ) ) ) = ( Base ‘ ( 𝐸 ↑_s ( Base ‘ 𝐸 ) ) )
24	16 23	rhmf	⊢ ( 𝑂 ∈ ( ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) RingHom ( 𝐸 ↑_s ( Base ‘ 𝐸 ) ) ) → 𝑂 : ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) ⟶ ( Base ‘ ( 𝐸 ↑_s ( Base ‘ 𝐸 ) ) ) )
25	22 24	syl	⊢ ( 𝜑 → 𝑂 : ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) ⟶ ( Base ‘ ( 𝐸 ↑_s ( Base ‘ 𝐸 ) ) ) )
26	25	fdmd	⊢ ( 𝜑 → dom 𝑂 = ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
27	26	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ) → dom 𝑂 = ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
28	19 27	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ) → 𝑝 ∈ dom 𝑂 )
29		eqid	⊢ ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) = ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) )
30	15 29 17	mon1pn0	⊢ ( 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) → 𝑝 ≠ ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
31	30	adantl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ) → 𝑝 ≠ ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
32		eqid	⊢ ( Poly₁ ‘ 𝐸 ) = ( Poly₁ ‘ 𝐸 )
33	32 6 15 16 11 2	ressply10g	⊢ ( 𝜑 → 𝑍 = ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
34	33	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ) → 𝑍 = ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
35	31 34	neeqtrrd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ) → 𝑝 ≠ 𝑍 )
36		eldifsn	⊢ ( 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ↔ ( 𝑝 ∈ dom 𝑂 ∧ 𝑝 ≠ 𝑍 ) )
37	28 35 36	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ) → 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) )
38	37	ad2ant2r	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) ∧ ( 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) → 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) )
39	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) ∧ ( 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) → 𝐸 ∈ Field )
40		fvexd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) ∧ ( 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) → ( Base ‘ 𝐸 ) ∈ V )
41	25	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) ∧ ( 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) → 𝑂 : ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) ⟶ ( Base ‘ ( 𝐸 ↑_s ( Base ‘ 𝐸 ) ) ) )
42	18	ad2antrl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) ∧ ( 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) → 𝑝 ∈ ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
43	41 42	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) ∧ ( 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) → ( 𝑂 ‘ 𝑝 ) ∈ ( Base ‘ ( 𝐸 ↑_s ( Base ‘ 𝐸 ) ) ) )
44	20 7 23 39 40 43	pwselbas	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) ∧ ( 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) → ( 𝑂 ‘ 𝑝 ) : ( Base ‘ 𝐸 ) ⟶ ( Base ‘ 𝐸 ) )
45	44	ffnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) ∧ ( 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) → ( 𝑂 ‘ 𝑝 ) Fn ( Base ‘ 𝐸 ) )
46	13	simpld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) → 𝑥 ∈ ( Base ‘ 𝐸 ) )
47	46	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) ∧ ( 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ∧ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑥 ) = 0 ) ) → 𝑥 ∈ ( Base ‘ 𝐸 ) )
48		simprr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ) ∧ ( 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_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 𝐹 ) ) ∧ ( 𝑝 ∈ ( Monic_1p ‘ ( 𝐸 ↾_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 ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) ⟶ ( Base ‘ ( 𝐸 ↑_s ( Base ‘ 𝐸 ) ) ) )
70	26	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ) → dom 𝑂 = ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
71	62 70	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ) → 𝑝 ∈ ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_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	bilani	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ( ^◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) ) → ∃ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) 𝑥 ∈ ( ^◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) )
82	58 80 81	r19.29af	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ∪ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ( ^◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) ) → 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) )
83	54 82	impbida	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐸 IntgRing 𝐹 ) ↔ 𝑥 ∈ ∪ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ( ^◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) ) )
84	83	eqrdv	⊢ ( 𝜑 → ( 𝐸 IntgRing 𝐹 ) = ∪ 𝑝 ∈ ( dom 𝑂 ∖ { 𝑍 } ) ( ^◡ ( 𝑂 ‘ 𝑝 ) “ { 0 } ) )

Metamath Proof Explorer

Theorem irngnzply1

Proof