This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐻 = ( 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 )