| Step | Hyp | Ref
| Expression |
| 1 | | irngnminplynz.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) |
| 2 | | sdrgsubrg 20792 |
. . . . . 6
⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ∈ (SubRing‘𝐸)) |
| 3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸)) |
| 4 | | eqid 2737 |
. . . . . 6
⊢ (𝐸 ↾s 𝐹) = (𝐸 ↾s 𝐹) |
| 5 | 4 | subrgring 20574 |
. . . . 5
⊢ (𝐹 ∈ (SubRing‘𝐸) → (𝐸 ↾s 𝐹) ∈ Ring) |
| 6 | 3, 5 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ Ring) |
| 7 | | eqid 2737 |
. . . . 5
⊢
(Poly1‘(𝐸 ↾s 𝐹)) = (Poly1‘(𝐸 ↾s 𝐹)) |
| 8 | 7 | ply1ring 22249 |
. . . 4
⊢ ((𝐸 ↾s 𝐹) ∈ Ring →
(Poly1‘(𝐸
↾s 𝐹))
∈ Ring) |
| 9 | 6, 8 | syl 17 |
. . 3
⊢ (𝜑 →
(Poly1‘(𝐸
↾s 𝐹))
∈ Ring) |
| 10 | | eqid 2737 |
. . . . . 6
⊢ (𝐸 evalSub1 𝐹) = (𝐸 evalSub1 𝐹) |
| 11 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐸) =
(Base‘𝐸) |
| 12 | | irngnminplynz.e |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ Field) |
| 13 | 12 | fldcrngd 20742 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ CRing) |
| 14 | | eqid 2737 |
. . . . . . . 8
⊢
(0g‘𝐸) = (0g‘𝐸) |
| 15 | 10, 4, 11, 14, 13, 3 | irngssv 33738 |
. . . . . . 7
⊢ (𝜑 → (𝐸 IntgRing 𝐹) ⊆ (Base‘𝐸)) |
| 16 | | irngnminplynz.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹)) |
| 17 | 15, 16 | sseldd 3984 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ (Base‘𝐸)) |
| 18 | | eqid 2737 |
. . . . . 6
⊢ {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)} = {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)} |
| 19 | 10, 7, 11, 13, 3, 17, 14, 18 | ply1annidl 33745 |
. . . . 5
⊢ (𝜑 → {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)} ∈
(LIdeal‘(Poly1‘(𝐸 ↾s 𝐹)))) |
| 20 | | eqid 2737 |
. . . . . 6
⊢
(Base‘(Poly1‘(𝐸 ↾s 𝐹))) =
(Base‘(Poly1‘(𝐸 ↾s 𝐹))) |
| 21 | | eqid 2737 |
. . . . . 6
⊢
(LIdeal‘(Poly1‘(𝐸 ↾s 𝐹))) =
(LIdeal‘(Poly1‘(𝐸 ↾s 𝐹))) |
| 22 | 20, 21 | lidlss 21222 |
. . . . 5
⊢ ({𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)} ∈
(LIdeal‘(Poly1‘(𝐸 ↾s 𝐹))) → {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)} ⊆
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) |
| 23 | 19, 22 | syl 17 |
. . . 4
⊢ (𝜑 → {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)} ⊆
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) |
| 24 | 4 | sdrgdrng 20791 |
. . . . . 6
⊢ (𝐹 ∈ (SubDRing‘𝐸) → (𝐸 ↾s 𝐹) ∈ DivRing) |
| 25 | 1, 24 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ DivRing) |
| 26 | | eqid 2737 |
. . . . . 6
⊢
(idlGen1p‘(𝐸 ↾s 𝐹)) = (idlGen1p‘(𝐸 ↾s 𝐹)) |
| 27 | 7, 26, 21 | ig1pcl 26218 |
. . . . 5
⊢ (((𝐸 ↾s 𝐹) ∈ DivRing ∧ {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)} ∈
(LIdeal‘(Poly1‘(𝐸 ↾s 𝐹)))) →
((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)}) ∈ {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)}) |
| 28 | 25, 19, 27 | syl2anc 584 |
. . . 4
⊢ (𝜑 →
((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)}) ∈ {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)}) |
| 29 | 23, 28 | sseldd 3984 |
. . 3
⊢ (𝜑 →
((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)}) ∈
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) |
| 30 | | eqid 2737 |
. . . . 5
⊢
(RSpan‘(Poly1‘(𝐸 ↾s 𝐹))) =
(RSpan‘(Poly1‘(𝐸 ↾s 𝐹))) |
| 31 | 10, 7, 11, 12, 1, 17, 14, 18, 30, 26 | ply1annig1p 33747 |
. . . 4
⊢ (𝜑 → {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)} =
((RSpan‘(Poly1‘(𝐸 ↾s 𝐹)))‘{((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)})})) |
| 32 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑞 = 𝑝 → ((𝐸 evalSub1 𝐹)‘𝑞) = ((𝐸 evalSub1 𝐹)‘𝑝)) |
| 33 | 32 | fveq1d 6908 |
. . . . . . . 8
⊢ (𝑞 = 𝑝 → (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (((𝐸 evalSub1 𝐹)‘𝑝)‘𝐴)) |
| 34 | 33 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑞 = 𝑝 → ((((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸) ↔ (((𝐸 evalSub1 𝐹)‘𝑝)‘𝐴) = (0g‘𝐸))) |
| 35 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍})) ∧ 𝐴 ∈ (◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)})) → 𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍})) |
| 36 | 35 | eldifad 3963 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍})) ∧ 𝐴 ∈ (◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)})) → 𝑝 ∈ dom (𝐸 evalSub1 𝐹)) |
| 37 | 13 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍})) ∧ 𝐴 ∈ (◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)})) → 𝐸 ∈ CRing) |
| 38 | 3 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍})) ∧ 𝐴 ∈ (◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)})) → 𝐹 ∈ (SubRing‘𝐸)) |
| 39 | 10, 7, 20, 13, 3 | evls1dm 33587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom (𝐸 evalSub1 𝐹) =
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) |
| 40 | 39 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍})) ∧ 𝐴 ∈ (◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)})) → dom (𝐸 evalSub1 𝐹) =
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) |
| 41 | 36, 40 | eleqtrd 2843 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍})) ∧ 𝐴 ∈ (◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)})) → 𝑝 ∈
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) |
| 42 | 10, 7, 20, 37, 38, 11, 41 | evls1fvf 33588 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍})) ∧ 𝐴 ∈ (◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)})) → ((𝐸 evalSub1 𝐹)‘𝑝):(Base‘𝐸)⟶(Base‘𝐸)) |
| 43 | 42 | ffnd 6737 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍})) ∧ 𝐴 ∈ (◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)})) → ((𝐸 evalSub1 𝐹)‘𝑝) Fn (Base‘𝐸)) |
| 44 | | elpreima 7078 |
. . . . . . . . . 10
⊢ (((𝐸 evalSub1 𝐹)‘𝑝) Fn (Base‘𝐸) → (𝐴 ∈ (◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)}) ↔ (𝐴 ∈ (Base‘𝐸) ∧ (((𝐸 evalSub1 𝐹)‘𝑝)‘𝐴) ∈ {(0g‘𝐸)}))) |
| 45 | 44 | simplbda 499 |
. . . . . . . . 9
⊢ ((((𝐸 evalSub1 𝐹)‘𝑝) Fn (Base‘𝐸) ∧ 𝐴 ∈ (◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)})) → (((𝐸 evalSub1 𝐹)‘𝑝)‘𝐴) ∈ {(0g‘𝐸)}) |
| 46 | 43, 45 | sylancom 588 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍})) ∧ 𝐴 ∈ (◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)})) → (((𝐸 evalSub1 𝐹)‘𝑝)‘𝐴) ∈ {(0g‘𝐸)}) |
| 47 | | elsni 4643 |
. . . . . . . 8
⊢ ((((𝐸 evalSub1 𝐹)‘𝑝)‘𝐴) ∈ {(0g‘𝐸)} → (((𝐸 evalSub1 𝐹)‘𝑝)‘𝐴) = (0g‘𝐸)) |
| 48 | 46, 47 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍})) ∧ 𝐴 ∈ (◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)})) → (((𝐸 evalSub1 𝐹)‘𝑝)‘𝐴) = (0g‘𝐸)) |
| 49 | 34, 36, 48 | elrabd 3694 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍})) ∧ 𝐴 ∈ (◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)})) → 𝑝 ∈ {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)}) |
| 50 | | eldifsni 4790 |
. . . . . . . . 9
⊢ (𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍}) → 𝑝 ≠ 𝑍) |
| 51 | 35, 50 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍})) ∧ 𝐴 ∈ (◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)})) → 𝑝 ≠ 𝑍) |
| 52 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Poly1‘𝐸) = (Poly1‘𝐸) |
| 53 | | irngnminplynz.z |
. . . . . . . . . 10
⊢ 𝑍 =
(0g‘(Poly1‘𝐸)) |
| 54 | 52, 4, 7, 20, 3, 53 | ressply10g 33592 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 =
(0g‘(Poly1‘(𝐸 ↾s 𝐹)))) |
| 55 | 54 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍})) ∧ 𝐴 ∈ (◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)})) → 𝑍 =
(0g‘(Poly1‘(𝐸 ↾s 𝐹)))) |
| 56 | 51, 55 | neeqtrd 3010 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍})) ∧ 𝐴 ∈ (◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)})) → 𝑝 ≠
(0g‘(Poly1‘(𝐸 ↾s 𝐹)))) |
| 57 | | nelsn 4666 |
. . . . . . 7
⊢ (𝑝 ≠
(0g‘(Poly1‘(𝐸 ↾s 𝐹))) → ¬ 𝑝 ∈
{(0g‘(Poly1‘(𝐸 ↾s 𝐹)))}) |
| 58 | 56, 57 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍})) ∧ 𝐴 ∈ (◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)})) → ¬ 𝑝 ∈
{(0g‘(Poly1‘(𝐸 ↾s 𝐹)))}) |
| 59 | | nelne1 3039 |
. . . . . 6
⊢ ((𝑝 ∈ {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)} ∧ ¬ 𝑝 ∈
{(0g‘(Poly1‘(𝐸 ↾s 𝐹)))}) → {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)} ≠
{(0g‘(Poly1‘(𝐸 ↾s 𝐹)))}) |
| 60 | 49, 58, 59 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ 𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍})) ∧ 𝐴 ∈ (◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)})) → {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)} ≠
{(0g‘(Poly1‘(𝐸 ↾s 𝐹)))}) |
| 61 | 10, 53, 14, 12, 1 | irngnzply1 33741 |
. . . . . . 7
⊢ (𝜑 → (𝐸 IntgRing 𝐹) = ∪
𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍})(◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)})) |
| 62 | 16, 61 | eleqtrd 2843 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ∪
𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍})(◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)})) |
| 63 | | eliun 4995 |
. . . . . 6
⊢ (𝐴 ∈ ∪ 𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍})(◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)}) ↔ ∃𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍})𝐴 ∈ (◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)})) |
| 64 | 62, 63 | sylib 218 |
. . . . 5
⊢ (𝜑 → ∃𝑝 ∈ (dom (𝐸 evalSub1 𝐹) ∖ {𝑍})𝐴 ∈ (◡((𝐸 evalSub1 𝐹)‘𝑝) “ {(0g‘𝐸)})) |
| 65 | 60, 64 | r19.29a 3162 |
. . . 4
⊢ (𝜑 → {𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)} ≠
{(0g‘(Poly1‘(𝐸 ↾s 𝐹)))}) |
| 66 | 31, 65 | eqnetrrd 3009 |
. . 3
⊢ (𝜑 →
((RSpan‘(Poly1‘(𝐸 ↾s 𝐹)))‘{((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)})}) ≠
{(0g‘(Poly1‘(𝐸 ↾s 𝐹)))}) |
| 67 | | eqid 2737 |
. . . . 5
⊢
(0g‘(Poly1‘(𝐸 ↾s 𝐹))) =
(0g‘(Poly1‘(𝐸 ↾s 𝐹))) |
| 68 | 20, 67, 30 | pidlnzb 33450 |
. . . 4
⊢
(((Poly1‘(𝐸 ↾s 𝐹)) ∈ Ring ∧
((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)}) ∈
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) →
(((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)}) ≠
(0g‘(Poly1‘(𝐸 ↾s 𝐹))) ↔
((RSpan‘(Poly1‘(𝐸 ↾s 𝐹)))‘{((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)})}) ≠
{(0g‘(Poly1‘(𝐸 ↾s 𝐹)))})) |
| 69 | 68 | biimpar 477 |
. . 3
⊢
((((Poly1‘(𝐸 ↾s 𝐹)) ∈ Ring ∧
((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)}) ∈
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) ∧
((RSpan‘(Poly1‘(𝐸 ↾s 𝐹)))‘{((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)})}) ≠
{(0g‘(Poly1‘(𝐸 ↾s 𝐹)))}) →
((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)}) ≠
(0g‘(Poly1‘(𝐸 ↾s 𝐹)))) |
| 70 | 9, 29, 66, 69 | syl21anc 838 |
. 2
⊢ (𝜑 →
((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)}) ≠
(0g‘(Poly1‘(𝐸 ↾s 𝐹)))) |
| 71 | | irngnminplynz.m |
. . 3
⊢ 𝑀 = (𝐸 minPoly 𝐹) |
| 72 | 10, 7, 11, 12, 1, 17, 14, 18, 30, 26, 71 | minplyval 33748 |
. 2
⊢ (𝜑 → (𝑀‘𝐴) = ((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom (𝐸 evalSub1 𝐹) ∣ (((𝐸 evalSub1 𝐹)‘𝑞)‘𝐴) = (0g‘𝐸)})) |
| 73 | 70, 72, 54 | 3netr4d 3018 |
1
⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍) |