Metamath Proof Explorer

Theorem diaelrnN

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

		Ref	Expression
	Hypotheses	diaelrn.h	$⊢ H = LHyp (K)$
		diaelrn.t	$⊢ T = LTrn (K) (W)$
		diaelrn.i	$⊢ I = DIsoA (K) (W)$
	Assertion	diaelrnN	$⊢ ((K \in V \land W \in H) \land S \in ran I) \to S \subseteq T$

Proof

Step	Hyp	Ref	Expression
1		diaelrn.h	$⊢ H = LHyp (K)$
2		diaelrn.t	$⊢ T = LTrn (K) (W)$
3		diaelrn.i	$⊢ I = DIsoA (K) (W)$
4		eqid	$⊢ {Base}_{K} = {Base}_{K}$
5		eqid	$⊢ \leq_{K} = \leq_{K}$
6	4 5 1 3	diafn	$⊢ (K \in V \land W \in H) \to I Fn \{y \in {Base}_{K} \| y \leq_{K} W\}$
7		fvelrnb	$⊢ I Fn \{y \in {Base}_{K} \| y \leq_{K} W\} \to (S \in ran I \leftrightarrow \exists x \in \{y \in {Base}_{K} \| y \leq_{K} W\} I (x) = S)$
8	6 7	syl	$⊢ (K \in V \land W \in H) \to (S \in ran I \leftrightarrow \exists x \in \{y \in {Base}_{K} \| y \leq_{K} W\} I (x) = S)$
9		breq1	$⊢ y = x \to (y \leq_{K} W \leftrightarrow x \leq_{K} W)$
10	9	elrab	$⊢ x \in \{y \in {Base}_{K} \| y \leq_{K} W\} \leftrightarrow (x \in {Base}_{K} \land x \leq_{K} W)$
11	4 5 1 2 3	diass	$⊢ ((K \in V \land W \in H) \land (x \in {Base}_{K} \land x \leq_{K} W)) \to I (x) \subseteq T$
12	11	ex	$⊢ (K \in V \land W \in H) \to ((x \in {Base}_{K} \land x \leq_{K} W) \to I (x) \subseteq T)$
13		sseq1	$⊢ I (x) = S \to (I (x) \subseteq T \leftrightarrow S \subseteq T)$
14	13	biimpcd	$⊢ I (x) \subseteq T \to (I (x) = S \to S \subseteq T)$
15	12 14	syl6	$⊢ (K \in V \land W \in H) \to ((x \in {Base}_{K} \land x \leq_{K} W) \to (I (x) = S \to S \subseteq T))$
16	10 15	biimtrid	$⊢ (K \in V \land W \in H) \to (x \in \{y \in {Base}_{K} \| y \leq_{K} W\} \to (I (x) = S \to S \subseteq T))$
17	16	rexlimdv	$⊢ (K \in V \land W \in H) \to (\exists x \in \{y \in {Base}_{K} \| y \leq_{K} W\} I (x) = S \to S \subseteq T)$
18	8 17	sylbid	$⊢ (K \in V \land W \in H) \to (S \in ran I \to S \subseteq T)$
19	18	imp	$⊢ ((K \in V \land W \in H) \land S \in ran I) \to S \subseteq T$