Metamath Proof Explorer

Theorem tendoplco2

Description: Value of result of endomorphism sum operation on a translation composition. (Contributed by NM, 10-Jun-2013)

Ref Expression
Hypotheses tendopl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
tendopl.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendopl.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
tendopl.p ⊢ 𝑃 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
Assertion tendoplco2 ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( 𝑈 𝑃 𝑉 ) ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) ∘ ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 tendopl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 tendopl.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 tendopl.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 tendopl.p ⊢ 𝑃 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
5 1 2 3 tendoco2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( 𝑈 ‘ ( 𝐹 ∘ 𝐺 ) ) ∘ ( 𝑉 ‘ ( 𝐹 ∘ 𝐺 ) ) ) = ( ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) ∘ ( ( 𝑈 ‘ 𝐺 ) ∘ ( 𝑉 ‘ 𝐺 ) ) ) )
6 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → 𝐹 ∈ 𝑇 )
8 simp3r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → 𝐺 ∈ 𝑇 )
9 1 2 ltrnco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 )
10 6 7 8 9 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 )
11 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 ) → 𝑈 ∈ 𝐸 )
12 simp2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 ) → 𝑉 ∈ 𝐸 )
13 simp3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 ) → ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 )
14 4 2 tendopl2 ⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 ) → ( ( 𝑈 𝑃 𝑉 ) ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑈 ‘ ( 𝐹 ∘ 𝐺 ) ) ∘ ( 𝑉 ‘ ( 𝐹 ∘ 𝐺 ) ) ) )
15 11 12 13 14 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝐹 ∘ 𝐺 ) ∈ 𝑇 ) → ( ( 𝑈 𝑃 𝑉 ) ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑈 ‘ ( 𝐹 ∘ 𝐺 ) ) ∘ ( 𝑉 ‘ ( 𝐹 ∘ 𝐺 ) ) ) )
16 10 15 syld3an3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( 𝑈 𝑃 𝑉 ) ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑈 ‘ ( 𝐹 ∘ 𝐺 ) ) ∘ ( 𝑉 ‘ ( 𝐹 ∘ 𝐺 ) ) ) )
17 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → 𝑈 ∈ 𝐸 )
18 simp2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → 𝑉 ∈ 𝐸 )
19 4 2 tendopl2 ⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) )
20 17 18 7 19 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) )
21 4 2 tendopl2 ⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐺 ) = ( ( 𝑈 ‘ 𝐺 ) ∘ ( 𝑉 ‘ 𝐺 ) ) )
22 17 18 8 21 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐺 ) = ( ( 𝑈 ‘ 𝐺 ) ∘ ( 𝑉 ‘ 𝐺 ) ) )
23 20 22 coeq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) ∘ ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐺 ) ) = ( ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) ∘ ( ( 𝑈 ‘ 𝐺 ) ∘ ( 𝑉 ‘ 𝐺 ) ) ) )
24 5 16 23 3eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( ( 𝑈 𝑃 𝑉 ) ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) ∘ ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐺 ) ) )