This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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. = ( 0g ` W )
lsatelb.n 
|- N = ( LSpan ` W )
lsatelb.a 
|- A = ( LSAtoms ` W )
lsatelb.w 
|- ( ph -> W e. LVec )
lsatelb.x 
|- ( ph -> X e. ( V \ { .0. } ) )
lsatelb.u 
|- ( ph -> U e. A )
Assertion lsatelbN 
|- ( ph -> ( X e. U <-> U = ( N ` { X } ) ) )

Proof

Step Hyp Ref Expression
1 lsatelb.v 
 |-  V = ( Base ` W )
2 lsatelb.o 
 |-  .0. = ( 0g ` W )
3 lsatelb.n 
 |-  N = ( LSpan ` W )
4 lsatelb.a 
 |-  A = ( LSAtoms ` W )
5 lsatelb.w 
 |-  ( ph -> W e. LVec )
6 lsatelb.x 
 |-  ( ph -> X e. ( V \ { .0. } ) )
7 lsatelb.u 
 |-  ( ph -> U e. A )
8 5 adantr 
 |-  ( ( ph /\ X e. U ) -> W e. LVec )
9 7 adantr 
 |-  ( ( ph /\ X e. U ) -> U e. A )
10 simpr 
 |-  ( ( ph /\ X e. U ) -> X e. U )
11 eldifsn 
 |-  ( X e. ( V \ { .0. } ) <-> ( X e. V /\ X =/= .0. ) )
12 6 11 sylib 
 |-  ( ph -> ( X e. V /\ X =/= .0. ) )
13 12 simprd 
 |-  ( ph -> X =/= .0. )
14 13 adantr 
 |-  ( ( ph /\ X e. U ) -> X =/= .0. )
15 2 3 4 8 9 10 14 lsatel 
 |-  ( ( ph /\ X e. U ) -> U = ( N ` { X } ) )
16 eqimss2 
 |-  ( U = ( N ` { X } ) -> ( N ` { X } ) C_ U )
17 16 adantl 
 |-  ( ( ph /\ U = ( N ` { X } ) ) -> ( N ` { X } ) C_ U )
18 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
19 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
20 5 19 syl 
 |-  ( ph -> W e. LMod )
21 18 4 20 7 lsatlssel 
 |-  ( ph -> U e. ( LSubSp ` W ) )
22 6 eldifad 
 |-  ( ph -> X e. V )
23 1 18 3 20 21 22 ellspsn5b 
 |-  ( ph -> ( X e. U <-> ( N ` { X } ) C_ U ) )
24 23 adantr 
 |-  ( ( ph /\ U = ( N ` { X } ) ) -> ( X e. U <-> ( N ` { X } ) C_ U ) )
25 17 24 mpbird 
 |-  ( ( ph /\ U = ( N ` { X } ) ) -> X e. U )
26 15 25 impbida 
 |-  ( ph -> ( X e. U <-> U = ( N ` { X } ) ) )