# Metamath Proof Explorer

## Theorem tgrpabl

Description: The translation group is an Abelian group. Lemma G of Crawley p. 116. (Contributed by NM, 6-Jun-2013)

Ref Expression
Hypotheses tgrpgrp.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
tgrpgrp.g ${⊢}{G}=\mathrm{TGrp}\left({K}\right)\left({W}\right)$
Assertion tgrpabl ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {G}\in \mathrm{Abel}$

### Proof

Step Hyp Ref Expression
1 tgrpgrp.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 tgrpgrp.g ${⊢}{G}=\mathrm{TGrp}\left({K}\right)\left({W}\right)$
3 eqid ${⊢}\mathrm{LTrn}\left({K}\right)\left({W}\right)=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
4 eqid ${⊢}{\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{G}}$
5 1 3 2 4 tgrpbase ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {\mathrm{Base}}_{{G}}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
6 5 eqcomd ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{LTrn}\left({K}\right)\left({W}\right)={\mathrm{Base}}_{{G}}$
7 eqidd ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {+}_{{G}}={+}_{{G}}$
8 1 2 tgrpgrp ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {G}\in \mathrm{Grp}$
9 1 3 ltrncom ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {f}\circ {g}={g}\circ {f}$
10 eqid ${⊢}{+}_{{G}}={+}_{{G}}$
11 1 3 2 10 tgrpov ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\wedge \left({f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\right)\to {f}{+}_{{G}}{g}={f}\circ {g}$
12 11 3expa ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\right)\to {f}{+}_{{G}}{g}={f}\circ {g}$
13 12 3impb ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {f}{+}_{{G}}{g}={f}\circ {g}$
14 1 3 2 10 tgrpov ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\wedge \left({g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\right)\to {g}{+}_{{G}}{f}={g}\circ {f}$
15 14 3expa ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\right)\to {g}{+}_{{G}}{f}={g}\circ {f}$
16 15 3impb ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {g}{+}_{{G}}{f}={g}\circ {f}$
17 16 3com23 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {g}{+}_{{G}}{f}={g}\circ {f}$
18 9 13 17 3eqtr4d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {f}{+}_{{G}}{g}={g}{+}_{{G}}{f}$
19 6 7 8 18 isabld ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {G}\in \mathrm{Abel}$