This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )