lspindp1

Description: Alternate way to say 3 vectors are mutually independent (swap 1st and 2nd). (Contributed by NM, 11-Apr-2015)

Step	Hyp	Ref	Expression
1		lspindp1.v	$⊢ V = {Base}_{W}$
2		lspindp1.o	$⊢ \underset{˙}{0} = 0_{W}$
3		lspindp1.n	$⊢ N = LSpan (W)$
4		lspindp1.w	$⊢ φ \to W \in LVec$
5		lspindp1.y	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
6		lspindp1.z	$⊢ φ \to Y \in V$
7		lspindp1.x	$⊢ φ \to Z \in V$
8		lspindp1.q	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
9		lspindp1.e	$⊢ φ \to \neg Z \in N (\{X, Y\})$
10	5	eldifad	$⊢ φ \to X \in V$
11	1 3 4 7 10 6 9	lspindpi	$⊢ φ \to (N (\{Z\}) \neq N (\{X\}) \land N (\{Z\}) \neq N (\{Y\}))$
12	11	simprd	$⊢ φ \to N (\{Z\}) \neq N (\{Y\})$
13	4	adantr	$⊢ (φ \land X \in N (\{Z, Y\})) \to W \in LVec$
14	5	adantr	$⊢ (φ \land X \in N (\{Z, Y\})) \to X \in (V ∖ \{\underset{˙}{0}\})$
15	7	adantr	$⊢ (φ \land X \in N (\{Z, Y\})) \to Z \in V$
16	6	adantr	$⊢ (φ \land X \in N (\{Z, Y\})) \to Y \in V$
17	8	adantr	$⊢ (φ \land X \in N (\{Z, Y\})) \to N (\{X\}) \neq N (\{Y\})$
18		simpr	$⊢ (φ \land X \in N (\{Z, Y\})) \to X \in N (\{Z, Y\})$
19	1 2 3 13 14 15 16 17 18	lspexch	$⊢ (φ \land X \in N (\{Z, Y\})) \to Z \in N (\{X, Y\})$
20	9 19	mtand	$⊢ φ \to \neg X \in N (\{Z, Y\})$
21	12 20	jca	$⊢ φ \to (N (\{Z\}) \neq N (\{Y\}) \land \neg X \in N (\{Z, Y\}))$

Metamath Proof Explorer