Metamath Proof Explorer

Theorem paddval

Description: Projective subspace sum operation value. (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 paddval 
|- ( ( K e. B /\ X C_ A /\ Y C_ A ) -> ( X .+ Y ) = ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y 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 biid 
 |-  ( K e. B <-> K e. B )
6 3 fvexi 
 |-  A e. _V
7 6 elpw2 
 |-  ( X e. ~P A <-> X C_ A )
8 6 elpw2 
 |-  ( Y e. ~P A <-> Y C_ A )
9 1 2 3 4 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 ) } ) ) )
10 9 oveqd 
 |-  ( K e. B -> ( X .+ Y ) = ( X ( 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 ) } ) ) Y ) )
11 10 3ad2ant1 
 |-  ( ( K e. B /\ X e. ~P A /\ Y e. ~P A ) -> ( X .+ Y ) = ( X ( 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 ) } ) ) Y ) )
12 simpl 
 |-  ( ( X e. ~P A /\ Y e. ~P A ) -> X e. ~P A )
13 simpr 
 |-  ( ( X e. ~P A /\ Y e. ~P A ) -> Y e. ~P A )
14 unexg 
 |-  ( ( X e. ~P A /\ Y e. ~P A ) -> ( X u. Y ) e. _V )
15 6 rabex 
 |-  { p e. A | E. q e. X E. r e. Y p .<_ ( q .\/ r ) } e. _V
16 unexg 
 |-  ( ( ( X u. Y ) e. _V /\ { p e. A | E. q e. X E. r e. Y p .<_ ( q .\/ r ) } e. _V ) -> ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y p .<_ ( q .\/ r ) } ) e. _V )
17 14 15 16 sylancl 
 |-  ( ( X e. ~P A /\ Y e. ~P A ) -> ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y p .<_ ( q .\/ r ) } ) e. _V )
18 12 13 17 3jca 
 |-  ( ( X e. ~P A /\ Y e. ~P A ) -> ( X e. ~P A /\ Y e. ~P A /\ ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y p .<_ ( q .\/ r ) } ) e. _V ) )
19 18 3adant1 
 |-  ( ( K e. B /\ X e. ~P A /\ Y e. ~P A ) -> ( X e. ~P A /\ Y e. ~P A /\ ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y p .<_ ( q .\/ r ) } ) e. _V ) )
20 uneq1 
 |-  ( m = X -> ( m u. n ) = ( X u. n ) )
21 rexeq 
 |-  ( m = X -> ( E. q e. m E. r e. n p .<_ ( q .\/ r ) <-> E. q e. X E. r e. n p .<_ ( q .\/ r ) ) )
22 21 rabbidv 
 |-  ( m = X -> { p e. A | E. q e. m E. r e. n p .<_ ( q .\/ r ) } = { p e. A | E. q e. X E. r e. n p .<_ ( q .\/ r ) } )
23 20 22 uneq12d 
 |-  ( m = X -> ( ( m u. n ) u. { p e. A | E. q e. m E. r e. n p .<_ ( q .\/ r ) } ) = ( ( X u. n ) u. { p e. A | E. q e. X E. r e. n p .<_ ( q .\/ r ) } ) )
24 uneq2 
 |-  ( n = Y -> ( X u. n ) = ( X u. Y ) )
25 rexeq 
 |-  ( n = Y -> ( E. r e. n p .<_ ( q .\/ r ) <-> E. r e. Y p .<_ ( q .\/ r ) ) )
26 25 rexbidv 
 |-  ( n = Y -> ( E. q e. X E. r e. n p .<_ ( q .\/ r ) <-> E. q e. X E. r e. Y p .<_ ( q .\/ r ) ) )
27 26 rabbidv 
 |-  ( n = Y -> { p e. A | E. q e. X E. r e. n p .<_ ( q .\/ r ) } = { p e. A | E. q e. X E. r e. Y p .<_ ( q .\/ r ) } )
28 24 27 uneq12d 
 |-  ( n = Y -> ( ( X u. n ) u. { p e. A | E. q e. X E. r e. n p .<_ ( q .\/ r ) } ) = ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y p .<_ ( q .\/ r ) } ) )
29 eqid 
 |-  ( 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 ) } ) ) = ( 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 ) } ) )
30 23 28 29 ovmpog 
 |-  ( ( X e. ~P A /\ Y e. ~P A /\ ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y p .<_ ( q .\/ r ) } ) e. _V ) -> ( X ( 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 ) } ) ) Y ) = ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y p .<_ ( q .\/ r ) } ) )
31 19 30 syl 
 |-  ( ( K e. B /\ X e. ~P A /\ Y e. ~P A ) -> ( X ( 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 ) } ) ) Y ) = ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y p .<_ ( q .\/ r ) } ) )
32 11 31 eqtrd 
 |-  ( ( K e. B /\ X e. ~P A /\ Y e. ~P A ) -> ( X .+ Y ) = ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y p .<_ ( q .\/ r ) } ) )
33 5 7 8 32 syl3anbr 
 |-  ( ( K e. B /\ X C_ A /\ Y C_ A ) -> ( X .+ Y ) = ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y p .<_ ( q .\/ r ) } ) )