# Metamath Proof Explorer

## Theorem archiabllem2b

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

Ref Expression
Hypotheses archiabllem.b ${⊢}{B}={\mathrm{Base}}_{{W}}$
archiabllem.0
archiabllem.e
archiabllem.t
archiabllem.m
archiabllem.g ${⊢}{\phi }\to {W}\in \mathrm{oGrp}$
archiabllem.a ${⊢}{\phi }\to {W}\in \mathrm{Archi}$
archiabllem2.1
archiabllem2.2 ${⊢}{\phi }\to {opp}_{𝑔}\left({W}\right)\in \mathrm{oGrp}$
archiabllem2.3
archiabllem2b.4 ${⊢}{\phi }\to {X}\in {B}$
archiabllem2b.5 ${⊢}{\phi }\to {Y}\in {B}$
Assertion archiabllem2b

### Proof

Step Hyp Ref Expression
1 archiabllem.b ${⊢}{B}={\mathrm{Base}}_{{W}}$
2 archiabllem.0
3 archiabllem.e
4 archiabllem.t
5 archiabllem.m
6 archiabllem.g ${⊢}{\phi }\to {W}\in \mathrm{oGrp}$
7 archiabllem.a ${⊢}{\phi }\to {W}\in \mathrm{Archi}$
8 archiabllem2.1
9 archiabllem2.2 ${⊢}{\phi }\to {opp}_{𝑔}\left({W}\right)\in \mathrm{oGrp}$
10 archiabllem2.3
11 archiabllem2b.4 ${⊢}{\phi }\to {X}\in {B}$
12 archiabllem2b.5 ${⊢}{\phi }\to {Y}\in {B}$
13 1 2 3 4 5 6 7 8 9 10 11 12 archiabllem2c
14 1 2 3 4 5 6 7 8 9 10 12 11 archiabllem2c
15 isogrp ${⊢}{W}\in \mathrm{oGrp}↔\left({W}\in \mathrm{Grp}\wedge {W}\in \mathrm{oMnd}\right)$
16 15 simprbi ${⊢}{W}\in \mathrm{oGrp}\to {W}\in \mathrm{oMnd}$
17 omndtos ${⊢}{W}\in \mathrm{oMnd}\to {W}\in \mathrm{Toset}$
18 6 16 17 3syl ${⊢}{\phi }\to {W}\in \mathrm{Toset}$
19 ogrpgrp ${⊢}{W}\in \mathrm{oGrp}\to {W}\in \mathrm{Grp}$
20 6 19 syl ${⊢}{\phi }\to {W}\in \mathrm{Grp}$
21 1 8 grpcl
22 20 11 12 21 syl3anc
23 1 8 grpcl
24 20 12 11 23 syl3anc
25 1 4 tlt3
26 18 22 24 25 syl3anc
27 13 14 26 ecase23d