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	⊢ ( 𝜑 → 𝑃 = 𝑄 )