Step |
Hyp |
Ref |
Expression |
1 |
|
archiabllem.b |
|- B = ( Base ` W ) |
2 |
|
archiabllem.0 |
|- .0. = ( 0g ` W ) |
3 |
|
archiabllem.e |
|- .<_ = ( le ` W ) |
4 |
|
archiabllem.t |
|- .< = ( lt ` W ) |
5 |
|
archiabllem.m |
|- .x. = ( .g ` W ) |
6 |
|
archiabllem.g |
|- ( ph -> W e. oGrp ) |
7 |
|
archiabllem.a |
|- ( ph -> W e. Archi ) |
8 |
|
archiabllem2.1 |
|- .+ = ( +g ` W ) |
9 |
|
archiabllem2.2 |
|- ( ph -> ( oppG ` W ) e. oGrp ) |
10 |
|
archiabllem2.3 |
|- ( ( ph /\ a e. B /\ .0. .< a ) -> E. b e. B ( .0. .< b /\ b .< a ) ) |
11 |
|
archiabllem2b.4 |
|- ( ph -> X e. B ) |
12 |
|
archiabllem2b.5 |
|- ( ph -> Y e. B ) |
13 |
1 2 3 4 5 6 7 8 9 10 11 12
|
archiabllem2c |
|- ( ph -> -. ( X .+ Y ) .< ( Y .+ X ) ) |
14 |
1 2 3 4 5 6 7 8 9 10 12 11
|
archiabllem2c |
|- ( ph -> -. ( Y .+ X ) .< ( X .+ Y ) ) |
15 |
|
isogrp |
|- ( W e. oGrp <-> ( W e. Grp /\ W e. oMnd ) ) |
16 |
15
|
simprbi |
|- ( W e. oGrp -> W e. oMnd ) |
17 |
|
omndtos |
|- ( W e. oMnd -> W e. Toset ) |
18 |
6 16 17
|
3syl |
|- ( ph -> W e. Toset ) |
19 |
|
ogrpgrp |
|- ( W e. oGrp -> W e. Grp ) |
20 |
6 19
|
syl |
|- ( ph -> W e. Grp ) |
21 |
1 8
|
grpcl |
|- ( ( W e. Grp /\ X e. B /\ Y e. B ) -> ( X .+ Y ) e. B ) |
22 |
20 11 12 21
|
syl3anc |
|- ( ph -> ( X .+ Y ) e. B ) |
23 |
1 8
|
grpcl |
|- ( ( W e. Grp /\ Y e. B /\ X e. B ) -> ( Y .+ X ) e. B ) |
24 |
20 12 11 23
|
syl3anc |
|- ( ph -> ( Y .+ X ) e. B ) |
25 |
1 4
|
tlt3 |
|- ( ( W e. Toset /\ ( X .+ Y ) e. B /\ ( Y .+ X ) e. B ) -> ( ( X .+ Y ) = ( Y .+ X ) \/ ( X .+ Y ) .< ( Y .+ X ) \/ ( Y .+ X ) .< ( X .+ Y ) ) ) |
26 |
18 22 24 25
|
syl3anc |
|- ( ph -> ( ( X .+ Y ) = ( Y .+ X ) \/ ( X .+ Y ) .< ( Y .+ X ) \/ ( Y .+ X ) .< ( X .+ Y ) ) ) |
27 |
13 14 26
|
ecase23d |
|- ( ph -> ( X .+ Y ) = ( Y .+ X ) ) |