Metamath Proof Explorer


Theorem polfvalN

Description: The projective subspace polarity function. (Contributed by NM, 23-Oct-2011) (New usage is discouraged.)

Ref Expression
Hypotheses polfval.o
|- ._|_ = ( oc ` K )
polfval.a
|- A = ( Atoms ` K )
polfval.m
|- M = ( pmap ` K )
polfval.p
|- P = ( _|_P ` K )
Assertion polfvalN
|- ( K e. B -> P = ( m e. ~P A |-> ( A i^i |^|_ p e. m ( M ` ( ._|_ ` p ) ) ) ) )

Proof

Step Hyp Ref Expression
1 polfval.o
 |-  ._|_ = ( oc ` K )
2 polfval.a
 |-  A = ( Atoms ` K )
3 polfval.m
 |-  M = ( pmap ` K )
4 polfval.p
 |-  P = ( _|_P ` K )
5 elex
 |-  ( K e. B -> K e. _V )
6 fveq2
 |-  ( h = K -> ( Atoms ` h ) = ( Atoms ` K ) )
7 6 2 eqtr4di
 |-  ( h = K -> ( Atoms ` h ) = A )
8 7 pweqd
 |-  ( h = K -> ~P ( Atoms ` h ) = ~P A )
9 fveq2
 |-  ( h = K -> ( pmap ` h ) = ( pmap ` K ) )
10 9 3 eqtr4di
 |-  ( h = K -> ( pmap ` h ) = M )
11 fveq2
 |-  ( h = K -> ( oc ` h ) = ( oc ` K ) )
12 11 1 eqtr4di
 |-  ( h = K -> ( oc ` h ) = ._|_ )
13 12 fveq1d
 |-  ( h = K -> ( ( oc ` h ) ` p ) = ( ._|_ ` p ) )
14 10 13 fveq12d
 |-  ( h = K -> ( ( pmap ` h ) ` ( ( oc ` h ) ` p ) ) = ( M ` ( ._|_ ` p ) ) )
15 14 adantr
 |-  ( ( h = K /\ p e. m ) -> ( ( pmap ` h ) ` ( ( oc ` h ) ` p ) ) = ( M ` ( ._|_ ` p ) ) )
16 15 iineq2dv
 |-  ( h = K -> |^|_ p e. m ( ( pmap ` h ) ` ( ( oc ` h ) ` p ) ) = |^|_ p e. m ( M ` ( ._|_ ` p ) ) )
17 7 16 ineq12d
 |-  ( h = K -> ( ( Atoms ` h ) i^i |^|_ p e. m ( ( pmap ` h ) ` ( ( oc ` h ) ` p ) ) ) = ( A i^i |^|_ p e. m ( M ` ( ._|_ ` p ) ) ) )
18 8 17 mpteq12dv
 |-  ( h = K -> ( m e. ~P ( Atoms ` h ) |-> ( ( Atoms ` h ) i^i |^|_ p e. m ( ( pmap ` h ) ` ( ( oc ` h ) ` p ) ) ) ) = ( m e. ~P A |-> ( A i^i |^|_ p e. m ( M ` ( ._|_ ` p ) ) ) ) )
19 df-polarityN
 |-  _|_P = ( h e. _V |-> ( m e. ~P ( Atoms ` h ) |-> ( ( Atoms ` h ) i^i |^|_ p e. m ( ( pmap ` h ) ` ( ( oc ` h ) ` p ) ) ) ) )
20 2 fvexi
 |-  A e. _V
21 20 pwex
 |-  ~P A e. _V
22 21 mptex
 |-  ( m e. ~P A |-> ( A i^i |^|_ p e. m ( M ` ( ._|_ ` p ) ) ) ) e. _V
23 18 19 22 fvmpt
 |-  ( K e. _V -> ( _|_P ` K ) = ( m e. ~P A |-> ( A i^i |^|_ p e. m ( M ` ( ._|_ ` p ) ) ) ) )
24 4 23 syl5eq
 |-  ( K e. _V -> P = ( m e. ~P A |-> ( A i^i |^|_ p e. m ( M ` ( ._|_ ` p ) ) ) ) )
25 5 24 syl
 |-  ( K e. B -> P = ( m e. ~P A |-> ( A i^i |^|_ p e. m ( M ` ( ._|_ ` p ) ) ) ) )