Metamath Proof Explorer

Theorem archiabllem1

Description: Archimedean ordered groups with a minimal positive value are abelian. (Contributed by Thierry Arnoux, 13-Apr-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 )
archiabllem1.u 
|- ( ph -> U e. B )
archiabllem1.p 
|- ( ph -> .0. .< U )
archiabllem1.s 
|- ( ( ph /\ x e. B /\ .0. .< x ) -> U .<_ x )
Assertion archiabllem1 
|- ( 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 archiabllem1.u 
 |-  ( ph -> U e. B )
9 archiabllem1.p 
 |-  ( ph -> .0. .< U )
10 archiabllem1.s 
 |-  ( ( ph /\ x e. B /\ .0. .< x ) -> U .<_ x )
11 ogrpgrp 
 |-  ( W e. oGrp -> W e. Grp )
12 6 11 syl 
 |-  ( ph -> W e. Grp )
13 simplr 
 |-  ( ( ( ph /\ m e. ZZ ) /\ n e. ZZ ) -> m e. ZZ )
14 13 zcnd 
 |-  ( ( ( ph /\ m e. ZZ ) /\ n e. ZZ ) -> m e. CC )
15 simpr 
 |-  ( ( ( ph /\ m e. ZZ ) /\ n e. ZZ ) -> n e. ZZ )
16 15 zcnd 
 |-  ( ( ( ph /\ m e. ZZ ) /\ n e. ZZ ) -> n e. CC )
17 14 16 addcomd 
 |-  ( ( ( ph /\ m e. ZZ ) /\ n e. ZZ ) -> ( m + n ) = ( n + m ) )
18 17 oveq1d 
 |-  ( ( ( ph /\ m e. ZZ ) /\ n e. ZZ ) -> ( ( m + n ) .x. U ) = ( ( n + m ) .x. U ) )
19 12 ad2antrr 
 |-  ( ( ( ph /\ m e. ZZ ) /\ n e. ZZ ) -> W e. Grp )
20 8 ad2antrr 
 |-  ( ( ( ph /\ m e. ZZ ) /\ n e. ZZ ) -> U e. B )
21 eqid 
 |-  ( +g ` W ) = ( +g ` W )
22 1 5 21 mulgdir 
 |-  ( ( W e. Grp /\ ( m e. ZZ /\ n e. ZZ /\ U e. B ) ) -> ( ( m + n ) .x. U ) = ( ( m .x. U ) ( +g ` W ) ( n .x. U ) ) )
23 19 13 15 20 22 syl13anc 
 |-  ( ( ( ph /\ m e. ZZ ) /\ n e. ZZ ) -> ( ( m + n ) .x. U ) = ( ( m .x. U ) ( +g ` W ) ( n .x. U ) ) )
24 1 5 21 mulgdir 
 |-  ( ( W e. Grp /\ ( n e. ZZ /\ m e. ZZ /\ U e. B ) ) -> ( ( n + m ) .x. U ) = ( ( n .x. U ) ( +g ` W ) ( m .x. U ) ) )
25 19 15 13 20 24 syl13anc 
 |-  ( ( ( ph /\ m e. ZZ ) /\ n e. ZZ ) -> ( ( n + m ) .x. U ) = ( ( n .x. U ) ( +g ` W ) ( m .x. U ) ) )
26 18 23 25 3eqtr3d 
 |-  ( ( ( ph /\ m e. ZZ ) /\ n e. ZZ ) -> ( ( m .x. U ) ( +g ` W ) ( n .x. U ) ) = ( ( n .x. U ) ( +g ` W ) ( m .x. U ) ) )
27 26 adantllr 
 |-  ( ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ m e. ZZ ) /\ n e. ZZ ) -> ( ( m .x. U ) ( +g ` W ) ( n .x. U ) ) = ( ( n .x. U ) ( +g ` W ) ( m .x. U ) ) )
28 27 adantlr 
 |-  ( ( ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ m e. ZZ ) /\ y = ( m .x. U ) ) /\ n e. ZZ ) -> ( ( m .x. U ) ( +g ` W ) ( n .x. U ) ) = ( ( n .x. U ) ( +g ` W ) ( m .x. U ) ) )
29 28 adantr 
 |-  ( ( ( ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ m e. ZZ ) /\ y = ( m .x. U ) ) /\ n e. ZZ ) /\ z = ( n .x. U ) ) -> ( ( m .x. U ) ( +g ` W ) ( n .x. U ) ) = ( ( n .x. U ) ( +g ` W ) ( m .x. U ) ) )
30 simpllr 
 |-  ( ( ( ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ m e. ZZ ) /\ y = ( m .x. U ) ) /\ n e. ZZ ) /\ z = ( n .x. U ) ) -> y = ( m .x. U ) )
31 simpr 
 |-  ( ( ( ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ m e. ZZ ) /\ y = ( m .x. U ) ) /\ n e. ZZ ) /\ z = ( n .x. U ) ) -> z = ( n .x. U ) )
32 30 31 oveq12d 
 |-  ( ( ( ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ m e. ZZ ) /\ y = ( m .x. U ) ) /\ n e. ZZ ) /\ z = ( n .x. U ) ) -> ( y ( +g ` W ) z ) = ( ( m .x. U ) ( +g ` W ) ( n .x. U ) ) )
33 31 30 oveq12d 
 |-  ( ( ( ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ m e. ZZ ) /\ y = ( m .x. U ) ) /\ n e. ZZ ) /\ z = ( n .x. U ) ) -> ( z ( +g ` W ) y ) = ( ( n .x. U ) ( +g ` W ) ( m .x. U ) ) )
34 29 32 33 3eqtr4d 
 |-  ( ( ( ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ m e. ZZ ) /\ y = ( m .x. U ) ) /\ n e. ZZ ) /\ z = ( n .x. U ) ) -> ( y ( +g ` W ) z ) = ( z ( +g ` W ) y ) )
35 simplll 
 |-  ( ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ m e. ZZ ) /\ y = ( m .x. U ) ) -> ph )
36 simpr1r 
 |-  ( ( ph /\ ( ( y e. B /\ z e. B ) /\ m e. ZZ /\ y = ( m .x. U ) ) ) -> z e. B )
37 36 3anassrs 
 |-  ( ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ m e. ZZ ) /\ y = ( m .x. U ) ) -> z e. B )
38 1 2 3 4 5 6 7 8 9 10 archiabllem1b 
 |-  ( ( ph /\ z e. B ) -> E. n e. ZZ z = ( n .x. U ) )
39 35 37 38 syl2anc 
 |-  ( ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ m e. ZZ ) /\ y = ( m .x. U ) ) -> E. n e. ZZ z = ( n .x. U ) )
40 34 39 r19.29a 
 |-  ( ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ m e. ZZ ) /\ y = ( m .x. U ) ) -> ( y ( +g ` W ) z ) = ( z ( +g ` W ) y ) )
41 1 2 3 4 5 6 7 8 9 10 archiabllem1b 
 |-  ( ( ph /\ y e. B ) -> E. m e. ZZ y = ( m .x. U ) )
42 41 adantrr 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> E. m e. ZZ y = ( m .x. U ) )
43 40 42 r19.29a 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y ( +g ` W ) z ) = ( z ( +g ` W ) y ) )
44 43 ralrimivva 
 |-  ( ph -> A. y e. B A. z e. B ( y ( +g ` W ) z ) = ( z ( +g ` W ) y ) )
45 1 21 isabl2 
 |-  ( W e. Abel <-> ( W e. Grp /\ A. y e. B A. z e. B ( y ( +g ` W ) z ) = ( z ( +g ` W ) y ) ) )
46 12 44 45 sylanbrc 
 |-  ( ph -> W e. Abel )