This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem archiabllem2

Description: Archimedean ordered groups with no minimal positive value are abelian. (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 ) )
Assertion archiabllem2 
|- ( ph -> W e. Abel )

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 ogrpgrp 
 |-  ( W e. oGrp -> W e. Grp )
12 6 11 syl 
 |-  ( ph -> W e. Grp )
13 6 3ad2ant1 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> W e. oGrp )
14 7 3ad2ant1 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> W e. Archi )
15 9 3ad2ant1 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( oppG ` W ) e. oGrp )
16 simp1 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ph )
17 16 10 syl3an1 
 |-  ( ( ( ph /\ x e. B /\ y e. B ) /\ a e. B /\ .0. .< a ) -> E. b e. B ( .0. .< b /\ b .< a ) )
18 simp2 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> x e. B )
19 simp3 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> y e. B )
20 1 2 3 4 5 13 14 8 15 17 18 19 archiabllem2b 
 |-  ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) = ( y .+ x ) )
21 20 3expb 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) = ( y .+ x ) )
22 21 ralrimivva 
 |-  ( ph -> A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) )
23 1 8 isabl2 
 |-  ( W e. Abel <-> ( W e. Grp /\ A. x e. B A. y e. B ( x .+ y ) = ( y .+ x ) ) )
24 12 22 23 sylanbrc 
 |-  ( ph -> W e. Abel )