Theorem islshp

Description: The predicate "is a hyperplane" (of a left module or left vector space). (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	islshp	|- ( W e. X -> ( U e. H <-> ( U e. S /\ U =/= V /\ E. v e. V ( N ` ( U 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	1 2 3 4	lshpset	|- ( W e. X -> H = { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } )
6	5	eleq2d	|- ( W e. X -> ( U e. H <-> U e. { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } ) )
7		neeq1	|- ( s = U -> ( s =/= V <-> U =/= V ) )
8		uneq1	|- ( s = U -> ( s u. { v } ) = ( U u. { v } ) )
9	8	fveqeq2d	|- ( s = U -> ( ( N ` ( s u. { v } ) ) = V <-> ( N ` ( U u. { v } ) ) = V ) )
10	9	rexbidv	|- ( s = U -> ( E. v e. V ( N ` ( s u. { v } ) ) = V <-> E. v e. V ( N ` ( U u. { v } ) ) = V ) )
11	7 10	anbi12d	|- ( s = U -> ( ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) <-> ( U =/= V /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) ) )
12	11	elrab	|- ( U e. { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } <-> ( U e. S /\ ( U =/= V /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) ) )
13		3anass	|- ( ( U e. S /\ U =/= V /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) <-> ( U e. S /\ ( U =/= V /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) ) )
14	12 13	bitr4i	|- ( U e. { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } <-> ( U e. S /\ U =/= V /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) )
15	6 14	bitrdi	|- ( W e. X -> ( U e. H <-> ( U e. S /\ U =/= V /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) ) )