Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . . 6
⊢
(Poly1‘𝐸) = (Poly1‘𝐸) |
2 | | eqid 2737 |
. . . . . 6
⊢ (𝐸 ↾s 𝐹) = (𝐸 ↾s 𝐹) |
3 | | eqid 2737 |
. . . . . 6
⊢
(Poly1‘(𝐸 ↾s 𝐹)) = (Poly1‘(𝐸 ↾s 𝐹)) |
4 | | eqid 2737 |
. . . . . 6
⊢
(Base‘(Poly1‘(𝐸 ↾s 𝐹))) =
(Base‘(Poly1‘(𝐸 ↾s 𝐹))) |
5 | | algnbval.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) |
6 | 5 | ad2antrr 724 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → 𝐹 ∈ (SubDRing‘𝐸)) |
7 | | issdrg 20213 |
. . . . . . . 8
⊢ (𝐹 ∈ (SubDRing‘𝐸) ↔ (𝐸 ∈ DivRing ∧ 𝐹 ∈ (SubRing‘𝐸) ∧ (𝐸 ↾s 𝐹) ∈ DivRing)) |
8 | 7 | simp2bi 1146 |
. . . . . . 7
⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ∈ (SubRing‘𝐸)) |
9 | 6, 8 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → 𝐹 ∈ (SubRing‘𝐸)) |
10 | | eqid 2737 |
. . . . . 6
⊢
(Monic1p‘𝐸) = (Monic1p‘𝐸) |
11 | | eqid 2737 |
. . . . . 6
⊢
(Monic1p‘(𝐸 ↾s 𝐹)) = (Monic1p‘(𝐸 ↾s 𝐹)) |
12 | 1, 2, 3, 4, 9, 10,
11 | ressply1mon1p 32094 |
. . . . 5
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) →
(Monic1p‘(𝐸 ↾s 𝐹)) =
((Base‘(Poly1‘(𝐸 ↾s 𝐹))) ∩ (Monic1p‘𝐸))) |
13 | | inss2 4187 |
. . . . 5
⊢
((Base‘(Poly1‘(𝐸 ↾s 𝐹))) ∩ (Monic1p‘𝐸)) ⊆
(Monic1p‘𝐸) |
14 | 12, 13 | eqsstrdi 3996 |
. . . 4
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) →
(Monic1p‘(𝐸 ↾s 𝐹)) ⊆ (Monic1p‘𝐸)) |
15 | 7 | simp3bi 1147 |
. . . . . . . 8
⊢ (𝐹 ∈ (SubDRing‘𝐸) → (𝐸 ↾s 𝐹) ∈ DivRing) |
16 | 5, 15 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ DivRing) |
17 | 16 | ad2antrr 724 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → (𝐸 ↾s 𝐹) ∈
DivRing) |
18 | 17 | drngringd 20145 |
. . . . 5
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → (𝐸 ↾s 𝐹) ∈ Ring) |
19 | | simplr 767 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) |
20 | 19 | eldifad 3920 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → 𝑞 ∈ dom 𝑂) |
21 | | algnbval.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 ∈ Field) |
22 | 21 | fldcrngd 20149 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ CRing) |
23 | 5, 8 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸)) |
24 | | algnbval.o |
. . . . . . . . . . . 12
⊢ 𝑂 = (𝐸 evalSub1 𝐹) |
25 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘𝐸) =
(Base‘𝐸) |
26 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝐸 ↑s
(Base‘𝐸)) = (𝐸 ↑s
(Base‘𝐸)) |
27 | 24, 25, 26, 2, 3 | evls1rhm 21639 |
. . . . . . . . . . 11
⊢ ((𝐸 ∈ CRing ∧ 𝐹 ∈ (SubRing‘𝐸)) → 𝑂 ∈ ((Poly1‘(𝐸 ↾s 𝐹)) RingHom (𝐸 ↑s (Base‘𝐸)))) |
28 | 22, 23, 27 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑂 ∈ ((Poly1‘(𝐸 ↾s 𝐹)) RingHom (𝐸 ↑s (Base‘𝐸)))) |
29 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘(𝐸
↑s (Base‘𝐸))) = (Base‘(𝐸 ↑s (Base‘𝐸))) |
30 | 4, 29 | rhmf 20110 |
. . . . . . . . . 10
⊢ (𝑂 ∈
((Poly1‘(𝐸
↾s 𝐹))
RingHom (𝐸
↑s (Base‘𝐸))) → 𝑂:(Base‘(Poly1‘(𝐸 ↾s 𝐹)))⟶(Base‘(𝐸 ↑s
(Base‘𝐸)))) |
31 | 28, 30 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑂:(Base‘(Poly1‘(𝐸 ↾s 𝐹)))⟶(Base‘(𝐸 ↑s
(Base‘𝐸)))) |
32 | 31 | fdmd 6676 |
. . . . . . . 8
⊢ (𝜑 → dom 𝑂 =
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) |
33 | 32 | ad2antrr 724 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → dom 𝑂 =
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) |
34 | 20, 33 | eleqtrd 2840 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → 𝑞 ∈
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) |
35 | | eldifsni 4748 |
. . . . . . . 8
⊢ (𝑞 ∈ (dom 𝑂 ∖ {𝑍}) → 𝑞 ≠ 𝑍) |
36 | 35 | ad2antlr 725 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → 𝑞 ≠ 𝑍) |
37 | | algnbval.z |
. . . . . . . . 9
⊢ 𝑍 =
(0g‘(Poly1‘𝐸)) |
38 | 1, 2, 3, 4, 23, 37 | ressply10g 32093 |
. . . . . . . 8
⊢ (𝜑 → 𝑍 =
(0g‘(Poly1‘(𝐸 ↾s 𝐹)))) |
39 | 38 | ad2antrr 724 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → 𝑍 =
(0g‘(Poly1‘(𝐸 ↾s 𝐹)))) |
40 | 36, 39 | neeqtrd 3011 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → 𝑞 ≠
(0g‘(Poly1‘(𝐸 ↾s 𝐹)))) |
41 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘(Poly1‘(𝐸 ↾s 𝐹))) =
(0g‘(Poly1‘(𝐸 ↾s 𝐹))) |
42 | | eqid 2737 |
. . . . . . 7
⊢
(Unic1p‘(𝐸 ↾s 𝐹)) = (Unic1p‘(𝐸 ↾s 𝐹)) |
43 | 3, 4, 41, 42 | drnguc1p 25486 |
. . . . . 6
⊢ (((𝐸 ↾s 𝐹) ∈ DivRing ∧ 𝑞 ∈
(Base‘(Poly1‘(𝐸 ↾s 𝐹))) ∧ 𝑞 ≠
(0g‘(Poly1‘(𝐸 ↾s 𝐹)))) → 𝑞 ∈ (Unic1p‘(𝐸 ↾s 𝐹))) |
44 | 17, 34, 40, 43 | syl3anc 1371 |
. . . . 5
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → 𝑞 ∈
(Unic1p‘(𝐸
↾s 𝐹))) |
45 | | eqid 2737 |
. . . . . 6
⊢
(.r‘(Poly1‘(𝐸 ↾s 𝐹))) =
(.r‘(Poly1‘(𝐸 ↾s 𝐹))) |
46 | | eqid 2737 |
. . . . . 6
⊢
(algSc‘(Poly1‘(𝐸 ↾s 𝐹))) =
(algSc‘(Poly1‘(𝐸 ↾s 𝐹))) |
47 | | eqid 2737 |
. . . . . 6
⊢ (
deg1 ‘(𝐸
↾s 𝐹)) = (
deg1 ‘(𝐸
↾s 𝐹)) |
48 | | eqid 2737 |
. . . . . 6
⊢
(invr‘(𝐸 ↾s 𝐹)) = (invr‘(𝐸 ↾s 𝐹)) |
49 | 42, 11, 3, 45, 46, 47, 48 | uc1pmon1p 25467 |
. . . . 5
⊢ (((𝐸 ↾s 𝐹) ∈ Ring ∧ 𝑞 ∈
(Unic1p‘(𝐸
↾s 𝐹)))
→ (((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1
‘(𝐸
↾s 𝐹))‘𝑞))))(.r‘(Poly1‘(𝐸 ↾s 𝐹)))𝑞) ∈ (Monic1p‘(𝐸 ↾s 𝐹))) |
50 | 18, 44, 49 | syl2anc 584 |
. . . 4
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) →
(((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1
‘(𝐸
↾s 𝐹))‘𝑞))))(.r‘(Poly1‘(𝐸 ↾s 𝐹)))𝑞) ∈ (Monic1p‘(𝐸 ↾s 𝐹))) |
51 | 14, 50 | sseldd 3943 |
. . 3
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) →
(((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1
‘(𝐸
↾s 𝐹))‘𝑞))))(.r‘(Poly1‘(𝐸 ↾s 𝐹)))𝑞) ∈ (Monic1p‘𝐸)) |
52 | | simpr 485 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) ∧ 𝑝 =
(((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1
‘(𝐸
↾s 𝐹))‘𝑞))))(.r‘(Poly1‘(𝐸 ↾s 𝐹)))𝑞)) → 𝑝 = (((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1 ‘(𝐸 ↾s 𝐹))‘𝑞))))(.r‘(Poly1‘(𝐸 ↾s 𝐹)))𝑞)) |
53 | 52 | fveq2d 6843 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) ∧ 𝑝 =
(((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1
‘(𝐸
↾s 𝐹))‘𝑞))))(.r‘(Poly1‘(𝐸 ↾s 𝐹)))𝑞)) → (𝑂‘𝑝) = (𝑂‘(((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1 ‘(𝐸 ↾s 𝐹))‘𝑞))))(.r‘(Poly1‘(𝐸 ↾s 𝐹)))𝑞))) |
54 | 53 | fveq1d 6841 |
. . . 4
⊢ ((((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) ∧ 𝑝 =
(((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1
‘(𝐸
↾s 𝐹))‘𝑞))))(.r‘(Poly1‘(𝐸 ↾s 𝐹)))𝑞)) → ((𝑂‘𝑝)‘𝑋) = ((𝑂‘(((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1 ‘(𝐸 ↾s 𝐹))‘𝑞))))(.r‘(Poly1‘(𝐸 ↾s 𝐹)))𝑞))‘𝑋)) |
55 | 54 | eqeq1d 2739 |
. . 3
⊢ ((((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) ∧ 𝑝 =
(((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1
‘(𝐸
↾s 𝐹))‘𝑞))))(.r‘(Poly1‘(𝐸 ↾s 𝐹)))𝑞)) → (((𝑂‘𝑝)‘𝑋) = 0 ↔ ((𝑂‘(((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1 ‘(𝐸 ↾s 𝐹))‘𝑞))))(.r‘(Poly1‘(𝐸 ↾s 𝐹)))𝑞))‘𝑋) = 0 )) |
56 | | eqid 2737 |
. . . . 5
⊢
(.r‘𝐸) = (.r‘𝐸) |
57 | 22 | ad2antrr 724 |
. . . . 5
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → 𝐸 ∈ CRing) |
58 | | eqid 2737 |
. . . . . . 7
⊢
(Scalar‘(Poly1‘(𝐸 ↾s 𝐹))) =
(Scalar‘(Poly1‘(𝐸 ↾s 𝐹))) |
59 | | fldsdrgfld 20217 |
. . . . . . . . . . . 12
⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐸)) → (𝐸 ↾s 𝐹) ∈ Field) |
60 | 21, 5, 59 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ Field) |
61 | 60 | fldcrngd 20149 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ CRing) |
62 | 3 | ply1assa 21521 |
. . . . . . . . . 10
⊢ ((𝐸 ↾s 𝐹) ∈ CRing →
(Poly1‘(𝐸
↾s 𝐹))
∈ AssAlg) |
63 | 61, 62 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 →
(Poly1‘(𝐸
↾s 𝐹))
∈ AssAlg) |
64 | 63 | ad2antrr 724 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) →
(Poly1‘(𝐸
↾s 𝐹))
∈ AssAlg) |
65 | | assaring 21219 |
. . . . . . . 8
⊢
((Poly1‘(𝐸 ↾s 𝐹)) ∈ AssAlg →
(Poly1‘(𝐸
↾s 𝐹))
∈ Ring) |
66 | 64, 65 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) →
(Poly1‘(𝐸
↾s 𝐹))
∈ Ring) |
67 | 61 | crngringd 19930 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ Ring) |
68 | 3 | ply1lmod 21574 |
. . . . . . . . 9
⊢ ((𝐸 ↾s 𝐹) ∈ Ring →
(Poly1‘(𝐸
↾s 𝐹))
∈ LMod) |
69 | 67, 68 | syl 17 |
. . . . . . . 8
⊢ (𝜑 →
(Poly1‘(𝐸
↾s 𝐹))
∈ LMod) |
70 | 69 | ad2antrr 724 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) →
(Poly1‘(𝐸
↾s 𝐹))
∈ LMod) |
71 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(Scalar‘(Poly1‘(𝐸 ↾s 𝐹)))) =
(Base‘(Scalar‘(Poly1‘(𝐸 ↾s 𝐹)))) |
72 | 46, 58, 66, 70, 71, 4 | asclf 21237 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) →
(algSc‘(Poly1‘(𝐸 ↾s 𝐹))):(Base‘(Scalar‘(Poly1‘(𝐸 ↾s 𝐹))))⟶(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) |
73 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘(𝐸
↾s 𝐹)) =
(Base‘(𝐸
↾s 𝐹)) |
74 | | eqid 2737 |
. . . . . . . 8
⊢
(0g‘(𝐸 ↾s 𝐹)) = (0g‘(𝐸 ↾s 𝐹)) |
75 | 47, 3, 41, 4 | deg1nn0cl 25404 |
. . . . . . . . . 10
⊢ (((𝐸 ↾s 𝐹) ∈ Ring ∧ 𝑞 ∈
(Base‘(Poly1‘(𝐸 ↾s 𝐹))) ∧ 𝑞 ≠
(0g‘(Poly1‘(𝐸 ↾s 𝐹)))) → (( deg1 ‘(𝐸 ↾s 𝐹))‘𝑞) ∈
ℕ0) |
76 | 18, 34, 40, 75 | syl3anc 1371 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → ((
deg1 ‘(𝐸
↾s 𝐹))‘𝑞) ∈
ℕ0) |
77 | | eqid 2737 |
. . . . . . . . . 10
⊢
(coe1‘𝑞) = (coe1‘𝑞) |
78 | 77, 4, 3, 73 | coe1fvalcl 21534 |
. . . . . . . . 9
⊢ ((𝑞 ∈
(Base‘(Poly1‘(𝐸 ↾s 𝐹))) ∧ (( deg1 ‘(𝐸 ↾s 𝐹))‘𝑞) ∈ ℕ0) →
((coe1‘𝑞)‘(( deg1 ‘(𝐸 ↾s 𝐹))‘𝑞)) ∈ (Base‘(𝐸 ↾s 𝐹))) |
79 | 34, 76, 78 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) →
((coe1‘𝑞)‘(( deg1 ‘(𝐸 ↾s 𝐹))‘𝑞)) ∈ (Base‘(𝐸 ↾s 𝐹))) |
80 | 47, 3, 41, 4, 74, 77 | deg1ldg 25408 |
. . . . . . . . 9
⊢ (((𝐸 ↾s 𝐹) ∈ Ring ∧ 𝑞 ∈
(Base‘(Poly1‘(𝐸 ↾s 𝐹))) ∧ 𝑞 ≠
(0g‘(Poly1‘(𝐸 ↾s 𝐹)))) → ((coe1‘𝑞)‘(( deg1
‘(𝐸
↾s 𝐹))‘𝑞)) ≠ (0g‘(𝐸 ↾s 𝐹))) |
81 | 18, 34, 40, 80 | syl3anc 1371 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) →
((coe1‘𝑞)‘(( deg1 ‘(𝐸 ↾s 𝐹))‘𝑞)) ≠ (0g‘(𝐸 ↾s 𝐹))) |
82 | 73, 74, 48, 17, 79, 81 | drnginvrcld 20159 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) →
((invr‘(𝐸
↾s 𝐹))‘((coe1‘𝑞)‘(( deg1
‘(𝐸
↾s 𝐹))‘𝑞))) ∈ (Base‘(𝐸 ↾s 𝐹))) |
83 | 3 | ply1sca 21575 |
. . . . . . . . . 10
⊢ ((𝐸 ↾s 𝐹) ∈ Field → (𝐸 ↾s 𝐹) =
(Scalar‘(Poly1‘(𝐸 ↾s 𝐹)))) |
84 | 60, 83 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 ↾s 𝐹) =
(Scalar‘(Poly1‘(𝐸 ↾s 𝐹)))) |
85 | 84 | fveq2d 6843 |
. . . . . . . 8
⊢ (𝜑 → (Base‘(𝐸 ↾s 𝐹)) =
(Base‘(Scalar‘(Poly1‘(𝐸 ↾s 𝐹))))) |
86 | 85 | ad2antrr 724 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) →
(Base‘(𝐸
↾s 𝐹)) =
(Base‘(Scalar‘(Poly1‘(𝐸 ↾s 𝐹))))) |
87 | 82, 86 | eleqtrd 2840 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) →
((invr‘(𝐸
↾s 𝐹))‘((coe1‘𝑞)‘(( deg1
‘(𝐸
↾s 𝐹))‘𝑞))) ∈
(Base‘(Scalar‘(Poly1‘(𝐸 ↾s 𝐹))))) |
88 | 72, 87 | ffvelcdmd 7032 |
. . . . 5
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) →
((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1
‘(𝐸
↾s 𝐹))‘𝑞)))) ∈
(Base‘(Poly1‘(𝐸 ↾s 𝐹)))) |
89 | | minplyeulem.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ (𝐸 AlgNb 𝐹)) |
90 | | algnbval.1 |
. . . . . . . . 9
⊢ 0 =
(0g‘𝐸) |
91 | 24, 37, 90, 21, 5, 25 | isalgnb 32175 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 ∈ (𝐸 AlgNb 𝐹) ↔ (𝑋 ∈ (Base‘𝐸) ∧ ∃𝑞 ∈ (dom 𝑂 ∖ {𝑍})((𝑂‘𝑞)‘𝑋) = 0 ))) |
92 | 89, 91 | mpbid 231 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ∈ (Base‘𝐸) ∧ ∃𝑞 ∈ (dom 𝑂 ∖ {𝑍})((𝑂‘𝑞)‘𝑋) = 0 )) |
93 | 92 | simpld 495 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ (Base‘𝐸)) |
94 | 93 | ad2antrr 724 |
. . . . 5
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → 𝑋 ∈ (Base‘𝐸)) |
95 | 24, 25, 3, 2, 4, 45,
56, 57, 9, 88, 34, 94 | evls1muld 32090 |
. . . 4
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → ((𝑂‘(((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1 ‘(𝐸 ↾s 𝐹))‘𝑞))))(.r‘(Poly1‘(𝐸 ↾s 𝐹)))𝑞))‘𝑋) = (((𝑂‘((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1 ‘(𝐸 ↾s 𝐹))‘𝑞)))))‘𝑋)(.r‘𝐸)((𝑂‘𝑞)‘𝑋))) |
96 | | simpr 485 |
. . . . 5
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → ((𝑂‘𝑞)‘𝑋) = 0 ) |
97 | 96 | oveq2d 7367 |
. . . 4
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → (((𝑂‘((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1 ‘(𝐸 ↾s 𝐹))‘𝑞)))))‘𝑋)(.r‘𝐸)((𝑂‘𝑞)‘𝑋)) = (((𝑂‘((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1 ‘(𝐸 ↾s 𝐹))‘𝑞)))))‘𝑋)(.r‘𝐸) 0 )) |
98 | 22 | crngringd 19930 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ Ring) |
99 | 98 | ad2antrr 724 |
. . . . 5
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → 𝐸 ∈ Ring) |
100 | 21 | ad2antrr 724 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → 𝐸 ∈ Field) |
101 | | fvexd 6854 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → (Base‘𝐸) ∈ V) |
102 | 28 | ad2antrr 724 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → 𝑂 ∈ ((Poly1‘(𝐸 ↾s 𝐹)) RingHom (𝐸 ↑s (Base‘𝐸)))) |
103 | 102, 30 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → 𝑂:(Base‘(Poly1‘(𝐸 ↾s 𝐹)))⟶(Base‘(𝐸 ↑s
(Base‘𝐸)))) |
104 | 103, 88 | ffvelcdmd 7032 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → (𝑂‘((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1 ‘(𝐸 ↾s 𝐹))‘𝑞))))) ∈ (Base‘(𝐸 ↑s (Base‘𝐸)))) |
105 | 26, 25, 29, 100, 101, 104 | pwselbas 17330 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → (𝑂‘((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1 ‘(𝐸 ↾s 𝐹))‘𝑞))))):(Base‘𝐸)⟶(Base‘𝐸)) |
106 | 105, 94 | ffvelcdmd 7032 |
. . . . 5
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → ((𝑂‘((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1 ‘(𝐸 ↾s 𝐹))‘𝑞)))))‘𝑋) ∈ (Base‘𝐸)) |
107 | 25, 56, 90 | ringrz 19964 |
. . . . 5
⊢ ((𝐸 ∈ Ring ∧ ((𝑂‘((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1 ‘(𝐸 ↾s 𝐹))‘𝑞)))))‘𝑋) ∈ (Base‘𝐸)) → (((𝑂‘((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1 ‘(𝐸 ↾s 𝐹))‘𝑞)))))‘𝑋)(.r‘𝐸) 0 ) = 0 ) |
108 | 99, 106, 107 | syl2anc 584 |
. . . 4
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → (((𝑂‘((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1 ‘(𝐸 ↾s 𝐹))‘𝑞)))))‘𝑋)(.r‘𝐸) 0 ) = 0 ) |
109 | 95, 97, 108 | 3eqtrd 2781 |
. . 3
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → ((𝑂‘(((algSc‘(Poly1‘(𝐸 ↾s 𝐹)))‘((invr‘(𝐸 ↾s 𝐹))‘((coe1‘𝑞)‘(( deg1 ‘(𝐸 ↾s 𝐹))‘𝑞))))(.r‘(Poly1‘(𝐸 ↾s 𝐹)))𝑞))‘𝑋) = 0 ) |
110 | 51, 55, 109 | rspcedvd 3581 |
. 2
⊢ (((𝜑 ∧ 𝑞 ∈ (dom 𝑂 ∖ {𝑍})) ∧ ((𝑂‘𝑞)‘𝑋) = 0 ) → ∃𝑝 ∈
(Monic1p‘𝐸)((𝑂‘𝑝)‘𝑋) = 0 ) |
111 | 92 | simprd 496 |
. 2
⊢ (𝜑 → ∃𝑞 ∈ (dom 𝑂 ∖ {𝑍})((𝑂‘𝑞)‘𝑋) = 0 ) |
112 | 110, 111 | r19.29a 3157 |
1
⊢ (𝜑 → ∃𝑝 ∈ (Monic1p‘𝐸)((𝑂‘𝑝)‘𝑋) = 0 ) |