dihprrn

Description: The span of a vector pair belongs to the range of isomorphism H i.e. is a closed subspace. (Contributed by NM, 29-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dihprrn.h	$⊢ H = LHyp (K)$
2		dihprrn.u	$⊢ U = DVecH (K) (W)$
3		dihprrn.v	$⊢ V = {Base}_{U}$
4		dihprrn.n	$⊢ N = LSpan (U)$
5		dihprrn.i	$⊢ I = DIsoH (K) (W)$
6		dihprrn.k	$⊢ φ \to (K \in HL \land W \in H)$
7		dihprrn.x	$⊢ φ \to X \in V$
8		dihprrn.y	$⊢ φ \to Y \in V$
9		prcom	$⊢ \{X, Y\} = \{Y, X\}$
10		preq2	$⊢ X = 0_{U} \to \{Y, X\} = \{Y, 0_{U}\}$
11	9 10	syl5eq	$⊢ X = 0_{U} \to \{X, Y\} = \{Y, 0_{U}\}$
12	11	fveq2d	$⊢ X = 0_{U} \to N (\{X, Y\}) = N (\{Y, 0_{U}\})$
13		eqid	$⊢ 0_{U} = 0_{U}$
14	1 2 6	dvhlmod	$⊢ φ \to U \in LMod$
15	3 13 4 14 8	lsppr0	$⊢ φ \to N (\{Y, 0_{U}\}) = N (\{Y\})$
16	12 15	sylan9eqr	$⊢ (φ \land X = 0_{U}) \to N (\{X, Y\}) = N (\{Y\})$
17	1 2 3 4 5	dihlsprn	$⊢ ((K \in HL \land W \in H) \land Y \in V) \to N (\{Y\}) \in ran I$
18	6 8 17	syl2anc	$⊢ φ \to N (\{Y\}) \in ran I$
19	18	adantr	$⊢ (φ \land X = 0_{U}) \to N (\{Y\}) \in ran I$
20	16 19	eqeltrd	$⊢ (φ \land X = 0_{U}) \to N (\{X, Y\}) \in ran I$
21		preq2	$⊢ Y = 0_{U} \to \{X, Y\} = \{X, 0_{U}\}$
22	21	fveq2d	$⊢ Y = 0_{U} \to N (\{X, Y\}) = N (\{X, 0_{U}\})$
23	3 13 4 14 7	lsppr0	$⊢ φ \to N (\{X, 0_{U}\}) = N (\{X\})$
24	22 23	sylan9eqr	$⊢ (φ \land Y = 0_{U}) \to N (\{X, Y\}) = N (\{X\})$
25	1 2 3 4 5	dihlsprn	$⊢ ((K \in HL \land W \in H) \land X \in V) \to N (\{X\}) \in ran I$
26	6 7 25	syl2anc	$⊢ φ \to N (\{X\}) \in ran I$
27	26	adantr	$⊢ (φ \land Y = 0_{U}) \to N (\{X\}) \in ran I$
28	24 27	eqeltrd	$⊢ (φ \land Y = 0_{U}) \to N (\{X, Y\}) \in ran I$
29	6	adantr	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U})) \to (K \in HL \land W \in H)$
30	7	adantr	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U})) \to X \in V$
31	8	adantr	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U})) \to Y \in V$
32		simprl	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U})) \to X \neq 0_{U}$
33		simprr	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U})) \to Y \neq 0_{U}$
34	1 2 3 4 5 29 30 31 13 32 33	dihprrnlem2	$⊢ (φ \land (X \neq 0_{U} \land Y \neq 0_{U})) \to N (\{X, Y\}) \in ran I$
35	20 28 34	pm2.61da2ne	$⊢ φ \to N (\{X, Y\}) \in ran I$

Metamath Proof Explorer

Theorem dihprrn

Proof