Metamath Proof Explorer

Theorem tendocoval

Description: Value of composition of endomorphisms in a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013)

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

Proof

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