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 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐸 ∈ 𝑇 ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝐷 ∘ 𝐸 ) ∘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝐷 ∘ 𝐹 ) ∘ ( 𝐸 ∘ 𝐺 ) ) )