| 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 ) ) |