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 =/= (/) )

Metamath Proof Explorer

Theorem lbsextlem1

Proof