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

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 ˙ = 0 W
lsat2el.a ⊢ A = LSAtoms ⁡ W
lsat2el.w ⊢ φ → W ∈ LVec
lsat2el.p ⊢ φ → P ∈ A
lsat2el.q ⊢ φ → Q ∈ A
lsat2el.x ⊢ φ → X ≠ 0 ˙
lsat2el.x1 ⊢ φ → X ∈ P
lsat2el.x2 ⊢ φ → X ∈ Q
Assertion lsat2el ⊢ φ → P = Q

Proof

Step Hyp Ref Expression
1 lsat2el.o ⊢ 0 ˙ = 0 W
2 lsat2el.a ⊢ A = LSAtoms ⁡ W
3 lsat2el.w ⊢ φ → W ∈ LVec
4 lsat2el.p ⊢ φ → P ∈ A
5 lsat2el.q ⊢ φ → Q ∈ A
6 lsat2el.x ⊢ φ → X ≠ 0 ˙
7 lsat2el.x1 ⊢ φ → X ∈ P
8 lsat2el.x2 ⊢ φ → X ∈ Q
9 eqid ⊢ LSpan ⁡ W = LSpan ⁡ W
10 1 9 2 3 4 7 6 lsatel ⊢ φ → P = LSpan ⁡ W ⁡ X
11 1 9 2 3 5 8 6 lsatel ⊢ φ → Q = LSpan ⁡ W ⁡ X
12 10 11 eqtr4d ⊢ φ → P = Q