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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
orngmul.1 ⊢ ≤ = ( le ‘ 𝑅 )
orngmul.2 ⊢ 0 = ( 0g ‘ 𝑅 )
orngmul.3 ⊢ · = ( .r ‘ 𝑅 )
Assertion orngsqr ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ) → 0 ≤ ( 𝑋 · 𝑋 ) )

Proof

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