Metamath Proof Explorer

Theorem archiabllem2a

Description: Lemma for archiabl , which requires the group to be both left- and right-ordered. (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 )
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 ) )
archiabllem2a.4 
|- ( ph -> X e. B )
archiabllem2a.5 
|- ( ph -> .0. .< X )
Assertion archiabllem2a 
|- ( ph -> E. c e. B ( .0. .< c /\ ( c .+ c ) .<_ 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 archiabllem2a.4 
 |-  ( ph -> X e. B )
12 archiabllem2a.5 
 |-  ( ph -> .0. .< X )
13 simpllr 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ ( b .+ b ) .<_ X ) -> b e. B )
14 simplrl 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ ( b .+ b ) .<_ X ) -> .0. .< b )
15 simpr 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ ( b .+ b ) .<_ X ) -> ( b .+ b ) .<_ X )
16 breq2 
 |-  ( c = b -> ( .0. .< c <-> .0. .< b ) )
17 id 
 |-  ( c = b -> c = b )
18 17 17 oveq12d 
 |-  ( c = b -> ( c .+ c ) = ( b .+ b ) )
19 18 breq1d 
 |-  ( c = b -> ( ( c .+ c ) .<_ X <-> ( b .+ b ) .<_ X ) )
20 16 19 anbi12d 
 |-  ( c = b -> ( ( .0. .< c /\ ( c .+ c ) .<_ X ) <-> ( .0. .< b /\ ( b .+ b ) .<_ X ) ) )
21 20 rspcev 
 |-  ( ( b e. B /\ ( .0. .< b /\ ( b .+ b ) .<_ X ) ) -> E. c e. B ( .0. .< c /\ ( c .+ c ) .<_ X ) )
22 13 14 15 21 syl12anc 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ ( b .+ b ) .<_ X ) -> E. c e. B ( .0. .< c /\ ( c .+ c ) .<_ X ) )
23 simplll 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> ph )
24 ogrpgrp 
 |-  ( W e. oGrp -> W e. Grp )
25 23 6 24 3syl 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> W e. Grp )
26 23 11 syl 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> X e. B )
27 simpllr 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> b e. B )
28 eqid 
 |-  ( -g ` W ) = ( -g ` W )
29 1 28 grpsubcl 
 |-  ( ( W e. Grp /\ X e. B /\ b e. B ) -> ( X ( -g ` W ) b ) e. B )
30 25 26 27 29 syl3anc 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> ( X ( -g ` W ) b ) e. B )
31 1 2 28 grpsubid 
 |-  ( ( W e. Grp /\ b e. B ) -> ( b ( -g ` W ) b ) = .0. )
32 25 27 31 syl2anc 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> ( b ( -g ` W ) b ) = .0. )
33 23 6 syl 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> W e. oGrp )
34 simplrr 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> b .< X )
35 1 4 28 ogrpsublt 
 |-  ( ( W e. oGrp /\ ( b e. B /\ X e. B /\ b e. B ) /\ b .< X ) -> ( b ( -g ` W ) b ) .< ( X ( -g ` W ) b ) )
36 33 27 26 27 34 35 syl131anc 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> ( b ( -g ` W ) b ) .< ( X ( -g ` W ) b ) )
37 32 36 eqbrtrrd 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> .0. .< ( X ( -g ` W ) b ) )
38 23 9 syl 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> ( oppG ` W ) e. oGrp )
39 1 8 grpcl 
 |-  ( ( W e. Grp /\ b e. B /\ b e. B ) -> ( b .+ b ) e. B )
40 25 27 27 39 syl3anc 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> ( b .+ b ) e. B )
41 simpr 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> X .< ( b .+ b ) )
42 1 4 28 ogrpsublt 
 |-  ( ( W e. oGrp /\ ( X e. B /\ ( b .+ b ) e. B /\ b e. B ) /\ X .< ( b .+ b ) ) -> ( X ( -g ` W ) b ) .< ( ( b .+ b ) ( -g ` W ) b ) )
43 33 26 40 27 41 42 syl131anc 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> ( X ( -g ` W ) b ) .< ( ( b .+ b ) ( -g ` W ) b ) )
44 1 8 28 grpaddsubass 
 |-  ( ( W e. Grp /\ ( b e. B /\ b e. B /\ b e. B ) ) -> ( ( b .+ b ) ( -g ` W ) b ) = ( b .+ ( b ( -g ` W ) b ) ) )
45 25 27 27 27 44 syl13anc 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> ( ( b .+ b ) ( -g ` W ) b ) = ( b .+ ( b ( -g ` W ) b ) ) )
46 32 oveq2d 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> ( b .+ ( b ( -g ` W ) b ) ) = ( b .+ .0. ) )
47 1 8 2 grprid 
 |-  ( ( W e. Grp /\ b e. B ) -> ( b .+ .0. ) = b )
48 25 27 47 syl2anc 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> ( b .+ .0. ) = b )
49 45 46 48 3eqtrd 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> ( ( b .+ b ) ( -g ` W ) b ) = b )
50 43 49 breqtrd 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> ( X ( -g ` W ) b ) .< b )
51 1 4 8 25 38 30 27 30 50 ogrpaddltrd 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> ( ( X ( -g ` W ) b ) .+ ( X ( -g ` W ) b ) ) .< ( ( X ( -g ` W ) b ) .+ b ) )
52 1 8 28 grpnpcan 
 |-  ( ( W e. Grp /\ X e. B /\ b e. B ) -> ( ( X ( -g ` W ) b ) .+ b ) = X )
53 25 26 27 52 syl3anc 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> ( ( X ( -g ` W ) b ) .+ b ) = X )
54 51 53 breqtrd 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> ( ( X ( -g ` W ) b ) .+ ( X ( -g ` W ) b ) ) .< X )
55 ovexd 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> ( ( X ( -g ` W ) b ) .+ ( X ( -g ` W ) b ) ) e. _V )
56 3 4 pltle 
 |-  ( ( W e. Grp /\ ( ( X ( -g ` W ) b ) .+ ( X ( -g ` W ) b ) ) e. _V /\ X e. B ) -> ( ( ( X ( -g ` W ) b ) .+ ( X ( -g ` W ) b ) ) .< X -> ( ( X ( -g ` W ) b ) .+ ( X ( -g ` W ) b ) ) .<_ X ) )
57 25 55 26 56 syl3anc 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> ( ( ( X ( -g ` W ) b ) .+ ( X ( -g ` W ) b ) ) .< X -> ( ( X ( -g ` W ) b ) .+ ( X ( -g ` W ) b ) ) .<_ X ) )
58 54 57 mpd 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> ( ( X ( -g ` W ) b ) .+ ( X ( -g ` W ) b ) ) .<_ X )
59 breq2 
 |-  ( c = ( X ( -g ` W ) b ) -> ( .0. .< c <-> .0. .< ( X ( -g ` W ) b ) ) )
60 id 
 |-  ( c = ( X ( -g ` W ) b ) -> c = ( X ( -g ` W ) b ) )
61 60 60 oveq12d 
 |-  ( c = ( X ( -g ` W ) b ) -> ( c .+ c ) = ( ( X ( -g ` W ) b ) .+ ( X ( -g ` W ) b ) ) )
62 61 breq1d 
 |-  ( c = ( X ( -g ` W ) b ) -> ( ( c .+ c ) .<_ X <-> ( ( X ( -g ` W ) b ) .+ ( X ( -g ` W ) b ) ) .<_ X ) )
63 59 62 anbi12d 
 |-  ( c = ( X ( -g ` W ) b ) -> ( ( .0. .< c /\ ( c .+ c ) .<_ X ) <-> ( .0. .< ( X ( -g ` W ) b ) /\ ( ( X ( -g ` W ) b ) .+ ( X ( -g ` W ) b ) ) .<_ X ) ) )
64 63 rspcev 
 |-  ( ( ( X ( -g ` W ) b ) e. B /\ ( .0. .< ( X ( -g ` W ) b ) /\ ( ( X ( -g ` W ) b ) .+ ( X ( -g ` W ) b ) ) .<_ X ) ) -> E. c e. B ( .0. .< c /\ ( c .+ c ) .<_ X ) )
65 30 37 58 64 syl12anc 
 |-  ( ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) /\ X .< ( b .+ b ) ) -> E. c e. B ( .0. .< c /\ ( c .+ c ) .<_ X ) )
66 6 ad2antrr 
 |-  ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) -> W e. oGrp )
67 isogrp 
 |-  ( W e. oGrp <-> ( W e. Grp /\ W e. oMnd ) )
68 67 simprbi 
 |-  ( W e. oGrp -> W e. oMnd )
69 omndtos 
 |-  ( W e. oMnd -> W e. Toset )
70 66 68 69 3syl 
 |-  ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) -> W e. Toset )
71 66 24 syl 
 |-  ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) -> W e. Grp )
72 simplr 
 |-  ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) -> b e. B )
73 71 72 72 39 syl3anc 
 |-  ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) -> ( b .+ b ) e. B )
74 11 ad2antrr 
 |-  ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) -> X e. B )
75 1 3 4 tlt2 
 |-  ( ( W e. Toset /\ ( b .+ b ) e. B /\ X e. B ) -> ( ( b .+ b ) .<_ X \/ X .< ( b .+ b ) ) )
76 70 73 74 75 syl3anc 
 |-  ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) -> ( ( b .+ b ) .<_ X \/ X .< ( b .+ b ) ) )
77 22 65 76 mpjaodan 
 |-  ( ( ( ph /\ b e. B ) /\ ( .0. .< b /\ b .< X ) ) -> E. c e. B ( .0. .< c /\ ( c .+ c ) .<_ X ) )
78 10 3expia 
 |-  ( ( ph /\ a e. B ) -> ( .0. .< a -> E. b e. B ( .0. .< b /\ b .< a ) ) )
79 78 ralrimiva 
 |-  ( ph -> A. a e. B ( .0. .< a -> E. b e. B ( .0. .< b /\ b .< a ) ) )
80 breq2 
 |-  ( a = X -> ( .0. .< a <-> .0. .< X ) )
81 breq2 
 |-  ( a = X -> ( b .< a <-> b .< X ) )
82 81 anbi2d 
 |-  ( a = X -> ( ( .0. .< b /\ b .< a ) <-> ( .0. .< b /\ b .< X ) ) )
83 82 rexbidv 
 |-  ( a = X -> ( E. b e. B ( .0. .< b /\ b .< a ) <-> E. b e. B ( .0. .< b /\ b .< X ) ) )
84 80 83 imbi12d 
 |-  ( a = X -> ( ( .0. .< a -> E. b e. B ( .0. .< b /\ b .< a ) ) <-> ( .0. .< X -> E. b e. B ( .0. .< b /\ b .< X ) ) ) )
85 84 rspcv 
 |-  ( X e. B -> ( A. a e. B ( .0. .< a -> E. b e. B ( .0. .< b /\ b .< a ) ) -> ( .0. .< X -> E. b e. B ( .0. .< b /\ b .< X ) ) ) )
86 11 79 12 85 syl3c 
 |-  ( ph -> E. b e. B ( .0. .< b /\ b .< X ) )
87 77 86 r19.29a 
 |-  ( ph -> E. c e. B ( .0. .< c /\ ( c .+ c ) .<_ X ) )