Metamath Proof Explorer


Theorem lsatelbN

Description: A nonzero vector in an atom determines the atom. (Contributed by NM, 3-Feb-2015) (New usage is discouraged.)

Ref Expression
Hypotheses lsatelb.v V = Base W
lsatelb.o 0 ˙ = 0 W
lsatelb.n N = LSpan W
lsatelb.a A = LSAtoms W
lsatelb.w φ W LVec
lsatelb.x φ X V 0 ˙
lsatelb.u φ U A
Assertion lsatelbN φ X U U = N X

Proof

Step Hyp Ref Expression
1 lsatelb.v V = Base W
2 lsatelb.o 0 ˙ = 0 W
3 lsatelb.n N = LSpan W
4 lsatelb.a A = LSAtoms W
5 lsatelb.w φ W LVec
6 lsatelb.x φ X V 0 ˙
7 lsatelb.u φ U A
8 5 adantr φ X U W LVec
9 7 adantr φ X U U A
10 simpr φ X U X U
11 eldifsn X V 0 ˙ X V X 0 ˙
12 6 11 sylib φ X V X 0 ˙
13 12 simprd φ X 0 ˙
14 13 adantr φ X U X 0 ˙
15 2 3 4 8 9 10 14 lsatel φ X U U = N X
16 eqimss2 U = N X N X U
17 16 adantl φ U = N X N X U
18 eqid LSubSp W = LSubSp W
19 lveclmod W LVec W LMod
20 5 19 syl φ W LMod
21 18 4 20 7 lsatlssel φ U LSubSp W
22 6 eldifad φ X V
23 1 18 3 20 21 22 lspsnel5 φ X U N X U
24 23 adantr φ U = N X X U N X U
25 17 24 mpbird φ U = N X X U
26 15 25 impbida φ X U U = N X