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

Metamath Proof Explorer

Theorem tendopl

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

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

Proof

Step Hyp Ref Expression
1 tendoplcbv.p ⊢ 𝑃 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
2 tendopl2.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 fveq1 ⊢ ( 𝑢 = 𝑈 → ( 𝑢 ‘ 𝑔 ) = ( 𝑈 ‘ 𝑔 ) )
4 3 coeq1d ⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 ‘ 𝑔 ) ∘ ( 𝑣 ‘ 𝑔 ) ) = ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑣 ‘ 𝑔 ) ) )
5 4 mpteq2dv ⊢ ( 𝑢 = 𝑈 → ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑢 ‘ 𝑔 ) ∘ ( 𝑣 ‘ 𝑔 ) ) ) = ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑣 ‘ 𝑔 ) ) ) )
6 fveq1 ⊢ ( 𝑣 = 𝑉 → ( 𝑣 ‘ 𝑔 ) = ( 𝑉 ‘ 𝑔 ) )
7 6 coeq2d ⊢ ( 𝑣 = 𝑉 → ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑣 ‘ 𝑔 ) ) = ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) )
8 7 mpteq2dv ⊢ ( 𝑣 = 𝑉 → ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑣 ‘ 𝑔 ) ) ) = ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) ) )
9 1 tendoplcbv ⊢ 𝑃 = ( 𝑢 ∈ 𝐸 , 𝑣 ∈ 𝐸 ↦ ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑢 ‘ 𝑔 ) ∘ ( 𝑣 ‘ 𝑔 ) ) ) )
10 2 fvexi ⊢ 𝑇 ∈ V
11 10 mptex ⊢ ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) ) ∈ V
12 5 8 9 11 ovmpo ⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) → ( 𝑈 𝑃 𝑉 ) = ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) ) )