Step | Hyp | Ref
| Expression |
1 | | 0zd 12570 |
. . 3
β’ (((π β§ π¦ β π΅) β§ π¦ = 0 ) β 0 β
β€) |
2 | | simpr 486 |
. . . 4
β’ (((π β§ π¦ β π΅) β§ π¦ = 0 ) β π¦ = 0 ) |
3 | | archiabllem1.u |
. . . . . 6
β’ (π β π β π΅) |
4 | | archiabllem.b |
. . . . . . 7
β’ π΅ = (Baseβπ) |
5 | | archiabllem.0 |
. . . . . . 7
β’ 0 =
(0gβπ) |
6 | | archiabllem.m |
. . . . . . 7
β’ Β· =
(.gβπ) |
7 | 4, 5, 6 | mulg0 18957 |
. . . . . 6
β’ (π β π΅ β (0 Β· π) = 0 ) |
8 | 3, 7 | syl 17 |
. . . . 5
β’ (π β (0 Β· π) = 0 ) |
9 | 8 | ad2antrr 725 |
. . . 4
β’ (((π β§ π¦ β π΅) β§ π¦ = 0 ) β (0 Β· π) = 0 ) |
10 | 2, 9 | eqtr4d 2776 |
. . 3
β’ (((π β§ π¦ β π΅) β§ π¦ = 0 ) β π¦ = (0 Β· π)) |
11 | | oveq1 7416 |
. . . 4
β’ (π = 0 β (π Β· π) = (0 Β· π)) |
12 | 11 | rspceeqv 3634 |
. . 3
β’ ((0
β β€ β§ π¦ = (0
Β·
π)) β βπ β β€ π¦ = (π Β· π)) |
13 | 1, 10, 12 | syl2anc 585 |
. 2
β’ (((π β§ π¦ β π΅) β§ π¦ = 0 ) β βπ β β€ π¦ = (π Β· π)) |
14 | | simplr 768 |
. . . . . . 7
β’ ((((π β§ π¦ β π΅ β§ π¦ < 0 ) β§ π β β) β§
((invgβπ)βπ¦) = (π Β· π)) β π β β) |
15 | 14 | nnzd 12585 |
. . . . . 6
β’ ((((π β§ π¦ β π΅ β§ π¦ < 0 ) β§ π β β) β§
((invgβπ)βπ¦) = (π Β· π)) β π β β€) |
16 | 15 | znegcld 12668 |
. . . . 5
β’ ((((π β§ π¦ β π΅ β§ π¦ < 0 ) β§ π β β) β§
((invgβπ)βπ¦) = (π Β· π)) β -π β β€) |
17 | 3 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((π β§ π¦ β π΅ β§ π¦ < 0 ) β π β π΅) |
18 | 17 | ad2antrr 725 |
. . . . . . 7
β’ ((((π β§ π¦ β π΅ β§ π¦ < 0 ) β§ π β β) β§
((invgβπ)βπ¦) = (π Β· π)) β π β π΅) |
19 | | eqid 2733 |
. . . . . . . 8
β’
(invgβπ) = (invgβπ) |
20 | 4, 6, 19 | mulgnegnn 18964 |
. . . . . . 7
β’ ((π β β β§ π β π΅) β (-π Β· π) = ((invgβπ)β(π Β· π))) |
21 | 14, 18, 20 | syl2anc 585 |
. . . . . 6
β’ ((((π β§ π¦ β π΅ β§ π¦ < 0 ) β§ π β β) β§
((invgβπ)βπ¦) = (π Β· π)) β (-π Β· π) = ((invgβπ)β(π Β· π))) |
22 | | simpr 486 |
. . . . . . 7
β’ ((((π β§ π¦ β π΅ β§ π¦ < 0 ) β§ π β β) β§
((invgβπ)βπ¦) = (π Β· π)) β ((invgβπ)βπ¦) = (π Β· π)) |
23 | 22 | fveq2d 6896 |
. . . . . 6
β’ ((((π β§ π¦ β π΅ β§ π¦ < 0 ) β§ π β β) β§
((invgβπ)βπ¦) = (π Β· π)) β ((invgβπ)β((invgβπ)βπ¦)) = ((invgβπ)β(π Β· π))) |
24 | | archiabllem.g |
. . . . . . . . . 10
β’ (π β π β oGrp) |
25 | 24 | 3ad2ant1 1134 |
. . . . . . . . 9
β’ ((π β§ π¦ β π΅ β§ π¦ < 0 ) β π β oGrp) |
26 | | ogrpgrp 32221 |
. . . . . . . . 9
β’ (π β oGrp β π β Grp) |
27 | 25, 26 | syl 17 |
. . . . . . . 8
β’ ((π β§ π¦ β π΅ β§ π¦ < 0 ) β π β Grp) |
28 | | simp2 1138 |
. . . . . . . 8
β’ ((π β§ π¦ β π΅ β§ π¦ < 0 ) β π¦ β π΅) |
29 | 4, 19 | grpinvinv 18890 |
. . . . . . . 8
β’ ((π β Grp β§ π¦ β π΅) β ((invgβπ)β((invgβπ)βπ¦)) = π¦) |
30 | 27, 28, 29 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π¦ β π΅ β§ π¦ < 0 ) β
((invgβπ)β((invgβπ)βπ¦)) = π¦) |
31 | 30 | ad2antrr 725 |
. . . . . 6
β’ ((((π β§ π¦ β π΅ β§ π¦ < 0 ) β§ π β β) β§
((invgβπ)βπ¦) = (π Β· π)) β ((invgβπ)β((invgβπ)βπ¦)) = π¦) |
32 | 21, 23, 31 | 3eqtr2rd 2780 |
. . . . 5
β’ ((((π β§ π¦ β π΅ β§ π¦ < 0 ) β§ π β β) β§
((invgβπ)βπ¦) = (π Β· π)) β π¦ = (-π Β· π)) |
33 | | oveq1 7416 |
. . . . . 6
β’ (π = -π β (π Β· π) = (-π Β· π)) |
34 | 33 | rspceeqv 3634 |
. . . . 5
β’ ((-π β β€ β§ π¦ = (-π Β· π)) β βπ β β€ π¦ = (π Β· π)) |
35 | 16, 32, 34 | syl2anc 585 |
. . . 4
β’ ((((π β§ π¦ β π΅ β§ π¦ < 0 ) β§ π β β) β§
((invgβπ)βπ¦) = (π Β· π)) β βπ β β€ π¦ = (π Β· π)) |
36 | | archiabllem.e |
. . . . 5
β’ β€ =
(leβπ) |
37 | | archiabllem.t |
. . . . 5
β’ < =
(ltβπ) |
38 | | archiabllem.a |
. . . . . 6
β’ (π β π β Archi) |
39 | 38 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π¦ β π΅ β§ π¦ < 0 ) β π β Archi) |
40 | | archiabllem1.p |
. . . . . 6
β’ (π β 0 < π) |
41 | 40 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π¦ β π΅ β§ π¦ < 0 ) β 0 < π) |
42 | | simp1 1137 |
. . . . . 6
β’ ((π β§ π¦ β π΅ β§ π¦ < 0 ) β π) |
43 | | archiabllem1.s |
. . . . . 6
β’ ((π β§ π₯ β π΅ β§ 0 < π₯) β π β€ π₯) |
44 | 42, 43 | syl3an1 1164 |
. . . . 5
β’ (((π β§ π¦ β π΅ β§ π¦ < 0 ) β§ π₯ β π΅ β§ 0 < π₯) β π β€ π₯) |
45 | 4, 19 | grpinvcl 18872 |
. . . . . 6
β’ ((π β Grp β§ π¦ β π΅) β ((invgβπ)βπ¦) β π΅) |
46 | 27, 28, 45 | syl2anc 585 |
. . . . 5
β’ ((π β§ π¦ β π΅ β§ π¦ < 0 ) β
((invgβπ)βπ¦) β π΅) |
47 | 4, 5 | grpidcl 18850 |
. . . . . . . 8
β’ (π β Grp β 0 β π΅) |
48 | 27, 47 | syl 17 |
. . . . . . 7
β’ ((π β§ π¦ β π΅ β§ π¦ < 0 ) β 0 β π΅) |
49 | | simp3 1139 |
. . . . . . 7
β’ ((π β§ π¦ β π΅ β§ π¦ < 0 ) β π¦ < 0 ) |
50 | | eqid 2733 |
. . . . . . . 8
β’
(+gβπ) = (+gβπ) |
51 | 4, 37, 50 | ogrpaddlt 32235 |
. . . . . . 7
β’ ((π β oGrp β§ (π¦ β π΅ β§ 0 β π΅ β§ ((invgβπ)βπ¦) β π΅) β§ π¦ < 0 ) β (π¦(+gβπ)((invgβπ)βπ¦)) < ( 0 (+gβπ)((invgβπ)βπ¦))) |
52 | 25, 28, 48, 46, 49, 51 | syl131anc 1384 |
. . . . . 6
β’ ((π β§ π¦ β π΅ β§ π¦ < 0 ) β (π¦(+gβπ)((invgβπ)βπ¦)) < ( 0 (+gβπ)((invgβπ)βπ¦))) |
53 | 4, 50, 5, 19 | grprinv 18875 |
. . . . . . 7
β’ ((π β Grp β§ π¦ β π΅) β (π¦(+gβπ)((invgβπ)βπ¦)) = 0 ) |
54 | 27, 28, 53 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π¦ β π΅ β§ π¦ < 0 ) β (π¦(+gβπ)((invgβπ)βπ¦)) = 0 ) |
55 | 4, 50, 5 | grplid 18852 |
. . . . . . 7
β’ ((π β Grp β§
((invgβπ)βπ¦) β π΅) β ( 0 (+gβπ)((invgβπ)βπ¦)) = ((invgβπ)βπ¦)) |
56 | 27, 46, 55 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π¦ β π΅ β§ π¦ < 0 ) β ( 0
(+gβπ)((invgβπ)βπ¦)) = ((invgβπ)βπ¦)) |
57 | 52, 54, 56 | 3brtr3d 5180 |
. . . . 5
β’ ((π β§ π¦ β π΅ β§ π¦ < 0 ) β 0 <
((invgβπ)βπ¦)) |
58 | 4, 5, 36, 37, 6, 25, 39, 17, 41, 44, 46, 57 | archiabllem1a 32337 |
. . . 4
β’ ((π β§ π¦ β π΅ β§ π¦ < 0 ) β βπ β β
((invgβπ)βπ¦) = (π Β· π)) |
59 | 35, 58 | r19.29a 3163 |
. . 3
β’ ((π β§ π¦ β π΅ β§ π¦ < 0 ) β βπ β β€ π¦ = (π Β· π)) |
60 | 59 | 3expa 1119 |
. 2
β’ (((π β§ π¦ β π΅) β§ π¦ < 0 ) β βπ β β€ π¦ = (π Β· π)) |
61 | | nnssz 12580 |
. . 3
β’ β
β β€ |
62 | 24 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π¦ β π΅ β§ 0 < π¦) β π β oGrp) |
63 | 38 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π¦ β π΅ β§ 0 < π¦) β π β Archi) |
64 | 3 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π¦ β π΅ β§ 0 < π¦) β π β π΅) |
65 | 40 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β§ π¦ β π΅ β§ 0 < π¦) β 0 < π) |
66 | | simp1 1137 |
. . . . . 6
β’ ((π β§ π¦ β π΅ β§ 0 < π¦) β π) |
67 | 66, 43 | syl3an1 1164 |
. . . . 5
β’ (((π β§ π¦ β π΅ β§ 0 < π¦) β§ π₯ β π΅ β§ 0 < π₯) β π β€ π₯) |
68 | | simp2 1138 |
. . . . 5
β’ ((π β§ π¦ β π΅ β§ 0 < π¦) β π¦ β π΅) |
69 | | simp3 1139 |
. . . . 5
β’ ((π β§ π¦ β π΅ β§ 0 < π¦) β 0 < π¦) |
70 | 4, 5, 36, 37, 6, 62, 63, 64, 65, 67, 68, 69 | archiabllem1a 32337 |
. . . 4
β’ ((π β§ π¦ β π΅ β§ 0 < π¦) β βπ β β π¦ = (π Β· π)) |
71 | 70 | 3expa 1119 |
. . 3
β’ (((π β§ π¦ β π΅) β§ 0 < π¦) β βπ β β π¦ = (π Β· π)) |
72 | | ssrexv 4052 |
. . 3
β’ (β
β β€ β (βπ β β π¦ = (π Β· π) β βπ β β€ π¦ = (π Β· π))) |
73 | 61, 71, 72 | mpsyl 68 |
. 2
β’ (((π β§ π¦ β π΅) β§ 0 < π¦) β βπ β β€ π¦ = (π Β· π)) |
74 | | isogrp 32220 |
. . . . . 6
β’ (π β oGrp β (π β Grp β§ π β oMnd)) |
75 | 74 | simprbi 498 |
. . . . 5
β’ (π β oGrp β π β oMnd) |
76 | | omndtos 32223 |
. . . . 5
β’ (π β oMnd β π β Toset) |
77 | 24, 75, 76 | 3syl 18 |
. . . 4
β’ (π β π β Toset) |
78 | 77 | adantr 482 |
. . 3
β’ ((π β§ π¦ β π΅) β π β Toset) |
79 | | simpr 486 |
. . 3
β’ ((π β§ π¦ β π΅) β π¦ β π΅) |
80 | 24, 26, 47 | 3syl 18 |
. . . 4
β’ (π β 0 β π΅) |
81 | 80 | adantr 482 |
. . 3
β’ ((π β§ π¦ β π΅) β 0 β π΅) |
82 | 4, 37 | tlt3 32140 |
. . 3
β’ ((π β Toset β§ π¦ β π΅ β§ 0 β π΅) β (π¦ = 0 β¨ π¦ < 0 β¨ 0 < π¦)) |
83 | 78, 79, 81, 82 | syl3anc 1372 |
. 2
β’ ((π β§ π¦ β π΅) β (π¦ = 0 β¨ π¦ < 0 β¨ 0 < π¦)) |
84 | 13, 60, 73, 83 | mpjao3dan 1432 |
1
β’ ((π β§ π¦ β π΅) β βπ β β€ π¦ = (π Β· π)) |