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

Metamath Proof Explorer

Theorem ltrnco4

Description: Rearrange a composition of 4 translations, analogous to an4 . (Contributed by NM, 10-Jun-2013)

Ref Expression
Hypotheses ltrncom.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
ltrncom.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion ltrnco4 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐸 ∈ 𝑇 ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝐷 ∘ 𝐸 ) ∘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝐷 ∘ 𝐹 ) ∘ ( 𝐸 ∘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 ltrncom.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 ltrncom.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 1 2 ltrncom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐸 ∈ 𝑇 ∧ 𝐹 ∈ 𝑇 ) → ( 𝐸 ∘ 𝐹 ) = ( 𝐹 ∘ 𝐸 ) )
4 3 coeq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐸 ∈ 𝑇 ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝐸 ∘ 𝐹 ) ∘ 𝐺 ) = ( ( 𝐹 ∘ 𝐸 ) ∘ 𝐺 ) )
5 coass ⊢ ( ( 𝐸 ∘ 𝐹 ) ∘ 𝐺 ) = ( 𝐸 ∘ ( 𝐹 ∘ 𝐺 ) )
6 coass ⊢ ( ( 𝐹 ∘ 𝐸 ) ∘ 𝐺 ) = ( 𝐹 ∘ ( 𝐸 ∘ 𝐺 ) )
7 4 5 6 3eqtr3g ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐸 ∈ 𝑇 ∧ 𝐹 ∈ 𝑇 ) → ( 𝐸 ∘ ( 𝐹 ∘ 𝐺 ) ) = ( 𝐹 ∘ ( 𝐸 ∘ 𝐺 ) ) )
8 7 coeq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐸 ∈ 𝑇 ∧ 𝐹 ∈ 𝑇 ) → ( 𝐷 ∘ ( 𝐸 ∘ ( 𝐹 ∘ 𝐺 ) ) ) = ( 𝐷 ∘ ( 𝐹 ∘ ( 𝐸 ∘ 𝐺 ) ) ) )
9 coass ⊢ ( ( 𝐷 ∘ 𝐸 ) ∘ ( 𝐹 ∘ 𝐺 ) ) = ( 𝐷 ∘ ( 𝐸 ∘ ( 𝐹 ∘ 𝐺 ) ) )
10 coass ⊢ ( ( 𝐷 ∘ 𝐹 ) ∘ ( 𝐸 ∘ 𝐺 ) ) = ( 𝐷 ∘ ( 𝐹 ∘ ( 𝐸 ∘ 𝐺 ) ) )
11 8 9 10 3eqtr4g ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐸 ∈ 𝑇 ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝐷 ∘ 𝐸 ) ∘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝐷 ∘ 𝐹 ) ∘ ( 𝐸 ∘ 𝐺 ) ) )