Metamath Proof Explorer


Theorem pclfvalN

Description: The projective subspace closure function. (Contributed by NM, 7-Sep-2013) (New usage is discouraged.)

Ref Expression
Hypotheses pclfval.a
|- A = ( Atoms ` K )
pclfval.s
|- S = ( PSubSp ` K )
pclfval.c
|- U = ( PCl ` K )
Assertion pclfvalN
|- ( K e. V -> U = ( x e. ~P A |-> |^| { y e. S | x C_ y } ) )

Proof

Step Hyp Ref Expression
1 pclfval.a
 |-  A = ( Atoms ` K )
2 pclfval.s
 |-  S = ( PSubSp ` K )
3 pclfval.c
 |-  U = ( PCl ` K )
4 elex
 |-  ( K e. V -> K e. _V )
5 fveq2
 |-  ( k = K -> ( Atoms ` k ) = ( Atoms ` K ) )
6 5 1 eqtr4di
 |-  ( k = K -> ( Atoms ` k ) = A )
7 6 pweqd
 |-  ( k = K -> ~P ( Atoms ` k ) = ~P A )
8 fveq2
 |-  ( k = K -> ( PSubSp ` k ) = ( PSubSp ` K ) )
9 8 2 eqtr4di
 |-  ( k = K -> ( PSubSp ` k ) = S )
10 9 rabeqdv
 |-  ( k = K -> { y e. ( PSubSp ` k ) | x C_ y } = { y e. S | x C_ y } )
11 10 inteqd
 |-  ( k = K -> |^| { y e. ( PSubSp ` k ) | x C_ y } = |^| { y e. S | x C_ y } )
12 7 11 mpteq12dv
 |-  ( k = K -> ( x e. ~P ( Atoms ` k ) |-> |^| { y e. ( PSubSp ` k ) | x C_ y } ) = ( x e. ~P A |-> |^| { y e. S | x C_ y } ) )
13 df-pclN
 |-  PCl = ( k e. _V |-> ( x e. ~P ( Atoms ` k ) |-> |^| { y e. ( PSubSp ` k ) | x C_ y } ) )
14 1 fvexi
 |-  A e. _V
15 14 pwex
 |-  ~P A e. _V
16 15 mptex
 |-  ( x e. ~P A |-> |^| { y e. S | x C_ y } ) e. _V
17 12 13 16 fvmpt
 |-  ( K e. _V -> ( PCl ` K ) = ( x e. ~P A |-> |^| { y e. S | x C_ y } ) )
18 3 17 eqtrid
 |-  ( K e. _V -> U = ( x e. ~P A |-> |^| { y e. S | x C_ y } ) )
19 4 18 syl
 |-  ( K e. V -> U = ( x e. ~P A |-> |^| { y e. S | x C_ y } ) )