Step | Hyp | Ref
| Expression |
1 | | isogrp 31373 |
. . . . . 6
β’ (πΊ β oGrp β (πΊ β Grp β§ πΊ β oMnd)) |
2 | 1 | simprbi 498 |
. . . . 5
β’ (πΊ β oGrp β πΊ β oMnd) |
3 | 2 | ad2antrr 724 |
. . . 4
β’ (((πΊ β oGrp β§ π β π΅) β§ 0 β€ π) β πΊ β oMnd) |
4 | | omndmnd 31375 |
. . . . 5
β’ (πΊ β oMnd β πΊ β Mnd) |
5 | | ogrpsub.0 |
. . . . . 6
β’ π΅ = (BaseβπΊ) |
6 | | ogrpinv.3 |
. . . . . 6
β’ 0 =
(0gβπΊ) |
7 | 5, 6 | mndidcl 18445 |
. . . . 5
β’ (πΊ β Mnd β 0 β π΅) |
8 | 3, 4, 7 | 3syl 18 |
. . . 4
β’ (((πΊ β oGrp β§ π β π΅) β§ 0 β€ π) β 0 β π΅) |
9 | | simplr 767 |
. . . 4
β’ (((πΊ β oGrp β§ π β π΅) β§ 0 β€ π) β π β π΅) |
10 | | ogrpgrp 31374 |
. . . . . 6
β’ (πΊ β oGrp β πΊ β Grp) |
11 | 10 | ad2antrr 724 |
. . . . 5
β’ (((πΊ β oGrp β§ π β π΅) β§ 0 β€ π) β πΊ β Grp) |
12 | | ogrpinv.2 |
. . . . . 6
β’ πΌ = (invgβπΊ) |
13 | 5, 12 | grpinvcl 18672 |
. . . . 5
β’ ((πΊ β Grp β§ π β π΅) β (πΌβπ) β π΅) |
14 | 11, 9, 13 | syl2anc 585 |
. . . 4
β’ (((πΊ β oGrp β§ π β π΅) β§ 0 β€ π) β (πΌβπ) β π΅) |
15 | | simpr 486 |
. . . 4
β’ (((πΊ β oGrp β§ π β π΅) β§ 0 β€ π) β 0 β€ π) |
16 | | ogrpsub.1 |
. . . . 5
β’ β€ =
(leβπΊ) |
17 | | eqid 2736 |
. . . . 5
β’
(+gβπΊ) = (+gβπΊ) |
18 | 5, 16, 17 | omndadd 31377 |
. . . 4
β’ ((πΊ β oMnd β§ ( 0 β π΅ β§ π β π΅ β§ (πΌβπ) β π΅) β§ 0 β€ π) β ( 0 (+gβπΊ)(πΌβπ)) β€ (π(+gβπΊ)(πΌβπ))) |
19 | 3, 8, 9, 14, 15, 18 | syl131anc 1383 |
. . 3
β’ (((πΊ β oGrp β§ π β π΅) β§ 0 β€ π) β ( 0 (+gβπΊ)(πΌβπ)) β€ (π(+gβπΊ)(πΌβπ))) |
20 | 5, 17, 6 | grplid 18654 |
. . . 4
β’ ((πΊ β Grp β§ (πΌβπ) β π΅) β ( 0 (+gβπΊ)(πΌβπ)) = (πΌβπ)) |
21 | 11, 14, 20 | syl2anc 585 |
. . 3
β’ (((πΊ β oGrp β§ π β π΅) β§ 0 β€ π) β ( 0 (+gβπΊ)(πΌβπ)) = (πΌβπ)) |
22 | 5, 17, 6, 12 | grprinv 18674 |
. . . 4
β’ ((πΊ β Grp β§ π β π΅) β (π(+gβπΊ)(πΌβπ)) = 0 ) |
23 | 11, 9, 22 | syl2anc 585 |
. . 3
β’ (((πΊ β oGrp β§ π β π΅) β§ 0 β€ π) β (π(+gβπΊ)(πΌβπ)) = 0 ) |
24 | 19, 21, 23 | 3brtr3d 5112 |
. 2
β’ (((πΊ β oGrp β§ π β π΅) β§ 0 β€ π) β (πΌβπ) β€ 0 ) |
25 | 2 | ad2antrr 724 |
. . . 4
β’ (((πΊ β oGrp β§ π β π΅) β§ (πΌβπ) β€ 0 ) β πΊ β oMnd) |
26 | 10 | ad2antrr 724 |
. . . . 5
β’ (((πΊ β oGrp β§ π β π΅) β§ (πΌβπ) β€ 0 ) β πΊ β Grp) |
27 | | simplr 767 |
. . . . 5
β’ (((πΊ β oGrp β§ π β π΅) β§ (πΌβπ) β€ 0 ) β π β π΅) |
28 | 26, 27, 13 | syl2anc 585 |
. . . 4
β’ (((πΊ β oGrp β§ π β π΅) β§ (πΌβπ) β€ 0 ) β (πΌβπ) β π΅) |
29 | 25, 4, 7 | 3syl 18 |
. . . 4
β’ (((πΊ β oGrp β§ π β π΅) β§ (πΌβπ) β€ 0 ) β 0 β π΅) |
30 | | simpr 486 |
. . . 4
β’ (((πΊ β oGrp β§ π β π΅) β§ (πΌβπ) β€ 0 ) β (πΌβπ) β€ 0 ) |
31 | 5, 16, 17 | omndadd 31377 |
. . . 4
β’ ((πΊ β oMnd β§ ((πΌβπ) β π΅ β§ 0 β π΅ β§ π β π΅) β§ (πΌβπ) β€ 0 ) β ((πΌβπ)(+gβπΊ)π) β€ ( 0 (+gβπΊ)π)) |
32 | 25, 28, 29, 27, 30, 31 | syl131anc 1383 |
. . 3
β’ (((πΊ β oGrp β§ π β π΅) β§ (πΌβπ) β€ 0 ) β ((πΌβπ)(+gβπΊ)π) β€ ( 0 (+gβπΊ)π)) |
33 | 5, 17, 6, 12 | grplinv 18673 |
. . . 4
β’ ((πΊ β Grp β§ π β π΅) β ((πΌβπ)(+gβπΊ)π) = 0 ) |
34 | 26, 27, 33 | syl2anc 585 |
. . 3
β’ (((πΊ β oGrp β§ π β π΅) β§ (πΌβπ) β€ 0 ) β ((πΌβπ)(+gβπΊ)π) = 0 ) |
35 | 5, 17, 6 | grplid 18654 |
. . . 4
β’ ((πΊ β Grp β§ π β π΅) β ( 0 (+gβπΊ)π) = π) |
36 | 26, 27, 35 | syl2anc 585 |
. . 3
β’ (((πΊ β oGrp β§ π β π΅) β§ (πΌβπ) β€ 0 ) β ( 0
(+gβπΊ)π) = π) |
37 | 32, 34, 36 | 3brtr3d 5112 |
. 2
β’ (((πΊ β oGrp β§ π β π΅) β§ (πΌβπ) β€ 0 ) β 0 β€ π) |
38 | 24, 37 | impbida 799 |
1
β’ ((πΊ β oGrp β§ π β π΅) β ( 0 β€ π β (πΌβπ) β€ 0 )) |