Step | Hyp | Ref
| Expression |
1 | | isogrp 32261 |
. . . . . 6
β’ (πΊ β oGrp β (πΊ β Grp β§ πΊ β oMnd)) |
2 | 1 | simprbi 497 |
. . . . 5
β’ (πΊ β oGrp β πΊ β oMnd) |
3 | 2 | ad2antrr 724 |
. . . 4
β’ (((πΊ β oGrp β§ π β π΅) β§ 0 β€ π) β πΊ β oMnd) |
4 | | omndmnd 32263 |
. . . . 5
β’ (πΊ β oMnd β πΊ β Mnd) |
5 | | ogrpsub.0 |
. . . . . 6
β’ π΅ = (BaseβπΊ) |
6 | | ogrpinv.3 |
. . . . . 6
β’ 0 =
(0gβπΊ) |
7 | 5, 6 | mndidcl 18642 |
. . . . 5
β’ (πΊ β Mnd β 0 β π΅) |
8 | 3, 4, 7 | 3syl 18 |
. . . 4
β’ (((πΊ β oGrp β§ π β π΅) β§ 0 β€ π) β 0 β π΅) |
9 | | simplr 767 |
. . . 4
β’ (((πΊ β oGrp β§ π β π΅) β§ 0 β€ π) β π β π΅) |
10 | | ogrpgrp 32262 |
. . . . . 6
β’ (πΊ β oGrp β πΊ β Grp) |
11 | 10 | ad2antrr 724 |
. . . . 5
β’ (((πΊ β oGrp β§ π β π΅) β§ 0 β€ π) β πΊ β Grp) |
12 | | ogrpinv.2 |
. . . . . 6
β’ πΌ = (invgβπΊ) |
13 | 5, 12 | grpinvcl 18874 |
. . . . 5
β’ ((πΊ β Grp β§ π β π΅) β (πΌβπ) β π΅) |
14 | 11, 9, 13 | syl2anc 584 |
. . . 4
β’ (((πΊ β oGrp β§ π β π΅) β§ 0 β€ π) β (πΌβπ) β π΅) |
15 | | simpr 485 |
. . . 4
β’ (((πΊ β oGrp β§ π β π΅) β§ 0 β€ π) β 0 β€ π) |
16 | | ogrpsub.1 |
. . . . 5
β’ β€ =
(leβπΊ) |
17 | | eqid 2732 |
. . . . 5
β’
(+gβπΊ) = (+gβπΊ) |
18 | 5, 16, 17 | omndadd 32265 |
. . . 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 18854 |
. . . 4
β’ ((πΊ β Grp β§ (πΌβπ) β π΅) β ( 0 (+gβπΊ)(πΌβπ)) = (πΌβπ)) |
21 | 11, 14, 20 | syl2anc 584 |
. . 3
β’ (((πΊ β oGrp β§ π β π΅) β§ 0 β€ π) β ( 0 (+gβπΊ)(πΌβπ)) = (πΌβπ)) |
22 | 5, 17, 6, 12 | grprinv 18877 |
. . . 4
β’ ((πΊ β Grp β§ π β π΅) β (π(+gβπΊ)(πΌβπ)) = 0 ) |
23 | 11, 9, 22 | syl2anc 584 |
. . 3
β’ (((πΊ β oGrp β§ π β π΅) β§ 0 β€ π) β (π(+gβπΊ)(πΌβπ)) = 0 ) |
24 | 19, 21, 23 | 3brtr3d 5179 |
. 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 584 |
. . . 4
β’ (((πΊ β oGrp β§ π β π΅) β§ (πΌβπ) β€ 0 ) β (πΌβπ) β π΅) |
29 | 25, 4, 7 | 3syl 18 |
. . . 4
β’ (((πΊ β oGrp β§ π β π΅) β§ (πΌβπ) β€ 0 ) β 0 β π΅) |
30 | | simpr 485 |
. . . 4
β’ (((πΊ β oGrp β§ π β π΅) β§ (πΌβπ) β€ 0 ) β (πΌβπ) β€ 0 ) |
31 | 5, 16, 17 | omndadd 32265 |
. . . 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 18876 |
. . . 4
β’ ((πΊ β Grp β§ π β π΅) β ((πΌβπ)(+gβπΊ)π) = 0 ) |
34 | 26, 27, 33 | syl2anc 584 |
. . 3
β’ (((πΊ β oGrp β§ π β π΅) β§ (πΌβπ) β€ 0 ) β ((πΌβπ)(+gβπΊ)π) = 0 ) |
35 | 5, 17, 6 | grplid 18854 |
. . . 4
β’ ((πΊ β Grp β§ π β π΅) β ( 0 (+gβπΊ)π) = π) |
36 | 26, 27, 35 | syl2anc 584 |
. . 3
β’ (((πΊ β oGrp β§ π β π΅) β§ (πΌβπ) β€ 0 ) β ( 0
(+gβπΊ)π) = π) |
37 | 32, 34, 36 | 3brtr3d 5179 |
. 2
β’ (((πΊ β oGrp β§ π β π΅) β§ (πΌβπ) β€ 0 ) β 0 β€ π) |
38 | 24, 37 | impbida 799 |
1
β’ ((πΊ β oGrp β§ π β π΅) β ( 0 β€ π β (πΌβπ) β€ 0 )) |