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𝑊 )
lsat2el.a 𝐴 = ( LSAtoms ‘ 𝑊 )
lsat2el.w ( 𝜑𝑊 ∈ LVec )
lsat2el.p ( 𝜑𝑃𝐴 )
lsat2el.q ( 𝜑𝑄𝐴 )
lsat2el.x ( 𝜑𝑋0 )
lsat2el.x1 ( 𝜑𝑋𝑃 )
lsat2el.x2 ( 𝜑𝑋𝑄 )
Assertion lsat2el ( 𝜑𝑃 = 𝑄 )

Proof

Step Hyp Ref Expression
1 lsat2el.o 0 = ( 0g𝑊 )
2 lsat2el.a 𝐴 = ( LSAtoms ‘ 𝑊 )
3 lsat2el.w ( 𝜑𝑊 ∈ LVec )
4 lsat2el.p ( 𝜑𝑃𝐴 )
5 lsat2el.q ( 𝜑𝑄𝐴 )
6 lsat2el.x ( 𝜑𝑋0 )
7 lsat2el.x1 ( 𝜑𝑋𝑃 )
8 lsat2el.x2 ( 𝜑𝑋𝑄 )
9 eqid ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
10 1 9 2 3 4 7 6 lsatel ( 𝜑𝑃 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑋 } ) )
11 1 9 2 3 5 8 6 lsatel ( 𝜑𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑋 } ) )
12 10 11 eqtr4d ( 𝜑𝑃 = 𝑄 )