Metamath Proof Explorer

Theorem tendocl

Description: Closure 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	tendocl	$⊢ ((K \in V \land W \in H) \land S \in E \land F \in T) \to S (F) \in T$

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	1 2 3	tendof	$⊢ ((K \in V \land W \in H) \land S \in E) \to S : T ⟶ T$
5	4	3adant3	$⊢ ((K \in V \land W \in H) \land S \in E \land F \in T) \to S : T ⟶ T$
6		simp3	$⊢ ((K \in V \land W \in H) \land S \in E \land F \in T) \to F \in T$
7	5 6	ffvelrnd	$⊢ ((K \in V \land W \in H) \land S \in E \land F \in T) \to S (F) \in T$