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 = ( Base ` W )
lspprat.s 
|- S = ( LSubSp ` W )
lspprat.n 
|- N = ( LSpan ` W )
lspprat.w 
|- ( ph -> W e. LVec )
lspprat.u 
|- ( ph -> U e. S )
lspprat.x 
|- ( ph -> X e. V )
lspprat.y 
|- ( ph -> Y e. V )
lspprat.p 
|- ( ph -> U C. ( N ` { X , Y } ) )
lsppratlem1.o 
|- .0. = ( 0g ` W )
lsppratlem1.x2 
|- ( ph -> x e. ( U \ { .0. } ) )
lsppratlem1.y2 
|- ( ph -> y e. ( U \ ( N ` { x } ) ) )
Assertion lsppratlem1 
|- ( ph -> ( x e. ( N ` { Y } ) \/ X e. ( N ` { x , Y } ) ) )

Proof

Step Hyp Ref Expression
1 lspprat.v 
 |-  V = ( Base ` W )
2 lspprat.s 
 |-  S = ( LSubSp ` W )
3 lspprat.n 
 |-  N = ( LSpan ` W )
4 lspprat.w 
 |-  ( ph -> W e. LVec )
5 lspprat.u 
 |-  ( ph -> U e. S )
6 lspprat.x 
 |-  ( ph -> X e. V )
7 lspprat.y 
 |-  ( ph -> Y e. V )
8 lspprat.p 
 |-  ( ph -> U C. ( N ` { X , Y } ) )
9 lsppratlem1.o 
 |-  .0. = ( 0g ` W )
10 lsppratlem1.x2 
 |-  ( ph -> x e. ( U \ { .0. } ) )
11 lsppratlem1.y2 
 |-  ( ph -> y e. ( U \ ( N ` { x } ) ) )
12 4 adantr 
 |-  ( ( ph /\ -. x e. ( N ` { Y } ) ) -> W e. LVec )
13 7 snssd 
 |-  ( ph -> { Y } C_ V )
14 13 adantr 
 |-  ( ( ph /\ -. x e. ( N ` { Y } ) ) -> { Y } C_ V )
15 6 adantr 
 |-  ( ( ph /\ -. x e. ( N ` { Y } ) ) -> X e. V )
16 8 pssssd 
 |-  ( ph -> U C_ ( N ` { X , Y } ) )
17 10 eldifad 
 |-  ( ph -> x e. U )
18 16 17 sseldd 
 |-  ( ph -> x e. ( N ` { X , Y } ) )
19 prcom 
 |-  { X , Y } = { Y , X }
20 df-pr 
 |-  { Y , X } = ( { Y } u. { X } )
21 19 20 eqtri 
 |-  { X , Y } = ( { Y } u. { X } )
22 21 fveq2i 
 |-  ( N ` { X , Y } ) = ( N ` ( { Y } u. { X } ) )
23 18 22 eleqtrdi 
 |-  ( ph -> x e. ( N ` ( { Y } u. { X } ) ) )
24 23 anim1i 
 |-  ( ( ph /\ -. x e. ( N ` { Y } ) ) -> ( x e. ( N ` ( { Y } u. { X } ) ) /\ -. x e. ( N ` { Y } ) ) )
25 eldif 
 |-  ( x e. ( ( N ` ( { Y } u. { X } ) ) \ ( N ` { Y } ) ) <-> ( x e. ( N ` ( { Y } u. { X } ) ) /\ -. x e. ( N ` { Y } ) ) )
26 24 25 sylibr 
 |-  ( ( ph /\ -. x e. ( N ` { Y } ) ) -> x e. ( ( N ` ( { Y } u. { X } ) ) \ ( N ` { Y } ) ) )
27 1 2 3 lspsolv 
 |-  ( ( W e. LVec /\ ( { Y } C_ V /\ X e. V /\ x e. ( ( N ` ( { Y } u. { X } ) ) \ ( N ` { Y } ) ) ) ) -> X e. ( N ` ( { Y } u. { x } ) ) )
28 12 14 15 26 27 syl13anc 
 |-  ( ( ph /\ -. x e. ( N ` { Y } ) ) -> X e. ( N ` ( { Y } u. { x } ) ) )
29 df-pr 
 |-  { Y , x } = ( { Y } u. { x } )
30 prcom 
 |-  { Y , x } = { x , Y }
31 29 30 eqtr3i 
 |-  ( { Y } u. { x } ) = { x , Y }
32 31 fveq2i 
 |-  ( N ` ( { Y } u. { x } ) ) = ( N ` { x , Y } )
33 28 32 eleqtrdi 
 |-  ( ( ph /\ -. x e. ( N ` { Y } ) ) -> X e. ( N ` { x , Y } ) )
34 33 ex 
 |-  ( ph -> ( -. x e. ( N ` { Y } ) -> X e. ( N ` { x , Y } ) ) )
35 34 orrd 
 |-  ( ph -> ( x e. ( N ` { Y } ) \/ X e. ( N ` { x , Y } ) ) )