Proof of Theorem ogrpinvlt
Step | Hyp | Ref
| Expression |
1 | | simp1l 1198 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧
(oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐺 ∈ oGrp) |
2 | | simp2 1138 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧
(oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
3 | | simp3 1139 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧
(oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵) |
4 | | ogrpgrp 30898 |
. . . . . 6
⊢ (𝐺 ∈ oGrp → 𝐺 ∈ Grp) |
5 | 1, 4 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ oGrp ∧
(oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐺 ∈ Grp) |
6 | | ogrpinvlt.0 |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
7 | | ogrpinvlt.2 |
. . . . . 6
⊢ 𝐼 = (invg‘𝐺) |
8 | 6, 7 | grpinvcl 18262 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵) → (𝐼‘𝑌) ∈ 𝐵) |
9 | 5, 3, 8 | syl2anc 587 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧
(oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐼‘𝑌) ∈ 𝐵) |
10 | | ogrpinvlt.1 |
. . . . 5
⊢ < =
(lt‘𝐺) |
11 | | eqid 2738 |
. . . . 5
⊢
(+g‘𝐺) = (+g‘𝐺) |
12 | 6, 10, 11 | ogrpaddltbi 30913 |
. . . 4
⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝐼‘𝑌) ∈ 𝐵)) → (𝑋 < 𝑌 ↔ (𝑋(+g‘𝐺)(𝐼‘𝑌)) < (𝑌(+g‘𝐺)(𝐼‘𝑌)))) |
13 | 1, 2, 3, 9, 12 | syl13anc 1373 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧
(oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ (𝑋(+g‘𝐺)(𝐼‘𝑌)) < (𝑌(+g‘𝐺)(𝐼‘𝑌)))) |
14 | | eqid 2738 |
. . . . . 6
⊢
(0g‘𝐺) = (0g‘𝐺) |
15 | 6, 11, 14, 7 | grprinv 18264 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ 𝐵) → (𝑌(+g‘𝐺)(𝐼‘𝑌)) = (0g‘𝐺)) |
16 | 5, 3, 15 | syl2anc 587 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧
(oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑌(+g‘𝐺)(𝐼‘𝑌)) = (0g‘𝐺)) |
17 | 16 | breq2d 5039 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧
(oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋(+g‘𝐺)(𝐼‘𝑌)) < (𝑌(+g‘𝐺)(𝐼‘𝑌)) ↔ (𝑋(+g‘𝐺)(𝐼‘𝑌)) <
(0g‘𝐺))) |
18 | | simp1r 1199 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧
(oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (oppg‘𝐺) ∈ oGrp) |
19 | 6, 11 | grpcl 18220 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ (𝐼‘𝑌) ∈ 𝐵) → (𝑋(+g‘𝐺)(𝐼‘𝑌)) ∈ 𝐵) |
20 | 5, 2, 9, 19 | syl3anc 1372 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧
(oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(+g‘𝐺)(𝐼‘𝑌)) ∈ 𝐵) |
21 | 6, 14 | grpidcl 18242 |
. . . . 5
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝐵) |
22 | 1, 4, 21 | 3syl 18 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧
(oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (0g‘𝐺) ∈ 𝐵) |
23 | 6, 7 | grpinvcl 18262 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝐼‘𝑋) ∈ 𝐵) |
24 | 5, 2, 23 | syl2anc 587 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧
(oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐼‘𝑋) ∈ 𝐵) |
25 | 6, 10, 11, 1, 18, 20, 22, 24 | ogrpaddltrbid 30915 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧
(oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋(+g‘𝐺)(𝐼‘𝑌)) <
(0g‘𝐺)
↔ ((𝐼‘𝑋)(+g‘𝐺)(𝑋(+g‘𝐺)(𝐼‘𝑌))) < ((𝐼‘𝑋)(+g‘𝐺)(0g‘𝐺)))) |
26 | 13, 17, 25 | 3bitrd 308 |
. 2
⊢ (((𝐺 ∈ oGrp ∧
(oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ ((𝐼‘𝑋)(+g‘𝐺)(𝑋(+g‘𝐺)(𝐼‘𝑌))) < ((𝐼‘𝑋)(+g‘𝐺)(0g‘𝐺)))) |
27 | 6, 11, 14, 7 | grplinv 18263 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ((𝐼‘𝑋)(+g‘𝐺)𝑋) = (0g‘𝐺)) |
28 | 5, 2, 27 | syl2anc 587 |
. . . . 5
⊢ (((𝐺 ∈ oGrp ∧
(oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝐼‘𝑋)(+g‘𝐺)𝑋) = (0g‘𝐺)) |
29 | 28 | oveq1d 7179 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧
(oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((𝐼‘𝑋)(+g‘𝐺)𝑋)(+g‘𝐺)(𝐼‘𝑌)) = ((0g‘𝐺)(+g‘𝐺)(𝐼‘𝑌))) |
30 | 6, 11 | grpass 18221 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ ((𝐼‘𝑋) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ (𝐼‘𝑌) ∈ 𝐵)) → (((𝐼‘𝑋)(+g‘𝐺)𝑋)(+g‘𝐺)(𝐼‘𝑌)) = ((𝐼‘𝑋)(+g‘𝐺)(𝑋(+g‘𝐺)(𝐼‘𝑌)))) |
31 | 5, 24, 2, 9, 30 | syl13anc 1373 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧
(oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((𝐼‘𝑋)(+g‘𝐺)𝑋)(+g‘𝐺)(𝐼‘𝑌)) = ((𝐼‘𝑋)(+g‘𝐺)(𝑋(+g‘𝐺)(𝐼‘𝑌)))) |
32 | 6, 11, 14 | grplid 18244 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝐼‘𝑌) ∈ 𝐵) → ((0g‘𝐺)(+g‘𝐺)(𝐼‘𝑌)) = (𝐼‘𝑌)) |
33 | 5, 9, 32 | syl2anc 587 |
. . . 4
⊢ (((𝐺 ∈ oGrp ∧
(oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((0g‘𝐺)(+g‘𝐺)(𝐼‘𝑌)) = (𝐼‘𝑌)) |
34 | 29, 31, 33 | 3eqtr3d 2781 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧
(oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝐼‘𝑋)(+g‘𝐺)(𝑋(+g‘𝐺)(𝐼‘𝑌))) = (𝐼‘𝑌)) |
35 | 6, 11, 14 | grprid 18245 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝐼‘𝑋) ∈ 𝐵) → ((𝐼‘𝑋)(+g‘𝐺)(0g‘𝐺)) = (𝐼‘𝑋)) |
36 | 5, 24, 35 | syl2anc 587 |
. . 3
⊢ (((𝐺 ∈ oGrp ∧
(oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝐼‘𝑋)(+g‘𝐺)(0g‘𝐺)) = (𝐼‘𝑋)) |
37 | 34, 36 | breq12d 5040 |
. 2
⊢ (((𝐺 ∈ oGrp ∧
(oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((𝐼‘𝑋)(+g‘𝐺)(𝑋(+g‘𝐺)(𝐼‘𝑌))) < ((𝐼‘𝑋)(+g‘𝐺)(0g‘𝐺)) ↔ (𝐼‘𝑌) < (𝐼‘𝑋))) |
38 | 26, 37 | bitrd 282 |
1
⊢ (((𝐺 ∈ oGrp ∧
(oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ (𝐼‘𝑌) < (𝐼‘𝑋))) |