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 = ( Base ` R )
orngmul.1 
|- .<_ = ( le ` R )
orngmul.2 
|- .0. = ( 0g ` R )
orngmul.3 
|- .x. = ( .r ` R )
Assertion orngsqr 
|- ( ( R e. oRing /\ X e. B ) -> .0. .<_ ( X .x. X ) )

Proof

Step Hyp Ref Expression
1 orngmul.0 
 |-  B = ( Base ` R )
2 orngmul.1 
 |-  .<_ = ( le ` R )
3 orngmul.2 
 |-  .0. = ( 0g ` R )
4 orngmul.3 
 |-  .x. = ( .r ` R )
5 simpll 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ .0. .<_ X ) -> R e. oRing )
6 simplr 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ .0. .<_ X ) -> X e. B )
7 simpr 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ .0. .<_ X ) -> .0. .<_ X )
8 1 2 3 4 orngmul 
 |-  ( ( R e. oRing /\ ( X e. B /\ .0. .<_ X ) /\ ( X e. B /\ .0. .<_ X ) ) -> .0. .<_ ( X .x. X ) )
9 5 6 7 6 7 8 syl122anc 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ .0. .<_ X ) -> .0. .<_ ( X .x. X ) )
10 simpll 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> R e. oRing )
11 orngring 
 |-  ( R e. oRing -> R e. Ring )
12 11 ad2antrr 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> R e. Ring )
13 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
14 12 13 syl 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> R e. Grp )
15 simplr 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> X e. B )
16 eqid 
 |-  ( invg ` R ) = ( invg ` R )
17 1 16 grpinvcl 
 |-  ( ( R e. Grp /\ X e. B ) -> ( ( invg ` R ) ` X ) e. B )
18 14 15 17 syl2anc 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> ( ( invg ` R ) ` X ) e. B )
19 orngogrp 
 |-  ( R e. oRing -> R e. oGrp )
20 isogrp 
 |-  ( R e. oGrp <-> ( R e. Grp /\ R e. oMnd ) )
21 20 simprbi 
 |-  ( R e. oGrp -> R e. oMnd )
22 19 21 syl 
 |-  ( R e. oRing -> R e. oMnd )
23 10 22 syl 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> R e. oMnd )
24 1 3 grpidcl 
 |-  ( R e. Grp -> .0. e. B )
25 14 24 syl 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> .0. e. B )
26 simpl 
 |-  ( ( R e. oRing /\ X e. B ) -> R e. oRing )
27 26 11 13 24 4syl 
 |-  ( ( R e. oRing /\ X e. B ) -> .0. e. B )
28 simpr 
 |-  ( ( R e. oRing /\ X e. B ) -> X e. B )
29 26 27 28 3jca 
 |-  ( ( R e. oRing /\ X e. B ) -> ( R e. oRing /\ .0. e. B /\ X e. B ) )
30 eqid 
 |-  ( lt ` R ) = ( lt ` R )
31 2 30 pltle 
 |-  ( ( R e. oRing /\ .0. e. B /\ X e. B ) -> ( .0. ( lt ` R ) X -> .0. .<_ X ) )
32 31 con3dimp 
 |-  ( ( ( R e. oRing /\ .0. e. B /\ X e. B ) /\ -. .0. .<_ X ) -> -. .0. ( lt ` R ) X )
33 29 32 sylan 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> -. .0. ( lt ` R ) X )
34 omndtos 
 |-  ( R e. oMnd -> R e. Toset )
35 1 2 30 tosso 
 |-  ( R e. Toset -> ( R e. Toset <-> ( ( lt ` R ) Or B /\ ( _I |` B ) C_ .<_ ) ) )
36 35 ibi 
 |-  ( R e. Toset -> ( ( lt ` R ) Or B /\ ( _I |` B ) C_ .<_ ) )
37 36 simpld 
 |-  ( R e. Toset -> ( lt ` R ) Or B )
38 10 22 34 37 4syl 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> ( lt ` R ) Or B )
39 solin 
 |-  ( ( ( lt ` R ) Or B /\ ( .0. e. B /\ X e. B ) ) -> ( .0. ( lt ` R ) X \/ .0. = X \/ X ( lt ` R ) .0. ) )
40 38 25 15 39 syl12anc 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> ( .0. ( lt ` R ) X \/ .0. = X \/ X ( lt ` R ) .0. ) )
41 3orass 
 |-  ( ( .0. ( lt ` R ) X \/ .0. = X \/ X ( lt ` R ) .0. ) <-> ( .0. ( lt ` R ) X \/ ( .0. = X \/ X ( lt ` R ) .0. ) ) )
42 40 41 sylib 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> ( .0. ( lt ` R ) X \/ ( .0. = X \/ X ( lt ` R ) .0. ) ) )
43 orel1 
 |-  ( -. .0. ( lt ` R ) X -> ( ( .0. ( lt ` R ) X \/ ( .0. = X \/ X ( lt ` R ) .0. ) ) -> ( .0. = X \/ X ( lt ` R ) .0. ) ) )
44 33 42 43 sylc 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> ( .0. = X \/ X ( lt ` R ) .0. ) )
45 orcom 
 |-  ( ( .0. = X \/ X ( lt ` R ) .0. ) <-> ( X ( lt ` R ) .0. \/ .0. = X ) )
46 eqcom 
 |-  ( .0. = X <-> X = .0. )
47 46 orbi2i 
 |-  ( ( X ( lt ` R ) .0. \/ .0. = X ) <-> ( X ( lt ` R ) .0. \/ X = .0. ) )
48 45 47 bitri 
 |-  ( ( .0. = X \/ X ( lt ` R ) .0. ) <-> ( X ( lt ` R ) .0. \/ X = .0. ) )
49 44 48 sylib 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> ( X ( lt ` R ) .0. \/ X = .0. ) )
50 tospos 
 |-  ( R e. Toset -> R e. Poset )
51 10 22 34 50 4syl 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> R e. Poset )
52 1 2 30 pleval2 
 |-  ( ( R e. Poset /\ X e. B /\ .0. e. B ) -> ( X .<_ .0. <-> ( X ( lt ` R ) .0. \/ X = .0. ) ) )
53 51 15 25 52 syl3anc 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> ( X .<_ .0. <-> ( X ( lt ` R ) .0. \/ X = .0. ) ) )
54 49 53 mpbird 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> X .<_ .0. )
55 eqid 
 |-  ( +g ` R ) = ( +g ` R )
56 1 2 55 omndadd 
 |-  ( ( R e. oMnd /\ ( X e. B /\ .0. e. B /\ ( ( invg ` R ) ` X ) e. B ) /\ X .<_ .0. ) -> ( X ( +g ` R ) ( ( invg ` R ) ` X ) ) .<_ ( .0. ( +g ` R ) ( ( invg ` R ) ` X ) ) )
57 23 15 25 18 54 56 syl131anc 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> ( X ( +g ` R ) ( ( invg ` R ) ` X ) ) .<_ ( .0. ( +g ` R ) ( ( invg ` R ) ` X ) ) )
58 1 55 3 16 grprinv 
 |-  ( ( R e. Grp /\ X e. B ) -> ( X ( +g ` R ) ( ( invg ` R ) ` X ) ) = .0. )
59 14 15 58 syl2anc 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> ( X ( +g ` R ) ( ( invg ` R ) ` X ) ) = .0. )
60 1 55 3 grplid 
 |-  ( ( R e. Grp /\ ( ( invg ` R ) ` X ) e. B ) -> ( .0. ( +g ` R ) ( ( invg ` R ) ` X ) ) = ( ( invg ` R ) ` X ) )
61 14 18 60 syl2anc 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> ( .0. ( +g ` R ) ( ( invg ` R ) ` X ) ) = ( ( invg ` R ) ` X ) )
62 57 59 61 3brtr3d 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> .0. .<_ ( ( invg ` R ) ` X ) )
63 1 2 3 4 orngmul 
 |-  ( ( R e. oRing /\ ( ( ( invg ` R ) ` X ) e. B /\ .0. .<_ ( ( invg ` R ) ` X ) ) /\ ( ( ( invg ` R ) ` X ) e. B /\ .0. .<_ ( ( invg ` R ) ` X ) ) ) -> .0. .<_ ( ( ( invg ` R ) ` X ) .x. ( ( invg ` R ) ` X ) ) )
64 10 18 62 18 62 63 syl122anc 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> .0. .<_ ( ( ( invg ` R ) ` X ) .x. ( ( invg ` R ) ` X ) ) )
65 1 4 16 12 15 15 ringm2neg 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> ( ( ( invg ` R ) ` X ) .x. ( ( invg ` R ) ` X ) ) = ( X .x. X ) )
66 64 65 breqtrd 
 |-  ( ( ( R e. oRing /\ X e. B ) /\ -. .0. .<_ X ) -> .0. .<_ ( X .x. X ) )
67 9 66 pm2.61dan 
 |-  ( ( R e. oRing /\ X e. B ) -> .0. .<_ ( X .x. X ) )