Metamath Proof Explorer


Theorem archiabllem2b

Description: Lemma for archiabl . (Contributed by Thierry Arnoux, 1-May-2018)

Ref Expression
Hypotheses archiabllem.b B=BaseW
archiabllem.0 0˙=0W
archiabllem.e ˙=W
archiabllem.t <˙=<W
archiabllem.m ·˙=W
archiabllem.g φWoGrp
archiabllem.a φWArchi
archiabllem2.1 +˙=+W
archiabllem2.2 φopp𝑔WoGrp
archiabllem2.3 φaB0˙<˙abB0˙<˙bb<˙a
archiabllem2b.4 φXB
archiabllem2b.5 φYB
Assertion archiabllem2b φX+˙Y=Y+˙X

Proof

Step Hyp Ref Expression
1 archiabllem.b B=BaseW
2 archiabllem.0 0˙=0W
3 archiabllem.e ˙=W
4 archiabllem.t <˙=<W
5 archiabllem.m ·˙=W
6 archiabllem.g φWoGrp
7 archiabllem.a φWArchi
8 archiabllem2.1 +˙=+W
9 archiabllem2.2 φopp𝑔WoGrp
10 archiabllem2.3 φaB0˙<˙abB0˙<˙bb<˙a
11 archiabllem2b.4 φXB
12 archiabllem2b.5 φYB
13 1 2 3 4 5 6 7 8 9 10 11 12 archiabllem2c φ¬X+˙Y<˙Y+˙X
14 1 2 3 4 5 6 7 8 9 10 12 11 archiabllem2c φ¬Y+˙X<˙X+˙Y
15 isogrp WoGrpWGrpWoMnd
16 15 simprbi WoGrpWoMnd
17 omndtos WoMndWToset
18 6 16 17 3syl φWToset
19 ogrpgrp WoGrpWGrp
20 6 19 syl φWGrp
21 1 8 grpcl WGrpXBYBX+˙YB
22 20 11 12 21 syl3anc φX+˙YB
23 1 8 grpcl WGrpYBXBY+˙XB
24 20 12 11 23 syl3anc φY+˙XB
25 1 4 tlt3 WTosetX+˙YBY+˙XBX+˙Y=Y+˙XX+˙Y<˙Y+˙XY+˙X<˙X+˙Y
26 18 22 24 25 syl3anc φX+˙Y=Y+˙XX+˙Y<˙Y+˙XY+˙X<˙X+˙Y
27 13 14 26 ecase23d φX+˙Y=Y+˙X