Step | Hyp | Ref
| Expression |
1 | | ply1annig1p.o |
. . 3
⊢ 𝑂 = (𝐸 evalSub1 𝐹) |
2 | | ply1annig1p.p |
. . 3
⊢ 𝑃 =
(Poly1‘(𝐸
↾s 𝐹)) |
3 | | ply1annig1p.b |
. . 3
⊢ 𝐵 = (Base‘𝐸) |
4 | | ply1annig1p.e |
. . 3
⊢ (𝜑 → 𝐸 ∈ Field) |
5 | | ply1annig1p.f |
. . 3
⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) |
6 | | ply1annig1p.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝐵) |
7 | | eqid 2731 |
. . 3
⊢
(0g‘𝐸) = (0g‘𝐸) |
8 | | eqid 2731 |
. . 3
⊢ {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} |
9 | | eqid 2731 |
. . 3
⊢
(RSpan‘𝑃) =
(RSpan‘𝑃) |
10 | | eqid 2731 |
. . 3
⊢
(idlGen1p‘(𝐸 ↾s 𝐹)) = (idlGen1p‘(𝐸 ↾s 𝐹)) |
11 | | minplyirred.1 |
. . 3
⊢ 𝑀 = (𝐸 minPoly 𝐹) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | minplycl 33071 |
. 2
⊢ (𝜑 → (𝑀‘𝐴) ∈ (Base‘𝑃)) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | minplyval 33070 |
. . 3
⊢ (𝜑 → (𝑀‘𝐴) = ((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)})) |
14 | | eqid 2731 |
. . . 4
⊢
(Base‘𝑃) =
(Base‘𝑃) |
15 | | eqid 2731 |
. . . . . 6
⊢ (𝐸 ↾s 𝐹) = (𝐸 ↾s 𝐹) |
16 | 15 | sdrgdrng 20553 |
. . . . 5
⊢ (𝐹 ∈ (SubDRing‘𝐸) → (𝐸 ↾s 𝐹) ∈ DivRing) |
17 | 5, 16 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ DivRing) |
18 | 4 | fldcrngd 20517 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ CRing) |
19 | | sdrgsubrg 20554 |
. . . . . 6
⊢ (𝐹 ∈ (SubDRing‘𝐸) → 𝐹 ∈ (SubRing‘𝐸)) |
20 | 5, 19 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (SubRing‘𝐸)) |
21 | 1, 2, 3, 18, 20, 6, 7, 8 | ply1annidl 33067 |
. . . 4
⊢ (𝜑 → {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} ∈ (LIdeal‘𝑃)) |
22 | 4 | flddrngd 20516 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ DivRing) |
23 | | drngnzr 20524 |
. . . . . 6
⊢ (𝐸 ∈ DivRing → 𝐸 ∈ NzRing) |
24 | 22, 23 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ NzRing) |
25 | 1, 2, 3, 18, 20, 6, 7, 8, 14,
24 | ply1annnr 33068 |
. . . 4
⊢ (𝜑 → {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} ≠ (Base‘𝑃)) |
26 | 2, 10, 14, 17, 21, 25 | ig1pnunit 32961 |
. . 3
⊢ (𝜑 → ¬
((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)}) ∈ (Unit‘𝑃)) |
27 | 13, 26 | eqneltrd 2852 |
. 2
⊢ (𝜑 → ¬ (𝑀‘𝐴) ∈ (Unit‘𝑃)) |
28 | | fldidom 21127 |
. . . . . . . . . . 11
⊢ (𝐸 ∈ Field → 𝐸 ∈ IDomn) |
29 | 4, 28 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ IDomn) |
30 | 29 | idomdomd 32659 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ Domn) |
31 | 30 | ad3antrrr 727 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → 𝐸 ∈ Domn) |
32 | 18 | ad3antrrr 727 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → 𝐸 ∈ CRing) |
33 | 20 | ad3antrrr 727 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → 𝐹 ∈ (SubRing‘𝐸)) |
34 | 6 | ad3antrrr 727 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → 𝐴 ∈ 𝐵) |
35 | | simpllr 773 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → 𝑓 ∈ (Base‘𝑃)) |
36 | 1, 2, 3, 14, 32, 33, 34, 35 | evls1fvcl 33062 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → ((𝑂‘𝑓)‘𝐴) ∈ 𝐵) |
37 | | simplr 766 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → 𝑔 ∈ (Base‘𝑃)) |
38 | 1, 2, 3, 14, 32, 33, 34, 37 | evls1fvcl 33062 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → ((𝑂‘𝑔)‘𝐴) ∈ 𝐵) |
39 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) |
40 | 39 | fveq2d 6895 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → (𝑂‘(𝑓(.r‘𝑃)𝑔)) = (𝑂‘(𝑀‘𝐴))) |
41 | 40 | fveq1d 6893 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → ((𝑂‘(𝑓(.r‘𝑃)𝑔))‘𝐴) = ((𝑂‘(𝑀‘𝐴))‘𝐴)) |
42 | | eqid 2731 |
. . . . . . . . . 10
⊢
(.r‘𝑃) = (.r‘𝑃) |
43 | | eqid 2731 |
. . . . . . . . . 10
⊢
(.r‘𝐸) = (.r‘𝐸) |
44 | 1, 3, 2, 15, 14, 42, 43, 32, 33, 35, 37, 34 | evls1muld 32938 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → ((𝑂‘(𝑓(.r‘𝑃)𝑔))‘𝐴) = (((𝑂‘𝑓)‘𝐴)(.r‘𝐸)((𝑂‘𝑔)‘𝐴))) |
45 | | eqid 2731 |
. . . . . . . . . . . . . . 15
⊢
(LIdeal‘𝑃) =
(LIdeal‘𝑃) |
46 | 2, 10, 45 | ig1pcl 25942 |
. . . . . . . . . . . . . 14
⊢ (((𝐸 ↾s 𝐹) ∈ DivRing ∧ {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} ∈ (LIdeal‘𝑃)) → ((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)}) ∈ {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)}) |
47 | 17, 21, 46 | syl2anc 583 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((idlGen1p‘(𝐸 ↾s 𝐹))‘{𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)}) ∈ {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)}) |
48 | 13, 47 | eqeltrd 2832 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀‘𝐴) ∈ {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)}) |
49 | | fveq2 6891 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 = (𝑀‘𝐴) → (𝑂‘𝑞) = (𝑂‘(𝑀‘𝐴))) |
50 | 49 | fveq1d 6893 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = (𝑀‘𝐴) → ((𝑂‘𝑞)‘𝐴) = ((𝑂‘(𝑀‘𝐴))‘𝐴)) |
51 | 50 | eqeq1d 2733 |
. . . . . . . . . . . . 13
⊢ (𝑞 = (𝑀‘𝐴) → (((𝑂‘𝑞)‘𝐴) = (0g‘𝐸) ↔ ((𝑂‘(𝑀‘𝐴))‘𝐴) = (0g‘𝐸))) |
52 | 51 | elrab 3683 |
. . . . . . . . . . . 12
⊢ ((𝑀‘𝐴) ∈ {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = (0g‘𝐸)} ↔ ((𝑀‘𝐴) ∈ dom 𝑂 ∧ ((𝑂‘(𝑀‘𝐴))‘𝐴) = (0g‘𝐸))) |
53 | 48, 52 | sylib 217 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑀‘𝐴) ∈ dom 𝑂 ∧ ((𝑂‘(𝑀‘𝐴))‘𝐴) = (0g‘𝐸))) |
54 | 53 | simprd 495 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑂‘(𝑀‘𝐴))‘𝐴) = (0g‘𝐸)) |
55 | 54 | ad3antrrr 727 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → ((𝑂‘(𝑀‘𝐴))‘𝐴) = (0g‘𝐸)) |
56 | 41, 44, 55 | 3eqtr3d 2779 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → (((𝑂‘𝑓)‘𝐴)(.r‘𝐸)((𝑂‘𝑔)‘𝐴)) = (0g‘𝐸)) |
57 | 3, 43, 7 | domneq0 21117 |
. . . . . . . . 9
⊢ ((𝐸 ∈ Domn ∧ ((𝑂‘𝑓)‘𝐴) ∈ 𝐵 ∧ ((𝑂‘𝑔)‘𝐴) ∈ 𝐵) → ((((𝑂‘𝑓)‘𝐴)(.r‘𝐸)((𝑂‘𝑔)‘𝐴)) = (0g‘𝐸) ↔ (((𝑂‘𝑓)‘𝐴) = (0g‘𝐸) ∨ ((𝑂‘𝑔)‘𝐴) = (0g‘𝐸)))) |
58 | 57 | biimpa 476 |
. . . . . . . 8
⊢ (((𝐸 ∈ Domn ∧ ((𝑂‘𝑓)‘𝐴) ∈ 𝐵 ∧ ((𝑂‘𝑔)‘𝐴) ∈ 𝐵) ∧ (((𝑂‘𝑓)‘𝐴)(.r‘𝐸)((𝑂‘𝑔)‘𝐴)) = (0g‘𝐸)) → (((𝑂‘𝑓)‘𝐴) = (0g‘𝐸) ∨ ((𝑂‘𝑔)‘𝐴) = (0g‘𝐸))) |
59 | 31, 36, 38, 56, 58 | syl31anc 1372 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → (((𝑂‘𝑓)‘𝐴) = (0g‘𝐸) ∨ ((𝑂‘𝑔)‘𝐴) = (0g‘𝐸))) |
60 | 4 | ad4antr 729 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑓)‘𝐴) = (0g‘𝐸)) → 𝐸 ∈ Field) |
61 | 5 | ad4antr 729 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑓)‘𝐴) = (0g‘𝐸)) → 𝐹 ∈ (SubDRing‘𝐸)) |
62 | 34 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑓)‘𝐴) = (0g‘𝐸)) → 𝐴 ∈ 𝐵) |
63 | | minplyirred.2 |
. . . . . . . . . 10
⊢ 𝑍 = (0g‘𝑃) |
64 | | minplyirred.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍) |
65 | 64 | ad3antrrr 727 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → (𝑀‘𝐴) ≠ 𝑍) |
66 | 65 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑓)‘𝐴) = (0g‘𝐸)) → (𝑀‘𝐴) ≠ 𝑍) |
67 | 35 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑓)‘𝐴) = (0g‘𝐸)) → 𝑓 ∈ (Base‘𝑃)) |
68 | | simpllr 773 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑓)‘𝐴) = (0g‘𝐸)) → 𝑔 ∈ (Base‘𝑃)) |
69 | | simplr 766 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑓)‘𝐴) = (0g‘𝐸)) → (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) |
70 | | simpr 484 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑓)‘𝐴) = (0g‘𝐸)) → ((𝑂‘𝑓)‘𝐴) = (0g‘𝐸)) |
71 | | fldsdrgfld 20561 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ (SubDRing‘𝐸)) → (𝐸 ↾s 𝐹) ∈ Field) |
72 | 4, 5, 71 | syl2anc 583 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ Field) |
73 | | fldidom 21127 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸 ↾s 𝐹) ∈ Field → (𝐸 ↾s 𝐹) ∈ IDomn) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ IDomn) |
75 | 74 | idomdomd 32659 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ Domn) |
76 | 2 | ply1domn 25890 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐸 ↾s 𝐹) ∈ Domn → 𝑃 ∈ Domn) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑃 ∈ Domn) |
78 | 77 | ad3antrrr 727 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → 𝑃 ∈ Domn) |
79 | 39, 65 | eqnetrd 3007 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → (𝑓(.r‘𝑃)𝑔) ≠ 𝑍) |
80 | 14, 42, 63 | domneq0 21117 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Domn ∧ 𝑓 ∈ (Base‘𝑃) ∧ 𝑔 ∈ (Base‘𝑃)) → ((𝑓(.r‘𝑃)𝑔) = 𝑍 ↔ (𝑓 = 𝑍 ∨ 𝑔 = 𝑍))) |
81 | 80 | necon3abid 2976 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ Domn ∧ 𝑓 ∈ (Base‘𝑃) ∧ 𝑔 ∈ (Base‘𝑃)) → ((𝑓(.r‘𝑃)𝑔) ≠ 𝑍 ↔ ¬ (𝑓 = 𝑍 ∨ 𝑔 = 𝑍))) |
82 | 81 | biimpa 476 |
. . . . . . . . . . . . . 14
⊢ (((𝑃 ∈ Domn ∧ 𝑓 ∈ (Base‘𝑃) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) ≠ 𝑍) → ¬ (𝑓 = 𝑍 ∨ 𝑔 = 𝑍)) |
83 | 78, 35, 37, 79, 82 | syl31anc 1372 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → ¬ (𝑓 = 𝑍 ∨ 𝑔 = 𝑍)) |
84 | | neanior 3034 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ≠ 𝑍 ∧ 𝑔 ≠ 𝑍) ↔ ¬ (𝑓 = 𝑍 ∨ 𝑔 = 𝑍)) |
85 | 83, 84 | sylibr 233 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → (𝑓 ≠ 𝑍 ∧ 𝑔 ≠ 𝑍)) |
86 | 85 | simpld 494 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → 𝑓 ≠ 𝑍) |
87 | 86 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑓)‘𝐴) = (0g‘𝐸)) → 𝑓 ≠ 𝑍) |
88 | 85 | simprd 495 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → 𝑔 ≠ 𝑍) |
89 | 88 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑓)‘𝐴) = (0g‘𝐸)) → 𝑔 ≠ 𝑍) |
90 | 1, 2, 3, 60, 61, 62, 11, 63, 66, 67, 68, 69, 70, 87, 89 | minplyirredlem 33073 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑓)‘𝐴) = (0g‘𝐸)) → 𝑔 ∈ (Unit‘𝑃)) |
91 | 90 | ex 412 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → (((𝑂‘𝑓)‘𝐴) = (0g‘𝐸) → 𝑔 ∈ (Unit‘𝑃))) |
92 | 4 | ad4antr 729 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑔)‘𝐴) = (0g‘𝐸)) → 𝐸 ∈ Field) |
93 | 5 | ad4antr 729 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑔)‘𝐴) = (0g‘𝐸)) → 𝐹 ∈ (SubDRing‘𝐸)) |
94 | 34 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑔)‘𝐴) = (0g‘𝐸)) → 𝐴 ∈ 𝐵) |
95 | 65 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑔)‘𝐴) = (0g‘𝐸)) → (𝑀‘𝐴) ≠ 𝑍) |
96 | | simpllr 773 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑔)‘𝐴) = (0g‘𝐸)) → 𝑔 ∈ (Base‘𝑃)) |
97 | 35 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑔)‘𝐴) = (0g‘𝐸)) → 𝑓 ∈ (Base‘𝑃)) |
98 | 72 | fldcrngd 20517 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐸 ↾s 𝐹) ∈ CRing) |
99 | 2 | ply1crng 21954 |
. . . . . . . . . . . . . 14
⊢ ((𝐸 ↾s 𝐹) ∈ CRing → 𝑃 ∈ CRing) |
100 | 98, 99 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ CRing) |
101 | 100 | ad4antr 729 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑔)‘𝐴) = (0g‘𝐸)) → 𝑃 ∈ CRing) |
102 | 14, 42 | crngcom 20149 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ CRing ∧ 𝑔 ∈ (Base‘𝑃) ∧ 𝑓 ∈ (Base‘𝑃)) → (𝑔(.r‘𝑃)𝑓) = (𝑓(.r‘𝑃)𝑔)) |
103 | 101, 96, 97, 102 | syl3anc 1370 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑔)‘𝐴) = (0g‘𝐸)) → (𝑔(.r‘𝑃)𝑓) = (𝑓(.r‘𝑃)𝑔)) |
104 | | simplr 766 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑔)‘𝐴) = (0g‘𝐸)) → (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) |
105 | 103, 104 | eqtrd 2771 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑔)‘𝐴) = (0g‘𝐸)) → (𝑔(.r‘𝑃)𝑓) = (𝑀‘𝐴)) |
106 | | simpr 484 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑔)‘𝐴) = (0g‘𝐸)) → ((𝑂‘𝑔)‘𝐴) = (0g‘𝐸)) |
107 | 88 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑔)‘𝐴) = (0g‘𝐸)) → 𝑔 ≠ 𝑍) |
108 | 86 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑔)‘𝐴) = (0g‘𝐸)) → 𝑓 ≠ 𝑍) |
109 | 1, 2, 3, 92, 93, 94, 11, 63, 95, 96, 97, 105, 106, 107, 108 | minplyirredlem 33073 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) ∧ ((𝑂‘𝑔)‘𝐴) = (0g‘𝐸)) → 𝑓 ∈ (Unit‘𝑃)) |
110 | 109 | ex 412 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → (((𝑂‘𝑔)‘𝐴) = (0g‘𝐸) → 𝑓 ∈ (Unit‘𝑃))) |
111 | 91, 110 | orim12d 962 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → ((((𝑂‘𝑓)‘𝐴) = (0g‘𝐸) ∨ ((𝑂‘𝑔)‘𝐴) = (0g‘𝐸)) → (𝑔 ∈ (Unit‘𝑃) ∨ 𝑓 ∈ (Unit‘𝑃)))) |
112 | 59, 111 | mpd 15 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → (𝑔 ∈ (Unit‘𝑃) ∨ 𝑓 ∈ (Unit‘𝑃))) |
113 | 112 | orcomd 868 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) ∧ (𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴)) → (𝑓 ∈ (Unit‘𝑃) ∨ 𝑔 ∈ (Unit‘𝑃))) |
114 | 113 | ex 412 |
. . . 4
⊢ (((𝜑 ∧ 𝑓 ∈ (Base‘𝑃)) ∧ 𝑔 ∈ (Base‘𝑃)) → ((𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴) → (𝑓 ∈ (Unit‘𝑃) ∨ 𝑔 ∈ (Unit‘𝑃)))) |
115 | 114 | anasss 466 |
. . 3
⊢ ((𝜑 ∧ (𝑓 ∈ (Base‘𝑃) ∧ 𝑔 ∈ (Base‘𝑃))) → ((𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴) → (𝑓 ∈ (Unit‘𝑃) ∨ 𝑔 ∈ (Unit‘𝑃)))) |
116 | 115 | ralrimivva 3199 |
. 2
⊢ (𝜑 → ∀𝑓 ∈ (Base‘𝑃)∀𝑔 ∈ (Base‘𝑃)((𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴) → (𝑓 ∈ (Unit‘𝑃) ∨ 𝑔 ∈ (Unit‘𝑃)))) |
117 | | eqid 2731 |
. . 3
⊢
(Unit‘𝑃) =
(Unit‘𝑃) |
118 | | eqid 2731 |
. . 3
⊢
(Irred‘𝑃) =
(Irred‘𝑃) |
119 | 14, 117, 118, 42 | isirred2 20316 |
. 2
⊢ ((𝑀‘𝐴) ∈ (Irred‘𝑃) ↔ ((𝑀‘𝐴) ∈ (Base‘𝑃) ∧ ¬ (𝑀‘𝐴) ∈ (Unit‘𝑃) ∧ ∀𝑓 ∈ (Base‘𝑃)∀𝑔 ∈ (Base‘𝑃)((𝑓(.r‘𝑃)𝑔) = (𝑀‘𝐴) → (𝑓 ∈ (Unit‘𝑃) ∨ 𝑔 ∈ (Unit‘𝑃))))) |
120 | 12, 27, 116, 119 | syl3anbrc 1342 |
1
⊢ (𝜑 → (𝑀‘𝐴) ∈ (Irred‘𝑃)) |