This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 26 11 13 24 4syl ⊢ ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ) → 0 ∈ 𝐵 )
28 simpr ⊢ ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
29 26 27 28 3jca ⊢ ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑅 ∈ oRing ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
30 eqid ⊢ ( lt ‘ 𝑅 ) = ( lt ‘ 𝑅 )
31 2 30 pltle ⊢ ( ( 𝑅 ∈ oRing ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 0 ( lt ‘ 𝑅 ) 𝑋 → 0 ≤ 𝑋 ) )
32 31 con3dimp ⊢ ( ( ( 𝑅 ∈ oRing ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 0 ≤ 𝑋 ) → ¬ 0 ( lt ‘ 𝑅 ) 𝑋 )
33 29 32 sylan ⊢ ( ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 0 ≤ 𝑋 ) → ¬ 0 ( lt ‘ 𝑅 ) 𝑋 )
34 omndtos ⊢ ( 𝑅 ∈ oMnd → 𝑅 ∈ Toset )
35 1 2 30 tosso ⊢ ( 𝑅 ∈ Toset → ( 𝑅 ∈ Toset ↔ ( ( lt ‘ 𝑅 ) Or 𝐵 ∧ ( I ↾ 𝐵 ) ⊆ ≤ ) ) )
36 35 ibi ⊢ ( 𝑅 ∈ Toset → ( ( lt ‘ 𝑅 ) Or 𝐵 ∧ ( I ↾ 𝐵 ) ⊆ ≤ ) )
37 36 simpld ⊢ ( 𝑅 ∈ Toset → ( lt ‘ 𝑅 ) Or 𝐵 )
38 10 22 34 37 4syl ⊢ ( ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 0 ≤ 𝑋 ) → ( lt ‘ 𝑅 ) Or 𝐵 )
39 solin ⊢ ( ( ( lt ‘ 𝑅 ) Or 𝐵 ∧ ( 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( 0 ( lt ‘ 𝑅 ) 𝑋 ∨ 0 = 𝑋 ∨ 𝑋 ( lt ‘ 𝑅 ) 0 ) )
40 38 25 15 39 syl12anc ⊢ ( ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 0 ≤ 𝑋 ) → ( 0 ( lt ‘ 𝑅 ) 𝑋 ∨ 0 = 𝑋 ∨ 𝑋 ( lt ‘ 𝑅 ) 0 ) )
41 3orass ⊢ ( ( 0 ( lt ‘ 𝑅 ) 𝑋 ∨ 0 = 𝑋 ∨ 𝑋 ( lt ‘ 𝑅 ) 0 ) ↔ ( 0 ( lt ‘ 𝑅 ) 𝑋 ∨ ( 0 = 𝑋 ∨ 𝑋 ( lt ‘ 𝑅 ) 0 ) ) )
42 40 41 sylib ⊢ ( ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 0 ≤ 𝑋 ) → ( 0 ( lt ‘ 𝑅 ) 𝑋 ∨ ( 0 = 𝑋 ∨ 𝑋 ( lt ‘ 𝑅 ) 0 ) ) )
43 orel1 ⊢ ( ¬ 0 ( lt ‘ 𝑅 ) 𝑋 → ( ( 0 ( lt ‘ 𝑅 ) 𝑋 ∨ ( 0 = 𝑋 ∨ 𝑋 ( lt ‘ 𝑅 ) 0 ) ) → ( 0 = 𝑋 ∨ 𝑋 ( lt ‘ 𝑅 ) 0 ) ) )
44 33 42 43 sylc ⊢ ( ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 0 ≤ 𝑋 ) → ( 0 = 𝑋 ∨ 𝑋 ( lt ‘ 𝑅 ) 0 ) )
45 orcom ⊢ ( ( 0 = 𝑋 ∨ 𝑋 ( lt ‘ 𝑅 ) 0 ) ↔ ( 𝑋 ( lt ‘ 𝑅 ) 0 ∨ 0 = 𝑋 ) )
46 eqcom ⊢ ( 0 = 𝑋 ↔ 𝑋 = 0 )
47 46 orbi2i ⊢ ( ( 𝑋 ( lt ‘ 𝑅 ) 0 ∨ 0 = 𝑋 ) ↔ ( 𝑋 ( lt ‘ 𝑅 ) 0 ∨ 𝑋 = 0 ) )
48 45 47 bitri ⊢ ( ( 0 = 𝑋 ∨ 𝑋 ( lt ‘ 𝑅 ) 0 ) ↔ ( 𝑋 ( lt ‘ 𝑅 ) 0 ∨ 𝑋 = 0 ) )
49 44 48 sylib ⊢ ( ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 0 ≤ 𝑋 ) → ( 𝑋 ( lt ‘ 𝑅 ) 0 ∨ 𝑋 = 0 ) )
50 tospos ⊢ ( 𝑅 ∈ Toset → 𝑅 ∈ Poset )
51 10 22 34 50 4syl ⊢ ( ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 0 ≤ 𝑋 ) → 𝑅 ∈ Poset )
52 1 2 30 pleval2 ⊢ ( ( 𝑅 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) → ( 𝑋 ≤ 0 ↔ ( 𝑋 ( lt ‘ 𝑅 ) 0 ∨ 𝑋 = 0 ) ) )
53 51 15 25 52 syl3anc ⊢ ( ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 0 ≤ 𝑋 ) → ( 𝑋 ≤ 0 ↔ ( 𝑋 ( lt ‘ 𝑅 ) 0 ∨ 𝑋 = 0 ) ) )
54 49 53 mpbird ⊢ ( ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 0 ≤ 𝑋 ) → 𝑋 ≤ 0 )
55 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
56 1 2 55 omndadd ⊢ ( ( 𝑅 ∈ oMnd ∧ ( 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ∈ 𝐵 ) ∧ 𝑋 ≤ 0 ) → ( 𝑋 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ) ≤ ( 0 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ) )
57 23 15 25 18 54 56 syl131anc ⊢ ( ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 0 ≤ 𝑋 ) → ( 𝑋 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ) ≤ ( 0 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ) )
58 1 55 3 16 grprinv ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ) = 0 )
59 14 15 58 syl2anc ⊢ ( ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 0 ≤ 𝑋 ) → ( 𝑋 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ) = 0 )
60 1 55 3 grplid ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ∈ 𝐵 ) → ( 0 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ) = ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) )
61 14 18 60 syl2anc ⊢ ( ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 0 ≤ 𝑋 ) → ( 0 ( +g ‘ 𝑅 ) ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ) = ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) )
62 57 59 61 3brtr3d ⊢ ( ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 0 ≤ 𝑋 ) → 0 ≤ ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) )
63 1 2 3 4 orngmul ⊢ ( ( 𝑅 ∈ oRing ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ∈ 𝐵 ∧ 0 ≤ ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ) ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ∈ 𝐵 ∧ 0 ≤ ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ) ) → 0 ≤ ( ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) · ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ) )
64 10 18 62 18 62 63 syl122anc ⊢ ( ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 0 ≤ 𝑋 ) → 0 ≤ ( ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) · ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ) )
65 1 4 16 12 15 15 ringm2neg ⊢ ( ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 0 ≤ 𝑋 ) → ( ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) · ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ) = ( 𝑋 · 𝑋 ) )
66 64 65 breqtrd ⊢ ( ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 0 ≤ 𝑋 ) → 0 ≤ ( 𝑋 · 𝑋 ) )
67 9 66 pm2.61dan ⊢ ( ( 𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐵 ) → 0 ≤ ( 𝑋 · 𝑋 ) )