dihlsprn

Description: The span of a vector belongs to the range of isomorphism H. (Contributed by NM, 27-Apr-2014)

	Ref	Expression
Hypotheses	dihlsprn.h	$⊢ H = LHyp (K)$
	dihlsprn.u	$⊢ U = DVecH (K) (W)$
	dihlsprn.v	$⊢ V = {Base}_{U}$
	dihlsprn.n	$⊢ N = LSpan (U)$
	dihlsprn.i	$⊢ I = DIsoH (K) (W)$
Assertion	dihlsprn	$⊢ ((K \in HL \land W \in H) \land X \in V) \to N (\{X\}) \in ran I$

Proof

Step	Hyp	Ref	Expression
1		dihlsprn.h	$⊢ H = LHyp (K)$
2		dihlsprn.u	$⊢ U = DVecH (K) (W)$
3		dihlsprn.v	$⊢ V = {Base}_{U}$
4		dihlsprn.n	$⊢ N = LSpan (U)$
5		dihlsprn.i	$⊢ I = DIsoH (K) (W)$
6		simpr	$⊢ (((K \in HL \land W \in H) \land X \in V) \land X = 0_{U}) \to X = 0_{U}$
7	6	sneqd	$⊢ (((K \in HL \land W \in H) \land X \in V) \land X = 0_{U}) \to \{X\} = \{0_{U}\}$
8	7	fveq2d	$⊢ (((K \in HL \land W \in H) \land X \in V) \land X = 0_{U}) \to N (\{X\}) = N (\{0_{U}\})$
9		simpll	$⊢ (((K \in HL \land W \in H) \land X \in V) \land X = 0_{U}) \to (K \in HL \land W \in H)$
10	1 2 9	dvhlmod	$⊢ (((K \in HL \land W \in H) \land X \in V) \land X = 0_{U}) \to U \in LMod$
11		eqid	$⊢ 0_{U} = 0_{U}$
12	11 4	lspsn0	$⊢ U \in LMod \to N (\{0_{U}\}) = \{0_{U}\}$
13	10 12	syl	$⊢ (((K \in HL \land W \in H) \land X \in V) \land X = 0_{U}) \to N (\{0_{U}\}) = \{0_{U}\}$
14	8 13	eqtrd	$⊢ (((K \in HL \land W \in H) \land X \in V) \land X = 0_{U}) \to N (\{X\}) = \{0_{U}\}$
15	1 5 2 11	dih0rn	$⊢ (K \in HL \land W \in H) \to \{0_{U}\} \in ran I$
16	15	ad2antrr	$⊢ (((K \in HL \land W \in H) \land X \in V) \land X = 0_{U}) \to \{0_{U}\} \in ran I$
17	14 16	eqeltrd	$⊢ (((K \in HL \land W \in H) \land X \in V) \land X = 0_{U}) \to N (\{X\}) \in ran I$
18		simpll	$⊢ (((K \in HL \land W \in H) \land X \in V) \land X \neq 0_{U}) \to (K \in HL \land W \in H)$
19	1 2 18	dvhlmod	$⊢ (((K \in HL \land W \in H) \land X \in V) \land X \neq 0_{U}) \to U \in LMod$
20		simplr	$⊢ (((K \in HL \land W \in H) \land X \in V) \land X \neq 0_{U}) \to X \in V$
21		simpr	$⊢ (((K \in HL \land W \in H) \land X \in V) \land X \neq 0_{U}) \to X \neq 0_{U}$
22		eqid	$⊢ LSAtoms (U) = LSAtoms (U)$
23	3 4 11 22	lsatlspsn2	$⊢ (U \in LMod \land X \in V \land X \neq 0_{U}) \to N (\{X\}) \in LSAtoms (U)$
24	19 20 21 23	syl3anc	$⊢ (((K \in HL \land W \in H) \land X \in V) \land X \neq 0_{U}) \to N (\{X\}) \in LSAtoms (U)$
25	1 2 5 22	dih1dimat	$⊢ ((K \in HL \land W \in H) \land N (\{X\}) \in LSAtoms (U)) \to N (\{X\}) \in ran I$
26	18 24 25	syl2anc	$⊢ (((K \in HL \land W \in H) \land X \in V) \land X \neq 0_{U}) \to N (\{X\}) \in ran I$
27	17 26	pm2.61dane	$⊢ ((K \in HL \land W \in H) \land X \in V) \to N (\{X\}) \in ran I$

Metamath Proof Explorer

Theorem dihlsprn

Proof