Metamath Proof Explorer

Theorem lbsextg

Description: For any linearly independent subset C of V , there is a basis containing the vectors in C . (Contributed by Mario Carneiro, 17-May-2015)

Ref Expression
Hypotheses lbsex.j 
|- J = ( LBasis ` W )
lbsex.v 
|- V = ( Base ` W )
lbsex.n 
|- N = ( LSpan ` W )
Assertion lbsextg 
|- ( ( ( W e. LVec /\ ~P V e. dom card ) /\ C C_ V /\ A. x e. C -. x e. ( N ` ( C \ { x } ) ) ) -> E. s e. J C C_ s )

Proof

Step Hyp Ref Expression
1 lbsex.j 
 |-  J = ( LBasis ` W )
2 lbsex.v 
 |-  V = ( Base ` W )
3 lbsex.n 
 |-  N = ( LSpan ` W )
4 simp1l 
 |-  ( ( ( W e. LVec /\ ~P V e. dom card ) /\ C C_ V /\ A. x e. C -. x e. ( N ` ( C \ { x } ) ) ) -> W e. LVec )
5 simp2 
 |-  ( ( ( W e. LVec /\ ~P V e. dom card ) /\ C C_ V /\ A. x e. C -. x e. ( N ` ( C \ { x } ) ) ) -> C C_ V )
6 simp3 
 |-  ( ( ( W e. LVec /\ ~P V e. dom card ) /\ C C_ V /\ A. x e. C -. x e. ( N ` ( C \ { x } ) ) ) -> A. x e. C -. x e. ( N ` ( C \ { x } ) ) )
7 id 
 |-  ( x = y -> x = y )
8 sneq 
 |-  ( x = y -> { x } = { y } )
9 8 difeq2d 
 |-  ( x = y -> ( C \ { x } ) = ( C \ { y } ) )
10 9 fveq2d 
 |-  ( x = y -> ( N ` ( C \ { x } ) ) = ( N ` ( C \ { y } ) ) )
11 7 10 eleq12d 
 |-  ( x = y -> ( x e. ( N ` ( C \ { x } ) ) <-> y e. ( N ` ( C \ { y } ) ) ) )
12 11 notbid 
 |-  ( x = y -> ( -. x e. ( N ` ( C \ { x } ) ) <-> -. y e. ( N ` ( C \ { y } ) ) ) )
13 12 cbvralvw 
 |-  ( A. x e. C -. x e. ( N ` ( C \ { x } ) ) <-> A. y e. C -. y e. ( N ` ( C \ { y } ) ) )
14 6 13 sylib 
 |-  ( ( ( W e. LVec /\ ~P V e. dom card ) /\ C C_ V /\ A. x e. C -. x e. ( N ` ( C \ { x } ) ) ) -> A. y e. C -. y e. ( N ` ( C \ { y } ) ) )
15 8 difeq2d 
 |-  ( x = y -> ( z \ { x } ) = ( z \ { y } ) )
16 15 fveq2d 
 |-  ( x = y -> ( N ` ( z \ { x } ) ) = ( N ` ( z \ { y } ) ) )
17 7 16 eleq12d 
 |-  ( x = y -> ( x e. ( N ` ( z \ { x } ) ) <-> y e. ( N ` ( z \ { y } ) ) ) )
18 17 notbid 
 |-  ( x = y -> ( -. x e. ( N ` ( z \ { x } ) ) <-> -. y e. ( N ` ( z \ { y } ) ) ) )
19 18 cbvralvw 
 |-  ( A. x e. z -. x e. ( N ` ( z \ { x } ) ) <-> A. y e. z -. y e. ( N ` ( z \ { y } ) ) )
20 19 anbi2i 
 |-  ( ( C C_ z /\ A. x e. z -. x e. ( N ` ( z \ { x } ) ) ) <-> ( C C_ z /\ A. y e. z -. y e. ( N ` ( z \ { y } ) ) ) )
21 20 rabbii 
 |-  { z e. ~P V | ( C C_ z /\ A. x e. z -. x e. ( N ` ( z \ { x } ) ) ) } = { z e. ~P V | ( C C_ z /\ A. y e. z -. y e. ( N ` ( z \ { y } ) ) ) }
22 simp1r 
 |-  ( ( ( W e. LVec /\ ~P V e. dom card ) /\ C C_ V /\ A. x e. C -. x e. ( N ` ( C \ { x } ) ) ) -> ~P V e. dom card )
23 2 1 3 4 5 14 21 22 lbsextlem4 
 |-  ( ( ( W e. LVec /\ ~P V e. dom card ) /\ C C_ V /\ A. x e. C -. x e. ( N ` ( C \ { x } ) ) ) -> E. s e. J C C_ s )