Metamath Proof Explorer

Theorem lsppratlem6

Description: Lemma for lspprat . Negating the assumption on y , we arrive close to the desired conclusion. (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 } ) )
lsppratlem6.o 
|- .0. = ( 0g ` W )
Assertion lsppratlem6 
|- ( ph -> ( x e. ( U \ { .0. } ) -> U = ( N ` { x } ) ) )

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 lsppratlem6.o 
 |-  .0. = ( 0g ` W )
10 8 adantr 
 |-  ( ( ph /\ x e. ( U \ { .0. } ) ) -> U C. ( N ` { X , Y } ) )
11 4 adantr 
 |-  ( ( ph /\ ( x e. ( U \ { .0. } ) /\ y e. ( U \ ( N ` { x } ) ) ) ) -> W e. LVec )
12 5 adantr 
 |-  ( ( ph /\ ( x e. ( U \ { .0. } ) /\ y e. ( U \ ( N ` { x } ) ) ) ) -> U e. S )
13 6 adantr 
 |-  ( ( ph /\ ( x e. ( U \ { .0. } ) /\ y e. ( U \ ( N ` { x } ) ) ) ) -> X e. V )
14 7 adantr 
 |-  ( ( ph /\ ( x e. ( U \ { .0. } ) /\ y e. ( U \ ( N ` { x } ) ) ) ) -> Y e. V )
15 8 adantr 
 |-  ( ( ph /\ ( x e. ( U \ { .0. } ) /\ y e. ( U \ ( N ` { x } ) ) ) ) -> U C. ( N ` { X , Y } ) )
16 simprl 
 |-  ( ( ph /\ ( x e. ( U \ { .0. } ) /\ y e. ( U \ ( N ` { x } ) ) ) ) -> x e. ( U \ { .0. } ) )
17 simprr 
 |-  ( ( ph /\ ( x e. ( U \ { .0. } ) /\ y e. ( U \ ( N ` { x } ) ) ) ) -> y e. ( U \ ( N ` { x } ) ) )
18 1 2 3 11 12 13 14 15 9 16 17 lsppratlem5 
 |-  ( ( ph /\ ( x e. ( U \ { .0. } ) /\ y e. ( U \ ( N ` { x } ) ) ) ) -> ( N ` { X , Y } ) C_ U )
19 ssnpss 
 |-  ( ( N ` { X , Y } ) C_ U -> -. U C. ( N ` { X , Y } ) )
20 18 19 syl 
 |-  ( ( ph /\ ( x e. ( U \ { .0. } ) /\ y e. ( U \ ( N ` { x } ) ) ) ) -> -. U C. ( N ` { X , Y } ) )
21 20 expr 
 |-  ( ( ph /\ x e. ( U \ { .0. } ) ) -> ( y e. ( U \ ( N ` { x } ) ) -> -. U C. ( N ` { X , Y } ) ) )
22 10 21 mt2d 
 |-  ( ( ph /\ x e. ( U \ { .0. } ) ) -> -. y e. ( U \ ( N ` { x } ) ) )
23 22 eq0rdv 
 |-  ( ( ph /\ x e. ( U \ { .0. } ) ) -> ( U \ ( N ` { x } ) ) = (/) )
24 ssdif0 
 |-  ( U C_ ( N ` { x } ) <-> ( U \ ( N ` { x } ) ) = (/) )
25 23 24 sylibr 
 |-  ( ( ph /\ x e. ( U \ { .0. } ) ) -> U C_ ( N ` { x } ) )
26 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
27 4 26 syl 
 |-  ( ph -> W e. LMod )
28 27 adantr 
 |-  ( ( ph /\ x e. ( U \ { .0. } ) ) -> W e. LMod )
29 5 adantr 
 |-  ( ( ph /\ x e. ( U \ { .0. } ) ) -> U e. S )
30 eldifi 
 |-  ( x e. ( U \ { .0. } ) -> x e. U )
31 30 adantl 
 |-  ( ( ph /\ x e. ( U \ { .0. } ) ) -> x e. U )
32 2 3 28 29 31 ellspsn5 
 |-  ( ( ph /\ x e. ( U \ { .0. } ) ) -> ( N ` { x } ) C_ U )
33 25 32 eqssd 
 |-  ( ( ph /\ x e. ( U \ { .0. } ) ) -> U = ( N ` { x } ) )
34 33 ex 
 |-  ( ph -> ( x e. ( U \ { .0. } ) -> U = ( N ` { x } ) ) )