Metamath Proof Explorer


Theorem orngrmulle

Description: In an ordered ring, multiplication with a positive does not change comparison. (Contributed by Thierry Arnoux, 10-Apr-2018)

Ref Expression
Hypotheses ornglmullt.b B=BaseR
ornglmullt.t ·˙=R
ornglmullt.0 0˙=0R
ornglmullt.1 φRoRing
ornglmullt.2 φXB
ornglmullt.3 φYB
ornglmullt.4 φZB
orngmulle.l ˙=R
orngmulle.5 φX˙Y
orngmulle.6 φ0˙˙Z
Assertion orngrmulle φX·˙Z˙Y·˙Z

Proof

Step Hyp Ref Expression
1 ornglmullt.b B=BaseR
2 ornglmullt.t ·˙=R
3 ornglmullt.0 0˙=0R
4 ornglmullt.1 φRoRing
5 ornglmullt.2 φXB
6 ornglmullt.3 φYB
7 ornglmullt.4 φZB
8 orngmulle.l ˙=R
9 orngmulle.5 φX˙Y
10 orngmulle.6 φ0˙˙Z
11 orngogrp RoRingRoGrp
12 4 11 syl φRoGrp
13 isogrp RoGrpRGrpRoMnd
14 13 simprbi RoGrpRoMnd
15 12 14 syl φRoMnd
16 orngring RoRingRRing
17 4 16 syl φRRing
18 ringgrp RRingRGrp
19 17 18 syl φRGrp
20 1 3 grpidcl RGrp0˙B
21 19 20 syl φ0˙B
22 1 2 ringcl RRingYBZBY·˙ZB
23 17 6 7 22 syl3anc φY·˙ZB
24 1 2 ringcl RRingXBZBX·˙ZB
25 17 5 7 24 syl3anc φX·˙ZB
26 eqid -R=-R
27 1 26 grpsubcl RGrpY·˙ZBX·˙ZBY·˙Z-RX·˙ZB
28 19 23 25 27 syl3anc φY·˙Z-RX·˙ZB
29 1 26 grpsubcl RGrpYBXBY-RXB
30 19 6 5 29 syl3anc φY-RXB
31 1 3 26 grpsubid RGrpXBX-RX=0˙
32 19 5 31 syl2anc φX-RX=0˙
33 1 8 26 ogrpsub RoGrpXBYBXBX˙YX-RX˙Y-RX
34 12 5 6 5 9 33 syl131anc φX-RX˙Y-RX
35 32 34 eqbrtrrd φ0˙˙Y-RX
36 1 8 3 2 orngmul RoRingY-RXB0˙˙Y-RXZB0˙˙Z0˙˙Y-RX·˙Z
37 4 30 35 7 10 36 syl122anc φ0˙˙Y-RX·˙Z
38 1 2 26 17 6 5 7 ringsubdir φY-RX·˙Z=Y·˙Z-RX·˙Z
39 37 38 breqtrd φ0˙˙Y·˙Z-RX·˙Z
40 eqid +R=+R
41 1 8 40 omndadd RoMnd0˙BY·˙Z-RX·˙ZBX·˙ZB0˙˙Y·˙Z-RX·˙Z0˙+RX·˙Z˙Y·˙Z-RX·˙Z+RX·˙Z
42 15 21 28 25 39 41 syl131anc φ0˙+RX·˙Z˙Y·˙Z-RX·˙Z+RX·˙Z
43 1 40 3 grplid RGrpX·˙ZB0˙+RX·˙Z=X·˙Z
44 19 25 43 syl2anc φ0˙+RX·˙Z=X·˙Z
45 1 40 26 grpnpcan RGrpY·˙ZBX·˙ZBY·˙Z-RX·˙Z+RX·˙Z=Y·˙Z
46 19 23 25 45 syl3anc φY·˙Z-RX·˙Z+RX·˙Z=Y·˙Z
47 42 44 46 3brtr3d φX·˙Z˙Y·˙Z