Proof of Theorem ogrpinv0lt
| Step | Hyp | Ref
| Expression |
| 1 | | simpll 767 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 < 𝑋) → 𝐺 ∈ oGrp) |
| 2 | | ogrpgrp 33080 |
. . . . . 6
⊢ (𝐺 ∈ oGrp → 𝐺 ∈ Grp) |
| 3 | 1, 2 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 < 𝑋) → 𝐺 ∈ Grp) |
| 4 | | ogrpinvlt.0 |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
| 5 | | ogrpinv0lt.3 |
. . . . . 6
⊢ 0 =
(0g‘𝐺) |
| 6 | 4, 5 | grpidcl 18983 |
. . . . 5
⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵) |
| 7 | 3, 6 | syl 17 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 < 𝑋) → 0 ∈ 𝐵) |
| 8 | | simplr 769 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 < 𝑋) → 𝑋 ∈ 𝐵) |
| 9 | | ogrpinvlt.2 |
. . . . . 6
⊢ 𝐼 = (invg‘𝐺) |
| 10 | 4, 9 | grpinvcl 19005 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝐼‘𝑋) ∈ 𝐵) |
| 11 | 3, 8, 10 | syl2anc 584 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 < 𝑋) → (𝐼‘𝑋) ∈ 𝐵) |
| 12 | | simpr 484 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 < 𝑋) → 0 < 𝑋) |
| 13 | | ogrpinvlt.1 |
. . . . 5
⊢ < =
(lt‘𝐺) |
| 14 | | eqid 2737 |
. . . . 5
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 15 | 4, 13, 14 | ogrpaddlt 33094 |
. . . 4
⊢ ((𝐺 ∈ oGrp ∧ ( 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ (𝐼‘𝑋) ∈ 𝐵) ∧ 0 < 𝑋) → ( 0 (+g‘𝐺)(𝐼‘𝑋)) < (𝑋(+g‘𝐺)(𝐼‘𝑋))) |
| 16 | 1, 7, 8, 11, 12, 15 | syl131anc 1385 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 < 𝑋) → ( 0 (+g‘𝐺)(𝐼‘𝑋)) < (𝑋(+g‘𝐺)(𝐼‘𝑋))) |
| 17 | 4, 14, 5 | grplid 18985 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝐼‘𝑋) ∈ 𝐵) → ( 0 (+g‘𝐺)(𝐼‘𝑋)) = (𝐼‘𝑋)) |
| 18 | 3, 11, 17 | syl2anc 584 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 < 𝑋) → ( 0 (+g‘𝐺)(𝐼‘𝑋)) = (𝐼‘𝑋)) |
| 19 | 4, 14, 5, 9 | grprinv 19008 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋(+g‘𝐺)(𝐼‘𝑋)) = 0 ) |
| 20 | 3, 8, 19 | syl2anc 584 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 < 𝑋) → (𝑋(+g‘𝐺)(𝐼‘𝑋)) = 0 ) |
| 21 | 16, 18, 20 | 3brtr3d 5174 |
. 2
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 < 𝑋) → (𝐼‘𝑋) < 0 ) |
| 22 | | simpll 767 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) < 0 ) → 𝐺 ∈ oGrp) |
| 23 | 22, 2 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) < 0 ) → 𝐺 ∈ Grp) |
| 24 | | simplr 769 |
. . . . 5
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) < 0 ) → 𝑋 ∈ 𝐵) |
| 25 | 23, 24, 10 | syl2anc 584 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) < 0 ) → (𝐼‘𝑋) ∈ 𝐵) |
| 26 | 22, 2, 6 | 3syl 18 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) < 0 ) → 0 ∈ 𝐵) |
| 27 | | simpr 484 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) < 0 ) → (𝐼‘𝑋) < 0 ) |
| 28 | 4, 13, 14 | ogrpaddlt 33094 |
. . . 4
⊢ ((𝐺 ∈ oGrp ∧ ((𝐼‘𝑋) ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) < 0 ) → ((𝐼‘𝑋)(+g‘𝐺)𝑋) < ( 0 (+g‘𝐺)𝑋)) |
| 29 | 22, 25, 26, 24, 27, 28 | syl131anc 1385 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) < 0 ) → ((𝐼‘𝑋)(+g‘𝐺)𝑋) < ( 0 (+g‘𝐺)𝑋)) |
| 30 | 4, 14, 5, 9 | grplinv 19007 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ((𝐼‘𝑋)(+g‘𝐺)𝑋) = 0 ) |
| 31 | 23, 24, 30 | syl2anc 584 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) < 0 ) → ((𝐼‘𝑋)(+g‘𝐺)𝑋) = 0 ) |
| 32 | 4, 14, 5 | grplid 18985 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ( 0 (+g‘𝐺)𝑋) = 𝑋) |
| 33 | 23, 24, 32 | syl2anc 584 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) < 0 ) → ( 0
(+g‘𝐺)𝑋) = 𝑋) |
| 34 | 29, 31, 33 | 3brtr3d 5174 |
. 2
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) < 0 ) → 0 < 𝑋) |
| 35 | 21, 34 | impbida 801 |
1
⊢ ((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) → ( 0 < 𝑋 ↔ (𝐼‘𝑋) < 0 )) |