Theorem pol0N

Description: The polarity of the empty projective subspace is the whole space. (Contributed by NM, 29-Oct-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	polssat.a	|- A = ( Atoms ` K )
	polssat.p	|- ._|_ = ( _|_P ` K )
Assertion	pol0N	|- ( K e. B -> ( ._|_ ` (/) ) = A )

Proof

Step	Hyp	Ref	Expression
1		polssat.a	|- A = ( Atoms ` K )
2		polssat.p	|- ._|_ = ( _|_P ` K )
3		0ss	|- (/) C_ A
4		eqid	|- ( oc ` K ) = ( oc ` K )
5		eqid	|- ( pmap ` K ) = ( pmap ` K )
6	4 1 5 2	polvalN	|- ( ( K e. B /\ (/) C_ A ) -> ( ._|_ ` (/) ) = ( A i^i |^|_ p e. (/) ( ( pmap ` K ) ` ( ( oc ` K ) ` p ) ) ) )
7	3 6	mpan2	|- ( K e. B -> ( ._|_ ` (/) ) = ( A i^i |^|_ p e. (/) ( ( pmap ` K ) ` ( ( oc ` K ) ` p ) ) ) )
8		0iin	|- |^|_ p e. (/) ( ( pmap ` K ) ` ( ( oc ` K ) ` p ) ) = _V
9	8	ineq2i	|- ( A i^i |^|_ p e. (/) ( ( pmap ` K ) ` ( ( oc ` K ) ` p ) ) ) = ( A i^i _V )
10		inv1	|- ( A i^i _V ) = A
11	9 10	eqtri	|- ( A i^i |^|_ p e. (/) ( ( pmap ` K ) ` ( ( oc ` K ) ` p ) ) ) = A
12	7 11	eqtrdi	|- ( K e. B -> ( ._|_ ` (/) ) = A )