Step | Hyp | Ref
| Expression |
1 | | ply1annig1p.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) |
2 | | eqid 2731 |
. . . . . 6
⊢ (𝐸 ↾s 𝐹) = (𝐸 ↾s 𝐹) |
3 | 2 | sdrgdrng 20553 |
. . . . 5
⊢ (𝐹 ∈ (SubDRing‘𝐸) → (𝐸 ↾s 𝐹) ∈ DivRing) |
4 | 1, 3 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ DivRing) |
5 | 4 | drngringd 20512 |
. . 3
⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ Ring) |
6 | | minplyirredlem.2 |
. . 3
⊢ (𝜑 → 𝐻 ∈ (Base‘𝑃)) |
7 | | minplyirredlem.1 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ (Base‘𝑃)) |
8 | | minplyirredlem.5 |
. . . . . 6
⊢ (𝜑 → 𝐺 ≠ 𝑍) |
9 | | eqid 2731 |
. . . . . . 7
⊢ (
deg1 ‘(𝐸
↾s 𝐹)) = (
deg1 ‘(𝐸
↾s 𝐹)) |
10 | | ply1annig1p.p |
. . . . . . 7
⊢ 𝑃 =
(Poly1‘(𝐸
↾s 𝐹)) |
11 | | minplyirred.2 |
. . . . . . 7
⊢ 𝑍 = (0g‘𝑃) |
12 | | eqid 2731 |
. . . . . . 7
⊢
(Base‘𝑃) =
(Base‘𝑃) |
13 | 9, 10, 11, 12 | deg1nn0cl 25855 |
. . . . . 6
⊢ (((𝐸 ↾s 𝐹) ∈ Ring ∧ 𝐺 ∈ (Base‘𝑃) ∧ 𝐺 ≠ 𝑍) → (( deg1 ‘(𝐸 ↾s 𝐹))‘𝐺) ∈
ℕ0) |
14 | 5, 7, 8, 13 | syl3anc 1370 |
. . . . 5
⊢ (𝜑 → (( deg1
‘(𝐸
↾s 𝐹))‘𝐺) ∈
ℕ0) |
15 | 14 | nn0red 12540 |
. . . 4
⊢ (𝜑 → (( deg1
‘(𝐸
↾s 𝐹))‘𝐺) ∈ ℝ) |
16 | | minplyirredlem.6 |
. . . . . 6
⊢ (𝜑 → 𝐻 ≠ 𝑍) |
17 | 9, 10, 11, 12 | deg1nn0cl 25855 |
. . . . . 6
⊢ (((𝐸 ↾s 𝐹) ∈ Ring ∧ 𝐻 ∈ (Base‘𝑃) ∧ 𝐻 ≠ 𝑍) → (( deg1 ‘(𝐸 ↾s 𝐹))‘𝐻) ∈
ℕ0) |
18 | 5, 6, 16, 17 | syl3anc 1370 |
. . . . 5
⊢ (𝜑 → (( deg1
‘(𝐸
↾s 𝐹))‘𝐻) ∈
ℕ0) |
19 | 18 | nn0red 12540 |
. . . 4
⊢ (𝜑 → (( deg1
‘(𝐸
↾s 𝐹))‘𝐻) ∈ ℝ) |
20 | | eqid 2731 |
. . . . . 6
⊢
(RLReg‘(𝐸
↾s 𝐹)) =
(RLReg‘(𝐸
↾s 𝐹)) |
21 | | eqid 2731 |
. . . . . 6
⊢
(.r‘𝑃) = (.r‘𝑃) |
22 | | ply1annig1p.e |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ Field) |
23 | | fldsdrgfld 20561 |
. . . . . . . . . 10
⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐸)) → (𝐸 ↾s 𝐹) ∈ Field) |
24 | 22, 1, 23 | syl2anc 583 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ Field) |
25 | | fldidom 21127 |
. . . . . . . . 9
⊢ ((𝐸 ↾s 𝐹) ∈ Field → (𝐸 ↾s 𝐹) ∈ IDomn) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ IDomn) |
27 | 26 | idomdomd 32659 |
. . . . . . 7
⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ Domn) |
28 | | eqid 2731 |
. . . . . . . 8
⊢
(coe1‘𝐺) = (coe1‘𝐺) |
29 | 9, 10, 11, 12, 20, 28 | deg1ldgdomn 25861 |
. . . . . . 7
⊢ (((𝐸 ↾s 𝐹) ∈ Domn ∧ 𝐺 ∈ (Base‘𝑃) ∧ 𝐺 ≠ 𝑍) → ((coe1‘𝐺)‘(( deg1
‘(𝐸
↾s 𝐹))‘𝐺)) ∈ (RLReg‘(𝐸 ↾s 𝐹))) |
30 | 27, 7, 8, 29 | syl3anc 1370 |
. . . . . 6
⊢ (𝜑 →
((coe1‘𝐺)‘(( deg1 ‘(𝐸 ↾s 𝐹))‘𝐺)) ∈ (RLReg‘(𝐸 ↾s 𝐹))) |
31 | 9, 10, 20, 12, 21, 11, 5, 7, 8,
30, 6, 16 | deg1mul2 25881 |
. . . . 5
⊢ (𝜑 → (( deg1
‘(𝐸
↾s 𝐹))‘(𝐺(.r‘𝑃)𝐻)) = ((( deg1 ‘(𝐸 ↾s 𝐹))‘𝐺) + (( deg1 ‘(𝐸 ↾s 𝐹))‘𝐻))) |
32 | | minplyirredlem.3 |
. . . . . . . 8
⊢ (𝜑 → (𝐺(.r‘𝑃)𝐻) = (𝑀‘𝐴)) |
33 | | ply1annig1p.o |
. . . . . . . . 9
⊢ 𝑂 = (𝐸 evalSub1 𝐹) |
34 | | ply1annig1p.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐸) |
35 | | ply1annig1p.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝐵) |
36 | | eqid 2731 |
. . . . . . . . 9
⊢
(0g‘𝐸) = (0g‘𝐸) |
37 | | eqid 2731 |
. . . . . . . . 9
⊢ {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} |
38 | | eqid 2731 |
. . . . . . . . 9
⊢
(RSpan‘𝑃) =
(RSpan‘𝑃) |
39 | | eqid 2731 |
. . . . . . . . 9
⊢
(idlGen1p‘(𝐸 ↾s 𝐹)) = (idlGen1p‘(𝐸 ↾s 𝐹)) |
40 | | minplyirred.1 |
. . . . . . . . 9
⊢ 𝑀 = (𝐸 minPoly 𝐹) |
41 | 33, 10, 34, 22, 1, 35, 36, 37, 38, 39, 40 | minplyval 33070 |
. . . . . . . 8
⊢ (𝜑 → (𝑀‘𝐴) = ((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})) |
42 | 32, 41 | eqtrd 2771 |
. . . . . . 7
⊢ (𝜑 → (𝐺(.r‘𝑃)𝐻) = ((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})) |
43 | 42 | fveq2d 6895 |
. . . . . 6
⊢ (𝜑 → (( deg1
‘(𝐸
↾s 𝐹))‘(𝐺(.r‘𝑃)𝐻)) = (( deg1 ‘(𝐸 ↾s 𝐹))‘((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)}))) |
44 | 22 | fldcrngd 20517 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ CRing) |
45 | | sdrgsubrg 20554 |
. . . . . . . . 9
⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ∈ (SubRing‘𝐸)) |
46 | 1, 45 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸)) |
47 | 33, 10, 34, 44, 46, 35, 36, 37 | ply1annidl 33067 |
. . . . . . 7
⊢ (𝜑 → {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} ∈ (LIdeal‘𝑃)) |
48 | | fveq2 6891 |
. . . . . . . . . 10
⊢ (𝑞 = 𝐺 → (𝑂‘𝑞) = (𝑂‘𝐺)) |
49 | 48 | fveq1d 6893 |
. . . . . . . . 9
⊢ (𝑞 = 𝐺 → ((𝑂‘𝑞)‘𝐴) = ((𝑂‘𝐺)‘𝐴)) |
50 | 49 | eqeq1d 2733 |
. . . . . . . 8
⊢ (𝑞 = 𝐺 → (((𝑂‘𝑞)‘𝐴) = (0g‘𝐸) ↔ ((𝑂‘𝐺)‘𝐴) = (0g‘𝐸))) |
51 | 33, 10, 12, 44, 46 | evls1dm 32930 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝑂 = (Base‘𝑃)) |
52 | 7, 51 | eleqtrrd 2835 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ dom 𝑂) |
53 | | minplyirredlem.4 |
. . . . . . . 8
⊢ (𝜑 → ((𝑂‘𝐺)‘𝐴) = (0g‘𝐸)) |
54 | 50, 52, 53 | elrabd 3685 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)}) |
55 | 10, 39, 12, 4, 47, 9, 11, 54, 8 | ig1pmindeg 32962 |
. . . . . 6
⊢ (𝜑 → (( deg1
‘(𝐸
↾s 𝐹))‘((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})) ≤ (( deg1 ‘(𝐸 ↾s 𝐹))‘𝐺)) |
56 | 43, 55 | eqbrtrd 5170 |
. . . . 5
⊢ (𝜑 → (( deg1
‘(𝐸
↾s 𝐹))‘(𝐺(.r‘𝑃)𝐻)) ≤ (( deg1 ‘(𝐸 ↾s 𝐹))‘𝐺)) |
57 | 31, 56 | eqbrtrrd 5172 |
. . . 4
⊢ (𝜑 → ((( deg1
‘(𝐸
↾s 𝐹))‘𝐺) + (( deg1 ‘(𝐸 ↾s 𝐹))‘𝐻)) ≤ (( deg1 ‘(𝐸 ↾s 𝐹))‘𝐺)) |
58 | | leaddle0 11736 |
. . . . 5
⊢ ((((
deg1 ‘(𝐸
↾s 𝐹))‘𝐺) ∈ ℝ ∧ (( deg1
‘(𝐸
↾s 𝐹))‘𝐻) ∈ ℝ) → ((((
deg1 ‘(𝐸
↾s 𝐹))‘𝐺) + (( deg1 ‘(𝐸 ↾s 𝐹))‘𝐻)) ≤ (( deg1 ‘(𝐸 ↾s 𝐹))‘𝐺) ↔ (( deg1 ‘(𝐸 ↾s 𝐹))‘𝐻) ≤ 0)) |
59 | 58 | biimpa 476 |
. . . 4
⊢ (((((
deg1 ‘(𝐸
↾s 𝐹))‘𝐺) ∈ ℝ ∧ (( deg1
‘(𝐸
↾s 𝐹))‘𝐻) ∈ ℝ) ∧ ((( deg1
‘(𝐸
↾s 𝐹))‘𝐺) + (( deg1 ‘(𝐸 ↾s 𝐹))‘𝐻)) ≤ (( deg1 ‘(𝐸 ↾s 𝐹))‘𝐺)) → (( deg1 ‘(𝐸 ↾s 𝐹))‘𝐻) ≤ 0) |
60 | 15, 19, 57, 59 | syl21anc 835 |
. . 3
⊢ (𝜑 → (( deg1
‘(𝐸
↾s 𝐹))‘𝐻) ≤ 0) |
61 | | eqid 2731 |
. . . . 5
⊢
(algSc‘𝑃) =
(algSc‘𝑃) |
62 | 9, 10, 12, 61 | deg1le0 25878 |
. . . 4
⊢ (((𝐸 ↾s 𝐹) ∈ Ring ∧ 𝐻 ∈ (Base‘𝑃)) → ((( deg1
‘(𝐸
↾s 𝐹))‘𝐻) ≤ 0 ↔ 𝐻 = ((algSc‘𝑃)‘((coe1‘𝐻)‘0)))) |
63 | 62 | biimpa 476 |
. . 3
⊢ ((((𝐸 ↾s 𝐹) ∈ Ring ∧ 𝐻 ∈ (Base‘𝑃)) ∧ (( deg1
‘(𝐸
↾s 𝐹))‘𝐻) ≤ 0) → 𝐻 = ((algSc‘𝑃)‘((coe1‘𝐻)‘0))) |
64 | 5, 6, 60, 63 | syl21anc 835 |
. 2
⊢ (𝜑 → 𝐻 = ((algSc‘𝑃)‘((coe1‘𝐻)‘0))) |
65 | | eqid 2731 |
. . 3
⊢
(Base‘(𝐸
↾s 𝐹)) =
(Base‘(𝐸
↾s 𝐹)) |
66 | | eqid 2731 |
. . 3
⊢
(0g‘(𝐸 ↾s 𝐹)) = (0g‘(𝐸 ↾s 𝐹)) |
67 | | 0nn0 12494 |
. . . 4
⊢ 0 ∈
ℕ0 |
68 | | eqid 2731 |
. . . . 5
⊢
(coe1‘𝐻) = (coe1‘𝐻) |
69 | 68, 12, 10, 65 | coe1fvalcl 21968 |
. . . 4
⊢ ((𝐻 ∈ (Base‘𝑃) ∧ 0 ∈
ℕ0) → ((coe1‘𝐻)‘0) ∈ (Base‘(𝐸 ↾s 𝐹))) |
70 | 6, 67, 69 | sylancl 585 |
. . 3
⊢ (𝜑 →
((coe1‘𝐻)‘0) ∈ (Base‘(𝐸 ↾s 𝐹))) |
71 | 9, 10, 66, 12, 11, 5, 6, 60 | deg1le0eq0 32944 |
. . . . 5
⊢ (𝜑 → (𝐻 = 𝑍 ↔ ((coe1‘𝐻)‘0) =
(0g‘(𝐸
↾s 𝐹)))) |
72 | 71 | necon3bid 2984 |
. . . 4
⊢ (𝜑 → (𝐻 ≠ 𝑍 ↔ ((coe1‘𝐻)‘0) ≠
(0g‘(𝐸
↾s 𝐹)))) |
73 | 16, 72 | mpbid 231 |
. . 3
⊢ (𝜑 →
((coe1‘𝐻)‘0) ≠ (0g‘(𝐸 ↾s 𝐹))) |
74 | 10, 61, 65, 66, 24, 70, 73 | ply1asclunit 32943 |
. 2
⊢ (𝜑 → ((algSc‘𝑃)‘((coe1‘𝐻)‘0)) ∈
(Unit‘𝑃)) |
75 | 64, 74 | eqeltrd 2832 |
1
⊢ (𝜑 → 𝐻 ∈ (Unit‘𝑃)) |