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

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