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

Metamath Proof Explorer

Theorem tendopl2

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

Ref Expression
Hypotheses tendoplcbv.p ⊢ 𝑃 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
tendopl2.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion tendopl2 ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 tendoplcbv.p ⊢ 𝑃 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
2 tendopl2.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 1 2 tendopl ⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) → ( 𝑈 𝑃 𝑉 ) = ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) ) )
4 3 3adant3 ⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝑈 𝑃 𝑉 ) = ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) ) )
5 fveq2 ⊢ ( 𝑔 = 𝐹 → ( 𝑈 ‘ 𝑔 ) = ( 𝑈 ‘ 𝐹 ) )
6 fveq2 ⊢ ( 𝑔 = 𝐹 → ( 𝑉 ‘ 𝑔 ) = ( 𝑉 ‘ 𝐹 ) )
7 5 6 coeq12d ⊢ ( 𝑔 = 𝐹 → ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) )
8 7 adantl ⊢ ( ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑔 = 𝐹 ) → ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) )
9 simp3 ⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → 𝐹 ∈ 𝑇 )
10 fvex ⊢ ( 𝑈 ‘ 𝐹 ) ∈ V
11 fvex ⊢ ( 𝑉 ‘ 𝐹 ) ∈ V
12 10 11 coex ⊢ ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) ∈ V
13 12 a1i ⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) ∈ V )
14 4 8 9 13 fvmptd ⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) )