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	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	tgrpgrp.g	⊢ 𝐺 = ( ( TGrp ‘ 𝐾 ) ‘ 𝑊 )
Assertion	tgrpabl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐺 ∈ Abel )

Proof

Step	Hyp	Ref	Expression
1		tgrpgrp.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		tgrpgrp.g	⊢ 𝐺 = ( ( TGrp ‘ 𝐾 ) ‘ 𝑊 )
3		eqid	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5	1 3 2 4	tgrpbase	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝐺 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
6	5	eqcomd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( Base ‘ 𝐺 ) )
7		eqidd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) )
8	1 2	tgrpgrp	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐺 ∈ Grp )
9	1 3	ltrncom	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑓 ∘ 𝑔 ) = ( 𝑔 ∘ 𝑓 ) )
10		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
11	1 3 2 10	tgrpov	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( 𝑓 ( +g ‘ 𝐺 ) 𝑔 ) = ( 𝑓 ∘ 𝑔 ) )
12	11	3expa	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( 𝑓 ( +g ‘ 𝐺 ) 𝑔 ) = ( 𝑓 ∘ 𝑔 ) )
13	12	3impb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑓 ( +g ‘ 𝐺 ) 𝑔 ) = ( 𝑓 ∘ 𝑔 ) )
14	1 3 2 10	tgrpov	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( 𝑔 ( +g ‘ 𝐺 ) 𝑓 ) = ( 𝑔 ∘ 𝑓 ) )
15	14	3expa	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( 𝑔 ( +g ‘ 𝐺 ) 𝑓 ) = ( 𝑔 ∘ 𝑓 ) )
16	15	3impb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑔 ( +g ‘ 𝐺 ) 𝑓 ) = ( 𝑔 ∘ 𝑓 ) )
17	16	3com23	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑔 ( +g ‘ 𝐺 ) 𝑓 ) = ( 𝑔 ∘ 𝑓 ) )
18	9 13 17	3eqtr4d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑓 ( +g ‘ 𝐺 ) 𝑔 ) = ( 𝑔 ( +g ‘ 𝐺 ) 𝑓 ) )
19	6 7 8 18	isabld	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐺 ∈ Abel )