diael

Description: A member of the value of the partial isomorphism A is a translation, i.e., a vector. (Contributed by NM, 17-Jan-2014)

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

Step	Hyp	Ref	Expression
1		diass.b	$⊢ B = {Base}_{K}$
2		diass.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		diass.h	$⊢ H = LHyp (K)$
4		diass.t	$⊢ T = LTrn (K) (W)$
5		diass.i	$⊢ I = DIsoA (K) (W)$
6	1 2 3 4 5	diass	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) \subseteq T$
7	6	sseld	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to (F \in I (X) \to F \in T)$
8	7	3impia	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land F \in I (X)) \to F \in T$

Metamath Proof Explorer