Metamath Proof Explorer


Theorem lsat2el

Description: Two atoms sharing a nonzero vector are equal. (Contributed by NM, 8-Mar-2015)

Ref Expression
Hypotheses lsat2el.o
|- .0. = ( 0g ` W )
lsat2el.a
|- A = ( LSAtoms ` W )
lsat2el.w
|- ( ph -> W e. LVec )
lsat2el.p
|- ( ph -> P e. A )
lsat2el.q
|- ( ph -> Q e. A )
lsat2el.x
|- ( ph -> X =/= .0. )
lsat2el.x1
|- ( ph -> X e. P )
lsat2el.x2
|- ( ph -> X e. Q )
Assertion lsat2el
|- ( ph -> P = Q )

Proof

Step Hyp Ref Expression
1 lsat2el.o
 |-  .0. = ( 0g ` W )
2 lsat2el.a
 |-  A = ( LSAtoms ` W )
3 lsat2el.w
 |-  ( ph -> W e. LVec )
4 lsat2el.p
 |-  ( ph -> P e. A )
5 lsat2el.q
 |-  ( ph -> Q e. A )
6 lsat2el.x
 |-  ( ph -> X =/= .0. )
7 lsat2el.x1
 |-  ( ph -> X e. P )
8 lsat2el.x2
 |-  ( ph -> X e. Q )
9 eqid
 |-  ( LSpan ` W ) = ( LSpan ` W )
10 1 9 2 3 4 7 6 lsatel
 |-  ( ph -> P = ( ( LSpan ` W ) ` { X } ) )
11 1 9 2 3 5 8 6 lsatel
 |-  ( ph -> Q = ( ( LSpan ` W ) ` { X } ) )
12 10 11 eqtr4d
 |-  ( ph -> P = Q )