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

Definition df-padd 30607
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 30606 . 2  class  + P
2 vl . . 3  set  l
3 cvv 2801 . . 3  class  _V
4 vm . . . 4  set  m
5 vn . . . 4  set  n
62cv 1631 . . . . . 6  class  l
7 catm 30075 . . . . . 6  class  Atoms
86, 7cfv 5271 . . . . 5  class  ( Atoms `  l )
98cpw 3638 . . . 4  class  ~P ( Atoms `  l )
104cv 1631 . . . . . 6  class  m
115cv 1631 . . . . . 6  class  n
1210, 11cun 3163 . . . . 5  class  ( m  u.  n )
13 vp . . . . . . . . . 10  set  p
1413cv 1631 . . . . . . . . 9  class  p
15 vq . . . . . . . . . . 11  set  q
1615cv 1631 . . . . . . . . . 10  class  q
17 vr . . . . . . . . . . 11  set  r
1817cv 1631 . . . . . . . . . 10  class  r
19 cjn 14094 . . . . . . . . . . 11  class  join
206, 19cfv 5271 . . . . . . . . . 10  class  ( join `  l )
2116, 18, 20co 5874 . . . . . . . . 9  class  ( q ( join `  l
) r )
22 cple 13231 . . . . . . . . . 10  class  le
236, 22cfv 5271 . . . . . . . . 9  class  ( le
`  l )
2414, 21, 23wbr 4039 . . . . . . . 8  wff  p ( le `  l ) ( q ( join `  l ) r )
2524, 17, 11wrex 2557 . . . . . . 7  wff  E. r  e.  n  p ( le `  l ) ( q ( join `  l
) r )
2625, 15, 10wrex 2557 . . . . . 6  wff  E. q  e.  m  E. r  e.  n  p ( le `  l ) ( q ( join `  l
) r )
2726, 13, 8crab 2560 . . . . 5  class  { p  e.  ( Atoms `  l )  |  E. q  e.  m  E. r  e.  n  p ( le `  l ) ( q ( join `  l
) r ) }
2812, 27cun 3163 . . . 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 5876 . . 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 4093 . 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 1632 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  30608
  Copyright terms: Public domain W3C validator