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 = ( 0_g ‘ 𝐹 )
	ply1dg3rt0irred.o	⊢ 𝑂 = ( eval₁ ‘ 𝐹 )
	ply1dg3rt0irred.d	⊢ 𝐷 = ( deg₁ ‘ 𝐹 )
	ply1dg3rt0irred.p	⊢ 𝑃 = ( Poly₁ ‘ 𝐹 )
	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 = ( 0_g ‘ 𝐹 )
2		ply1dg3rt0irred.o	⊢ 𝑂 = ( eval₁ ‘ 𝐹 )
3		ply1dg3rt0irred.d	⊢ 𝐷 = ( deg₁ ‘ 𝐹 )
4		ply1dg3rt0irred.p	⊢ 𝑃 = ( Poly₁ ‘ 𝐹 )
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	⊢ ( 0_g ‘ 𝑃 ) = ( 0_g ‘ 𝑃 )
77	59	idomdomd	⊢ ( 𝜑 → 𝑃 ∈ Domn )
78	77	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ 𝑞 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ ( 𝑝 ( ._r ‘ 𝑃 ) 𝑞 ) = 𝑄 ) → 𝑃 ∈ Domn )
79		3nn0	⊢ 3 ∈ ℕ₀
80	9 79	eqeltrdi	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑄 ) ∈ ℕ₀ )
81	3 4 76 5	deg1nn0clb	⊢ ( ( 𝐹 ∈ Ring ∧ 𝑄 ∈ 𝐵 ) → ( 𝑄 ≠ ( 0_g ‘ 𝑃 ) ↔ ( 𝐷 ‘ 𝑄 ) ∈ ℕ₀ ) )
82	81	biimpar	⊢ ( ( ( 𝐹 ∈ Ring ∧ 𝑄 ∈ 𝐵 ) ∧ ( 𝐷 ‘ 𝑄 ) ∈ ℕ₀ ) → 𝑄 ≠ ( 0_g ‘ 𝑃 ) )
83	74 7 80 82	syl21anc	⊢ ( 𝜑 → 𝑄 ≠ ( 0_g ‘ 𝑃 ) )
84	83	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ 𝑞 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ ( 𝑝 ( ._r ‘ 𝑃 ) 𝑞 ) = 𝑄 ) → 𝑄 ≠ ( 0_g ‘ 𝑃 ) )
85	36 84	eqnetrd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ 𝑞 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ ( 𝑝 ( ._r ‘ 𝑃 ) 𝑞 ) = 𝑄 ) → ( 𝑝 ( ._r ‘ 𝑃 ) 𝑞 ) ≠ ( 0_g ‘ 𝑃 ) )
86	5 34 76 78 22 33 85	domnmuln0rd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ 𝑞 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ ( 𝑝 ( ._r ‘ 𝑃 ) 𝑞 ) = 𝑄 ) → ( 𝑝 ≠ ( 0_g ‘ 𝑃 ) ∧ 𝑞 ≠ ( 0_g ‘ 𝑃 ) ) )
87	86	simpld	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ 𝑞 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ ( 𝑝 ( ._r ‘ 𝑃 ) 𝑞 ) = 𝑄 ) → 𝑝 ≠ ( 0_g ‘ 𝑃 ) )
88	3 4 76 5	deg1nn0cl	⊢ ( ( 𝐹 ∈ Ring ∧ 𝑝 ∈ 𝐵 ∧ 𝑝 ≠ ( 0_g ‘ 𝑃 ) ) → ( 𝐷 ‘ 𝑝 ) ∈ ℕ₀ )
89	75 22 87 88	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ 𝑞 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ ( 𝑝 ( ._r ‘ 𝑃 ) 𝑞 ) = 𝑄 ) → ( 𝐷 ‘ 𝑝 ) ∈ ℕ₀ )
90	89	nn0cnd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ 𝑞 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ ( 𝑝 ( ._r ‘ 𝑃 ) 𝑞 ) = 𝑄 ) → ( 𝐷 ‘ 𝑝 ) ∈ ℂ )
91	86	simprd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ 𝑞 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ ( 𝑝 ( ._r ‘ 𝑃 ) 𝑞 ) = 𝑄 ) → 𝑞 ≠ ( 0_g ‘ 𝑃 ) )
92	3 4 76 5	deg1nn0cl	⊢ ( ( 𝐹 ∈ Ring ∧ 𝑞 ∈ 𝐵 ∧ 𝑞 ≠ ( 0_g ‘ 𝑃 ) ) → ( 𝐷 ‘ 𝑞 ) ∈ ℕ₀ )
93	75 33 91 92	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ 𝑞 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ ( 𝑝 ( ._r ‘ 𝑃 ) 𝑞 ) = 𝑄 ) → ( 𝐷 ‘ 𝑞 ) ∈ ℕ₀ )
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 ∈ ℕ₀ )
134	89	nn0red	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ 𝑞 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ ( 𝑝 ( ._r ‘ 𝑃 ) 𝑞 ) = 𝑄 ) → ( 𝐷 ‘ 𝑝 ) ∈ ℝ )
135		nn0addge1	⊢ ( ( ( 𝐷 ‘ 𝑝 ) ∈ ℝ ∧ ( 𝐷 ‘ 𝑞 ) ∈ ℕ₀ ) → ( 𝐷 ‘ 𝑝 ) ≤ ( ( 𝐷 ‘ 𝑝 ) + ( 𝐷 ‘ 𝑞 ) ) )
136	134 93 135	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ 𝑞 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ ( 𝑝 ( ._r ‘ 𝑃 ) 𝑞 ) = 𝑄 ) → ( 𝐷 ‘ 𝑝 ) ≤ ( ( 𝐷 ‘ 𝑝 ) + ( 𝐷 ‘ 𝑞 ) ) )
137	136 100	breqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ 𝑞 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑃 ) ) ) ∧ ( 𝑝 ( ._r ‘ 𝑃 ) 𝑞 ) = 𝑄 ) → ( 𝐷 ‘ 𝑝 ) ≤ 3 )
138		fznn0	⊢ ( 3 ∈ ℕ₀ → ( ( 𝐷 ‘ 𝑝 ) ∈ ( 0 ... 3 ) ↔ ( ( 𝐷 ‘ 𝑝 ) ∈ ℕ₀ ∧ ( 𝐷 ‘ 𝑝 ) ≤ 3 ) ) )
139	138	biimpar	⊢ ( ( 3 ∈ ℕ₀ ∧ ( ( 𝐷 ‘ 𝑝 ) ∈ ℕ₀ ∧ ( 𝐷 ‘ 𝑝 ) ≤ 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 ‘ 𝑃 ) )

Metamath Proof Explorer

Theorem ply1dg3rt0irred

Proof