diasslssN

Description: The partial isomorphism A maps to subspaces of partial vector space A. (Contributed by NM, 17-Jan-2014) (New usage is discouraged.)

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

Step	Hyp	Ref	Expression
1		diasslss.h	$⊢ H = LHyp (K)$
2		diasslss.u	$⊢ U = DVecA (K) (W)$
3		diasslss.i	$⊢ I = DIsoA (K) (W)$
4		diasslss.s	$⊢ S = LSubSp (U)$
5	1 3	diaf11N	$⊢ (K \in HL \land W \in H) \to I : dom I \underset{1-1 onto}{⟶} ran I$
6		f1ocnvfv2	$⊢ (I : dom I \underset{1-1 onto}{⟶} ran I \land x \in ran I) \to I (I^{-1} (x)) = x$
7	5 6	sylan	$⊢ ((K \in HL \land W \in H) \land x \in ran I) \to I (I^{-1} (x)) = x$
8	1 3	diacnvclN	$⊢ ((K \in HL \land W \in H) \land x \in ran I) \to I^{-1} (x) \in dom I$
9		eqid	$⊢ {Base}_{K} = {Base}_{K}$
10		eqid	$⊢ \leq_{K} = \leq_{K}$
11	9 10 1 3	diaeldm	$⊢ (K \in HL \land W \in H) \to (I^{-1} (x) \in dom I \leftrightarrow (I^{-1} (x) \in {Base}_{K} \land I^{-1} (x) \leq_{K} W))$
12	11	adantr	$⊢ ((K \in HL \land W \in H) \land x \in ran I) \to (I^{-1} (x) \in dom I \leftrightarrow (I^{-1} (x) \in {Base}_{K} \land I^{-1} (x) \leq_{K} W))$
13	8 12	mpbid	$⊢ ((K \in HL \land W \in H) \land x \in ran I) \to (I^{-1} (x) \in {Base}_{K} \land I^{-1} (x) \leq_{K} W)$
14	9 10 1 2 3 4	dialss	$⊢ ((K \in HL \land W \in H) \land (I^{-1} (x) \in {Base}_{K} \land I^{-1} (x) \leq_{K} W)) \to I (I^{-1} (x)) \in S$
15	13 14	syldan	$⊢ ((K \in HL \land W \in H) \land x \in ran I) \to I (I^{-1} (x)) \in S$
16	7 15	eqeltrrd	$⊢ ((K \in HL \land W \in H) \land x \in ran I) \to x \in S$
17	16	ex	$⊢ (K \in HL \land W \in H) \to (x \in ran I \to x \in S)$
18	17	ssrdv	$⊢ (K \in HL \land W \in H) \to ran I \subseteq S$

Metamath Proof Explorer