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

Metamath Proof Explorer

Theorem tendoplcl2

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

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

Proof

Step Hyp Ref Expression
1 tendopl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 tendopl.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 tendopl.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 tendopl.p ⊢ 𝑃 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
5 4 2 tendopl2 ⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) )
6 5 3expa ⊢ ( ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) )
7 6 3adant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) )
8 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 1 2 3 tendocl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝑈 ‘ 𝐹 ) ∈ 𝑇 )
10 9 3adant2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑈 ‘ 𝐹 ) ∈ 𝑇 )
11 1 2 3 tendocl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝑉 ‘ 𝐹 ) ∈ 𝑇 )
12 11 3adant2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑉 ‘ 𝐹 ) ∈ 𝑇 )
13 1 2 ltrnco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ‘ 𝐹 ) ∈ 𝑇 ∧ ( 𝑉 ‘ 𝐹 ) ∈ 𝑇 ) → ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) ∈ 𝑇 )
14 8 10 12 13 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) ∈ 𝑇 )
15 7 14 eqeltrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) ∈ 𝑇 )