Theorem r1pid2OLD

Description: Obsolete version of r1pid2 as of 21-Jun-2025. (Contributed by Thierry Arnoux, 2-Apr-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	r1padd1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	r1padd1.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
	r1padd1.n	⊢ 𝑁 = ( Unic1p ‘ 𝑅 )
	r1padd1.e	⊢ 𝐸 = ( rem1p ‘ 𝑅 )
	r1pid2OLD.r	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
	r1pid2OLD.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	r1pid2OLD.p	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	r1pid2OLD.q	⊢ ( 𝜑 → 𝐵 ∈ 𝑁 )
Assertion	r1pid2OLD	⊢ ( 𝜑 → ( ( 𝐴 𝐸 𝐵 ) = 𝐴 ↔ ( 𝐷 ‘ 𝐴 ) < ( 𝐷 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		r1padd1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		r1padd1.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
3		r1padd1.n	⊢ 𝑁 = ( Unic1p ‘ 𝑅 )
4		r1padd1.e	⊢ 𝐸 = ( rem1p ‘ 𝑅 )
5		r1pid2OLD.r	⊢ ( 𝜑 → 𝑅 ∈ IDomn )
6		r1pid2OLD.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
7		r1pid2OLD.p	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
8		r1pid2OLD.q	⊢ ( 𝜑 → 𝐵 ∈ 𝑁 )
9	5	idomringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
10		eqid	⊢ ( quot1p ‘ 𝑅 ) = ( quot1p ‘ 𝑅 )
11		eqid	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
12		eqid	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
13	1 2 3 10 4 11 12	r1pid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑁 ) → 𝐴 = ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) )
14	9 7 8 13	syl3anc	⊢ ( 𝜑 → 𝐴 = ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) )
15	14	eqeq2d	⊢ ( 𝜑 → ( ( 𝐴 𝐸 𝐵 ) = 𝐴 ↔ ( 𝐴 𝐸 𝐵 ) = ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) ) )
16		eqcom	⊢ ( ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) = ( 𝐴 𝐸 𝐵 ) ↔ ( 𝐴 𝐸 𝐵 ) = ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) )
17	15 16	bitr4di	⊢ ( 𝜑 → ( ( 𝐴 𝐸 𝐵 ) = 𝐴 ↔ ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) = ( 𝐴 𝐸 𝐵 ) ) )
18		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
19	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
20	9 19	syl	⊢ ( 𝜑 → 𝑃 ∈ Ring )
21	20	ringgrpd	⊢ ( 𝜑 → 𝑃 ∈ Grp )
22	4 1 2 3	r1pcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑁 ) → ( 𝐴 𝐸 𝐵 ) ∈ 𝑈 )
23	9 7 8 22	syl3anc	⊢ ( 𝜑 → ( 𝐴 𝐸 𝐵 ) ∈ 𝑈 )
24	2 12 18 21 23	grplidd	⊢ ( 𝜑 → ( ( 0g ‘ 𝑃 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) = ( 𝐴 𝐸 𝐵 ) )
25	24	eqeq2d	⊢ ( 𝜑 → ( ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) = ( ( 0g ‘ 𝑃 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) ↔ ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) = ( 𝐴 𝐸 𝐵 ) ) )
26	10 1 2 3	q1pcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑁 ) → ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ∈ 𝑈 )
27	9 7 8 26	syl3anc	⊢ ( 𝜑 → ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ∈ 𝑈 )
28	1 2 3	uc1pcl	⊢ ( 𝐵 ∈ 𝑁 → 𝐵 ∈ 𝑈 )
29	8 28	syl	⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
30	2 11 20 27 29	ringcld	⊢ ( 𝜑 → ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ∈ 𝑈 )
31	2 18	ring0cl	⊢ ( 𝑃 ∈ Ring → ( 0g ‘ 𝑃 ) ∈ 𝑈 )
32	9 19 31	3syl	⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) ∈ 𝑈 )
33	2 12	grprcan	⊢ ( ( 𝑃 ∈ Grp ∧ ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ∈ 𝑈 ∧ ( 0g ‘ 𝑃 ) ∈ 𝑈 ∧ ( 𝐴 𝐸 𝐵 ) ∈ 𝑈 ) ) → ( ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) = ( ( 0g ‘ 𝑃 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) ↔ ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
34	21 30 32 23 33	syl13anc	⊢ ( 𝜑 → ( ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) = ( ( 0g ‘ 𝑃 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) ↔ ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
35	17 25 34	3bitr2d	⊢ ( 𝜑 → ( ( 𝐴 𝐸 𝐵 ) = 𝐴 ↔ ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
36		isidom	⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
37	5 36	sylib	⊢ ( 𝜑 → ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
38	37	simpld	⊢ ( 𝜑 → 𝑅 ∈ CRing )
39	1	ply1crng	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
40	38 39	syl	⊢ ( 𝜑 → 𝑃 ∈ CRing )
41	2 11	crngcom	⊢ ( ( 𝑃 ∈ CRing ∧ 𝐵 ∈ 𝑈 ∧ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ∈ 𝑈 ) → ( 𝐵 ( .r ‘ 𝑃 ) ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ) = ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) )
42	40 29 27 41	syl3anc	⊢ ( 𝜑 → ( 𝐵 ( .r ‘ 𝑃 ) ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ) = ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) )
43	42	eqeq1d	⊢ ( 𝜑 → ( ( 𝐵 ( .r ‘ 𝑃 ) ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ) = ( 0g ‘ 𝑃 ) ↔ ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
44	5	idomdomd	⊢ ( 𝜑 → 𝑅 ∈ Domn )
45	1	ply1domn	⊢ ( 𝑅 ∈ Domn → 𝑃 ∈ Domn )
46	44 45	syl	⊢ ( 𝜑 → 𝑃 ∈ Domn )
47	1 18 3	uc1pn0	⊢ ( 𝐵 ∈ 𝑁 → 𝐵 ≠ ( 0g ‘ 𝑃 ) )
48	8 47	syl	⊢ ( 𝜑 → 𝐵 ≠ ( 0g ‘ 𝑃 ) )
49		eqid	⊢ ( RLReg ‘ 𝑃 ) = ( RLReg ‘ 𝑃 )
50	2 49 18	domnrrg	⊢ ( ( 𝑃 ∈ Domn ∧ 𝐵 ∈ 𝑈 ∧ 𝐵 ≠ ( 0g ‘ 𝑃 ) ) → 𝐵 ∈ ( RLReg ‘ 𝑃 ) )
51	46 29 48 50	syl3anc	⊢ ( 𝜑 → 𝐵 ∈ ( RLReg ‘ 𝑃 ) )
52	49 2 11 18	rrgeq0	⊢ ( ( 𝑃 ∈ Ring ∧ 𝐵 ∈ ( RLReg ‘ 𝑃 ) ∧ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ∈ 𝑈 ) → ( ( 𝐵 ( .r ‘ 𝑃 ) ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ) = ( 0g ‘ 𝑃 ) ↔ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
53	20 51 27 52	syl3anc	⊢ ( 𝜑 → ( ( 𝐵 ( .r ‘ 𝑃 ) ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ) = ( 0g ‘ 𝑃 ) ↔ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
54	35 43 53	3bitr2d	⊢ ( 𝜑 → ( ( 𝐴 𝐸 𝐵 ) = 𝐴 ↔ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
55	2 11 18 20 29	ringlzd	⊢ ( 𝜑 → ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) = ( 0g ‘ 𝑃 ) )
56	55	oveq2d	⊢ ( 𝜑 → ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) = ( 𝐴 ( -g ‘ 𝑃 ) ( 0g ‘ 𝑃 ) ) )
57		eqid	⊢ ( -g ‘ 𝑃 ) = ( -g ‘ 𝑃 )
58	2 18 57	grpsubid1	⊢ ( ( 𝑃 ∈ Grp ∧ 𝐴 ∈ 𝑈 ) → ( 𝐴 ( -g ‘ 𝑃 ) ( 0g ‘ 𝑃 ) ) = 𝐴 )
59	21 7 58	syl2anc	⊢ ( 𝜑 → ( 𝐴 ( -g ‘ 𝑃 ) ( 0g ‘ 𝑃 ) ) = 𝐴 )
60	56 59	eqtr2d	⊢ ( 𝜑 → 𝐴 = ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) )
61	60	fveq2d	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) ) )
62	61	breq1d	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐴 ) < ( 𝐷 ‘ 𝐵 ) ↔ ( 𝐷 ‘ ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) ) < ( 𝐷 ‘ 𝐵 ) ) )
63	32	biantrurd	⊢ ( 𝜑 → ( ( 𝐷 ‘ ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) ) < ( 𝐷 ‘ 𝐵 ) ↔ ( ( 0g ‘ 𝑃 ) ∈ 𝑈 ∧ ( 𝐷 ‘ ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) ) < ( 𝐷 ‘ 𝐵 ) ) ) )
64	10 1 2 6 57 11 3	q1peqb	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑁 ) → ( ( ( 0g ‘ 𝑃 ) ∈ 𝑈 ∧ ( 𝐷 ‘ ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) ) < ( 𝐷 ‘ 𝐵 ) ) ↔ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
65	9 7 8 64	syl3anc	⊢ ( 𝜑 → ( ( ( 0g ‘ 𝑃 ) ∈ 𝑈 ∧ ( 𝐷 ‘ ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) ) < ( 𝐷 ‘ 𝐵 ) ) ↔ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
66	62 63 65	3bitrd	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐴 ) < ( 𝐷 ‘ 𝐵 ) ↔ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
67	54 66	bitr4d	⊢ ( 𝜑 → ( ( 𝐴 𝐸 𝐵 ) = 𝐴 ↔ ( 𝐷 ‘ 𝐴 ) < ( 𝐷 ‘ 𝐵 ) ) )