diatrl

Description: Trace of a member of the partial isomorphism A. (Contributed by NM, 17-Jan-2014)

	Ref	Expression
Hypotheses	diatrl.b	$⊢ B = {Base}_{K}$
	diatrl.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	diatrl.h	$⊢ H = LHyp (K)$
	diatrl.t	$⊢ T = LTrn (K) (W)$
	diatrl.r	$⊢ R = trL (K) (W)$
	diatrl.i	$⊢ I = DIsoA (K) (W)$
Assertion	diatrl	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land F \in I (X)) \to R (F) \underset{˙}{\leq} X$

Step	Hyp	Ref	Expression
1		diatrl.b	$⊢ B = {Base}_{K}$
2		diatrl.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		diatrl.h	$⊢ H = LHyp (K)$
4		diatrl.t	$⊢ T = LTrn (K) (W)$
5		diatrl.r	$⊢ R = trL (K) (W)$
6		diatrl.i	$⊢ I = DIsoA (K) (W)$
7	1 2 3 4 5 6	diaelval	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to (F \in I (X) \leftrightarrow (F \in T \land R (F) \underset{˙}{\leq} X))$
8		simpr	$⊢ (F \in T \land R (F) \underset{˙}{\leq} X) \to R (F) \underset{˙}{\leq} X$
9	7 8	biimtrdi	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to (F \in I (X) \to R (F) \underset{˙}{\leq} X)$
10	9	3impia	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land F \in I (X)) \to R (F) \underset{˙}{\leq} X$

Metamath Proof Explorer