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

Metamath Proof Explorer

Theorem tendospdi1

Description: Forward distributive law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013)

Ref Expression
Hypotheses tendosp.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
tendosp.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendosp.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
Assertion tendospdi1 ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( 𝑈 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑈 ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 tendosp.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 tendosp.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 tendosp.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 simpll ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → 𝐾 ∈ 𝑉 )
5 simplr ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → 𝑊 ∈ 𝐻 )
6 simpr1 ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → 𝑈 ∈ 𝐸 )
7 simpr2 ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → 𝐹 ∈ 𝑇 )
8 simpr3 ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → 𝐺 ∈ 𝑇 )
9 1 2 3 tendovalco ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ∧ 𝑈 ∈ 𝐸 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( 𝑈 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑈 ‘ 𝐺 ) ) )
10 4 5 6 7 8 9 syl32anc ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ) → ( 𝑈 ‘ ( 𝐹 ∘ 𝐺 ) ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑈 ‘ 𝐺 ) ) )