# Metamath Proof Explorer

## Theorem orngsqr

Description: In an ordered ring, all squares are positive. (Contributed by Thierry Arnoux, 20-Jan-2018)

Ref Expression
Hypotheses orngmul.0 ${⊢}{B}={\mathrm{Base}}_{{R}}$
orngmul.1
orngmul.2
orngmul.3
Assertion orngsqr

### Proof

Step Hyp Ref Expression
1 orngmul.0 ${⊢}{B}={\mathrm{Base}}_{{R}}$
2 orngmul.1
3 orngmul.2
4 orngmul.3
5 simpll
6 simplr
7 simpr
8 1 2 3 4 orngmul
9 5 6 7 6 7 8 syl122anc
10 simpll
11 orngring ${⊢}{R}\in \mathrm{oRing}\to {R}\in \mathrm{Ring}$
13 ringgrp ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Grp}$
14 12 13 syl
15 simplr
16 eqid ${⊢}{inv}_{g}\left({R}\right)={inv}_{g}\left({R}\right)$
17 1 16 grpinvcl ${⊢}\left({R}\in \mathrm{Grp}\wedge {X}\in {B}\right)\to {inv}_{g}\left({R}\right)\left({X}\right)\in {B}$
18 14 15 17 syl2anc
19 orngogrp ${⊢}{R}\in \mathrm{oRing}\to {R}\in \mathrm{oGrp}$
20 isogrp ${⊢}{R}\in \mathrm{oGrp}↔\left({R}\in \mathrm{Grp}\wedge {R}\in \mathrm{oMnd}\right)$
21 20 simprbi ${⊢}{R}\in \mathrm{oGrp}\to {R}\in \mathrm{oMnd}$
22 19 21 syl ${⊢}{R}\in \mathrm{oRing}\to {R}\in \mathrm{oMnd}$
23 10 22 syl
24 1 3 grpidcl
25 14 24 syl
26 simpl ${⊢}\left({R}\in \mathrm{oRing}\wedge {X}\in {B}\right)\to {R}\in \mathrm{oRing}$
27 11 13 24 3syl
28 26 27 syl
29 simpr ${⊢}\left({R}\in \mathrm{oRing}\wedge {X}\in {B}\right)\to {X}\in {B}$
30 26 28 29 3jca
31 eqid ${⊢}{<}_{{R}}={<}_{{R}}$
32 2 31 pltle
33 32 con3dimp
34 30 33 sylan
35 omndtos ${⊢}{R}\in \mathrm{oMnd}\to {R}\in \mathrm{Toset}$
36 22 35 syl ${⊢}{R}\in \mathrm{oRing}\to {R}\in \mathrm{Toset}$
37 1 2 31 tosso
38 37 ibi
39 38 simpld ${⊢}{R}\in \mathrm{Toset}\to {<}_{{R}}\mathrm{Or}{B}$
40 10 36 39 3syl
41 solin
42 40 25 15 41 syl12anc
43 3orass
44 42 43 sylib
45 orel1
46 34 44 45 sylc
47 orcom
48 eqcom
49 48 orbi2i
50 47 49 bitri
51 46 50 sylib
52 tospos ${⊢}{R}\in \mathrm{Toset}\to {R}\in \mathrm{Poset}$
53 10 36 52 3syl
54 1 2 31 pleval2
55 53 15 25 54 syl3anc
56 51 55 mpbird
57 eqid ${⊢}{+}_{{R}}={+}_{{R}}$