Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  orngsqr Structured version   Visualization version   GIF version
Theorem orngsqr 32411
Description: In an ordered ring, all squares are positive. (Contributed by Thierry Arnoux, 20-Jan-2018.)
Hypotheses
Ref Expression
orngmul.0 𝐡 = (Baseβ€˜π‘…)
orngmul.1 ≀ = (leβ€˜π‘…)
orngmul.2 0 = (0gβ€˜π‘…)
orngmul.3 Β· = (.rβ€˜π‘…)
Assertion
Ref Expression
orngsqr ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) β†’ 0 ≀ (𝑋 Β· 𝑋))
Proof of Theorem orngsqr
StepHypRef Expression
1 simpll 766 . . 3 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ 0 ≀ 𝑋) β†’ 𝑅 ∈ oRing)
2 simplr 768 . . 3 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ 0 ≀ 𝑋) β†’ 𝑋 ∈ 𝐡)
3 simpr 486 . . 3 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ 0 ≀ 𝑋) β†’ 0 ≀ 𝑋)
4 orngmul.0 . . . 4 𝐡 = (Baseβ€˜π‘…)
5 orngmul.1 . . . 4 ≀ = (leβ€˜π‘…)
6 orngmul.2 . . . 4 0 = (0gβ€˜π‘…)
7 orngmul.3 . . . 4 Β· = (.rβ€˜π‘…)
84, 5, 6, 7orngmul 32410 . . 3 ((𝑅 ∈ oRing ∧ (𝑋 ∈ 𝐡 ∧ 0 ≀ 𝑋) ∧ (𝑋 ∈ 𝐡 ∧ 0 ≀ 𝑋)) β†’ 0 ≀ (𝑋 Β· 𝑋))
91, 2, 3, 2, 3, 8syl122anc 1380 . 2 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ 0 ≀ 𝑋) β†’ 0 ≀ (𝑋 Β· 𝑋))
10 simpll 766 . . . 4 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ 𝑅 ∈ oRing)
11 orngring 32407 . . . . . . 7 (𝑅 ∈ oRing β†’ 𝑅 ∈ Ring)
1211ad2antrr 725 . . . . . 6 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ 𝑅 ∈ Ring)
13 ringgrp 20055 . . . . . 6 (𝑅 ∈ Ring β†’ 𝑅 ∈ Grp)
1412, 13syl 17 . . . . 5 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ 𝑅 ∈ Grp)
15 simplr 768 . . . . 5 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ 𝑋 ∈ 𝐡)
16 eqid 2733 . . . . . 6 (invgβ€˜π‘…) = (invgβ€˜π‘…)
174, 16grpinvcl 18869 . . . . 5 ((𝑅 ∈ Grp ∧ 𝑋 ∈ 𝐡) β†’ ((invgβ€˜π‘…)β€˜π‘‹) ∈ 𝐡)
1814, 15, 17syl2anc 585 . . . 4 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ ((invgβ€˜π‘…)β€˜π‘‹) ∈ 𝐡)
19 orngogrp 32408 . . . . . . . 8 (𝑅 ∈ oRing β†’ 𝑅 ∈ oGrp)
20 isogrp 32208 . . . . . . . . 9 (𝑅 ∈ oGrp ↔ (𝑅 ∈ Grp ∧ 𝑅 ∈ oMnd))
2120simprbi 498 . . . . . . . 8 (𝑅 ∈ oGrp β†’ 𝑅 ∈ oMnd)
2219, 21syl 17 . . . . . . 7 (𝑅 ∈ oRing β†’ 𝑅 ∈ oMnd)
2310, 22syl 17 . . . . . 6 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ 𝑅 ∈ oMnd)
244, 6grpidcl 18847 . . . . . . 7 (𝑅 ∈ Grp β†’ 0 ∈ 𝐡)
2514, 24syl 17 . . . . . 6 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ 0 ∈ 𝐡)
26 simpl 484 . . . . . . . . . . 11 ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) β†’ 𝑅 ∈ oRing)
2711, 13, 243syl 18 . . . . . . . . . . . 12 (𝑅 ∈ oRing β†’ 0 ∈ 𝐡)
2826, 27syl 17 . . . . . . . . . . 11 ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) β†’ 0 ∈ 𝐡)
29 simpr 486 . . . . . . . . . . 11 ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) β†’ 𝑋 ∈ 𝐡)
3026, 28, 293jca 1129 . . . . . . . . . 10 ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) β†’ (𝑅 ∈ oRing ∧ 0 ∈ 𝐡 ∧ 𝑋 ∈ 𝐡))
31 eqid 2733 . . . . . . . . . . . 12 (ltβ€˜π‘…) = (ltβ€˜π‘…)
325, 31pltle 18283 . . . . . . . . . . 11 ((𝑅 ∈ oRing ∧ 0 ∈ 𝐡 ∧ 𝑋 ∈ 𝐡) β†’ ( 0 (ltβ€˜π‘…)𝑋 β†’ 0 ≀ 𝑋))
3332con3dimp 410 . . . . . . . . . 10 (((𝑅 ∈ oRing ∧ 0 ∈ 𝐡 ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ Β¬ 0 (ltβ€˜π‘…)𝑋)
3430, 33sylan 581 . . . . . . . . 9 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ Β¬ 0 (ltβ€˜π‘…)𝑋)
35 omndtos 32211 . . . . . . . . . . . . 13 (𝑅 ∈ oMnd β†’ 𝑅 ∈ Toset)
3622, 35syl 17 . . . . . . . . . . . 12 (𝑅 ∈ oRing β†’ 𝑅 ∈ Toset)
374, 5, 31tosso 18369 . . . . . . . . . . . . . 14 (𝑅 ∈ Toset β†’ (𝑅 ∈ Toset ↔ ((ltβ€˜π‘…) Or 𝐡 ∧ ( I β†Ύ 𝐡) βŠ† ≀ )))
3837ibi 267 . . . . . . . . . . . . 13 (𝑅 ∈ Toset β†’ ((ltβ€˜π‘…) Or 𝐡 ∧ ( I β†Ύ 𝐡) βŠ† ≀ ))
3938simpld 496 . . . . . . . . . . . 12 (𝑅 ∈ Toset β†’ (ltβ€˜π‘…) Or 𝐡)
4010, 36, 393syl 18 . . . . . . . . . . 11 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ (ltβ€˜π‘…) Or 𝐡)
41 solin 5613 . . . . . . . . . . 11 (((ltβ€˜π‘…) Or 𝐡 ∧ ( 0 ∈ 𝐡 ∧ 𝑋 ∈ 𝐡)) β†’ ( 0 (ltβ€˜π‘…)𝑋 ∨ 0 = 𝑋 ∨ 𝑋(ltβ€˜π‘…) 0 ))
4240, 25, 15, 41syl12anc 836 . . . . . . . . . 10 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ ( 0 (ltβ€˜π‘…)𝑋 ∨ 0 = 𝑋 ∨ 𝑋(ltβ€˜π‘…) 0 ))
43 3orass 1091 . . . . . . . . . 10 (( 0 (ltβ€˜π‘…)𝑋 ∨ 0 = 𝑋 ∨ 𝑋(ltβ€˜π‘…) 0 ) ↔ ( 0 (ltβ€˜π‘…)𝑋 ∨ ( 0 = 𝑋 ∨ 𝑋(ltβ€˜π‘…) 0 )))
4442, 43sylib 217 . . . . . . . . 9 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ ( 0 (ltβ€˜π‘…)𝑋 ∨ ( 0 = 𝑋 ∨ 𝑋(ltβ€˜π‘…) 0 )))
45 orel1 888 . . . . . . . . 9 (Β¬ 0 (ltβ€˜π‘…)𝑋 β†’ (( 0 (ltβ€˜π‘…)𝑋 ∨ ( 0 = 𝑋 ∨ 𝑋(ltβ€˜π‘…) 0 )) β†’ ( 0 = 𝑋 ∨ 𝑋(ltβ€˜π‘…) 0 )))
4634, 44, 45sylc 65 . . . . . . . 8 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ ( 0 = 𝑋 ∨ 𝑋(ltβ€˜π‘…) 0 ))
47 orcom 869 . . . . . . . . 9 (( 0 = 𝑋 ∨ 𝑋(ltβ€˜π‘…) 0 ) ↔ (𝑋(ltβ€˜π‘…) 0 ∨ 0 = 𝑋))
48 eqcom 2740 . . . . . . . . . 10 ( 0 = 𝑋 ↔ 𝑋 = 0 )
4948orbi2i 912 . . . . . . . . 9 ((𝑋(ltβ€˜π‘…) 0 ∨ 0 = 𝑋) ↔ (𝑋(ltβ€˜π‘…) 0 ∨ 𝑋 = 0 ))
5047, 49bitri 275 . . . . . . . 8 (( 0 = 𝑋 ∨ 𝑋(ltβ€˜π‘…) 0 ) ↔ (𝑋(ltβ€˜π‘…) 0 ∨ 𝑋 = 0 ))
5146, 50sylib 217 . . . . . . 7 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ (𝑋(ltβ€˜π‘…) 0 ∨ 𝑋 = 0 ))
52 tospos 18370 . . . . . . . . 9 (𝑅 ∈ Toset β†’ 𝑅 ∈ Poset)
5310, 36, 523syl 18 . . . . . . . 8 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ 𝑅 ∈ Poset)
544, 5, 31pleval2 18287 . . . . . . . 8 ((𝑅 ∈ Poset ∧ 𝑋 ∈ 𝐡 ∧ 0 ∈ 𝐡) β†’ (𝑋 ≀ 0 ↔ (𝑋(ltβ€˜π‘…) 0 ∨ 𝑋 = 0 )))
5553, 15, 25, 54syl3anc 1372 . . . . . . 7 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ (𝑋 ≀ 0 ↔ (𝑋(ltβ€˜π‘…) 0 ∨ 𝑋 = 0 )))
5651, 55mpbird 257 . . . . . 6 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ 𝑋 ≀ 0 )
57 eqid 2733 . . . . . . 7 (+gβ€˜π‘…) = (+gβ€˜π‘…)
584, 5, 57omndadd 32212 . . . . . 6 ((𝑅 ∈ oMnd ∧ (𝑋 ∈ 𝐡 ∧ 0 ∈ 𝐡 ∧ ((invgβ€˜π‘…)β€˜π‘‹) ∈ 𝐡) ∧ 𝑋 ≀ 0 ) β†’ (𝑋(+gβ€˜π‘…)((invgβ€˜π‘…)β€˜π‘‹)) ≀ ( 0 (+gβ€˜π‘…)((invgβ€˜π‘…)β€˜π‘‹)))
5923, 15, 25, 18, 56, 58syl131anc 1384 . . . . 5 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ (𝑋(+gβ€˜π‘…)((invgβ€˜π‘…)β€˜π‘‹)) ≀ ( 0 (+gβ€˜π‘…)((invgβ€˜π‘…)β€˜π‘‹)))
604, 57, 6, 16grprinv 18872 . . . . . 6 ((𝑅 ∈ Grp ∧ 𝑋 ∈ 𝐡) β†’ (𝑋(+gβ€˜π‘…)((invgβ€˜π‘…)β€˜π‘‹)) = 0 )
6114, 15, 60syl2anc 585 . . . . 5 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ (𝑋(+gβ€˜π‘…)((invgβ€˜π‘…)β€˜π‘‹)) = 0 )
624, 57, 6grplid 18849 . . . . . 6 ((𝑅 ∈ Grp ∧ ((invgβ€˜π‘…)β€˜π‘‹) ∈ 𝐡) β†’ ( 0 (+gβ€˜π‘…)((invgβ€˜π‘…)β€˜π‘‹)) = ((invgβ€˜π‘…)β€˜π‘‹))
6314, 18, 62syl2anc 585 . . . . 5 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ ( 0 (+gβ€˜π‘…)((invgβ€˜π‘…)β€˜π‘‹)) = ((invgβ€˜π‘…)β€˜π‘‹))
6459, 61, 633brtr3d 5179 . . . 4 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ 0 ≀ ((invgβ€˜π‘…)β€˜π‘‹))
654, 5, 6, 7orngmul 32410 . . . 4 ((𝑅 ∈ oRing ∧ (((invgβ€˜π‘…)β€˜π‘‹) ∈ 𝐡 ∧ 0 ≀ ((invgβ€˜π‘…)β€˜π‘‹)) ∧ (((invgβ€˜π‘…)β€˜π‘‹) ∈ 𝐡 ∧ 0 ≀ ((invgβ€˜π‘…)β€˜π‘‹))) β†’ 0 ≀ (((invgβ€˜π‘…)β€˜π‘‹) Β· ((invgβ€˜π‘…)β€˜π‘‹)))
6610, 18, 64, 18, 64, 65syl122anc 1380 . . 3 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ 0 ≀ (((invgβ€˜π‘…)β€˜π‘‹) Β· ((invgβ€˜π‘…)β€˜π‘‹)))
674, 7, 16, 12, 15, 15ringm2neg 20112 . . 3 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ (((invgβ€˜π‘…)β€˜π‘‹) Β· ((invgβ€˜π‘…)β€˜π‘‹)) = (𝑋 Β· 𝑋))
6866, 67breqtrd 5174 . 2 (((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) ∧ Β¬ 0 ≀ 𝑋) β†’ 0 ≀ (𝑋 Β· 𝑋))
699, 68pm2.61dan 812 1 ((𝑅 ∈ oRing ∧ 𝑋 ∈ 𝐡) β†’ 0 ≀ (𝑋 Β· 𝑋))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∨ w3o 1087   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   βŠ† wss 3948   class class class wbr 5148   I cid 5573   Or wor 5587   β†Ύ cres 5678  β€˜cfv 6541  (class class class)co 7406  Basecbs 17141  +gcplusg 17194  .rcmulr 17195  lecple 17201  0gc0g 17382  Posetcpo 18257  ltcplt 18258  Tosetctos 18366  Grpcgrp 18816  invgcminusg 18817  Ringcrg 20050  oMndcomnd 32203  oGrpcogrp 32204  oRingcorng 32402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-nn 12210  df-2 12272  df-sets 17094  df-slot 17112  df-ndx 17124  df-base 17142  df-plusg 17207  df-0g 17384  df-proset 18245  df-poset 18263  df-plt 18280  df-toset 18367  df-mgm 18558  df-sgrp 18607  df-mnd 18623  df-grp 18819  df-minusg 18820  df-mgp 19983  df-ur 20000  df-ring 20052  df-omnd 32205  df-ogrp 32206  df-orng 32404
This theorem is referenced by:  orng0le1  32419
  Copyright terms: Public domain W3C validator