Metamath Proof Explorer

Theorem archiabllem2b

Description: Lemma for archiabl . (Contributed by Thierry Arnoux, 1-May-2018)

Ref Expression
Hypotheses archiabllem.b 
|- B = ( Base ` W )
archiabllem.0 
|- .0. = ( 0g ` W )
archiabllem.e 
|- .<_ = ( le ` W )
archiabllem.t 
|- .< = ( lt ` W )
archiabllem.m 
|- .x. = ( .g ` W )
archiabllem.g 
|- ( ph -> W e. oGrp )
archiabllem.a 
|- ( ph -> W e. Archi )
archiabllem2.1 
|- .+ = ( +g ` W )
archiabllem2.2 
|- ( ph -> ( oppG ` W ) e. oGrp )
archiabllem2.3 
|- ( ( ph /\ a e. B /\ .0. .< a ) -> E. b e. B ( .0. .< b /\ b .< a ) )
archiabllem2b.4 
|- ( ph -> X e. B )
archiabllem2b.5 
|- ( ph -> Y e. B )
Assertion archiabllem2b 
|- ( ph -> ( X .+ Y ) = ( Y .+ X ) )

Proof

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