Metamath Proof Explorer


Theorem lsppratlem1

Description: Lemma for lspprat . Let x e. ( U \ { 0 } ) (if there is no such x then U is the zero subspace), and let y e. ( U \ ( N{ x } ) ) (assuming the conclusion is false). The goal is to write X , Y in terms of x , y , which would normally be done by solving the system of linear equations. The span equivalent of this process is lspsolv (hence the name), which we use extensively below. In this lemma, we show that since x e. ( N{ X , Y } ) , either x e. ( N{ Y } ) or X e. ( N{ x , Y } ) . (Contributed by NM, 29-Aug-2014)

Ref Expression
Hypotheses lspprat.v V=BaseW
lspprat.s S=LSubSpW
lspprat.n N=LSpanW
lspprat.w φWLVec
lspprat.u φUS
lspprat.x φXV
lspprat.y φYV
lspprat.p φUNXY
lsppratlem1.o 0˙=0W
lsppratlem1.x2 φxU0˙
lsppratlem1.y2 φyUNx
Assertion lsppratlem1 φxNYXNxY

Proof

Step Hyp Ref Expression
1 lspprat.v V=BaseW
2 lspprat.s S=LSubSpW
3 lspprat.n N=LSpanW
4 lspprat.w φWLVec
5 lspprat.u φUS
6 lspprat.x φXV
7 lspprat.y φYV
8 lspprat.p φUNXY
9 lsppratlem1.o 0˙=0W
10 lsppratlem1.x2 φxU0˙
11 lsppratlem1.y2 φyUNx
12 4 adantr φ¬xNYWLVec
13 7 snssd φYV
14 13 adantr φ¬xNYYV
15 6 adantr φ¬xNYXV
16 8 pssssd φUNXY
17 10 eldifad φxU
18 16 17 sseldd φxNXY
19 prcom XY=YX
20 df-pr YX=YX
21 19 20 eqtri XY=YX
22 21 fveq2i NXY=NYX
23 18 22 eleqtrdi φxNYX
24 23 anim1i φ¬xNYxNYX¬xNY
25 eldif xNYXNYxNYX¬xNY
26 24 25 sylibr φ¬xNYxNYXNY
27 1 2 3 lspsolv WLVecYVXVxNYXNYXNYx
28 12 14 15 26 27 syl13anc φ¬xNYXNYx
29 df-pr Yx=Yx
30 prcom Yx=xY
31 29 30 eqtr3i Yx=xY
32 31 fveq2i NYx=NxY
33 28 32 eleqtrdi φ¬xNYXNxY
34 33 ex φ¬xNYXNxY
35 34 orrd φxNYXNxY