lspindp3

Description: Independence of 2 vectors is preserved by vector sum. (Contributed by NM, 26-Apr-2015)

Step	Hyp	Ref	Expression
1		lspindp3.v	$⊢ V = {Base}_{W}$
2		lspindp3.p	$⊢ \underset{˙}{+} = +_{W}$
3		lspindp3.o	$⊢ \underset{˙}{0} = 0_{W}$
4		lspindp3.n	$⊢ N = LSpan (W)$
5		lspindp3.w	$⊢ φ \to W \in LVec$
6		lspindp3.x	$⊢ φ \to X \in V$
7		lspindp3.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
8		lspindp3.e	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
9	5	adantr	$⊢ (φ \land N (\{X\}) = N (\{X \underset{˙}{+} Y\})) \to W \in LVec$
10	6	adantr	$⊢ (φ \land N (\{X\}) = N (\{X \underset{˙}{+} Y\})) \to X \in V$
11	7	adantr	$⊢ (φ \land N (\{X\}) = N (\{X \underset{˙}{+} Y\})) \to Y \in (V ∖ \{\underset{˙}{0}\})$
12		simpr	$⊢ (φ \land N (\{X\}) = N (\{X \underset{˙}{+} Y\})) \to N (\{X\}) = N (\{X \underset{˙}{+} Y\})$
13	1 2 3 4 9 10 11 12	lspabs2	$⊢ (φ \land N (\{X\}) = N (\{X \underset{˙}{+} Y\})) \to N (\{X\}) = N (\{Y\})$
14	13	ex	$⊢ φ \to (N (\{X\}) = N (\{X \underset{˙}{+} Y\}) \to N (\{X\}) = N (\{Y\}))$
15	14	necon3d	$⊢ φ \to (N (\{X\}) \neq N (\{Y\}) \to N (\{X\}) \neq N (\{X \underset{˙}{+} Y\}))$
16	8 15	mpd	$⊢ φ \to N (\{X\}) \neq N (\{X \underset{˙}{+} Y\})$

Metamath Proof Explorer