Metamath Proof Explorer

Theorem paddfval

Description: Projective subspace sum operation. (Contributed by NM, 29-Dec-2011)

Ref Expression
Hypotheses paddfval.l 
|- .<_ = ( le ` K )
paddfval.j 
|- .\/ = ( join ` K )
paddfval.a 
|- A = ( Atoms ` K )
paddfval.p 
|- .+ = ( +P ` K )
Assertion paddfval 
|- ( K e. B -> .+ = ( m e. ~P A , n e. ~P A |-> ( ( m u. n ) u. { p e. A | E. q e. m E. r e. n p .<_ ( q .\/ r ) } ) ) )

Proof

Step Hyp Ref Expression
1 paddfval.l 
 |-  .<_ = ( le ` K )
2 paddfval.j 
 |-  .\/ = ( join ` K )
3 paddfval.a 
 |-  A = ( Atoms ` K )
4 paddfval.p 
 |-  .+ = ( +P ` K )
5 elex 
 |-  ( K e. B -> K e. _V )
6 fveq2 
 |-  ( h = K -> ( Atoms ` h ) = ( Atoms ` K ) )
7 6 3 eqtr4di 
 |-  ( h = K -> ( Atoms ` h ) = A )
8 7 pweqd 
 |-  ( h = K -> ~P ( Atoms ` h ) = ~P A )
9 eqidd 
 |-  ( h = K -> p = p )
10 fveq2 
 |-  ( h = K -> ( le ` h ) = ( le ` K ) )
11 10 1 eqtr4di 
 |-  ( h = K -> ( le ` h ) = .<_ )
12 fveq2 
 |-  ( h = K -> ( join ` h ) = ( join ` K ) )
13 12 2 eqtr4di 
 |-  ( h = K -> ( join ` h ) = .\/ )
14 13 oveqd 
 |-  ( h = K -> ( q ( join ` h ) r ) = ( q .\/ r ) )
15 9 11 14 breq123d 
 |-  ( h = K -> ( p ( le ` h ) ( q ( join ` h ) r ) <-> p .<_ ( q .\/ r ) ) )
16 15 2rexbidv 
 |-  ( h = K -> ( E. q e. m E. r e. n p ( le ` h ) ( q ( join ` h ) r ) <-> E. q e. m E. r e. n p .<_ ( q .\/ r ) ) )
17 7 16 rabeqbidv 
 |-  ( h = K -> { p e. ( Atoms ` h ) | E. q e. m E. r e. n p ( le ` h ) ( q ( join ` h ) r ) } = { p e. A | E. q e. m E. r e. n p .<_ ( q .\/ r ) } )
18 17 uneq2d 
 |-  ( h = K -> ( ( m u. n ) u. { p e. ( Atoms ` h ) | E. q e. m E. r e. n p ( le ` h ) ( q ( join ` h ) r ) } ) = ( ( m u. n ) u. { p e. A | E. q e. m E. r e. n p .<_ ( q .\/ r ) } ) )
19 8 8 18 mpoeq123dv 
 |-  ( h = K -> ( m e. ~P ( Atoms ` h ) , n e. ~P ( Atoms ` h ) |-> ( ( m u. n ) u. { p e. ( Atoms ` h ) | E. q e. m E. r e. n p ( le ` h ) ( q ( join ` h ) r ) } ) ) = ( m e. ~P A , n e. ~P A |-> ( ( m u. n ) u. { p e. A | E. q e. m E. r e. n p .<_ ( q .\/ r ) } ) ) )
20 df-padd 
 |-  +P = ( h e. _V |-> ( m e. ~P ( Atoms ` h ) , n e. ~P ( Atoms ` h ) |-> ( ( m u. n ) u. { p e. ( Atoms ` h ) | E. q e. m E. r e. n p ( le ` h ) ( q ( join ` h ) r ) } ) ) )
21 3 fvexi 
 |-  A e. _V
22 21 pwex 
 |-  ~P A e. _V
23 22 22 mpoex 
 |-  ( m e. ~P A , n e. ~P A |-> ( ( m u. n ) u. { p e. A | E. q e. m E. r e. n p .<_ ( q .\/ r ) } ) ) e. _V
24 19 20 23 fvmpt 
 |-  ( K e. _V -> ( +P ` K ) = ( m e. ~P A , n e. ~P A |-> ( ( m u. n ) u. { p e. A | E. q e. m E. r e. n p .<_ ( q .\/ r ) } ) ) )
25 4 24 syl5eq 
 |-  ( K e. _V -> .+ = ( m e. ~P A , n e. ~P A |-> ( ( m u. n ) u. { p e. A | E. q e. m E. r e. n p .<_ ( q .\/ r ) } ) ) )
26 5 25 syl 
 |-  ( K e. B -> .+ = ( m e. ~P A , n e. ~P A |-> ( ( m u. n ) u. { p e. A | E. q e. m E. r e. n p .<_ ( q .\/ r ) } ) ) )