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 ) |
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 ) |