Theorem lshpset

Description: The set of all hyperplanes of a left module or left vector space. The vector v is called a generating vector for the hyperplane. (Contributed by NM, 29-Jun-2014)

	Ref	Expression
Hypotheses	lshpset.v	|- V = ( Base ` W )
	lshpset.n	|- N = ( LSpan ` W )
	lshpset.s	|- S = ( LSubSp ` W )
	lshpset.h	|- H = ( LSHyp ` W )
Assertion	lshpset	|- ( W e. X -> H = { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } )

Proof

Step	Hyp	Ref	Expression
1		lshpset.v	|- V = ( Base ` W )
2		lshpset.n	|- N = ( LSpan ` W )
3		lshpset.s	|- S = ( LSubSp ` W )
4		lshpset.h	|- H = ( LSHyp ` W )
5		elex	|- ( W e. X -> W e. _V )
6		fveq2	|- ( w = W -> ( LSubSp ` w ) = ( LSubSp ` W ) )
7	6 3	eqtr4di	|- ( w = W -> ( LSubSp ` w ) = S )
8		fveq2	|- ( w = W -> ( Base ` w ) = ( Base ` W ) )
9	8 1	eqtr4di	|- ( w = W -> ( Base ` w ) = V )
10	9	neeq2d	|- ( w = W -> ( s =/= ( Base ` w ) <-> s =/= V ) )
11		fveq2	|- ( w = W -> ( LSpan ` w ) = ( LSpan ` W ) )
12	11 2	eqtr4di	|- ( w = W -> ( LSpan ` w ) = N )
13	12	fveq1d	|- ( w = W -> ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( N ` ( s u. { v } ) ) )
14	13 9	eqeq12d	|- ( w = W -> ( ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) <-> ( N ` ( s u. { v } ) ) = V ) )
15	9 14	rexeqbidv	|- ( w = W -> ( E. v e. ( Base ` w ) ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) <-> E. v e. V ( N ` ( s u. { v } ) ) = V ) )
16	10 15	anbi12d	|- ( w = W -> ( ( s =/= ( Base ` w ) /\ E. v e. ( Base ` w ) ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) ) <-> ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) ) )
17	7 16	rabeqbidv	|- ( w = W -> { s e. ( LSubSp ` w ) | ( s =/= ( Base ` w ) /\ E. v e. ( Base ` w ) ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) ) } = { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } )
18		df-lshyp	|- LSHyp = ( w e. _V |-> { s e. ( LSubSp ` w ) | ( s =/= ( Base ` w ) /\ E. v e. ( Base ` w ) ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) ) } )
19	3	fvexi	|- S e. _V
20	19	rabex	|- { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } e. _V
21	17 18 20	fvmpt	|- ( W e. _V -> ( LSHyp ` W ) = { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } )
22	5 21	syl	|- ( W e. X -> ( LSHyp ` W ) = { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } )
23	4 22	syl5eq	|- ( W e. X -> H = { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } )