Theorem lpolfN

Description: Functionality of a polarity. (Contributed by NM, 26-Nov-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lpolf.v	|- V = ( Base ` W )
	lpolf.s	|- S = ( LSubSp ` W )
	lpolf.p	|- P = ( LPol ` W )
	lpolf.w	|- ( ph -> W e. X )
	lpolf.o	|- ( ph -> ._|_ e. P )
Assertion	lpolfN	|- ( ph -> ._|_ : ~P V --> S )

Proof

Step	Hyp	Ref	Expression
1		lpolf.v	|- V = ( Base ` W )
2		lpolf.s	|- S = ( LSubSp ` W )
3		lpolf.p	|- P = ( LPol ` W )
4		lpolf.w	|- ( ph -> W e. X )
5		lpolf.o	|- ( ph -> ._|_ e. P )
6		eqid	|- ( 0g ` W ) = ( 0g ` W )
7		eqid	|- ( LSAtoms ` W ) = ( LSAtoms ` W )
8		eqid	|- ( LSHyp ` W ) = ( LSHyp ` W )
9	1 2 6 7 8 3	islpolN	|- ( W e. X -> ( ._|_ e. P <-> ( ._|_ : ~P V --> S /\ ( ( ._|_ ` V ) = { ( 0g ` W ) } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. ( LSAtoms ` W ) ( ( ._|_ ` x ) e. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) ) )
10	4 9	syl	|- ( ph -> ( ._|_ e. P <-> ( ._|_ : ~P V --> S /\ ( ( ._|_ ` V ) = { ( 0g ` W ) } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. ( LSAtoms ` W ) ( ( ._|_ ` x ) e. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) ) )
11	5 10	mpbid	|- ( ph -> ( ._|_ : ~P V --> S /\ ( ( ._|_ ` V ) = { ( 0g ` W ) } /\ A. x A. y ( ( x C_ V /\ y C_ V /\ x C_ y ) -> ( ._|_ ` y ) C_ ( ._|_ ` x ) ) /\ A. x e. ( LSAtoms ` W ) ( ( ._|_ ` x ) e. ( LSHyp ` W ) /\ ( ._|_ ` ( ._|_ ` x ) ) = x ) ) ) )
12	11	simpld	|- ( ph -> ._|_ : ~P V --> S )