dihsslss

Description: The isomorphism H maps to subspaces. (Contributed by NM, 14-Mar-2014)

	Ref	Expression
Hypotheses	dihsslss.h	$⊢ H = LHyp (K)$
	dihsslss.u	$⊢ U = DVecH (K) (W)$
	dihsslss.i	$⊢ I = DIsoH (K) (W)$
	dihsslss.s	$⊢ S = LSubSp (U)$
Assertion	dihsslss	$⊢ (K \in HL \land W \in H) \to ran I \subseteq S$

Step	Hyp	Ref	Expression
1		dihsslss.h	$⊢ H = LHyp (K)$
2		dihsslss.u	$⊢ U = DVecH (K) (W)$
3		dihsslss.i	$⊢ I = DIsoH (K) (W)$
4		dihsslss.s	$⊢ S = LSubSp (U)$
5	1 3	dihcnvid2	$⊢ ((K \in HL \land W \in H) \land x \in ran I) \to I (I^{-1} (x)) = x$
6		eqid	$⊢ {Base}_{K} = {Base}_{K}$
7	6 1 3	dihcnvcl	$⊢ ((K \in HL \land W \in H) \land x \in ran I) \to I^{-1} (x) \in {Base}_{K}$
8	6 1 3 2 4	dihlss	$⊢ ((K \in HL \land W \in H) \land I^{-1} (x) \in {Base}_{K}) \to I (I^{-1} (x)) \in S$
9	7 8	syldan	$⊢ ((K \in HL \land W \in H) \land x \in ran I) \to I (I^{-1} (x)) \in S$
10	5 9	eqeltrrd	$⊢ ((K \in HL \land W \in H) \land x \in ran I) \to x \in S$
11	10	ex	$⊢ (K \in HL \land W \in H) \to (x \in ran I \to x \in S)$
12	11	ssrdv	$⊢ (K \in HL \land W \in H) \to ran I \subseteq S$

Metamath Proof Explorer