Metamath Proof Explorer

Theorem tendospass

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

Ref Expression
Hypotheses tendosp.h ⊢ H = LHyp ⁡ K
tendosp.t ⊢ T = LTrn ⁡ K ⁡ W
tendosp.e ⊢ E = TEndo ⁡ K ⁡ W
Assertion tendospass ⊢ K ∈ X ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → U ∘ V ⁡ F = U ⁡ V ⁡ F

Proof

Step Hyp Ref Expression
1 tendosp.h ⊢ H = LHyp ⁡ K
2 tendosp.t ⊢ T = LTrn ⁡ K ⁡ W
3 tendosp.e ⊢ E = TEndo ⁡ K ⁡ W
4 1 2 3 tendof ⊢ K ∈ X ∧ W ∈ H ∧ V ∈ E → V : T ⟶ T
5 4 3ad2antr2 ⊢ K ∈ X ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → V : T ⟶ T
6 simpr3 ⊢ K ∈ X ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → F ∈ T
7 fvco3 ⊢ V : T ⟶ T ∧ F ∈ T → U ∘ V ⁡ F = U ⁡ V ⁡ F
8 5 6 7 syl2anc ⊢ K ∈ X ∧ W ∈ H ∧ U ∈ E ∧ V ∈ E ∧ F ∈ T → U ∘ V ⁡ F = U ⁡ V ⁡ F