Theorem ply1divalg2

Description: Reverse the order of multiplication in ply1divalg via the opposite ring. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	ply1divalg.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1divalg.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	ply1divalg.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	ply1divalg.m	⊢ − = ( -g ‘ 𝑃 )
	ply1divalg.z	⊢ 0 = ( 0g ‘ 𝑃 )
	ply1divalg.t	⊢ ∙ = ( .r ‘ 𝑃 )
	ply1divalg.r1	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	ply1divalg.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	ply1divalg.g1	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
	ply1divalg.g2	⊢ ( 𝜑 → 𝐺 ≠ 0 )
	ply1divalg.g3	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ 𝑈 )
	ply1divalg.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
Assertion	ply1divalg2	⊢ ( 𝜑 → ∃! 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝑞 ∙ 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		ply1divalg.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1divalg.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
3		ply1divalg.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		ply1divalg.m	⊢ − = ( -g ‘ 𝑃 )
5		ply1divalg.z	⊢ 0 = ( 0g ‘ 𝑃 )
6		ply1divalg.t	⊢ ∙ = ( .r ‘ 𝑃 )
7		ply1divalg.r1	⊢ ( 𝜑 → 𝑅 ∈ Ring )
8		ply1divalg.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
9		ply1divalg.g1	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
10		ply1divalg.g2	⊢ ( 𝜑 → 𝐺 ≠ 0 )
11		ply1divalg.g3	⊢ ( 𝜑 → ( ( coe1 ‘ 𝐺 ) ‘ ( 𝐷 ‘ 𝐺 ) ) ∈ 𝑈 )
12		ply1divalg.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
13		eqid	⊢ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) = ( Poly1 ‘ ( oppr ‘ 𝑅 ) )
14		eqidd	⊢ ( ⊤ → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
15		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
16		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
17	15 16	opprbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( oppr ‘ 𝑅 ) )
18	17	a1i	⊢ ( ⊤ → ( Base ‘ 𝑅 ) = ( Base ‘ ( oppr ‘ 𝑅 ) ) )
19		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
20	15 19	oppradd	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ ( oppr ‘ 𝑅 ) )
21	20	oveqi	⊢ ( 𝑞 ( +g ‘ 𝑅 ) 𝑟 ) = ( 𝑞 ( +g ‘ ( oppr ‘ 𝑅 ) ) 𝑟 )
22	21	a1i	⊢ ( ( ⊤ ∧ ( 𝑞 ∈ ( Base ‘ 𝑅 ) ∧ 𝑟 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑞 ( +g ‘ 𝑅 ) 𝑟 ) = ( 𝑞 ( +g ‘ ( oppr ‘ 𝑅 ) ) 𝑟 ) )
23	14 18 22	deg1propd	⊢ ( ⊤ → ( deg1 ‘ 𝑅 ) = ( deg1 ‘ ( oppr ‘ 𝑅 ) ) )
24	23	mptru	⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ ( oppr ‘ 𝑅 ) )
25	2 24	eqtri	⊢ 𝐷 = ( deg1 ‘ ( oppr ‘ 𝑅 ) )
26	1	fveq2i	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
27	14 18 22	ply1baspropd	⊢ ( ⊤ → ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) ) )
28	27	mptru	⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) )
29	26 28	eqtri	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) )
30	3 29	eqtri	⊢ 𝐵 = ( Base ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) )
31	29	a1i	⊢ ( ⊤ → ( Base ‘ 𝑃 ) = ( Base ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) ) )
32	1	fveq2i	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ ( Poly1 ‘ 𝑅 ) )
33	14 18 22	ply1plusgpropd	⊢ ( ⊤ → ( +g ‘ ( Poly1 ‘ 𝑅 ) ) = ( +g ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) ) )
34	33	mptru	⊢ ( +g ‘ ( Poly1 ‘ 𝑅 ) ) = ( +g ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) )
35	32 34	eqtri	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) )
36	35	a1i	⊢ ( ⊤ → ( +g ‘ 𝑃 ) = ( +g ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) ) )
37	31 36	grpsubpropd	⊢ ( ⊤ → ( -g ‘ 𝑃 ) = ( -g ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) ) )
38	37	mptru	⊢ ( -g ‘ 𝑃 ) = ( -g ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) )
39	4 38	eqtri	⊢ − = ( -g ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) )
40	3	a1i	⊢ ( ⊤ → 𝐵 = ( Base ‘ 𝑃 ) )
41	30	a1i	⊢ ( ⊤ → 𝐵 = ( Base ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) ) )
42	35	oveqi	⊢ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) = ( 𝑞 ( +g ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) ) 𝑟 )
43	42	a1i	⊢ ( ( ⊤ ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) = ( 𝑞 ( +g ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) ) 𝑟 ) )
44	40 41 43	grpidpropd	⊢ ( ⊤ → ( 0g ‘ 𝑃 ) = ( 0g ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) ) )
45	44	mptru	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) )
46	5 45	eqtri	⊢ 0 = ( 0g ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) )
47		eqid	⊢ ( .r ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) ) = ( .r ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) )
48	15	opprring	⊢ ( 𝑅 ∈ Ring → ( oppr ‘ 𝑅 ) ∈ Ring )
49	7 48	syl	⊢ ( 𝜑 → ( oppr ‘ 𝑅 ) ∈ Ring )
50	12 15	opprunit	⊢ 𝑈 = ( Unit ‘ ( oppr ‘ 𝑅 ) )
51	13 25 30 39 46 47 49 8 9 10 11 50	ply1divalg	⊢ ( 𝜑 → ∃! 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ( .r ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) ) 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) )
52	7	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → 𝑅 ∈ Ring )
53	9	adantr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → 𝐺 ∈ 𝐵 )
54		simpr	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → 𝑞 ∈ 𝐵 )
55	1 15 13 6 47 3	ply1opprmul	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) → ( 𝐺 ( .r ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) ) 𝑞 ) = ( 𝑞 ∙ 𝐺 ) )
56	52 53 54 55	syl3anc	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( 𝐺 ( .r ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) ) 𝑞 ) = ( 𝑞 ∙ 𝐺 ) )
57	56	eqcomd	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( 𝑞 ∙ 𝐺 ) = ( 𝐺 ( .r ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) ) 𝑞 ) )
58	57	oveq2d	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( 𝐹 − ( 𝑞 ∙ 𝐺 ) ) = ( 𝐹 − ( 𝐺 ( .r ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) ) 𝑞 ) ) )
59	58	fveq2d	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( 𝐷 ‘ ( 𝐹 − ( 𝑞 ∙ 𝐺 ) ) ) = ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ( .r ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) ) 𝑞 ) ) ) )
60	59	breq1d	⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐵 ) → ( ( 𝐷 ‘ ( 𝐹 − ( 𝑞 ∙ 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ( .r ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) ) 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
61	60	reubidva	⊢ ( 𝜑 → ( ∃! 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝑞 ∙ 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) ↔ ∃! 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝐺 ( .r ‘ ( Poly1 ‘ ( oppr ‘ 𝑅 ) ) ) 𝑞 ) ) ) < ( 𝐷 ‘ 𝐺 ) ) )
62	51 61	mpbird	⊢ ( 𝜑 → ∃! 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝑞 ∙ 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) )