This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ply1dg3rt0irred

Description: If a cubic polynomial over a field has no roots, it is irreducible. (Proposed by Saveliy Skresanov, 5-Jun-2025.) (Contributed by Thierry Arnoux, 8-Jun-2025)

Ref Expression
Hypotheses ply1dg3rt0irred.z 
|- .0. = ( 0g ` F )
ply1dg3rt0irred.o 
|- O = ( eval1 ` F )
ply1dg3rt0irred.d 
|- D = ( deg1 ` F )
ply1dg3rt0irred.p 
|- P = ( Poly1 ` F )
ply1dg3rt0irred.b 
|- B = ( Base ` P )
ply1dg3rt0irred.f 
|- ( ph -> F e. Field )
ply1dg3rt0irred.q 
|- ( ph -> Q e. B )
ply1dg3rt0irred.1 
|- ( ph -> ( `' ( O ` Q ) " { .0. } ) = (/) )
ply1dg3rt0irred.2 
|- ( ph -> ( D ` Q ) = 3 )
Assertion ply1dg3rt0irred 
|- ( ph -> Q e. ( Irred ` P ) )

Proof

Step Hyp Ref Expression
1 ply1dg3rt0irred.z 
 |-  .0. = ( 0g ` F )
2 ply1dg3rt0irred.o 
 |-  O = ( eval1 ` F )
3 ply1dg3rt0irred.d 
 |-  D = ( deg1 ` F )
4 ply1dg3rt0irred.p 
 |-  P = ( Poly1 ` F )
5 ply1dg3rt0irred.b 
 |-  B = ( Base ` P )
6 ply1dg3rt0irred.f 
 |-  ( ph -> F e. Field )
7 ply1dg3rt0irred.q 
 |-  ( ph -> Q e. B )
8 ply1dg3rt0irred.1 
 |-  ( ph -> ( `' ( O ` Q ) " { .0. } ) = (/) )
9 ply1dg3rt0irred.2 
 |-  ( ph -> ( D ` Q ) = 3 )
10 3ne0 
 |-  3 =/= 0
11 10 a1i 
 |-  ( ph -> 3 =/= 0 )
12 9 11 eqnetrd 
 |-  ( ph -> ( D ` Q ) =/= 0 )
13 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
14 eqid 
 |-  ( Base ` F ) = ( Base ` F )
15 7 5 eleqtrdi 
 |-  ( ph -> Q e. ( Base ` P ) )
16 4 13 14 1 6 3 15 ply1unit 
 |-  ( ph -> ( Q e. ( Unit ` P ) <-> ( D ` Q ) = 0 ) )
17 16 necon3bbid 
 |-  ( ph -> ( -. Q e. ( Unit ` P ) <-> ( D ` Q ) =/= 0 ) )
18 12 17 mpbird 
 |-  ( ph -> -. Q e. ( Unit ` P ) )
19 7 18 eldifd 
 |-  ( ph -> Q e. ( B \ ( Unit ` P ) ) )
20 6 ad3antrrr 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> F e. Field )
21 simpllr 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> p e. ( B \ ( Unit ` P ) ) )
22 21 eldifad 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> p e. B )
23 22 5 eleqtrdi 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> p e. ( Base ` P ) )
24 4 13 14 1 20 3 23 ply1unit 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( p e. ( Unit ` P ) <-> ( D ` p ) = 0 ) )
25 24 biimpar 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 0 ) -> p e. ( Unit ` P ) )
26 21 eldifbd 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> -. p e. ( Unit ` P ) )
27 26 adantr 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 0 ) -> -. p e. ( Unit ` P ) )
28 25 27 pm2.21fal 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 0 ) -> F. )
29 28 adantlr 
 |-  ( ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) e. { 0 , 1 } ) /\ ( D ` p ) = 0 ) -> F. )
30 6 fldcrngd 
 |-  ( ph -> F e. CRing )
31 30 ad3antrrr 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> F e. CRing )
32 simplr 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> q e. ( B \ ( Unit ` P ) ) )
33 32 eldifad 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> q e. B )
34 eqid 
 |-  ( .r ` P ) = ( .r ` P )
35 4 5 2 3 1 31 22 33 34 ply1mulrtss 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( `' ( O ` p ) " { .0. } ) C_ ( `' ( O ` ( p ( .r ` P ) q ) ) " { .0. } ) )
36 simpr 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( p ( .r ` P ) q ) = Q )
37 36 fveq2d 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( O ` ( p ( .r ` P ) q ) ) = ( O ` Q ) )
38 37 cnveqd 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> `' ( O ` ( p ( .r ` P ) q ) ) = `' ( O ` Q ) )
39 38 imaeq1d 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( `' ( O ` ( p ( .r ` P ) q ) ) " { .0. } ) = ( `' ( O ` Q ) " { .0. } ) )
40 35 39 sseqtrd 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( `' ( O ` p ) " { .0. } ) C_ ( `' ( O ` Q ) " { .0. } ) )
41 8 ad3antrrr 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( `' ( O ` Q ) " { .0. } ) = (/) )
42 40 41 sseqtrd 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( `' ( O ` p ) " { .0. } ) C_ (/) )
43 ss0 
 |-  ( ( `' ( O ` p ) " { .0. } ) C_ (/) -> ( `' ( O ` p ) " { .0. } ) = (/) )
44 42 43 syl 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( `' ( O ` p ) " { .0. } ) = (/) )
45 44 adantr 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 1 ) -> ( `' ( O ` p ) " { .0. } ) = (/) )
46 20 adantr 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 1 ) -> F e. Field )
47 22 adantr 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 1 ) -> p e. B )
48 simpr 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 1 ) -> ( D ` p ) = 1 )
49 4 5 2 3 1 46 47 48 ply1dg1rtn0 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 1 ) -> ( `' ( O ` p ) " { .0. } ) =/= (/) )
50 45 49 pm2.21ddne 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 1 ) -> F. )
51 50 adantlr 
 |-  ( ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) e. { 0 , 1 } ) /\ ( D ` p ) = 1 ) -> F. )
52 elpri 
 |-  ( ( D ` p ) e. { 0 , 1 } -> ( ( D ` p ) = 0 \/ ( D ` p ) = 1 ) )
53 52 adantl 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) e. { 0 , 1 } ) -> ( ( D ` p ) = 0 \/ ( D ` p ) = 1 ) )
54 29 51 53 mpjaodan 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) e. { 0 , 1 } ) -> F. )
55 4 5 2 3 1 31 33 22 34 ply1mulrtss 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( `' ( O ` q ) " { .0. } ) C_ ( `' ( O ` ( q ( .r ` P ) p ) ) " { .0. } ) )
56 fldidom 
 |-  ( F e. Field -> F e. IDomn )
57 6 56 syl 
 |-  ( ph -> F e. IDomn )
58 4 ply1idom 
 |-  ( F e. IDomn -> P e. IDomn )
59 57 58 syl 
 |-  ( ph -> P e. IDomn )
60 59 idomcringd 
 |-  ( ph -> P e. CRing )
61 60 ad3antrrr 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> P e. CRing )
62 5 34 61 33 22 crngcomd 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( q ( .r ` P ) p ) = ( p ( .r ` P ) q ) )
63 62 36 eqtrd 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( q ( .r ` P ) p ) = Q )
64 63 fveq2d 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( O ` ( q ( .r ` P ) p ) ) = ( O ` Q ) )
65 64 cnveqd 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> `' ( O ` ( q ( .r ` P ) p ) ) = `' ( O ` Q ) )
66 65 imaeq1d 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( `' ( O ` ( q ( .r ` P ) p ) ) " { .0. } ) = ( `' ( O ` Q ) " { .0. } ) )
67 66 41 eqtrd 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( `' ( O ` ( q ( .r ` P ) p ) ) " { .0. } ) = (/) )
68 55 67 sseqtrd 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( `' ( O ` q ) " { .0. } ) C_ (/) )
69 ss0 
 |-  ( ( `' ( O ` q ) " { .0. } ) C_ (/) -> ( `' ( O ` q ) " { .0. } ) = (/) )
70 68 69 syl 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( `' ( O ` q ) " { .0. } ) = (/) )
71 70 adantr 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 2 ) -> ( `' ( O ` q ) " { .0. } ) = (/) )
72 20 adantr 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 2 ) -> F e. Field )
73 33 adantr 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 2 ) -> q e. B )
74 30 crngringd 
 |-  ( ph -> F e. Ring )
75 74 ad3antrrr 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> F e. Ring )
76 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
77 59 idomdomd 
 |-  ( ph -> P e. Domn )
78 77 ad3antrrr 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> P e. Domn )
79 3nn0 
 |-  3 e. NN0
80 9 79 eqeltrdi 
 |-  ( ph -> ( D ` Q ) e. NN0 )
81 3 4 76 5 deg1nn0clb 
 |-  ( ( F e. Ring /\ Q e. B ) -> ( Q =/= ( 0g ` P ) <-> ( D ` Q ) e. NN0 ) )
82 81 biimpar 
 |-  ( ( ( F e. Ring /\ Q e. B ) /\ ( D ` Q ) e. NN0 ) -> Q =/= ( 0g ` P ) )
83 74 7 80 82 syl21anc 
 |-  ( ph -> Q =/= ( 0g ` P ) )
84 83 ad3antrrr 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> Q =/= ( 0g ` P ) )
85 36 84 eqnetrd 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( p ( .r ` P ) q ) =/= ( 0g ` P ) )
86 5 34 76 78 22 33 85 domnmuln0rd 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( p =/= ( 0g ` P ) /\ q =/= ( 0g ` P ) ) )
87 86 simpld 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> p =/= ( 0g ` P ) )
88 3 4 76 5 deg1nn0cl 
 |-  ( ( F e. Ring /\ p e. B /\ p =/= ( 0g ` P ) ) -> ( D ` p ) e. NN0 )
89 75 22 87 88 syl3anc 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( D ` p ) e. NN0 )
90 89 nn0cnd 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( D ` p ) e. CC )
91 86 simprd 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> q =/= ( 0g ` P ) )
92 3 4 76 5 deg1nn0cl 
 |-  ( ( F e. Ring /\ q e. B /\ q =/= ( 0g ` P ) ) -> ( D ` q ) e. NN0 )
93 75 33 91 92 syl3anc 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( D ` q ) e. NN0 )
94 93 nn0cnd 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( D ` q ) e. CC )
95 36 fveq2d 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( D ` ( p ( .r ` P ) q ) ) = ( D ` Q ) )
96 57 idomdomd 
 |-  ( ph -> F e. Domn )
97 96 ad3antrrr 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> F e. Domn )
98 3 4 5 34 76 97 22 87 33 91 deg1mul 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( D ` ( p ( .r ` P ) q ) ) = ( ( D ` p ) + ( D ` q ) ) )
99 9 ad3antrrr 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( D ` Q ) = 3 )
100 95 98 99 3eqtr3d 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( ( D ` p ) + ( D ` q ) ) = 3 )
101 90 94 100 mvlladdd 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( D ` q ) = ( 3 - ( D ` p ) ) )
102 101 adantr 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 2 ) -> ( D ` q ) = ( 3 - ( D ` p ) ) )
103 simpr 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 2 ) -> ( D ` p ) = 2 )
104 103 oveq2d 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 2 ) -> ( 3 - ( D ` p ) ) = ( 3 - 2 ) )
105 3cn 
 |-  3 e. CC
106 2cn 
 |-  2 e. CC
107 ax-1cn 
 |-  1 e. CC
108 2p1e3 
 |-  ( 2 + 1 ) = 3
109 105 106 107 108 subaddrii 
 |-  ( 3 - 2 ) = 1
110 109 a1i 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 2 ) -> ( 3 - 2 ) = 1 )
111 102 104 110 3eqtrd 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 2 ) -> ( D ` q ) = 1 )
112 4 5 2 3 1 72 73 111 ply1dg1rtn0 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 2 ) -> ( `' ( O ` q ) " { .0. } ) =/= (/) )
113 71 112 pm2.21ddne 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 2 ) -> F. )
114 113 adantlr 
 |-  ( ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) e. { 2 , 3 } ) /\ ( D ` p ) = 2 ) -> F. )
115 101 adantr 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 3 ) -> ( D ` q ) = ( 3 - ( D ` p ) ) )
116 simpr 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 3 ) -> ( D ` p ) = 3 )
117 116 oveq2d 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 3 ) -> ( 3 - ( D ` p ) ) = ( 3 - 3 ) )
118 105 subidi 
 |-  ( 3 - 3 ) = 0
119 118 a1i 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 3 ) -> ( 3 - 3 ) = 0 )
120 115 117 119 3eqtrd 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 3 ) -> ( D ` q ) = 0 )
121 20 adantr 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 3 ) -> F e. Field )
122 33 5 eleqtrdi 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> q e. ( Base ` P ) )
123 122 adantr 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 3 ) -> q e. ( Base ` P ) )
124 4 13 14 1 121 3 123 ply1unit 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 3 ) -> ( q e. ( Unit ` P ) <-> ( D ` q ) = 0 ) )
125 120 124 mpbird 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 3 ) -> q e. ( Unit ` P ) )
126 32 eldifbd 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> -. q e. ( Unit ` P ) )
127 126 adantr 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 3 ) -> -. q e. ( Unit ` P ) )
128 125 127 pm2.21fal 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) = 3 ) -> F. )
129 128 adantlr 
 |-  ( ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) e. { 2 , 3 } ) /\ ( D ` p ) = 3 ) -> F. )
130 elpri 
 |-  ( ( D ` p ) e. { 2 , 3 } -> ( ( D ` p ) = 2 \/ ( D ` p ) = 3 ) )
131 130 adantl 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) e. { 2 , 3 } ) -> ( ( D ` p ) = 2 \/ ( D ` p ) = 3 ) )
132 114 129 131 mpjaodan 
 |-  ( ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) /\ ( D ` p ) e. { 2 , 3 } ) -> F. )
133 79 a1i 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> 3 e. NN0 )
134 89 nn0red 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( D ` p ) e. RR )
135 nn0addge1 
 |-  ( ( ( D ` p ) e. RR /\ ( D ` q ) e. NN0 ) -> ( D ` p ) <_ ( ( D ` p ) + ( D ` q ) ) )
136 134 93 135 syl2anc 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( D ` p ) <_ ( ( D ` p ) + ( D ` q ) ) )
137 136 100 breqtrd 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( D ` p ) <_ 3 )
138 fznn0 
 |-  ( 3 e. NN0 -> ( ( D ` p ) e. ( 0 ... 3 ) <-> ( ( D ` p ) e. NN0 /\ ( D ` p ) <_ 3 ) ) )
139 138 biimpar 
 |-  ( ( 3 e. NN0 /\ ( ( D ` p ) e. NN0 /\ ( D ` p ) <_ 3 ) ) -> ( D ` p ) e. ( 0 ... 3 ) )
140 133 89 137 139 syl12anc 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( D ` p ) e. ( 0 ... 3 ) )
141 fz0to3un2pr 
 |-  ( 0 ... 3 ) = ( { 0 , 1 } u. { 2 , 3 } )
142 140 141 eleqtrdi 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( D ` p ) e. ( { 0 , 1 } u. { 2 , 3 } ) )
143 elun 
 |-  ( ( D ` p ) e. ( { 0 , 1 } u. { 2 , 3 } ) <-> ( ( D ` p ) e. { 0 , 1 } \/ ( D ` p ) e. { 2 , 3 } ) )
144 142 143 sylib 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> ( ( D ` p ) e. { 0 , 1 } \/ ( D ` p ) e. { 2 , 3 } ) )
145 54 132 144 mpjaodan 
 |-  ( ( ( ( ph /\ p e. ( B \ ( Unit ` P ) ) ) /\ q e. ( B \ ( Unit ` P ) ) ) /\ ( p ( .r ` P ) q ) = Q ) -> F. )
146 145 r19.29ffa 
 |-  ( ( ph /\ E. p e. ( B \ ( Unit ` P ) ) E. q e. ( B \ ( Unit ` P ) ) ( p ( .r ` P ) q ) = Q ) -> F. )
147 146 inegd 
 |-  ( ph -> -. E. p e. ( B \ ( Unit ` P ) ) E. q e. ( B \ ( Unit ` P ) ) ( p ( .r ` P ) q ) = Q )
148 ralnex2 
 |-  ( A. p e. ( B \ ( Unit ` P ) ) A. q e. ( B \ ( Unit ` P ) ) -. ( p ( .r ` P ) q ) = Q <-> -. E. p e. ( B \ ( Unit ` P ) ) E. q e. ( B \ ( Unit ` P ) ) ( p ( .r ` P ) q ) = Q )
149 147 148 sylibr 
 |-  ( ph -> A. p e. ( B \ ( Unit ` P ) ) A. q e. ( B \ ( Unit ` P ) ) -. ( p ( .r ` P ) q ) = Q )
150 df-ne 
 |-  ( ( p ( .r ` P ) q ) =/= Q <-> -. ( p ( .r ` P ) q ) = Q )
151 150 2ralbii 
 |-  ( A. p e. ( B \ ( Unit ` P ) ) A. q e. ( B \ ( Unit ` P ) ) ( p ( .r ` P ) q ) =/= Q <-> A. p e. ( B \ ( Unit ` P ) ) A. q e. ( B \ ( Unit ` P ) ) -. ( p ( .r ` P ) q ) = Q )
152 149 151 sylibr 
 |-  ( ph -> A. p e. ( B \ ( Unit ` P ) ) A. q e. ( B \ ( Unit ` P ) ) ( p ( .r ` P ) q ) =/= Q )
153 eqid 
 |-  ( Unit ` P ) = ( Unit ` P )
154 eqid 
 |-  ( Irred ` P ) = ( Irred ` P )
155 eqid 
 |-  ( B \ ( Unit ` P ) ) = ( B \ ( Unit ` P ) )
156 5 153 154 155 34 isirred 
 |-  ( Q e. ( Irred ` P ) <-> ( Q e. ( B \ ( Unit ` P ) ) /\ A. p e. ( B \ ( Unit ` P ) ) A. q e. ( B \ ( Unit ` P ) ) ( p ( .r ` P ) q ) =/= Q ) )
157 19 152 156 sylanbrc 
 |-  ( ph -> Q e. ( Irred ` P ) )