Step | Hyp | Ref
| Expression |
1 | | irngnzply1.o |
. . . . . . . 8
⊢ 𝑂 = (𝐸 evalSub1 𝐹) |
2 | | eqid 2732 |
. . . . . . . 8
⊢ (𝐸 ↾s 𝐹) = (𝐸 ↾s 𝐹) |
3 | | eqid 2732 |
. . . . . . . 8
⊢
(Base‘𝐸) =
(Base‘𝐸) |
4 | | irngnzply1.1 |
. . . . . . . 8
⊢ 0 =
(0g‘𝐸) |
5 | | irngnzply1.e |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ Field) |
6 | 5 | fldcrngd 20279 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ CRing) |
7 | | irngnzply1.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) |
8 | | issdrg 20355 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s 𝐹) ∈ DivRing)) |
9 | 7, 8 | sylib 217 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s 𝐹) ∈ DivRing)) |
10 | 9 | simp2d 1143 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸)) |
11 | 1, 2, 3, 4, 6, 10 | elirng 32652 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝐸 IntgRing 𝐹) ↔ (𝑥 ∈ (Base‘𝐸) ∧ ∃𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹))((𝑂‘𝑝)‘𝑥) = 0 ))) |
12 | 11 | biimpa 477 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) → (𝑥 ∈ (Base‘𝐸) ∧ ∃𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹))((𝑂‘𝑝)‘𝑥) = 0 )) |
13 | 12 | simprd 496 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) → ∃𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹))((𝑂‘𝑝)‘𝑥) = 0 ) |
14 | | eqid 2732 |
. . . . . . . . . 10
⊢
(Poly1‘(𝐸 ↾s 𝐹)) = (Poly1‘(𝐸 ↾s 𝐹)) |
15 | | eqid 2732 |
. . . . . . . . . 10
⊢
(Base‘(Poly1‘(𝐸 ↾s 𝐹))) =
(Base‘(Poly1‘(𝐸 ↾s 𝐹))) |
16 | | eqid 2732 |
. . . . . . . . . 10
⊢
(Monic1p‘(𝐸 ↾s 𝐹)) = (Monic1p‘(𝐸 ↾s 𝐹)) |
17 | 14, 15, 16 | mon1pcl 25593 |
. . . . . . . . 9
⊢ (𝑝 ∈
(Monic1p‘(𝐸 ↾s 𝐹)) → 𝑝 ∈
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) |
18 | 17 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹))) → 𝑝 ∈
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) |
19 | | eqid 2732 |
. . . . . . . . . . . . 13
⊢ (𝐸 ↑s
(Base‘𝐸)) = (𝐸 ↑s
(Base‘𝐸)) |
20 | 1, 3, 19, 2, 14 | evls1rhm 21772 |
. . . . . . . . . . . 12
⊢ ((𝐸 ∈ CRing ∧ 𝐹 ∈ (SubRing‘𝐸)) → 𝑂 ∈ ((Poly1‘(𝐸 ↾s 𝐹)) RingHom (𝐸 ↑s (Base‘𝐸)))) |
21 | 6, 10, 20 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑂 ∈ ((Poly1‘(𝐸 ↾s 𝐹)) RingHom (𝐸 ↑s (Base‘𝐸)))) |
22 | | eqid 2732 |
. . . . . . . . . . . 12
⊢
(Base‘(𝐸
↑s (Base‘𝐸))) = (Base‘(𝐸 ↑s (Base‘𝐸))) |
23 | 15, 22 | rhmf 20215 |
. . . . . . . . . . 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 6716 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝑂 =
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) |
26 | 25 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹))) → dom 𝑂 =
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) |
27 | 18, 26 | eleqtrrd 2836 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹))) → 𝑝 ∈ dom 𝑂) |
28 | | eqid 2732 |
. . . . . . . . . 10
⊢
(0g‘(Poly1‘(𝐸 ↾s 𝐹))) =
(0g‘(Poly1‘(𝐸 ↾s 𝐹))) |
29 | 14, 28, 16 | mon1pn0 25595 |
. . . . . . . . 9
⊢ (𝑝 ∈
(Monic1p‘(𝐸 ↾s 𝐹)) → 𝑝 ≠
(0g‘(Poly1‘(𝐸 ↾s 𝐹)))) |
30 | 29 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹))) → 𝑝 ≠
(0g‘(Poly1‘(𝐸 ↾s 𝐹)))) |
31 | | eqid 2732 |
. . . . . . . . . 10
⊢
(Poly1‘𝐸) = (Poly1‘𝐸) |
32 | | irngnzply1.z |
. . . . . . . . . 10
⊢ 𝑍 =
(0g‘(Poly1‘𝐸)) |
33 | 31, 2, 14, 15, 10, 32 | ressply10g 32560 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 =
(0g‘(Poly1‘(𝐸 ↾s 𝐹)))) |
34 | 33 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹))) → 𝑍 =
(0g‘(Poly1‘(𝐸 ↾s 𝐹)))) |
35 | 30, 34 | neeqtrrd 3015 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹))) → 𝑝 ≠ 𝑍) |
36 | | eldifsn 4784 |
. . . . . . 7
⊢ (𝑝 ∈ (dom 𝑂 ∖ {𝑍}) ↔ (𝑝 ∈ dom 𝑂 ∧ 𝑝 ≠ 𝑍)) |
37 | 27, 35, 36 | sylanbrc 583 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹))) → 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) |
38 | 37 | ad2ant2r 745 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) ∧ (𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹)) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) → 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) |
39 | 5 | ad2antrr 724 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) ∧ (𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹)) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) → 𝐸 ∈ Field) |
40 | | fvexd 6894 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) ∧ (𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹)) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) →
(Base‘𝐸) ∈
V) |
41 | 24 | ad2antrr 724 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) ∧ (𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹)) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) → 𝑂:(Base‘(Poly1‘(𝐸 ↾s 𝐹)))⟶(Base‘(𝐸 ↑s
(Base‘𝐸)))) |
42 | 17 | ad2antrl 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) ∧ (𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹)) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) → 𝑝 ∈
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) |
43 | 41, 42 | ffvelcdmd 7073 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) ∧ (𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹)) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) → (𝑂‘𝑝) ∈ (Base‘(𝐸 ↑s (Base‘𝐸)))) |
44 | 19, 3, 22, 39, 40, 43 | pwselbas 17419 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) ∧ (𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹)) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) → (𝑂‘𝑝):(Base‘𝐸)⟶(Base‘𝐸)) |
45 | 44 | ffnd 6706 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) ∧ (𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹)) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) → (𝑂‘𝑝) Fn (Base‘𝐸)) |
46 | 12 | simpld 495 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) → 𝑥 ∈ (Base‘𝐸)) |
47 | 46 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) ∧ (𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹)) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) → 𝑥 ∈ (Base‘𝐸)) |
48 | | simprr 771 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) ∧ (𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹)) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) → ((𝑂‘𝑝)‘𝑥) = 0 ) |
49 | | fniniseg 7047 |
. . . . . . 7
⊢ ((𝑂‘𝑝) Fn (Base‘𝐸) → (𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 }) ↔ (𝑥 ∈ (Base‘𝐸) ∧ ((𝑂‘𝑝)‘𝑥) = 0 ))) |
50 | 49 | biimpar 478 |
. . . . . 6
⊢ (((𝑂‘𝑝) Fn (Base‘𝐸) ∧ (𝑥 ∈ (Base‘𝐸) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) → 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) |
51 | 45, 47, 48, 50 | syl12anc 835 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) ∧ (𝑝 ∈ (Monic1p‘(𝐸 ↾s 𝐹)) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) → 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) |
52 | 13, 38, 51 | reximssdv 3172 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) → ∃𝑝 ∈ (dom 𝑂 ∖ {𝑍})𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) |
53 | | eliun 4995 |
. . . 4
⊢ (𝑥 ∈ ∪ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 }) ↔ ∃𝑝 ∈ (dom 𝑂 ∖ {𝑍})𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) |
54 | 52, 53 | sylibr 233 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐸 IntgRing 𝐹)) → 𝑥 ∈ ∪
𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 })) |
55 | | nfv 1917 |
. . . . 5
⊢
Ⅎ𝑝𝜑 |
56 | | nfiu1 5025 |
. . . . . 6
⊢
Ⅎ𝑝∪ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 }) |
57 | 56 | nfcri 2890 |
. . . . 5
⊢
Ⅎ𝑝 𝑥 ∈ ∪ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 }) |
58 | 55, 57 | nfan 1902 |
. . . 4
⊢
Ⅎ𝑝(𝜑 ∧ 𝑥 ∈ ∪
𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 })) |
59 | 5 | ad2antrr 724 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) ∧ 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) → 𝐸 ∈ Field) |
60 | 7 | ad2antrr 724 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) ∧ 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) → 𝐹 ∈ (SubDRing‘𝐸)) |
61 | | eldifi 4123 |
. . . . . . . 8
⊢ (𝑝 ∈ (dom 𝑂 ∖ {𝑍}) → 𝑝 ∈ dom 𝑂) |
62 | 61 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) → 𝑝 ∈ dom 𝑂) |
63 | 62 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) ∧ 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) → 𝑝 ∈ dom 𝑂) |
64 | | eldifsni 4787 |
. . . . . . . 8
⊢ (𝑝 ∈ (dom 𝑂 ∖ {𝑍}) → 𝑝 ≠ 𝑍) |
65 | 64 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) → 𝑝 ≠ 𝑍) |
66 | 65 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) ∧ 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) → 𝑝 ≠ 𝑍) |
67 | 5 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) → 𝐸 ∈ Field) |
68 | | fvexd 6894 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) → (Base‘𝐸) ∈ V) |
69 | 24 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) → 𝑂:(Base‘(Poly1‘(𝐸 ↾s 𝐹)))⟶(Base‘(𝐸 ↑s
(Base‘𝐸)))) |
70 | 25 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) → dom 𝑂 =
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) |
71 | 62, 70 | eleqtrd 2835 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) → 𝑝 ∈
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) |
72 | 69, 71 | ffvelcdmd 7073 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) → (𝑂‘𝑝) ∈ (Base‘(𝐸 ↑s (Base‘𝐸)))) |
73 | 19, 3, 22, 67, 68, 72 | pwselbas 17419 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) → (𝑂‘𝑝):(Base‘𝐸)⟶(Base‘𝐸)) |
74 | 73 | ffnd 6706 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) → (𝑂‘𝑝) Fn (Base‘𝐸)) |
75 | 49 | biimpa 477 |
. . . . . . . 8
⊢ (((𝑂‘𝑝) Fn (Base‘𝐸) ∧ 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) → (𝑥 ∈ (Base‘𝐸) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) |
76 | 74, 75 | sylan 580 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) ∧ 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) → (𝑥 ∈ (Base‘𝐸) ∧ ((𝑂‘𝑝)‘𝑥) = 0 )) |
77 | 76 | simprd 496 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) ∧ 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) → ((𝑂‘𝑝)‘𝑥) = 0 ) |
78 | 76 | simpld 495 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) ∧ 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) → 𝑥 ∈ (Base‘𝐸)) |
79 | 1, 32, 4, 59, 60, 3, 63, 66, 77, 78 | irngnzply1lem 32656 |
. . . . 5
⊢ (((𝜑 ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) ∧ 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) → 𝑥 ∈ (𝐸 IntgRing 𝐹)) |
80 | 79 | adantllr 717 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ ∪
𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 })) ∧ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})) ∧ 𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) → 𝑥 ∈ (𝐸 IntgRing 𝐹)) |
81 | 53 | biimpi 215 |
. . . . 5
⊢ (𝑥 ∈ ∪ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 }) → ∃𝑝 ∈ (dom 𝑂 ∖ {𝑍})𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) |
82 | 81 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 })) → ∃𝑝 ∈ (dom 𝑂 ∖ {𝑍})𝑥 ∈ (◡(𝑂‘𝑝) “ { 0 })) |
83 | 58, 80, 82 | r19.29af 3265 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 })) → 𝑥 ∈ (𝐸 IntgRing 𝐹)) |
84 | 54, 83 | impbida 799 |
. 2
⊢ (𝜑 → (𝑥 ∈ (𝐸 IntgRing 𝐹) ↔ 𝑥 ∈ ∪
𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 }))) |
85 | 84 | eqrdv 2730 |
1
⊢ (𝜑 → (𝐸 IntgRing 𝐹) = ∪
𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 })) |