Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-padd Unicode version

Definition df-padd 30058
Description: Define projective sum of two subspaces (or more generally two sets of atoms), which is the union of all lines generated by pairs of atoms from each subspace. Lemma 16.2 of [MaedaMaeda] p. 68. For convenience, our definition is generalized to apply to empty sets. (Contributed by NM, 29-Dec-2011.)
Assertion
Ref Expression
df-padd  |-  + P  =  ( l  e. 
_V  |->  ( m  e. 
~P ( Atoms `  l
) ,  n  e. 
~P ( Atoms `  l
)  |->  ( ( m  u.  n )  u. 
{ p  e.  (
Atoms `  l )  |  E. q  e.  m  E. r  e.  n  p ( le `  l ) ( q ( join `  l
) r ) } ) ) )
Distinct variable group:    m, l, n, p, q, r

Detailed syntax breakdown of Definition df-padd
StepHypRef Expression
1 cpadd 30057 . 2  class  + P
2 vl . . 3  set  l
3 cvv 2790 . . 3  class  _V
4 vm . . . 4  set  m
5 vn . . . 4  set  n
62cv 1624 . . . . . 6  class  l
7 catm 29526 . . . . . 6  class  Atoms
86, 7cfv 5257 . . . . 5  class  ( Atoms `  l )
98cpw 3627 . . . 4  class  ~P ( Atoms `  l )
104cv 1624 . . . . . 6  class  m
115cv 1624 . . . . . 6  class  n
1210, 11cun 3152 . . . . 5  class  ( m  u.  n )
13 vp . . . . . . . . . 10  set  p
1413cv 1624 . . . . . . . . 9  class  p
15 vq . . . . . . . . . . 11  set  q
1615cv 1624 . . . . . . . . . 10  class  q
17 vr . . . . . . . . . . 11  set  r
1817cv 1624 . . . . . . . . . 10  class  r
19 cjn 14080 . . . . . . . . . . 11  class  join
206, 19cfv 5257 . . . . . . . . . 10  class  ( join `  l )
2116, 18, 20co 5860 . . . . . . . . 9  class  ( q ( join `  l
) r )
22 cple 13217 . . . . . . . . . 10  class  le
236, 22cfv 5257 . . . . . . . . 9  class  ( le
`  l )
2414, 21, 23wbr 4025 . . . . . . . 8  wff  p ( le `  l ) ( q ( join `  l ) r )
2524, 17, 11wrex 2546 . . . . . . 7  wff  E. r  e.  n  p ( le `  l ) ( q ( join `  l
) r )
2625, 15, 10wrex 2546 . . . . . 6  wff  E. q  e.  m  E. r  e.  n  p ( le `  l ) ( q ( join `  l
) r )
2726, 13, 8crab 2549 . . . . 5  class  { p  e.  ( Atoms `  l )  |  E. q  e.  m  E. r  e.  n  p ( le `  l ) ( q ( join `  l
) r ) }
2812, 27cun 3152 . . . 4  class  ( ( m  u.  n )  u.  { p  e.  ( Atoms `  l )  |  E. q  e.  m  E. r  e.  n  p ( le `  l ) ( q ( join `  l
) r ) } )
294, 5, 9, 9, 28cmpt2 5862 . . 3  class  ( m  e.  ~P ( Atoms `  l ) ,  n  e.  ~P ( Atoms `  l
)  |->  ( ( m  u.  n )  u. 
{ p  e.  (
Atoms `  l )  |  E. q  e.  m  E. r  e.  n  p ( le `  l ) ( q ( join `  l
) r ) } ) )
302, 3, 29cmpt 4079 . 2  class  ( l  e.  _V  |->  ( m  e.  ~P ( Atoms `  l ) ,  n  e.  ~P ( Atoms `  l
)  |->  ( ( m  u.  n )  u. 
{ p  e.  (
Atoms `  l )  |  E. q  e.  m  E. r  e.  n  p ( le `  l ) ( q ( join `  l
) r ) } ) ) )
311, 30wceq 1625 1  wff  + P  =  ( l  e. 
_V  |->  ( m  e. 
~P ( Atoms `  l
) ,  n  e. 
~P ( Atoms `  l
)  |->  ( ( m  u.  n )  u. 
{ p  e.  (
Atoms `  l )  |  E. q  e.  m  E. r  e.  n  p ( le `  l ) ( q ( join `  l
) r ) } ) ) )
Colors of variables: wff set class
This definition is referenced by:  paddfval  30059
  Copyright terms: Public domain W3C validator