| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | irngnzply1.o | . . . . . . . 8
⊢ 𝑂 = (𝐸 evalSub1 𝐹) | 
| 2 |  | eqid 2736 | . . . . . . . 8
⊢ (𝐸 ↾s 𝐹) = (𝐸 ↾s 𝐹) | 
| 3 |  | eqid 2736 | . . . . . . . 8
⊢
(Base‘𝐸) =
(Base‘𝐸) | 
| 4 |  | irngnzply1.1 | . . . . . . . 8
⊢  0 =
(0g‘𝐸) | 
| 5 |  | irngnzply1.e | . . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ Field) | 
| 6 | 5 | fldcrngd 20743 | . . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ CRing) | 
| 7 |  | irngnzply1.f | . . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) | 
| 8 |  | issdrg 20790 | . . . . . . . . . 10
⊢ (𝐹 ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s 𝐹) ∈ DivRing)) | 
| 9 | 7, 8 | sylib 218 | . . . . . . . . 9
⊢ (𝜑 → (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s 𝐹) ∈ DivRing)) | 
| 10 | 9 | simp2d 1143 | . . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸)) | 
| 11 | 1, 2, 3, 4, 6, 10 | elirng 33737 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝐸 IntgRing 𝐹) ↔ (𝑥 ∈ (Base‘𝐸) ∧ ∃𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹))((𝑂‘𝑝)‘𝑥) = 0 ))) | 
| 12 | 11 | biimpa 476 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) → (𝑥 ∈ (Base‘𝐸) ∧ ∃𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹))((𝑂‘𝑝)‘𝑥) = 0 )) | 
| 13 | 12 | simprd 495 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) → ∃𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹))((𝑂‘𝑝)‘𝑥) = 0 ) | 
| 14 |  | eqid 2736 | . . . . . . . . . 10
⊢
(Poly1‘(𝐸 ↾s 𝐹)) = (Poly1‘(𝐸 ↾s 𝐹)) | 
| 15 |  | eqid 2736 | . . . . . . . . . 10
⊢
(Base‘(Poly1‘(𝐸 ↾s 𝐹))) =
(Base‘(Poly1‘(𝐸 ↾s 𝐹))) | 
| 16 |  | eqid 2736 | . . . . . . . . . 10
⊢
(Monic1p‘(𝐸 ↾s 𝐹)) = (Monic1p‘(𝐸 ↾s 𝐹)) | 
| 17 | 14, 15, 16 | mon1pcl 26185 | . . . . . . . . 9
⊢ (𝑝 ∈
(Monic1p‘(𝐸 ↾s 𝐹)) → 𝑝 ∈
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) | 
| 18 | 17 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹))) → 𝑝 ∈
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) | 
| 19 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢ (𝐸 ↑s
(Base‘𝐸)) = (𝐸 ↑s
(Base‘𝐸)) | 
| 20 | 1, 3, 19, 2, 14 | evls1rhm 22327 | . . . . . . . . . . . 12
⊢ ((𝐸 ∈ CRing ∧ 𝐹 ∈ (SubRing‘𝐸)) → 𝑂 ∈ ((Poly1‘(𝐸 ↾s 𝐹)) RingHom (𝐸 ↑s (Base‘𝐸)))) | 
| 21 | 6, 10, 20 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑂 ∈ ((Poly1‘(𝐸 ↾s 𝐹)) RingHom (𝐸 ↑s (Base‘𝐸)))) | 
| 22 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(Base‘(𝐸
↑s (Base‘𝐸))) = (Base‘(𝐸 ↑s (Base‘𝐸))) | 
| 23 | 15, 22 | rhmf 20486 | . . . . . . . . . . 11
⊢ (𝑂 ∈
((Poly1‘(𝐸
↾s 𝐹))
RingHom (𝐸
↑s (Base‘𝐸))) → 𝑂:(Base‘(Poly1‘(𝐸 ↾s 𝐹)))⟶(Base‘(𝐸 ↑s
(Base‘𝐸)))) | 
| 24 | 21, 23 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝑂:(Base‘(Poly1‘(𝐸 ↾s 𝐹)))⟶(Base‘(𝐸 ↑s
(Base‘𝐸)))) | 
| 25 | 24 | fdmd 6745 | . . . . . . . . 9
⊢ (𝜑 → dom 𝑂 =
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) | 
| 26 | 25 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹))) → dom 𝑂 =
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) | 
| 27 | 18, 26 | eleqtrrd 2843 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹))) → 𝑝 ∈ dom 𝑂) | 
| 28 |  | eqid 2736 | . . . . . . . . . 10
⊢
(0g‘(Poly1‘(𝐸 ↾s 𝐹))) =
(0g‘(Poly1‘(𝐸 ↾s 𝐹))) | 
| 29 | 14, 28, 16 | mon1pn0 26187 | . . . . . . . . 9
⊢ (𝑝 ∈
(Monic1p‘(𝐸 ↾s 𝐹)) → 𝑝 ≠
(0g‘(Poly1‘(𝐸 ↾s 𝐹)))) | 
| 30 | 29 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹))) → 𝑝 ≠
(0g‘(Poly1‘(𝐸 ↾s 𝐹)))) | 
| 31 |  | eqid 2736 | . . . . . . . . . 10
⊢
(Poly1‘𝐸) = (Poly1‘𝐸) | 
| 32 |  | irngnzply1.z | . . . . . . . . . 10
⊢ 𝑍 =
(0g‘(Poly1‘𝐸)) | 
| 33 | 31, 2, 14, 15, 10, 32 | ressply10g 33593 | . . . . . . . . 9
⊢ (𝜑 → 𝑍 =
(0g‘(Poly1‘(𝐸 ↾s 𝐹)))) | 
| 34 | 33 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹))) → 𝑍 =
(0g‘(Poly1‘(𝐸 ↾s 𝐹)))) | 
| 35 | 30, 34 | neeqtrrd 3014 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹))) → 𝑝 ≠ 𝑍) | 
| 36 |  | eldifsn 4785 | . . . . . . 7
⊢ (𝑝 ∈ (dom 𝑂 ∖ {𝑍}) ↔ (𝑝 ∈ dom 𝑂 ∧ 𝑝 ≠ 𝑍)) | 
| 37 | 27, 35, 36 | sylanbrc 583 | . . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹))) → 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) | 
| 38 | 37 | ad2ant2r 747 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) ∧ (𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹)) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) → 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) | 
| 39 | 5 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) ∧ (𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹)) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) → 𝐸 ∈ Field) | 
| 40 |  | fvexd 6920 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) ∧ (𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹)) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) →
(Base‘𝐸) ∈
V) | 
| 41 | 24 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) ∧ (𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹)) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) → 𝑂:(Base‘(Poly1‘(𝐸 ↾s 𝐹)))⟶(Base‘(𝐸 ↑s
(Base‘𝐸)))) | 
| 42 | 17 | ad2antrl 728 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) ∧ (𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹)) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) → 𝑝 ∈
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) | 
| 43 | 41, 42 | ffvelcdmd 7104 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) ∧ (𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹)) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) → (𝑂‘𝑝) ∈ (Base‘(𝐸 ↑s (Base‘𝐸)))) | 
| 44 | 19, 3, 22, 39, 40, 43 | pwselbas 17535 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) ∧ (𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹)) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) → (𝑂‘𝑝):(Base‘𝐸)⟶(Base‘𝐸)) | 
| 45 | 44 | ffnd 6736 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) ∧ (𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹)) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) → (𝑂‘𝑝) Fn (Base‘𝐸)) | 
| 46 | 12 | simpld 494 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) → 𝑥 ∈ (Base‘𝐸)) | 
| 47 | 46 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) ∧ (𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹)) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) → 𝑥 ∈ (Base‘𝐸)) | 
| 48 |  | simprr 772 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) ∧ (𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹)) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) → ((𝑂‘𝑝)‘𝑥) = 0 ) | 
| 49 |  | fniniseg 7079 | . . . . . . 7
⊢ ((𝑂‘𝑝) Fn (Base‘𝐸) → (𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 }) ↔ (𝑥 ∈ (Base‘𝐸) ∧ ((𝑂‘𝑝)‘𝑥) = 0 ))) | 
| 50 | 49 | biimpar 477 | . . . . . 6
⊢ (((𝑂‘𝑝) Fn (Base‘𝐸) ∧ (𝑥 ∈ (Base‘𝐸) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) → 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) | 
| 51 | 45, 47, 48, 50 | syl12anc 836 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) ∧ (𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹)) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) → 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) | 
| 52 | 13, 38, 51 | reximssdv 3172 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) → ∃𝑝 ∈ (dom 𝑂 ∖ {𝑍})𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) | 
| 53 |  | eliun 4994 | . . . 4
⊢ (𝑥 ∈ ∪ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 }) ↔ ∃𝑝 ∈ (dom 𝑂 ∖ {𝑍})𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) | 
| 54 | 52, 53 | sylibr 234 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) → 𝑥 ∈ ∪
𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 })) | 
| 55 |  | nfv 1913 | . . . . 5
⊢
Ⅎ𝑝𝜑 | 
| 56 |  | nfiu1 5026 | . . . . . 6
⊢
Ⅎ𝑝∪ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 }) | 
| 57 | 56 | nfcri 2896 | . . . . 5
⊢
Ⅎ𝑝 𝑥 ∈ ∪ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 }) | 
| 58 | 55, 57 | nfan 1898 | . . . 4
⊢
Ⅎ𝑝(𝜑 ∧ 𝑥 ∈ ∪
𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 })) | 
| 59 | 5 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) ∧ 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) → 𝐸 ∈ Field) | 
| 60 | 7 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) ∧ 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) → 𝐹 ∈ (SubDRing‘𝐸)) | 
| 61 |  | eldifi 4130 | . . . . . . . 8
⊢ (𝑝 ∈ (dom 𝑂 ∖ {𝑍}) → 𝑝 ∈ dom 𝑂) | 
| 62 | 61 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) → 𝑝 ∈ dom 𝑂) | 
| 63 | 62 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) ∧ 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) → 𝑝 ∈ dom 𝑂) | 
| 64 |  | eldifsni 4789 | . . . . . . . 8
⊢ (𝑝 ∈ (dom 𝑂 ∖ {𝑍}) → 𝑝 ≠ 𝑍) | 
| 65 | 64 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) → 𝑝 ≠ 𝑍) | 
| 66 | 65 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) ∧ 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) → 𝑝 ≠ 𝑍) | 
| 67 | 5 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) → 𝐸 ∈ Field) | 
| 68 |  | fvexd 6920 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) → (Base‘𝐸) ∈ V) | 
| 69 | 24 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) → 𝑂:(Base‘(Poly1‘(𝐸 ↾s 𝐹)))⟶(Base‘(𝐸 ↑s
(Base‘𝐸)))) | 
| 70 | 25 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) → dom 𝑂 =
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) | 
| 71 | 62, 70 | eleqtrd 2842 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) → 𝑝 ∈
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) | 
| 72 | 69, 71 | ffvelcdmd 7104 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) → (𝑂‘𝑝) ∈ (Base‘(𝐸 ↑s (Base‘𝐸)))) | 
| 73 | 19, 3, 22, 67, 68, 72 | pwselbas 17535 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) → (𝑂‘𝑝):(Base‘𝐸)⟶(Base‘𝐸)) | 
| 74 | 73 | ffnd 6736 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) → (𝑂‘𝑝) Fn (Base‘𝐸)) | 
| 75 | 49 | biimpa 476 | . . . . . . . 8
⊢ (((𝑂‘𝑝) Fn (Base‘𝐸) ∧ 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) → (𝑥 ∈ (Base‘𝐸) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) | 
| 76 | 74, 75 | sylan 580 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) ∧ 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) → (𝑥 ∈ (Base‘𝐸) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) | 
| 77 | 76 | simprd 495 | . . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) ∧ 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) → ((𝑂‘𝑝)‘𝑥) = 0 ) | 
| 78 | 76 | simpld 494 | . . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) ∧ 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) → 𝑥 ∈ (Base‘𝐸)) | 
| 79 | 1, 32, 4, 59, 60, 3, 63, 66, 77, 78 | irngnzply1lem 33741 | . . . . 5
⊢ (((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) ∧ 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) → 𝑥 ∈ (𝐸 IntgRing 𝐹)) | 
| 80 | 79 | adantllr 719 | . . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ ∪
𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 })) ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) ∧ 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) → 𝑥 ∈ (𝐸 IntgRing 𝐹)) | 
| 81 | 53 | biimpi 216 | . . . . 5
⊢ (𝑥 ∈ ∪ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 }) → ∃𝑝 ∈ (dom 𝑂 ∖ {𝑍})𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) | 
| 82 | 81 | adantl 481 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 })) → ∃𝑝 ∈ (dom 𝑂 ∖ {𝑍})𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) | 
| 83 | 58, 80, 82 | r19.29af 3267 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 })) → 𝑥 ∈ (𝐸 IntgRing 𝐹)) | 
| 84 | 54, 83 | impbida 800 | . 2
⊢ (𝜑 → (𝑥 ∈ (𝐸 IntgRing 𝐹) ↔ 𝑥 ∈ ∪
𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 }))) | 
| 85 | 84 | eqrdv 2734 | 1
⊢ (𝜑 → (𝐸 IntgRing 𝐹) = ∪
𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 })) |