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 ˙ = 0 W
archiabllem.e ˙ = W
archiabllem.t < ˙ = < W
archiabllem.m · ˙ = W
archiabllem.g φ W oGrp
archiabllem.a φ W Archi
archiabllem2.1 + ˙ = + W
archiabllem2.2 φ opp 𝑔 W oGrp
archiabllem2.3 φ a B 0 ˙ < ˙ a b B 0 ˙ < ˙ b b < ˙ a
archiabllem2a.4 φ X B
archiabllem2a.5 φ 0 ˙ < ˙ X
Assertion archiabllem2a φ c B 0 ˙ < ˙ c c + ˙ c ˙ X

Proof

Step Hyp Ref Expression
1 archiabllem.b B = Base W
2 archiabllem.0 0 ˙ = 0 W
3 archiabllem.e ˙ = W
4 archiabllem.t < ˙ = < W
5 archiabllem.m · ˙ = W
6 archiabllem.g φ W oGrp
7 archiabllem.a φ W Archi
8 archiabllem2.1 + ˙ = + W
9 archiabllem2.2 φ opp 𝑔 W oGrp
10 archiabllem2.3 φ a B 0 ˙ < ˙ a b B 0 ˙ < ˙ b b < ˙ a
11 archiabllem2a.4 φ X B
12 archiabllem2a.5 φ 0 ˙ < ˙ X
13 simpllr φ b B 0 ˙ < ˙ b b < ˙ X b + ˙ b ˙ X b B
14 simplrl φ b B 0 ˙ < ˙ b b < ˙ X b + ˙ b ˙ X 0 ˙ < ˙ b
15 simpr φ b 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 B 0 ˙ < ˙ b b + ˙ b ˙ X c B 0 ˙ < ˙ c c + ˙ c ˙ X
22 13 14 15 21 syl12anc φ b B 0 ˙ < ˙ b b < ˙ X b + ˙ b ˙ X c B 0 ˙ < ˙ c c + ˙ c ˙ X
23 simplll φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b φ
24 ogrpgrp W oGrp W Grp
25 23 6 24 3syl φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b W Grp
26 23 11 syl φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b X B
27 simpllr φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b b B
28 eqid - W = - W
29 1 28 grpsubcl W Grp X B b B X - W b B
30 25 26 27 29 syl3anc φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b X - W b B
31 1 2 28 grpsubid W Grp b B b - W b = 0 ˙
32 25 27 31 syl2anc φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b b - W b = 0 ˙
33 23 6 syl φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b W oGrp
34 simplrr φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b b < ˙ X
35 1 4 28 ogrpsublt W oGrp b B X B b B b < ˙ X b - W b < ˙ X - W b
36 33 27 26 27 34 35 syl131anc φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b b - W b < ˙ X - W b
37 32 36 eqbrtrrd φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b 0 ˙ < ˙ X - W b
38 23 9 syl φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b opp 𝑔 W oGrp
39 1 8 grpcl W Grp b B b B b + ˙ b B
40 25 27 27 39 syl3anc φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b b + ˙ b B
41 simpr φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b X < ˙ b + ˙ b
42 1 4 28 ogrpsublt W oGrp X B b + ˙ b B b B X < ˙ b + ˙ b X - W b < ˙ b + ˙ b - W b
43 33 26 40 27 41 42 syl131anc φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b X - W b < ˙ b + ˙ b - W b
44 1 8 28 grpaddsubass W Grp b B b B b B b + ˙ b - W b = b + ˙ b - W b
45 25 27 27 27 44 syl13anc φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b b + ˙ b - W b = b + ˙ b - W b
46 32 oveq2d φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b b + ˙ b - W b = b + ˙ 0 ˙
47 1 8 2 grprid W Grp b B b + ˙ 0 ˙ = b
48 25 27 47 syl2anc φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b b + ˙ 0 ˙ = b
49 45 46 48 3eqtrd φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b b + ˙ b - W b = b
50 43 49 breqtrd φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b X - W b < ˙ b
51 1 4 8 25 38 30 27 30 50 ogrpaddltrd φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b X - W b + ˙ X - W b < ˙ X - W b + ˙ b
52 1 8 28 grpnpcan W Grp X B b B X - W b + ˙ b = X
53 25 26 27 52 syl3anc φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b X - W b + ˙ b = X
54 51 53 breqtrd φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b X - W b + ˙ X - W b < ˙ X
55 ovexd φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b X - W b + ˙ X - W b V
56 3 4 pltle W Grp X - W b + ˙ X - W b V X B X - W b + ˙ X - W b < ˙ X X - W b + ˙ X - W b ˙ X
57 25 55 26 56 syl3anc φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b X - W b + ˙ X - W b < ˙ X X - W b + ˙ X - W b ˙ X
58 54 57 mpd φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b X - W b + ˙ X - W b ˙ X
59 breq2 c = X - W b 0 ˙ < ˙ c 0 ˙ < ˙ X - W b
60 id c = X - W b c = X - W b
61 60 60 oveq12d c = X - W b c + ˙ c = X - W b + ˙ X - W b
62 61 breq1d c = X - W b c + ˙ c ˙ X X - W b + ˙ X - W b ˙ X
63 59 62 anbi12d c = X - W b 0 ˙ < ˙ c c + ˙ c ˙ X 0 ˙ < ˙ X - W b X - W b + ˙ X - W b ˙ X
64 63 rspcev X - W b B 0 ˙ < ˙ X - W b X - W b + ˙ X - W b ˙ X c B 0 ˙ < ˙ c c + ˙ c ˙ X
65 30 37 58 64 syl12anc φ b B 0 ˙ < ˙ b b < ˙ X X < ˙ b + ˙ b c B 0 ˙ < ˙ c c + ˙ c ˙ X
66 6 ad2antrr φ b B 0 ˙ < ˙ b b < ˙ X W oGrp
67 isogrp W oGrp W Grp W oMnd
68 67 simprbi W oGrp W oMnd
69 omndtos W oMnd W Toset
70 66 68 69 3syl φ b B 0 ˙ < ˙ b b < ˙ X W Toset
71 66 24 syl φ b B 0 ˙ < ˙ b b < ˙ X W Grp
72 simplr φ b B 0 ˙ < ˙ b b < ˙ X b B
73 71 72 72 39 syl3anc φ b B 0 ˙ < ˙ b b < ˙ X b + ˙ b B
74 11 ad2antrr φ b B 0 ˙ < ˙ b b < ˙ X X B
75 1 3 4 tlt2 W Toset b + ˙ b B X B b + ˙ b ˙ X X < ˙ b + ˙ b
76 70 73 74 75 syl3anc φ b B 0 ˙ < ˙ b b < ˙ X b + ˙ b ˙ X X < ˙ b + ˙ b
77 22 65 76 mpjaodan φ b B 0 ˙ < ˙ b b < ˙ X c B 0 ˙ < ˙ c c + ˙ c ˙ X
78 10 3expia φ a B 0 ˙ < ˙ a b B 0 ˙ < ˙ b b < ˙ a
79 78 ralrimiva φ a B 0 ˙ < ˙ a b 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 b B 0 ˙ < ˙ b b < ˙ a b B 0 ˙ < ˙ b b < ˙ X
84 80 83 imbi12d a = X 0 ˙ < ˙ a b B 0 ˙ < ˙ b b < ˙ a 0 ˙ < ˙ X b B 0 ˙ < ˙ b b < ˙ X
85 84 rspcv X B a B 0 ˙ < ˙ a b B 0 ˙ < ˙ b b < ˙ a 0 ˙ < ˙ X b B 0 ˙ < ˙ b b < ˙ X
86 11 79 12 85 syl3c φ b B 0 ˙ < ˙ b b < ˙ X
87 77 86 r19.29a φ c B 0 ˙ < ˙ c c + ˙ c ˙ X