# Metamath Proof Explorer

## Theorem lspindp1

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

Ref Expression
Hypotheses lspindp1.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
lspindp1.o
lspindp1.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
lspindp1.w ${⊢}{\phi }\to {W}\in \mathrm{LVec}$
lspindp1.y
lspindp1.z ${⊢}{\phi }\to {Y}\in {V}$
lspindp1.x ${⊢}{\phi }\to {Z}\in {V}$
lspindp1.q ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
lspindp1.e ${⊢}{\phi }\to ¬{Z}\in {N}\left(\left\{{X},{Y}\right\}\right)$
Assertion lspindp1 ${⊢}{\phi }\to \left({N}\left(\left\{{Z}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)\wedge ¬{X}\in {N}\left(\left\{{Z},{Y}\right\}\right)\right)$

### Proof

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