Metamath Proof Explorer


Theorem lspsnne1

Description: Two ways to express that vectors have different spans. (Contributed by NM, 28-May-2015)

Ref Expression
Hypotheses lspsnne1.v V=BaseW
lspsnne1.o 0˙=0W
lspsnne1.n N=LSpanW
lspsnne1.w φWLVec
lspsnne1.x φXV0˙
lspsnne1.y φYV
lspsnne1.e φNXNY
Assertion lspsnne1 φ¬XNY

Proof

Step Hyp Ref Expression
1 lspsnne1.v V=BaseW
2 lspsnne1.o 0˙=0W
3 lspsnne1.n N=LSpanW
4 lspsnne1.w φWLVec
5 lspsnne1.x φXV0˙
6 lspsnne1.y φYV
7 lspsnne1.e φNXNY
8 eqid LSubSpW=LSubSpW
9 lveclmod WLVecWLMod
10 4 9 syl φWLMod
11 1 8 3 lspsncl WLModYVNYLSubSpW
12 10 6 11 syl2anc φNYLSubSpW
13 5 eldifad φXV
14 1 8 3 10 12 13 lspsnel5 φXNYNXNY
15 14 notbid φ¬XNY¬NXNY
16 1 2 3 4 5 6 lspsncmp φNXNYNX=NY
17 16 necon3bbid φ¬NXNYNXNY
18 15 17 bitrd φ¬XNYNXNY
19 7 18 mpbird φ¬XNY