diass

Description: The value of the partial isomorphism A is a set of translations, i.e., a set of vectors. (Contributed by NM, 26-Nov-2013)

	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	diass	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) \subseteq 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		eqid	$⊢ trL (K) (W) = trL (K) (W)$
7	1 2 3 4 6 5	diaval	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) = \{f \in T \| trL (K) (W) (f) \underset{˙}{\leq} X\}$
8		ssrab2	$⊢ \{f \in T \| trL (K) (W) (f) \underset{˙}{\leq} X\} \subseteq T$
9	7 8	eqsstrdi	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) \subseteq T$

Metamath Proof Explorer