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 )

Metamath Proof Explorer

Theorem lbsextg

Proof