Metamath Proof Explorer

Theorem tendof

Description: Functionality of 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 tendof ⊢ K ∈ V ∧ W ∈ H ∧ S ∈ E → S : T ⟶ T

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 eqid ⊢ ≤ K = ≤ K
5 eqid ⊢ trL ⁡ K ⁡ W = trL ⁡ K ⁡ W
6 4 1 2 5 3 istendo ⊢ K ∈ V ∧ W ∈ H → S ∈ E ↔ S : T ⟶ T ∧ ∀ f ∈ T ∀ g ∈ T S ⁡ f ∘ g = S ⁡ f ∘ S ⁡ g ∧ ∀ f ∈ T trL ⁡ K ⁡ W ⁡ S ⁡ f ≤ K trL ⁡ K ⁡ W ⁡ f
7 simp1 ⊢ S : T ⟶ T ∧ ∀ f ∈ T ∀ g ∈ T S ⁡ f ∘ g = S ⁡ f ∘ S ⁡ g ∧ ∀ f ∈ T trL ⁡ K ⁡ W ⁡ S ⁡ f ≤ K trL ⁡ K ⁡ W ⁡ f → S : T ⟶ T
8 6 7 biimtrdi ⊢ K ∈ V ∧ W ∈ H → S ∈ E → S : T ⟶ T
9 8 imp ⊢ K ∈ V ∧ W ∈ H ∧ S ∈ E → S : T ⟶ T