Step | Hyp | Ref
| Expression |
1 | | simp3 1139 |
. . . . 5
β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π < π) β π < π) |
2 | | simp1 1137 |
. . . . . 6
β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π < π) β πΊ β oGrp) |
3 | | simp21 1207 |
. . . . . 6
β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π < π) β π β π΅) |
4 | | simp22 1208 |
. . . . . 6
β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π < π) β π β π΅) |
5 | | eqid 2733 |
. . . . . . 7
β’
(leβπΊ) =
(leβπΊ) |
6 | | ogrpsublt.1 |
. . . . . . 7
β’ < =
(ltβπΊ) |
7 | 5, 6 | pltval 18285 |
. . . . . 6
β’ ((πΊ β oGrp β§ π β π΅ β§ π β π΅) β (π < π β (π(leβπΊ)π β§ π β π))) |
8 | 2, 3, 4, 7 | syl3anc 1372 |
. . . . 5
β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π < π) β (π < π β (π(leβπΊ)π β§ π β π))) |
9 | 1, 8 | mpbid 231 |
. . . 4
β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π < π) β (π(leβπΊ)π β§ π β π)) |
10 | 9 | simpld 496 |
. . 3
β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π < π) β π(leβπΊ)π) |
11 | | ogrpsublt.0 |
. . . 4
β’ π΅ = (BaseβπΊ) |
12 | | ogrpsublt.2 |
. . . 4
β’ β =
(-gβπΊ) |
13 | 11, 5, 12 | ogrpsub 32234 |
. . 3
β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π(leβπΊ)π) β (π β π)(leβπΊ)(π β π)) |
14 | 10, 13 | syld3an3 1410 |
. 2
β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π < π) β (π β π)(leβπΊ)(π β π)) |
15 | 9 | simprd 497 |
. . 3
β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π < π) β π β π) |
16 | | ogrpgrp 32221 |
. . . . . 6
β’ (πΊ β oGrp β πΊ β Grp) |
17 | 2, 16 | syl 17 |
. . . . 5
β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π < π) β πΊ β Grp) |
18 | | simp23 1209 |
. . . . 5
β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π < π) β π β π΅) |
19 | 11, 12 | grpsubrcan 18904 |
. . . . 5
β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β π) = (π β π) β π = π)) |
20 | 17, 3, 4, 18, 19 | syl13anc 1373 |
. . . 4
β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π < π) β ((π β π) = (π β π) β π = π)) |
21 | 20 | necon3bid 2986 |
. . 3
β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π < π) β ((π β π) β (π β π) β π β π)) |
22 | 15, 21 | mpbird 257 |
. 2
β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π < π) β (π β π) β (π β π)) |
23 | 11, 12 | grpsubcl 18903 |
. . . 4
β’ ((πΊ β Grp β§ π β π΅ β§ π β π΅) β (π β π) β π΅) |
24 | 17, 3, 18, 23 | syl3anc 1372 |
. . 3
β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π < π) β (π β π) β π΅) |
25 | 11, 12 | grpsubcl 18903 |
. . . 4
β’ ((πΊ β Grp β§ π β π΅ β§ π β π΅) β (π β π) β π΅) |
26 | 17, 4, 18, 25 | syl3anc 1372 |
. . 3
β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π < π) β (π β π) β π΅) |
27 | 5, 6 | pltval 18285 |
. . 3
β’ ((πΊ β oGrp β§ (π β π) β π΅ β§ (π β π) β π΅) β ((π β π) < (π β π) β ((π β π)(leβπΊ)(π β π) β§ (π β π) β (π β π)))) |
28 | 2, 24, 26, 27 | syl3anc 1372 |
. 2
β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π < π) β ((π β π) < (π β π) β ((π β π)(leβπΊ)(π β π) β§ (π β π) β (π β π)))) |
29 | 14, 22, 28 | mpbir2and 712 |
1
β’ ((πΊ β oGrp β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ π < π) β (π β π) < (π β π)) |