Metamath Proof Explorer


Theorem lspsncmp

Description: Comparable spans of nonzero singletons are equal. (Contributed by NM, 27-Apr-2015)

Ref Expression
Hypotheses lspsncmp.v V = Base W
lspsncmp.o 0 ˙ = 0 W
lspsncmp.n N = LSpan W
lspsncmp.w φ W LVec
lspsncmp.x φ X V 0 ˙
lspsncmp.y φ Y V
Assertion lspsncmp φ N X N Y N X = N Y

Proof

Step Hyp Ref Expression
1 lspsncmp.v V = Base W
2 lspsncmp.o 0 ˙ = 0 W
3 lspsncmp.n N = LSpan W
4 lspsncmp.w φ W LVec
5 lspsncmp.x φ X V 0 ˙
6 lspsncmp.y φ Y V
7 4 adantr φ N X N Y W LVec
8 6 adantr φ N X N Y Y V
9 eqid LSubSp W = LSubSp W
10 lveclmod W LVec W LMod
11 4 10 syl φ W LMod
12 1 9 3 lspsncl W LMod Y V N Y LSubSp W
13 11 6 12 syl2anc φ N Y LSubSp W
14 5 eldifad φ X V
15 1 9 3 11 13 14 lspsnel5 φ X N Y N X N Y
16 15 biimpar φ N X N Y X N Y
17 eldifsni X V 0 ˙ X 0 ˙
18 5 17 syl φ X 0 ˙
19 18 adantr φ N X N Y X 0 ˙
20 1 2 3 7 8 16 19 lspsneleq φ N X N Y N X = N Y
21 20 ex φ N X N Y N X = N Y
22 eqimss N X = N Y N X N Y
23 21 22 impbid1 φ N X N Y N X = N Y