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	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply1divalg.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	ply1divalg.b	$$⊢B={\mathrm{Base}}_P$$
	ply1divalg.m	$$⊢\underset{\dot{}}{-}={-}_P$$
	ply1divalg.z	$$⊢\underset{\dot{}}{0}=0_P$$
	ply1divalg.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_P$$
	ply1divalg.r1	$$⊢\phi \to R\in \mathrm{Ring}$$
	ply1divalg.f	$$⊢\phi \to F\in B$$
	ply1divalg.g1	$$⊢\phi \to G\in B$$
	ply1divalg.g2	$$⊢\phi \to G\ne \underset{\dot{}}{0}$$
	ply1divalg.g3	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\in U$$
	ply1divalg.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
Assertion	ply1divalg2	$$⊢\phi \to \exists !q\in BD\left(F\underset{\dot{}}{-}\left(q\underset{\dot{}}{\bullet }G\right)\right)<D\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		ply1divalg.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		ply1divalg.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
3		ply1divalg.b	$$⊢B={\mathrm{Base}}_P$$
4		ply1divalg.m	$$⊢\underset{\dot{}}{-}={-}_P$$
5		ply1divalg.z	$$⊢\underset{\dot{}}{0}=0_P$$
6		ply1divalg.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_P$$
7		ply1divalg.r1	$$⊢\phi \to R\in \mathrm{Ring}$$
8		ply1divalg.f	$$⊢\phi \to F\in B$$
9		ply1divalg.g1	$$⊢\phi \to G\in B$$
10		ply1divalg.g2	$$⊢\phi \to G\ne \underset{\dot{}}{0}$$
11		ply1divalg.g3	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\in U$$
12		ply1divalg.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
13		eqid	$$⊢{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)={\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)$$
14		eqidd	$$⊢\top \to {\mathrm{Base}}_R={\mathrm{Base}}_R$$
15		eqid	$$⊢{opp}_r\left(R\right)={opp}_r\left(R\right)$$
16		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
17	15 16	opprbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{{opp}_r\left(R\right)}$$
18	17	a1i	$$⊢\top \to {\mathrm{Base}}_R={\mathrm{Base}}_{{opp}_r\left(R\right)}$$
19		eqid	$$⊢{+}_R={+}_R$$
20	15 19	oppradd	$$⊢{+}_R={+}_{{opp}_r\left(R\right)}$$
21	20	oveqi	$$⊢q{+}_{R}r=q{+}_{{opp}_r\left(R\right)}r$$
22	21	a1i	$$⊢\left(\top \wedge \left(q\in {\mathrm{Base}}_R\wedge r\in {\mathrm{Base}}_R\right)\right)\to q{+}_{R}r=q{+}_{{opp}_r\left(R\right)}r$$
23	14 18 22	deg1propd	$$⊢\top \to {\mathrm{deg}}_1\left(R\right)={\mathrm{deg}}_1\left({opp}_r\left(R\right)\right)$$
24	23	mptru	$$⊢{\mathrm{deg}}_1\left(R\right)={\mathrm{deg}}_1\left({opp}_r\left(R\right)\right)$$
25	2 24	eqtri	$$⊢D={\mathrm{deg}}_1\left({opp}_r\left(R\right)\right)$$
26	1	fveq2i	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
27	14 18 22	ply1baspropd	$$⊢\top \to {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}$$
28	27	mptru	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}$$
29	26 28	eqtri	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}$$
30	3 29	eqtri	$$⊢B={\mathrm{Base}}_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}$$
31	29	a1i	$$⊢\top \to {\mathrm{Base}}_P={\mathrm{Base}}_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}$$
32	1	fveq2i	$$⊢{+}_P={+}_{{\mathrm{Poly}}_1\left(R\right)}$$
33	14 18 22	ply1plusgpropd	$$⊢\top \to {+}_{{\mathrm{Poly}}_1\left(R\right)}={+}_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}$$
34	33	mptru	$$⊢{+}_{{\mathrm{Poly}}_1\left(R\right)}={+}_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}$$
35	32 34	eqtri	$$⊢{+}_P={+}_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}$$
36	35	a1i	$$⊢\top \to {+}_P={+}_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}$$
37	31 36	grpsubpropd	$$⊢\top \to {-}_P={-}_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}$$
38	37	mptru	$$⊢{-}_P={-}_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}$$
39	4 38	eqtri	$$⊢\underset{\dot{}}{-}={-}_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}$$
40	3	a1i	$$⊢\top \to B={\mathrm{Base}}_P$$
41	30	a1i	$$⊢\top \to B={\mathrm{Base}}_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}$$
42	35	oveqi	$$⊢q{+}_{P}r=q{+}_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}r$$
43	42	a1i	$$⊢\left(\top \wedge \left(q\in B\wedge r\in B\right)\right)\to q{+}_{P}r=q{+}_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}r$$
44	40 41 43	grpidpropd	$$⊢\top \to 0_P=0_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}$$
45	44	mptru	$$⊢0_P=0_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}$$
46	5 45	eqtri	$$⊢\underset{\dot{}}{0}=0_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}$$
47		eqid	$$⊢{\cdot }_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}={\cdot }_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}$$
48	15	opprring	$$⊢R\in \mathrm{Ring}\to {opp}_r\left(R\right)\in \mathrm{Ring}$$
49	7 48	syl	$$⊢\phi \to {opp}_r\left(R\right)\in \mathrm{Ring}$$
50	12 15	opprunit	$$⊢U=\mathrm{Unit}\left({opp}_r\left(R\right)\right)$$
51	13 25 30 39 46 47 49 8 9 10 11 50	ply1divalg	$$⊢\phi \to \exists !q\in BD\left(F\underset{\dot{}}{-}\left(G{\cdot }_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}q\right)\right)<D\left(G\right)$$
52	7	adantr	$$⊢\left(\phi \wedge q\in B\right)\to R\in \mathrm{Ring}$$
53	9	adantr	$$⊢\left(\phi \wedge q\in B\right)\to G\in B$$
54		simpr	$$⊢\left(\phi \wedge q\in B\right)\to q\in B$$
55	1 15 13 6 47 3	ply1opprmul	$$⊢\left(R\in \mathrm{Ring}\wedge G\in B\wedge q\in B\right)\to G{\cdot }_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}q=q\underset{\dot{}}{\bullet }G$$
56	52 53 54 55	syl3anc	$$⊢\left(\phi \wedge q\in B\right)\to G{\cdot }_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}q=q\underset{\dot{}}{\bullet }G$$
57	56	eqcomd	$$⊢\left(\phi \wedge q\in B\right)\to q\underset{\dot{}}{\bullet }G=G{\cdot }_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}q$$
58	57	oveq2d	$$⊢\left(\phi \wedge q\in B\right)\to F\underset{\dot{}}{-}\left(q\underset{\dot{}}{\bullet }G\right)=F\underset{\dot{}}{-}\left(G{\cdot }_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}q\right)$$
59	58	fveq2d	$$⊢\left(\phi \wedge q\in B\right)\to D\left(F\underset{\dot{}}{-}\left(q\underset{\dot{}}{\bullet }G\right)\right)=D\left(F\underset{\dot{}}{-}\left(G{\cdot }_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}q\right)\right)$$
60	59	breq1d	$$⊢\left(\phi \wedge q\in B\right)\to \left(D\left(F\underset{\dot{}}{-}\left(q\underset{\dot{}}{\bullet }G\right)\right)<D\left(G\right)\leftrightarrow D\left(F\underset{\dot{}}{-}\left(G{\cdot }_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}q\right)\right)<D\left(G\right)\right)$$
61	60	reubidva	$$⊢\phi \to \left(\exists !q\in BD\left(F\underset{\dot{}}{-}\left(q\underset{\dot{}}{\bullet }G\right)\right)<D\left(G\right)\leftrightarrow \exists !q\in BD\left(F\underset{\dot{}}{-}\left(G{\cdot }_{{\mathrm{Poly}}_1\left({opp}_r\left(R\right)\right)}q\right)\right)<D\left(G\right)\right)$$
62	51 61	mpbird	$$⊢\phi \to \exists !q\in BD\left(F\underset{\dot{}}{-}\left(q\underset{\dot{}}{\bullet }G\right)\right)<D\left(G\right)$$