This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lsppratlem5

Description: Lemma for lspprat . Combine the two cases and show a contradiction to U C. ( N{ X , Y } ) under the assumptions on x and 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 lsppratlem5 
|- ( ph -> ( N ` { X , Y } ) C_ U )

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 5 adantr 
 |-  ( ( ph /\ x e. ( N ` { Y } ) ) -> U e. S )
14 6 adantr 
 |-  ( ( ph /\ x e. ( N ` { Y } ) ) -> X e. V )
15 7 adantr 
 |-  ( ( ph /\ x e. ( N ` { Y } ) ) -> Y e. V )
16 8 adantr 
 |-  ( ( ph /\ x e. ( N ` { Y } ) ) -> U C. ( N ` { X , Y } ) )
17 10 adantr 
 |-  ( ( ph /\ x e. ( N ` { Y } ) ) -> x e. ( U \ { .0. } ) )
18 11 adantr 
 |-  ( ( ph /\ x e. ( N ` { Y } ) ) -> y e. ( U \ ( N ` { x } ) ) )
19 simpr 
 |-  ( ( ph /\ x e. ( N ` { Y } ) ) -> x e. ( N ` { Y } ) )
20 1 2 3 12 13 14 15 16 9 17 18 19 lsppratlem3 
 |-  ( ( ph /\ x e. ( N ` { Y } ) ) -> ( X e. ( N ` { x , y } ) /\ Y e. ( N ` { x , y } ) ) )
21 4 adantr 
 |-  ( ( ph /\ X e. ( N ` { x , Y } ) ) -> W e. LVec )
22 5 adantr 
 |-  ( ( ph /\ X e. ( N ` { x , Y } ) ) -> U e. S )
23 6 adantr 
 |-  ( ( ph /\ X e. ( N ` { x , Y } ) ) -> X e. V )
24 7 adantr 
 |-  ( ( ph /\ X e. ( N ` { x , Y } ) ) -> Y e. V )
25 8 adantr 
 |-  ( ( ph /\ X e. ( N ` { x , Y } ) ) -> U C. ( N ` { X , Y } ) )
26 10 adantr 
 |-  ( ( ph /\ X e. ( N ` { x , Y } ) ) -> x e. ( U \ { .0. } ) )
27 11 adantr 
 |-  ( ( ph /\ X e. ( N ` { x , Y } ) ) -> y e. ( U \ ( N ` { x } ) ) )
28 simpr 
 |-  ( ( ph /\ X e. ( N ` { x , Y } ) ) -> X e. ( N ` { x , Y } ) )
29 1 2 3 21 22 23 24 25 9 26 27 28 lsppratlem4 
 |-  ( ( ph /\ X e. ( N ` { x , Y } ) ) -> ( X e. ( N ` { x , y } ) /\ Y e. ( N ` { x , y } ) ) )
30 1 2 3 4 5 6 7 8 9 10 11 lsppratlem1 
 |-  ( ph -> ( x e. ( N ` { Y } ) \/ X e. ( N ` { x , Y } ) ) )
31 20 29 30 mpjaodan 
 |-  ( ph -> ( X e. ( N ` { x , y } ) /\ Y e. ( N ` { x , y } ) ) )
32 4 adantr 
 |-  ( ( ph /\ ( X e. ( N ` { x , y } ) /\ Y e. ( N ` { x , y } ) ) ) -> W e. LVec )
33 5 adantr 
 |-  ( ( ph /\ ( X e. ( N ` { x , y } ) /\ Y e. ( N ` { x , y } ) ) ) -> U e. S )
34 6 adantr 
 |-  ( ( ph /\ ( X e. ( N ` { x , y } ) /\ Y e. ( N ` { x , y } ) ) ) -> X e. V )
35 7 adantr 
 |-  ( ( ph /\ ( X e. ( N ` { x , y } ) /\ Y e. ( N ` { x , y } ) ) ) -> Y e. V )
36 8 adantr 
 |-  ( ( ph /\ ( X e. ( N ` { x , y } ) /\ Y e. ( N ` { x , y } ) ) ) -> U C. ( N ` { X , Y } ) )
37 10 adantr 
 |-  ( ( ph /\ ( X e. ( N ` { x , y } ) /\ Y e. ( N ` { x , y } ) ) ) -> x e. ( U \ { .0. } ) )
38 11 adantr 
 |-  ( ( ph /\ ( X e. ( N ` { x , y } ) /\ Y e. ( N ` { x , y } ) ) ) -> y e. ( U \ ( N ` { x } ) ) )
39 simprl 
 |-  ( ( ph /\ ( X e. ( N ` { x , y } ) /\ Y e. ( N ` { x , y } ) ) ) -> X e. ( N ` { x , y } ) )
40 simprr 
 |-  ( ( ph /\ ( X e. ( N ` { x , y } ) /\ Y e. ( N ` { x , y } ) ) ) -> Y e. ( N ` { x , y } ) )
41 1 2 3 32 33 34 35 36 9 37 38 39 40 lsppratlem2 
 |-  ( ( ph /\ ( X e. ( N ` { x , y } ) /\ Y e. ( N ` { x , y } ) ) ) -> ( N ` { X , Y } ) C_ U )
42 31 41 mpdan 
 |-  ( ph -> ( N ` { X , Y } ) C_ U )