| Step | Hyp | Ref
| Expression |
| 1 | | ply1dg3rt0irred.q |
. . 3
⊢ (𝜑 → 𝑄 ∈ 𝐵) |
| 2 | | ply1dg3rt0irred.2 |
. . . . 5
⊢ (𝜑 → (𝐷‘𝑄) = 3) |
| 3 | | 3ne0 12372 |
. . . . . 6
⊢ 3 ≠
0 |
| 4 | 3 | a1i 11 |
. . . . 5
⊢ (𝜑 → 3 ≠ 0) |
| 5 | 2, 4 | eqnetrd 3008 |
. . . 4
⊢ (𝜑 → (𝐷‘𝑄) ≠ 0) |
| 6 | | ply1dg3rt0irred.p |
. . . . . 6
⊢ 𝑃 = (Poly1‘𝐹) |
| 7 | | eqid 2737 |
. . . . . 6
⊢
(algSc‘𝑃) =
(algSc‘𝑃) |
| 8 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐹) =
(Base‘𝐹) |
| 9 | | ply1dg3rt0irred.z |
. . . . . 6
⊢ 0 =
(0g‘𝐹) |
| 10 | | ply1dg3rt0irred.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ Field) |
| 11 | | ply1dg3rt0irred.d |
. . . . . 6
⊢ 𝐷 = (deg1‘𝐹) |
| 12 | | ply1dg3rt0irred.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑃) |
| 13 | 1, 12 | eleqtrdi 2851 |
. . . . . 6
⊢ (𝜑 → 𝑄 ∈ (Base‘𝑃)) |
| 14 | 6, 7, 8, 9, 10, 11, 13 | ply1unit 33600 |
. . . . 5
⊢ (𝜑 → (𝑄 ∈ (Unit‘𝑃) ↔ (𝐷‘𝑄) = 0)) |
| 15 | 14 | necon3bbid 2978 |
. . . 4
⊢ (𝜑 → (¬ 𝑄 ∈ (Unit‘𝑃) ↔ (𝐷‘𝑄) ≠ 0)) |
| 16 | 5, 15 | mpbird 257 |
. . 3
⊢ (𝜑 → ¬ 𝑄 ∈ (Unit‘𝑃)) |
| 17 | 1, 16 | eldifd 3962 |
. 2
⊢ (𝜑 → 𝑄 ∈ (𝐵 ∖ (Unit‘𝑃))) |
| 18 | 10 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → 𝐹 ∈ Field) |
| 19 | | simpllr 776 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) |
| 20 | 19 | eldifad 3963 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → 𝑝 ∈ 𝐵) |
| 21 | 20, 12 | eleqtrdi 2851 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → 𝑝 ∈ (Base‘𝑃)) |
| 22 | 6, 7, 8, 9, 18, 11, 21 | ply1unit 33600 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (𝑝 ∈ (Unit‘𝑃) ↔ (𝐷‘𝑝) = 0)) |
| 23 | 22 | biimpar 477 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 0) → 𝑝 ∈ (Unit‘𝑃)) |
| 24 | 19 | eldifbd 3964 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → ¬ 𝑝 ∈ (Unit‘𝑃)) |
| 25 | 24 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 0) → ¬ 𝑝 ∈ (Unit‘𝑃)) |
| 26 | 23, 25 | pm2.21fal 1562 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 0) → ⊥) |
| 27 | 26 | adantlr 715 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) ∈ {0, 1}) ∧ (𝐷‘𝑝) = 0) → ⊥) |
| 28 | | ply1dg3rt0irred.o |
. . . . . . . . . . . . . . 15
⊢ 𝑂 = (eval1‘𝐹) |
| 29 | 10 | fldcrngd 20742 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹 ∈ CRing) |
| 30 | 29 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → 𝐹 ∈ CRing) |
| 31 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) |
| 32 | 31 | eldifad 3963 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → 𝑞 ∈ 𝐵) |
| 33 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(.r‘𝑃) = (.r‘𝑃) |
| 34 | 6, 12, 28, 11, 9, 30, 20, 32, 33 | ply1mulrtss 33606 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (◡(𝑂‘𝑝) “ { 0 }) ⊆ (◡(𝑂‘(𝑝(.r‘𝑃)𝑞)) “ { 0 })) |
| 35 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (𝑝(.r‘𝑃)𝑞) = 𝑄) |
| 36 | 35 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (𝑂‘(𝑝(.r‘𝑃)𝑞)) = (𝑂‘𝑄)) |
| 37 | 36 | cnveqd 5886 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → ◡(𝑂‘(𝑝(.r‘𝑃)𝑞)) = ◡(𝑂‘𝑄)) |
| 38 | 37 | imaeq1d 6077 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (◡(𝑂‘(𝑝(.r‘𝑃)𝑞)) “ { 0 }) = (◡(𝑂‘𝑄) “ { 0 })) |
| 39 | 34, 38 | sseqtrd 4020 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (◡(𝑂‘𝑝) “ { 0 }) ⊆ (◡(𝑂‘𝑄) “ { 0 })) |
| 40 | | ply1dg3rt0irred.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (◡(𝑂‘𝑄) “ { 0 }) =
∅) |
| 41 | 40 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (◡(𝑂‘𝑄) “ { 0 }) =
∅) |
| 42 | 39, 41 | sseqtrd 4020 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (◡(𝑂‘𝑝) “ { 0 }) ⊆
∅) |
| 43 | | ss0 4402 |
. . . . . . . . . . . 12
⊢ ((◡(𝑂‘𝑝) “ { 0 }) ⊆ ∅ →
(◡(𝑂‘𝑝) “ { 0 }) =
∅) |
| 44 | 42, 43 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (◡(𝑂‘𝑝) “ { 0 }) =
∅) |
| 45 | 44 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 1) → (◡(𝑂‘𝑝) “ { 0 }) =
∅) |
| 46 | 18 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 1) → 𝐹 ∈ Field) |
| 47 | 20 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 1) → 𝑝 ∈ 𝐵) |
| 48 | | simpr 484 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 1) → (𝐷‘𝑝) = 1) |
| 49 | 6, 12, 28, 11, 9, 46, 47, 48 | ply1dg1rtn0 33605 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 1) → (◡(𝑂‘𝑝) “ { 0 }) ≠
∅) |
| 50 | 45, 49 | pm2.21ddne 3026 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 1) → ⊥) |
| 51 | 50 | adantlr 715 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) ∈ {0, 1}) ∧ (𝐷‘𝑝) = 1) → ⊥) |
| 52 | | elpri 4649 |
. . . . . . . . 9
⊢ ((𝐷‘𝑝) ∈ {0, 1} → ((𝐷‘𝑝) = 0 ∨ (𝐷‘𝑝) = 1)) |
| 53 | 52 | adantl 481 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) ∈ {0, 1}) → ((𝐷‘𝑝) = 0 ∨ (𝐷‘𝑝) = 1)) |
| 54 | 27, 51, 53 | mpjaodan 961 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) ∈ {0, 1}) →
⊥) |
| 55 | 6, 12, 28, 11, 9, 30, 32, 20, 33 | ply1mulrtss 33606 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (◡(𝑂‘𝑞) “ { 0 }) ⊆ (◡(𝑂‘(𝑞(.r‘𝑃)𝑝)) “ { 0 })) |
| 56 | | fldidom 20771 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹 ∈ Field → 𝐹 ∈ IDomn) |
| 57 | 10, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐹 ∈ IDomn) |
| 58 | 6 | ply1idom 26164 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹 ∈ IDomn → 𝑃 ∈ IDomn) |
| 59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑃 ∈ IDomn) |
| 60 | 59 | idomcringd 20727 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑃 ∈ CRing) |
| 61 | 60 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → 𝑃 ∈ CRing) |
| 62 | 12, 33, 61, 32, 20 | crngcomd 20252 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (𝑞(.r‘𝑃)𝑝) = (𝑝(.r‘𝑃)𝑞)) |
| 63 | 62, 35 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (𝑞(.r‘𝑃)𝑝) = 𝑄) |
| 64 | 63 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (𝑂‘(𝑞(.r‘𝑃)𝑝)) = (𝑂‘𝑄)) |
| 65 | 64 | cnveqd 5886 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → ◡(𝑂‘(𝑞(.r‘𝑃)𝑝)) = ◡(𝑂‘𝑄)) |
| 66 | 65 | imaeq1d 6077 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (◡(𝑂‘(𝑞(.r‘𝑃)𝑝)) “ { 0 }) = (◡(𝑂‘𝑄) “ { 0 })) |
| 67 | 66, 41 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (◡(𝑂‘(𝑞(.r‘𝑃)𝑝)) “ { 0 }) =
∅) |
| 68 | 55, 67 | sseqtrd 4020 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (◡(𝑂‘𝑞) “ { 0 }) ⊆
∅) |
| 69 | | ss0 4402 |
. . . . . . . . . . . 12
⊢ ((◡(𝑂‘𝑞) “ { 0 }) ⊆ ∅ →
(◡(𝑂‘𝑞) “ { 0 }) =
∅) |
| 70 | 68, 69 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (◡(𝑂‘𝑞) “ { 0 }) =
∅) |
| 71 | 70 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 2) → (◡(𝑂‘𝑞) “ { 0 }) =
∅) |
| 72 | 18 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 2) → 𝐹 ∈ Field) |
| 73 | 32 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 2) → 𝑞 ∈ 𝐵) |
| 74 | 29 | crngringd 20243 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 ∈ Ring) |
| 75 | 74 | ad3antrrr 730 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → 𝐹 ∈ Ring) |
| 76 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢
(0g‘𝑃) = (0g‘𝑃) |
| 77 | 59 | idomdomd 20726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑃 ∈ Domn) |
| 78 | 77 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → 𝑃 ∈ Domn) |
| 79 | | 3nn0 12544 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 3 ∈
ℕ0 |
| 80 | 2, 79 | eqeltrdi 2849 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐷‘𝑄) ∈
ℕ0) |
| 81 | 11, 6, 76, 12 | deg1nn0clb 26129 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 ∈ Ring ∧ 𝑄 ∈ 𝐵) → (𝑄 ≠ (0g‘𝑃) ↔ (𝐷‘𝑄) ∈
ℕ0)) |
| 82 | 81 | biimpar 477 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐹 ∈ Ring ∧ 𝑄 ∈ 𝐵) ∧ (𝐷‘𝑄) ∈ ℕ0) → 𝑄 ≠ (0g‘𝑃)) |
| 83 | 74, 1, 80, 82 | syl21anc 838 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑄 ≠ (0g‘𝑃)) |
| 84 | 83 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → 𝑄 ≠ (0g‘𝑃)) |
| 85 | 35, 84 | eqnetrd 3008 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (𝑝(.r‘𝑃)𝑞) ≠ (0g‘𝑃)) |
| 86 | 12, 33, 76, 78, 20, 32, 85 | domnmuln0rd 33278 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (𝑝 ≠ (0g‘𝑃) ∧ 𝑞 ≠ (0g‘𝑃))) |
| 87 | 86 | simpld 494 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → 𝑝 ≠ (0g‘𝑃)) |
| 88 | 11, 6, 76, 12 | deg1nn0cl 26127 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ Ring ∧ 𝑝 ∈ 𝐵 ∧ 𝑝 ≠ (0g‘𝑃)) → (𝐷‘𝑝) ∈
ℕ0) |
| 89 | 75, 20, 87, 88 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (𝐷‘𝑝) ∈
ℕ0) |
| 90 | 89 | nn0cnd 12589 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (𝐷‘𝑝) ∈ ℂ) |
| 91 | 86 | simprd 495 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → 𝑞 ≠ (0g‘𝑃)) |
| 92 | 11, 6, 76, 12 | deg1nn0cl 26127 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ Ring ∧ 𝑞 ∈ 𝐵 ∧ 𝑞 ≠ (0g‘𝑃)) → (𝐷‘𝑞) ∈
ℕ0) |
| 93 | 75, 32, 91, 92 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (𝐷‘𝑞) ∈
ℕ0) |
| 94 | 93 | nn0cnd 12589 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (𝐷‘𝑞) ∈ ℂ) |
| 95 | 35 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (𝐷‘(𝑝(.r‘𝑃)𝑞)) = (𝐷‘𝑄)) |
| 96 | 57 | idomdomd 20726 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 ∈ Domn) |
| 97 | 96 | ad3antrrr 730 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → 𝐹 ∈ Domn) |
| 98 | 11, 6, 12, 33, 76, 97, 20, 87, 32, 91 | deg1mul 26154 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (𝐷‘(𝑝(.r‘𝑃)𝑞)) = ((𝐷‘𝑝) + (𝐷‘𝑞))) |
| 99 | 2 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (𝐷‘𝑄) = 3) |
| 100 | 95, 98, 99 | 3eqtr3d 2785 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → ((𝐷‘𝑝) + (𝐷‘𝑞)) = 3) |
| 101 | 90, 94, 100 | mvlladdd 11674 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (𝐷‘𝑞) = (3 − (𝐷‘𝑝))) |
| 102 | 101 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 2) → (𝐷‘𝑞) = (3 − (𝐷‘𝑝))) |
| 103 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 2) → (𝐷‘𝑝) = 2) |
| 104 | 103 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 2) → (3 − (𝐷‘𝑝)) = (3 − 2)) |
| 105 | | 3cn 12347 |
. . . . . . . . . . . . . 14
⊢ 3 ∈
ℂ |
| 106 | | 2cn 12341 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ |
| 107 | | ax-1cn 11213 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ |
| 108 | | 2p1e3 12408 |
. . . . . . . . . . . . . 14
⊢ (2 + 1) =
3 |
| 109 | 105, 106,
107, 108 | subaddrii 11598 |
. . . . . . . . . . . . 13
⊢ (3
− 2) = 1 |
| 110 | 109 | a1i 11 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 2) → (3 − 2) =
1) |
| 111 | 102, 104,
110 | 3eqtrd 2781 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 2) → (𝐷‘𝑞) = 1) |
| 112 | 6, 12, 28, 11, 9, 72, 73, 111 | ply1dg1rtn0 33605 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 2) → (◡(𝑂‘𝑞) “ { 0 }) ≠
∅) |
| 113 | 71, 112 | pm2.21ddne 3026 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 2) → ⊥) |
| 114 | 113 | adantlr 715 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) ∈ {2, 3}) ∧ (𝐷‘𝑝) = 2) → ⊥) |
| 115 | 101 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 3) → (𝐷‘𝑞) = (3 − (𝐷‘𝑝))) |
| 116 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 3) → (𝐷‘𝑝) = 3) |
| 117 | 116 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 3) → (3 − (𝐷‘𝑝)) = (3 − 3)) |
| 118 | 105 | subidi 11580 |
. . . . . . . . . . . . 13
⊢ (3
− 3) = 0 |
| 119 | 118 | a1i 11 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 3) → (3 − 3) =
0) |
| 120 | 115, 117,
119 | 3eqtrd 2781 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 3) → (𝐷‘𝑞) = 0) |
| 121 | 18 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 3) → 𝐹 ∈ Field) |
| 122 | 32, 12 | eleqtrdi 2851 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → 𝑞 ∈ (Base‘𝑃)) |
| 123 | 122 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 3) → 𝑞 ∈ (Base‘𝑃)) |
| 124 | 6, 7, 8, 9, 121, 11, 123 | ply1unit 33600 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 3) → (𝑞 ∈ (Unit‘𝑃) ↔ (𝐷‘𝑞) = 0)) |
| 125 | 120, 124 | mpbird 257 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 3) → 𝑞 ∈ (Unit‘𝑃)) |
| 126 | 31 | eldifbd 3964 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → ¬ 𝑞 ∈ (Unit‘𝑃)) |
| 127 | 126 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 3) → ¬ 𝑞 ∈ (Unit‘𝑃)) |
| 128 | 125, 127 | pm2.21fal 1562 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) = 3) → ⊥) |
| 129 | 128 | adantlr 715 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) ∈ {2, 3}) ∧ (𝐷‘𝑝) = 3) → ⊥) |
| 130 | | elpri 4649 |
. . . . . . . . 9
⊢ ((𝐷‘𝑝) ∈ {2, 3} → ((𝐷‘𝑝) = 2 ∨ (𝐷‘𝑝) = 3)) |
| 131 | 130 | adantl 481 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) ∈ {2, 3}) → ((𝐷‘𝑝) = 2 ∨ (𝐷‘𝑝) = 3)) |
| 132 | 114, 129,
131 | mpjaodan 961 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) ∧ (𝐷‘𝑝) ∈ {2, 3}) →
⊥) |
| 133 | 79 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → 3 ∈
ℕ0) |
| 134 | 89 | nn0red 12588 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (𝐷‘𝑝) ∈ ℝ) |
| 135 | | nn0addge1 12572 |
. . . . . . . . . . . 12
⊢ (((𝐷‘𝑝) ∈ ℝ ∧ (𝐷‘𝑞) ∈ ℕ0) → (𝐷‘𝑝) ≤ ((𝐷‘𝑝) + (𝐷‘𝑞))) |
| 136 | 134, 93, 135 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (𝐷‘𝑝) ≤ ((𝐷‘𝑝) + (𝐷‘𝑞))) |
| 137 | 136, 100 | breqtrd 5169 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (𝐷‘𝑝) ≤ 3) |
| 138 | | fznn0 13659 |
. . . . . . . . . . 11
⊢ (3 ∈
ℕ0 → ((𝐷‘𝑝) ∈ (0...3) ↔ ((𝐷‘𝑝) ∈ ℕ0 ∧ (𝐷‘𝑝) ≤ 3))) |
| 139 | 138 | biimpar 477 |
. . . . . . . . . 10
⊢ ((3
∈ ℕ0 ∧ ((𝐷‘𝑝) ∈ ℕ0 ∧ (𝐷‘𝑝) ≤ 3)) → (𝐷‘𝑝) ∈ (0...3)) |
| 140 | 133, 89, 137, 139 | syl12anc 837 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (𝐷‘𝑝) ∈ (0...3)) |
| 141 | | fz0to3un2pr 13669 |
. . . . . . . . 9
⊢ (0...3) =
({0, 1} ∪ {2, 3}) |
| 142 | 140, 141 | eleqtrdi 2851 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → (𝐷‘𝑝) ∈ ({0, 1} ∪ {2,
3})) |
| 143 | | elun 4153 |
. . . . . . . 8
⊢ ((𝐷‘𝑝) ∈ ({0, 1} ∪ {2, 3}) ↔ ((𝐷‘𝑝) ∈ {0, 1} ∨ (𝐷‘𝑝) ∈ {2, 3})) |
| 144 | 142, 143 | sylib 218 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → ((𝐷‘𝑝) ∈ {0, 1} ∨ (𝐷‘𝑝) ∈ {2, 3})) |
| 145 | 54, 132, 144 | mpjaodan 961 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ 𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))) ∧ (𝑝(.r‘𝑃)𝑞) = 𝑄) → ⊥) |
| 146 | 145 | r19.29ffa 32490 |
. . . . 5
⊢ ((𝜑 ∧ ∃𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))∃𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))(𝑝(.r‘𝑃)𝑞) = 𝑄) → ⊥) |
| 147 | 146 | inegd 1560 |
. . . 4
⊢ (𝜑 → ¬ ∃𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))∃𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))(𝑝(.r‘𝑃)𝑞) = 𝑄) |
| 148 | | ralnex2 3133 |
. . . 4
⊢
(∀𝑝 ∈
(𝐵 ∖
(Unit‘𝑃))∀𝑞 ∈ (𝐵 ∖ (Unit‘𝑃)) ¬ (𝑝(.r‘𝑃)𝑞) = 𝑄 ↔ ¬ ∃𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))∃𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))(𝑝(.r‘𝑃)𝑞) = 𝑄) |
| 149 | 147, 148 | sylibr 234 |
. . 3
⊢ (𝜑 → ∀𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))∀𝑞 ∈ (𝐵 ∖ (Unit‘𝑃)) ¬ (𝑝(.r‘𝑃)𝑞) = 𝑄) |
| 150 | | df-ne 2941 |
. . . 4
⊢ ((𝑝(.r‘𝑃)𝑞) ≠ 𝑄 ↔ ¬ (𝑝(.r‘𝑃)𝑞) = 𝑄) |
| 151 | 150 | 2ralbii 3128 |
. . 3
⊢
(∀𝑝 ∈
(𝐵 ∖
(Unit‘𝑃))∀𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))(𝑝(.r‘𝑃)𝑞) ≠ 𝑄 ↔ ∀𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))∀𝑞 ∈ (𝐵 ∖ (Unit‘𝑃)) ¬ (𝑝(.r‘𝑃)𝑞) = 𝑄) |
| 152 | 149, 151 | sylibr 234 |
. 2
⊢ (𝜑 → ∀𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))∀𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))(𝑝(.r‘𝑃)𝑞) ≠ 𝑄) |
| 153 | | eqid 2737 |
. . 3
⊢
(Unit‘𝑃) =
(Unit‘𝑃) |
| 154 | | eqid 2737 |
. . 3
⊢
(Irred‘𝑃) =
(Irred‘𝑃) |
| 155 | | eqid 2737 |
. . 3
⊢ (𝐵 ∖ (Unit‘𝑃)) = (𝐵 ∖ (Unit‘𝑃)) |
| 156 | 12, 153, 154, 155, 33 | isirred 20419 |
. 2
⊢ (𝑄 ∈ (Irred‘𝑃) ↔ (𝑄 ∈ (𝐵 ∖ (Unit‘𝑃)) ∧ ∀𝑝 ∈ (𝐵 ∖ (Unit‘𝑃))∀𝑞 ∈ (𝐵 ∖ (Unit‘𝑃))(𝑝(.r‘𝑃)𝑞) ≠ 𝑄)) |
| 157 | 17, 152, 156 | sylanbrc 583 |
1
⊢ (𝜑 → 𝑄 ∈ (Irred‘𝑃)) |