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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ∃! 𝑞 ∈ 𝐵 ( 𝐷 ‘ ( 𝐹 − ( 𝑞 ∙ 𝐺 ) ) ) < ( 𝐷 ‘ 𝐺 ) )