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 ‘ 𝐹 )
ply1dg3rt0irred.o ⊢ 𝑂 = ( eval1 ‘ 𝐹 )
ply1dg3rt0irred.d ⊢ 𝐷 = ( deg1 ‘ 𝐹 )
ply1dg3rt0irred.p ⊢ 𝑃 = ( Poly1 ‘ 𝐹 )
ply1dg3rt0irred.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
ply1dg3rt0irred.f ⊢ ( 𝜑 → 𝐹 ∈ Field )
ply1dg3rt0irred.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
ply1dg3rt0irred.1 ⊢ ( 𝜑 → ( ◡ ( 𝑂 ‘ 𝑄 ) “ { 0 } ) = ∅ )
ply1dg3rt0irred.2 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑄 ) = 3 )
Assertion ply1dg3rt0irred ( 𝜑 → 𝑄 ∈ ( Irred ‘ 𝑃 ) )

Proof

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