Metamath Proof Explorer


Theorem lssneln0

Description: A vector X which doesn't belong to a subspace U is nonzero. (Contributed by NM, 14-May-2015) (Revised by AV, 17-Jul-2022) (Proof shortened by AV, 19-Jul-2022)

Ref Expression
Hypotheses lssneln0.o 0˙=0W
lssneln0.s S=LSubSpW
lssneln0.w φWLMod
lssneln0.u φUS
lssneln0.x φXV
lssneln0.n φ¬XU
Assertion lssneln0 φXV0˙

Proof

Step Hyp Ref Expression
1 lssneln0.o 0˙=0W
2 lssneln0.s S=LSubSpW
3 lssneln0.w φWLMod
4 lssneln0.u φUS
5 lssneln0.x φXV
6 lssneln0.n φ¬XU
7 1 2 3 4 6 lssvneln0 φX0˙
8 eldifsn XV0˙XVX0˙
9 5 7 8 sylanbrc φXV0˙