Proof of Theorem ogrpinv0lt
Step | Hyp | Ref
| Expression |
1 | | simpll 764 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 < 𝑋) → 𝐺 ∈ oGrp) |
2 | | ogrpgrp 31325 |
. . . . . 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 18605 |
. . . . 5
⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵) |
7 | 3, 6 | syl 17 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 < 𝑋) → 0 ∈ 𝐵) |
8 | | simplr 766 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 < 𝑋) → 𝑋 ∈ 𝐵) |
9 | | ogrpinvlt.2 |
. . . . . 6
⊢ 𝐼 = (invg‘𝐺) |
10 | 4, 9 | grpinvcl 18625 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝐼‘𝑋) ∈ 𝐵) |
11 | 3, 8, 10 | syl2anc 584 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 < 𝑋) → (𝐼‘𝑋) ∈ 𝐵) |
12 | | simpr 485 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 < 𝑋) → 0 < 𝑋) |
13 | | ogrpinvlt.1 |
. . . . 5
⊢ < =
(lt‘𝐺) |
14 | | eqid 2740 |
. . . . 5
⊢
(+g‘𝐺) = (+g‘𝐺) |
15 | 4, 13, 14 | ogrpaddlt 31339 |
. . . 4
⊢ ((𝐺 ∈ oGrp ∧ ( 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ (𝐼‘𝑋) ∈ 𝐵) ∧ 0 < 𝑋) → ( 0 (+g‘𝐺)(𝐼‘𝑋)) < (𝑋(+g‘𝐺)(𝐼‘𝑋))) |
16 | 1, 7, 8, 11, 12, 15 | syl131anc 1382 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 < 𝑋) → ( 0 (+g‘𝐺)(𝐼‘𝑋)) < (𝑋(+g‘𝐺)(𝐼‘𝑋))) |
17 | 4, 14, 5 | grplid 18607 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝐼‘𝑋) ∈ 𝐵) → ( 0 (+g‘𝐺)(𝐼‘𝑋)) = (𝐼‘𝑋)) |
18 | 3, 11, 17 | syl2anc 584 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 < 𝑋) → ( 0 (+g‘𝐺)(𝐼‘𝑋)) = (𝐼‘𝑋)) |
19 | 4, 14, 5, 9 | grprinv 18627 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋(+g‘𝐺)(𝐼‘𝑋)) = 0 ) |
20 | 3, 8, 19 | syl2anc 584 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 < 𝑋) → (𝑋(+g‘𝐺)(𝐼‘𝑋)) = 0 ) |
21 | 16, 18, 20 | 3brtr3d 5110 |
. 2
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ 0 < 𝑋) → (𝐼‘𝑋) < 0 ) |
22 | | simpll 764 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) < 0 ) → 𝐺 ∈ oGrp) |
23 | 22, 2 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) < 0 ) → 𝐺 ∈ Grp) |
24 | | simplr 766 |
. . . . 5
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) < 0 ) → 𝑋 ∈ 𝐵) |
25 | 23, 24, 10 | syl2anc 584 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) < 0 ) → (𝐼‘𝑋) ∈ 𝐵) |
26 | 22, 2, 6 | 3syl 18 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) < 0 ) → 0 ∈ 𝐵) |
27 | | simpr 485 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) < 0 ) → (𝐼‘𝑋) < 0 ) |
28 | 4, 13, 14 | ogrpaddlt 31339 |
. . . 4
⊢ ((𝐺 ∈ oGrp ∧ ((𝐼‘𝑋) ∈ 𝐵 ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) < 0 ) → ((𝐼‘𝑋)(+g‘𝐺)𝑋) < ( 0 (+g‘𝐺)𝑋)) |
29 | 22, 25, 26, 24, 27, 28 | syl131anc 1382 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) < 0 ) → ((𝐼‘𝑋)(+g‘𝐺)𝑋) < ( 0 (+g‘𝐺)𝑋)) |
30 | 4, 14, 5, 9 | grplinv 18626 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ((𝐼‘𝑋)(+g‘𝐺)𝑋) = 0 ) |
31 | 23, 24, 30 | syl2anc 584 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) < 0 ) → ((𝐼‘𝑋)(+g‘𝐺)𝑋) = 0 ) |
32 | 4, 14, 5 | grplid 18607 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ( 0 (+g‘𝐺)𝑋) = 𝑋) |
33 | 23, 24, 32 | syl2anc 584 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) < 0 ) → ( 0
(+g‘𝐺)𝑋) = 𝑋) |
34 | 29, 31, 33 | 3brtr3d 5110 |
. 2
⊢ (((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) ∧ (𝐼‘𝑋) < 0 ) → 0 < 𝑋) |
35 | 21, 34 | impbida 798 |
1
⊢ ((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) → ( 0 < 𝑋 ↔ (𝐼‘𝑋) < 0 )) |