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