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 ) ) ) ) )