Metamath Proof Explorer

Theorem lbsextlem1

Description: Lemma for lbsext . The set S is the set of all linearly independent sets containing C ; we show here that it is nonempty. (Contributed by Mario Carneiro, 25-Jun-2014)

Ref Expression
Hypotheses lbsext.v 
|- V = ( Base ` W )
lbsext.j 
|- J = ( LBasis ` W )
lbsext.n 
|- N = ( LSpan ` W )
lbsext.w 
|- ( ph -> W e. LVec )
lbsext.c 
|- ( ph -> C C_ V )
lbsext.x 
|- ( ph -> A. x e. C -. x e. ( N ` ( C \ { x } ) ) )
lbsext.s 
|- S = { z e. ~P V | ( C C_ z /\ A. x e. z -. x e. ( N ` ( z \ { x } ) ) ) }
Assertion lbsextlem1 
|- ( ph -> S =/= (/) )

Proof

Step Hyp Ref Expression
1 lbsext.v 
 |-  V = ( Base ` W )
2 lbsext.j 
 |-  J = ( LBasis ` W )
3 lbsext.n 
 |-  N = ( LSpan ` W )
4 lbsext.w 
 |-  ( ph -> W e. LVec )
5 lbsext.c 
 |-  ( ph -> C C_ V )
6 lbsext.x 
 |-  ( ph -> A. x e. C -. x e. ( N ` ( C \ { x } ) ) )
7 lbsext.s 
 |-  S = { z e. ~P V | ( C C_ z /\ A. x e. z -. x e. ( N ` ( z \ { x } ) ) ) }
8 1 fvexi 
 |-  V e. _V
9 8 elpw2 
 |-  ( C e. ~P V <-> C C_ V )
10 5 9 sylibr 
 |-  ( ph -> C e. ~P V )
11 ssid 
 |-  C C_ C
12 6 11 jctil 
 |-  ( ph -> ( C C_ C /\ A. x e. C -. x e. ( N ` ( C \ { x } ) ) ) )
13 sseq2 
 |-  ( z = C -> ( C C_ z <-> C C_ C ) )
14 difeq1 
 |-  ( z = C -> ( z \ { x } ) = ( C \ { x } ) )
15 14 fveq2d 
 |-  ( z = C -> ( N ` ( z \ { x } ) ) = ( N ` ( C \ { x } ) ) )
16 15 eleq2d 
 |-  ( z = C -> ( x e. ( N ` ( z \ { x } ) ) <-> x e. ( N ` ( C \ { x } ) ) ) )
17 16 notbid 
 |-  ( z = C -> ( -. x e. ( N ` ( z \ { x } ) ) <-> -. x e. ( N ` ( C \ { x } ) ) ) )
18 17 raleqbi1dv 
 |-  ( z = C -> ( A. x e. z -. x e. ( N ` ( z \ { x } ) ) <-> A. x e. C -. x e. ( N ` ( C \ { x } ) ) ) )
19 13 18 anbi12d 
 |-  ( z = C -> ( ( C C_ z /\ A. x e. z -. x e. ( N ` ( z \ { x } ) ) ) <-> ( C C_ C /\ A. x e. C -. x e. ( N ` ( C \ { x } ) ) ) ) )
20 19 7 elrab2 
 |-  ( C e. S <-> ( C e. ~P V /\ ( C C_ C /\ A. x e. C -. x e. ( N ` ( C \ { x } ) ) ) ) )
21 10 12 20 sylanbrc 
 |-  ( ph -> C e. S )
22 21 ne0d 
 |-  ( ph -> S =/= (/) )