Theorem ogrpinv0le 31335

Description: In an ordered group, the ordering is compatible with group inverse. (Contributed by Thierry Arnoux, 3-Sep-2018.)

Hypotheses

Ref	Expression
ogrpsub.0	⊢ 𝐵 = (Base‘𝐺)
ogrpsub.1	⊢ ≤ = (le‘𝐺)
ogrpinv.2	⊢ 𝐼 = (invg‘𝐺)
ogrpinv.3	⊢ 0 = (0g‘𝐺)

Assertion

Ref	Expression
ogrpinv0le	⊢ ((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) → ( 0 ≤ 𝑋 ↔ (𝐼‘𝑋) ≤ 0 ))

Proof of Theorem ogrpinv0le

Step	Hyp	Ref	Expression
1		isogrp 31322	. . . . . 6 ⊢ (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd))
2	1	simprbi 497	. . . . 5 ⊢ (𝐺 ∈ oGrp → 𝐺 ∈ oMnd)
3	2	ad2antrr 723	. . . 4 ⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 ≤ 𝑋) → 𝐺 ∈ oMnd)
4		omndmnd 31324	. . . . 5 ⊢ (𝐺 ∈ oMnd → 𝐺 ∈ Mnd)
5		ogrpsub.0	. . . . . 6 ⊢ 𝐵 = (Base‘𝐺)
6		ogrpinv.3	. . . . . 6 ⊢ 0 = (0g‘𝐺)
7	5, 6	mndidcl 18396	. . . . 5 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)
8	3, 4, 7	3syl 18	. . . 4 ⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 ≤ 𝑋) → 0 ∈ 𝐵)
9		simplr 766	. . . 4 ⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 ≤ 𝑋) → 𝑋 ∈ 𝐵)
10		ogrpgrp 31323	. . . . . 6 ⊢ (𝐺 ∈ oGrp → 𝐺 ∈ Grp)
11	10	ad2antrr 723	. . . . 5 ⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 ≤ 𝑋) → 𝐺 ∈ Grp)
12		ogrpinv.2	. . . . . 6 ⊢ 𝐼 = (invg‘𝐺)
13	5, 12	grpinvcl 18623	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝐼‘𝑋) ∈ 𝐵)
14	11, 9, 13	syl2anc 584	. . . 4 ⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 ≤ 𝑋) → (𝐼‘𝑋) ∈ 𝐵)
15		simpr 485	. . . 4 ⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 ≤ 𝑋) → 0 ≤ 𝑋)
16		ogrpsub.1	. . . . 5 ⊢ ≤ = (le‘𝐺)
17		eqid 2740	. . . . 5 ⊢ (+g‘𝐺) = (+g‘𝐺)
18	5, 16, 17	omndadd 31326	. . . 4 ⊢ ((𝐺 ∈ oMnd ∧ ( 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ (𝐼‘𝑋) ∈ 𝐵) ∧ 0 ≤ 𝑋) → ( 0 (+g‘𝐺)(𝐼‘𝑋)) ≤ (𝑋(+g‘𝐺)(𝐼‘𝑋)))
19	3, 8, 9, 14, 15, 18	syl131anc 1382	. . 3 ⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 ≤ 𝑋) → ( 0 (+g‘𝐺)(𝐼‘𝑋)) ≤ (𝑋(+g‘𝐺)(𝐼‘𝑋)))
20	5, 17, 6	grplid 18605	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ (𝐼‘𝑋) ∈ 𝐵) → ( 0 (+g‘𝐺)(𝐼‘𝑋)) = (𝐼‘𝑋))
21	11, 14, 20	syl2anc 584	. . 3 ⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 ≤ 𝑋) → ( 0 (+g‘𝐺)(𝐼‘𝑋)) = (𝐼‘𝑋))
22	5, 17, 6, 12	grprinv 18625	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋(+g‘𝐺)(𝐼‘𝑋)) = 0 )
23	11, 9, 22	syl2anc 584	. . 3 ⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 ≤ 𝑋) → (𝑋(+g‘𝐺)(𝐼‘𝑋)) = 0 )
24	19, 21, 23	3brtr3d 5110	. 2 ⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 ≤ 𝑋) → (𝐼‘𝑋) ≤ 0 )
25	2	ad2antrr 723	. . . 4 ⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) ≤ 0 ) → 𝐺 ∈ oMnd)
26	10	ad2antrr 723	. . . . 5 ⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) ≤ 0 ) → 𝐺 ∈ Grp)
27		simplr 766	. . . . 5 ⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) ≤ 0 ) → 𝑋 ∈ 𝐵)
28	26, 27, 13	syl2anc 584	. . . 4 ⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) ≤ 0 ) → (𝐼‘𝑋) ∈ 𝐵)
29	25, 4, 7	3syl 18	. . . 4 ⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) ≤ 0 ) → 0 ∈ 𝐵)
30		simpr 485	. . . 4 ⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) ≤ 0 ) → (𝐼‘𝑋) ≤ 0 )
31	5, 16, 17	omndadd 31326	. . . 4 ⊢ ((𝐺 ∈ oMnd ∧ ((𝐼‘𝑋) ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) ≤ 0 ) → ((𝐼‘𝑋)(+g‘𝐺)𝑋) ≤ ( 0 (+g‘𝐺)𝑋))
32	25, 28, 29, 27, 30, 31	syl131anc 1382	. . 3 ⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) ≤ 0 ) → ((𝐼‘𝑋)(+g‘𝐺)𝑋) ≤ ( 0 (+g‘𝐺)𝑋))
33	5, 17, 6, 12	grplinv 18624	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ((𝐼‘𝑋)(+g‘𝐺)𝑋) = 0 )
34	26, 27, 33	syl2anc 584	. . 3 ⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) ≤ 0 ) → ((𝐼‘𝑋)(+g‘𝐺)𝑋) = 0 )
35	5, 17, 6	grplid 18605	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ( 0 (+g‘𝐺)𝑋) = 𝑋)
36	26, 27, 35	syl2anc 584	. . 3 ⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) ≤ 0 ) → ( 0 (+g‘𝐺)𝑋) = 𝑋)
37	32, 34, 36	3brtr3d 5110	. 2 ⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) ≤ 0 ) → 0 ≤ 𝑋)
38	24, 37	impbida 798	1 ⊢ ((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) → ( 0 ≤ 𝑋 ↔ (𝐼‘𝑋) ≤ 0 ))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1542   ∈ wcel 2110   class class class wbr 5079  ‘cfv 6431  (class class class)co 7269  Basecbs 16908  +_gcplusg 16958  lecple 16965  0_gc0g 17146  Mndcmnd 18381  Grpcgrp 18573  inv_gcminusg 18574  oMndcomnd 31317  oGrpcogrp 31318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7580

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-ral 3071  df-rex 3072  df-reu 3073  df-rmo 3074  df-rab 3075  df-v 3433  df-sbc 3721  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6389  df-fun 6433  df-fn 6434  df-f 6435  df-fv 6439  df-riota 7226  df-ov 7272  df-0g 17148  df-mgm 18322  df-sgrp 18371  df-mnd 18382  df-grp 18576  df-minusg 18577  df-omnd 31319  df-ogrp 31320

This theorem is referenced by: (None)