Metamath Proof Explorer

Theorem diassdvaN

Description: The partial isomorphism A maps to a set of vectors in partial vector space A. (Contributed by NM, 1-Jan-2014) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	diassdva.b	$⊢ B = {Base}_{K}$
		diassdva.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		diassdva.h	$⊢ H = LHyp (K)$
		diassdva.i	$⊢ I = DIsoA (K) (W)$
		diassdva.u	$⊢ U = DVecA (K) (W)$
		diassdva.v	$⊢ V = {Base}_{U}$
	Assertion	diassdvaN	$⊢ ((K \in Y \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) \subseteq V$

Proof

Step	Hyp	Ref	Expression
1		diassdva.b	$⊢ B = {Base}_{K}$
2		diassdva.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		diassdva.h	$⊢ H = LHyp (K)$
4		diassdva.i	$⊢ I = DIsoA (K) (W)$
5		diassdva.u	$⊢ U = DVecA (K) (W)$
6		diassdva.v	$⊢ V = {Base}_{U}$
7		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
8		eqid	$⊢ trL (K) (W) = trL (K) (W)$
9	1 2 3 7 8 4	diaval	$⊢ ((K \in Y \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) = \{f \in LTrn (K) (W) \| trL (K) (W) (f) \underset{˙}{\leq} X\}$
10		ssrab2	$⊢ \{f \in LTrn (K) (W) \| trL (K) (W) (f) \underset{˙}{\leq} X\} \subseteq LTrn (K) (W)$
11	3 7 5 6	dvavbase	$⊢ (K \in Y \land W \in H) \to V = LTrn (K) (W)$
12	11	adantr	$⊢ ((K \in Y \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to V = LTrn (K) (W)$
13	10 12	sseqtrrid	$⊢ ((K \in Y \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to \{f \in LTrn (K) (W) \| trL (K) (W) (f) \underset{˙}{\leq} X\} \subseteq V$
14	9 13	eqsstrd	$⊢ ((K \in Y \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) \subseteq V$