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 𝐵 = ( Base ‘ 𝑊 )
archiabllem.0 0 = ( 0g𝑊 )
archiabllem.e = ( le ‘ 𝑊 )
archiabllem.t < = ( lt ‘ 𝑊 )
archiabllem.m · = ( .g𝑊 )
archiabllem.g ( 𝜑𝑊 ∈ oGrp )
archiabllem.a ( 𝜑𝑊 ∈ Archi )
archiabllem2.1 + = ( +g𝑊 )
archiabllem2.2 ( 𝜑 → ( oppg𝑊 ) ∈ oGrp )
archiabllem2.3 ( ( 𝜑𝑎𝐵0 < 𝑎 ) → ∃ 𝑏𝐵 ( 0 < 𝑏𝑏 < 𝑎 ) )
archiabllem2a.4 ( 𝜑𝑋𝐵 )
archiabllem2a.5 ( 𝜑0 < 𝑋 )
Assertion archiabllem2a ( 𝜑 → ∃ 𝑐𝐵 ( 0 < 𝑐 ∧ ( 𝑐 + 𝑐 ) 𝑋 ) )

Proof

Step Hyp Ref Expression
1 archiabllem.b 𝐵 = ( Base ‘ 𝑊 )
2 archiabllem.0 0 = ( 0g𝑊 )
3 archiabllem.e = ( le ‘ 𝑊 )
4 archiabllem.t < = ( lt ‘ 𝑊 )
5 archiabllem.m · = ( .g𝑊 )
6 archiabllem.g ( 𝜑𝑊 ∈ oGrp )
7 archiabllem.a ( 𝜑𝑊 ∈ Archi )
8 archiabllem2.1 + = ( +g𝑊 )
9 archiabllem2.2 ( 𝜑 → ( oppg𝑊 ) ∈ oGrp )
10 archiabllem2.3 ( ( 𝜑𝑎𝐵0 < 𝑎 ) → ∃ 𝑏𝐵 ( 0 < 𝑏𝑏 < 𝑎 ) )
11 archiabllem2a.4 ( 𝜑𝑋𝐵 )
12 archiabllem2a.5 ( 𝜑0 < 𝑋 )
13 simpllr ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ ( 𝑏 + 𝑏 ) 𝑋 ) → 𝑏𝐵 )
14 simplrl ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ ( 𝑏 + 𝑏 ) 𝑋 ) → 0 < 𝑏 )
15 simpr ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ ( 𝑏 + 𝑏 ) 𝑋 ) → ( 𝑏 + 𝑏 ) 𝑋 )
16 breq2 ( 𝑐 = 𝑏 → ( 0 < 𝑐0 < 𝑏 ) )
17 id ( 𝑐 = 𝑏𝑐 = 𝑏 )
18 17 17 oveq12d ( 𝑐 = 𝑏 → ( 𝑐 + 𝑐 ) = ( 𝑏 + 𝑏 ) )
19 18 breq1d ( 𝑐 = 𝑏 → ( ( 𝑐 + 𝑐 ) 𝑋 ↔ ( 𝑏 + 𝑏 ) 𝑋 ) )
20 16 19 anbi12d ( 𝑐 = 𝑏 → ( ( 0 < 𝑐 ∧ ( 𝑐 + 𝑐 ) 𝑋 ) ↔ ( 0 < 𝑏 ∧ ( 𝑏 + 𝑏 ) 𝑋 ) ) )
21 20 rspcev ( ( 𝑏𝐵 ∧ ( 0 < 𝑏 ∧ ( 𝑏 + 𝑏 ) 𝑋 ) ) → ∃ 𝑐𝐵 ( 0 < 𝑐 ∧ ( 𝑐 + 𝑐 ) 𝑋 ) )
22 13 14 15 21 syl12anc ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ ( 𝑏 + 𝑏 ) 𝑋 ) → ∃ 𝑐𝐵 ( 0 < 𝑐 ∧ ( 𝑐 + 𝑐 ) 𝑋 ) )
23 simplll ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → 𝜑 )
24 ogrpgrp ( 𝑊 ∈ oGrp → 𝑊 ∈ Grp )
25 23 6 24 3syl ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → 𝑊 ∈ Grp )
26 23 11 syl ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → 𝑋𝐵 )
27 simpllr ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → 𝑏𝐵 )
28 eqid ( -g𝑊 ) = ( -g𝑊 )
29 1 28 grpsubcl ( ( 𝑊 ∈ Grp ∧ 𝑋𝐵𝑏𝐵 ) → ( 𝑋 ( -g𝑊 ) 𝑏 ) ∈ 𝐵 )
30 25 26 27 29 syl3anc ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( 𝑋 ( -g𝑊 ) 𝑏 ) ∈ 𝐵 )
31 1 2 28 grpsubid ( ( 𝑊 ∈ Grp ∧ 𝑏𝐵 ) → ( 𝑏 ( -g𝑊 ) 𝑏 ) = 0 )
32 25 27 31 syl2anc ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( 𝑏 ( -g𝑊 ) 𝑏 ) = 0 )
33 23 6 syl ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → 𝑊 ∈ oGrp )
34 simplrr ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → 𝑏 < 𝑋 )
35 1 4 28 ogrpsublt ( ( 𝑊 ∈ oGrp ∧ ( 𝑏𝐵𝑋𝐵𝑏𝐵 ) ∧ 𝑏 < 𝑋 ) → ( 𝑏 ( -g𝑊 ) 𝑏 ) < ( 𝑋 ( -g𝑊 ) 𝑏 ) )
36 33 27 26 27 34 35 syl131anc ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( 𝑏 ( -g𝑊 ) 𝑏 ) < ( 𝑋 ( -g𝑊 ) 𝑏 ) )
37 32 36 eqbrtrrd ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → 0 < ( 𝑋 ( -g𝑊 ) 𝑏 ) )
38 23 9 syl ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( oppg𝑊 ) ∈ oGrp )
39 1 8 grpcl ( ( 𝑊 ∈ Grp ∧ 𝑏𝐵𝑏𝐵 ) → ( 𝑏 + 𝑏 ) ∈ 𝐵 )
40 25 27 27 39 syl3anc ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( 𝑏 + 𝑏 ) ∈ 𝐵 )
41 simpr ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → 𝑋 < ( 𝑏 + 𝑏 ) )
42 1 4 28 ogrpsublt ( ( 𝑊 ∈ oGrp ∧ ( 𝑋𝐵 ∧ ( 𝑏 + 𝑏 ) ∈ 𝐵𝑏𝐵 ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( 𝑋 ( -g𝑊 ) 𝑏 ) < ( ( 𝑏 + 𝑏 ) ( -g𝑊 ) 𝑏 ) )
43 33 26 40 27 41 42 syl131anc ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( 𝑋 ( -g𝑊 ) 𝑏 ) < ( ( 𝑏 + 𝑏 ) ( -g𝑊 ) 𝑏 ) )
44 1 8 28 grpaddsubass ( ( 𝑊 ∈ Grp ∧ ( 𝑏𝐵𝑏𝐵𝑏𝐵 ) ) → ( ( 𝑏 + 𝑏 ) ( -g𝑊 ) 𝑏 ) = ( 𝑏 + ( 𝑏 ( -g𝑊 ) 𝑏 ) ) )
45 25 27 27 27 44 syl13anc ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( ( 𝑏 + 𝑏 ) ( -g𝑊 ) 𝑏 ) = ( 𝑏 + ( 𝑏 ( -g𝑊 ) 𝑏 ) ) )
46 32 oveq2d ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( 𝑏 + ( 𝑏 ( -g𝑊 ) 𝑏 ) ) = ( 𝑏 + 0 ) )
47 1 8 2 grprid ( ( 𝑊 ∈ Grp ∧ 𝑏𝐵 ) → ( 𝑏 + 0 ) = 𝑏 )
48 25 27 47 syl2anc ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( 𝑏 + 0 ) = 𝑏 )
49 45 46 48 3eqtrd ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( ( 𝑏 + 𝑏 ) ( -g𝑊 ) 𝑏 ) = 𝑏 )
50 43 49 breqtrd ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( 𝑋 ( -g𝑊 ) 𝑏 ) < 𝑏 )
51 1 4 8 25 38 30 27 30 50 ogrpaddltrd ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( ( 𝑋 ( -g𝑊 ) 𝑏 ) + ( 𝑋 ( -g𝑊 ) 𝑏 ) ) < ( ( 𝑋 ( -g𝑊 ) 𝑏 ) + 𝑏 ) )
52 1 8 28 grpnpcan ( ( 𝑊 ∈ Grp ∧ 𝑋𝐵𝑏𝐵 ) → ( ( 𝑋 ( -g𝑊 ) 𝑏 ) + 𝑏 ) = 𝑋 )
53 25 26 27 52 syl3anc ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( ( 𝑋 ( -g𝑊 ) 𝑏 ) + 𝑏 ) = 𝑋 )
54 51 53 breqtrd ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( ( 𝑋 ( -g𝑊 ) 𝑏 ) + ( 𝑋 ( -g𝑊 ) 𝑏 ) ) < 𝑋 )
55 ovexd ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( ( 𝑋 ( -g𝑊 ) 𝑏 ) + ( 𝑋 ( -g𝑊 ) 𝑏 ) ) ∈ V )
56 3 4 pltle ( ( 𝑊 ∈ Grp ∧ ( ( 𝑋 ( -g𝑊 ) 𝑏 ) + ( 𝑋 ( -g𝑊 ) 𝑏 ) ) ∈ V ∧ 𝑋𝐵 ) → ( ( ( 𝑋 ( -g𝑊 ) 𝑏 ) + ( 𝑋 ( -g𝑊 ) 𝑏 ) ) < 𝑋 → ( ( 𝑋 ( -g𝑊 ) 𝑏 ) + ( 𝑋 ( -g𝑊 ) 𝑏 ) ) 𝑋 ) )
57 25 55 26 56 syl3anc ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( ( ( 𝑋 ( -g𝑊 ) 𝑏 ) + ( 𝑋 ( -g𝑊 ) 𝑏 ) ) < 𝑋 → ( ( 𝑋 ( -g𝑊 ) 𝑏 ) + ( 𝑋 ( -g𝑊 ) 𝑏 ) ) 𝑋 ) )
58 54 57 mpd ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ( ( 𝑋 ( -g𝑊 ) 𝑏 ) + ( 𝑋 ( -g𝑊 ) 𝑏 ) ) 𝑋 )
59 breq2 ( 𝑐 = ( 𝑋 ( -g𝑊 ) 𝑏 ) → ( 0 < 𝑐0 < ( 𝑋 ( -g𝑊 ) 𝑏 ) ) )
60 id ( 𝑐 = ( 𝑋 ( -g𝑊 ) 𝑏 ) → 𝑐 = ( 𝑋 ( -g𝑊 ) 𝑏 ) )
61 60 60 oveq12d ( 𝑐 = ( 𝑋 ( -g𝑊 ) 𝑏 ) → ( 𝑐 + 𝑐 ) = ( ( 𝑋 ( -g𝑊 ) 𝑏 ) + ( 𝑋 ( -g𝑊 ) 𝑏 ) ) )
62 61 breq1d ( 𝑐 = ( 𝑋 ( -g𝑊 ) 𝑏 ) → ( ( 𝑐 + 𝑐 ) 𝑋 ↔ ( ( 𝑋 ( -g𝑊 ) 𝑏 ) + ( 𝑋 ( -g𝑊 ) 𝑏 ) ) 𝑋 ) )
63 59 62 anbi12d ( 𝑐 = ( 𝑋 ( -g𝑊 ) 𝑏 ) → ( ( 0 < 𝑐 ∧ ( 𝑐 + 𝑐 ) 𝑋 ) ↔ ( 0 < ( 𝑋 ( -g𝑊 ) 𝑏 ) ∧ ( ( 𝑋 ( -g𝑊 ) 𝑏 ) + ( 𝑋 ( -g𝑊 ) 𝑏 ) ) 𝑋 ) ) )
64 63 rspcev ( ( ( 𝑋 ( -g𝑊 ) 𝑏 ) ∈ 𝐵 ∧ ( 0 < ( 𝑋 ( -g𝑊 ) 𝑏 ) ∧ ( ( 𝑋 ( -g𝑊 ) 𝑏 ) + ( 𝑋 ( -g𝑊 ) 𝑏 ) ) 𝑋 ) ) → ∃ 𝑐𝐵 ( 0 < 𝑐 ∧ ( 𝑐 + 𝑐 ) 𝑋 ) )
65 30 37 58 64 syl12anc ( ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) ∧ 𝑋 < ( 𝑏 + 𝑏 ) ) → ∃ 𝑐𝐵 ( 0 < 𝑐 ∧ ( 𝑐 + 𝑐 ) 𝑋 ) )
66 6 ad2antrr ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) → 𝑊 ∈ oGrp )
67 isogrp ( 𝑊 ∈ oGrp ↔ ( 𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd ) )
68 67 simprbi ( 𝑊 ∈ oGrp → 𝑊 ∈ oMnd )
69 omndtos ( 𝑊 ∈ oMnd → 𝑊 ∈ Toset )
70 66 68 69 3syl ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) → 𝑊 ∈ Toset )
71 66 24 syl ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) → 𝑊 ∈ Grp )
72 simplr ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) → 𝑏𝐵 )
73 71 72 72 39 syl3anc ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) → ( 𝑏 + 𝑏 ) ∈ 𝐵 )
74 11 ad2antrr ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) → 𝑋𝐵 )
75 1 3 4 tlt2 ( ( 𝑊 ∈ Toset ∧ ( 𝑏 + 𝑏 ) ∈ 𝐵𝑋𝐵 ) → ( ( 𝑏 + 𝑏 ) 𝑋𝑋 < ( 𝑏 + 𝑏 ) ) )
76 70 73 74 75 syl3anc ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) → ( ( 𝑏 + 𝑏 ) 𝑋𝑋 < ( 𝑏 + 𝑏 ) ) )
77 22 65 76 mpjaodan ( ( ( 𝜑𝑏𝐵 ) ∧ ( 0 < 𝑏𝑏 < 𝑋 ) ) → ∃ 𝑐𝐵 ( 0 < 𝑐 ∧ ( 𝑐 + 𝑐 ) 𝑋 ) )
78 10 3expia ( ( 𝜑𝑎𝐵 ) → ( 0 < 𝑎 → ∃ 𝑏𝐵 ( 0 < 𝑏𝑏 < 𝑎 ) ) )
79 78 ralrimiva ( 𝜑 → ∀ 𝑎𝐵 ( 0 < 𝑎 → ∃ 𝑏𝐵 ( 0 < 𝑏𝑏 < 𝑎 ) ) )
80 breq2 ( 𝑎 = 𝑋 → ( 0 < 𝑎0 < 𝑋 ) )
81 breq2 ( 𝑎 = 𝑋 → ( 𝑏 < 𝑎𝑏 < 𝑋 ) )
82 81 anbi2d ( 𝑎 = 𝑋 → ( ( 0 < 𝑏𝑏 < 𝑎 ) ↔ ( 0 < 𝑏𝑏 < 𝑋 ) ) )
83 82 rexbidv ( 𝑎 = 𝑋 → ( ∃ 𝑏𝐵 ( 0 < 𝑏𝑏 < 𝑎 ) ↔ ∃ 𝑏𝐵 ( 0 < 𝑏𝑏 < 𝑋 ) ) )
84 80 83 imbi12d ( 𝑎 = 𝑋 → ( ( 0 < 𝑎 → ∃ 𝑏𝐵 ( 0 < 𝑏𝑏 < 𝑎 ) ) ↔ ( 0 < 𝑋 → ∃ 𝑏𝐵 ( 0 < 𝑏𝑏 < 𝑋 ) ) ) )
85 84 rspcv ( 𝑋𝐵 → ( ∀ 𝑎𝐵 ( 0 < 𝑎 → ∃ 𝑏𝐵 ( 0 < 𝑏𝑏 < 𝑎 ) ) → ( 0 < 𝑋 → ∃ 𝑏𝐵 ( 0 < 𝑏𝑏 < 𝑋 ) ) ) )
86 11 79 12 85 syl3c ( 𝜑 → ∃ 𝑏𝐵 ( 0 < 𝑏𝑏 < 𝑋 ) )
87 77 86 r19.29a ( 𝜑 → ∃ 𝑐𝐵 ( 0 < 𝑐 ∧ ( 𝑐 + 𝑐 ) 𝑋 ) )