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 = LHyp (K)$
		tgrpgrp.g	$⊢ G = TGrp (K) (W)$
	Assertion	tgrpabl	$⊢ (K \in HL \land W \in H) \to G \in Abel$

Proof

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