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

Definition df-padd 28674
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 28673 . 2  class  + P
2 vl . . 3  set  l
3 cvv 2727 . . 3  class  _V
4 vm . . . 4  set  m
5 vn . . . 4  set  n
62cv 1618 . . . . . 6  class  l
7 catm 28142 . . . . . 6  class  Atoms
86, 7cfv 4592 . . . . 5  class  ( Atoms `  l )
98cpw 3530 . . . 4  class  ~P ( Atoms `  l )
104cv 1618 . . . . . 6  class  m
115cv 1618 . . . . . 6  class  n
1210, 11cun 3076 . . . . 5  class  ( m  u.  n )
13 vp . . . . . . . . . 10  set  p
1413cv 1618 . . . . . . . . 9  class  p
15 vq . . . . . . . . . . 11  set  q
1615cv 1618 . . . . . . . . . 10  class  q
17 vr . . . . . . . . . . 11  set  r
1817cv 1618 . . . . . . . . . 10  class  r
19 cjn 13922 . . . . . . . . . . 11  class  join
206, 19cfv 4592 . . . . . . . . . 10  class  ( join `  l )
2116, 18, 20co 5710 . . . . . . . . 9  class  ( q ( join `  l
) r )
22 cple 13089 . . . . . . . . . 10  class  le
236, 22cfv 4592 . . . . . . . . 9  class  ( le
`  l )
2414, 21, 23wbr 3920 . . . . . . . 8  wff  p ( le `  l ) ( q ( join `  l ) r )
2524, 17, 11wrex 2510 . . . . . . 7  wff  E. r  e.  n  p ( le `  l ) ( q ( join `  l
) r )
2625, 15, 10wrex 2510 . . . . . 6  wff  E. q  e.  m  E. r  e.  n  p ( le `  l ) ( q ( join `  l
) r )
2726, 13, 8crab 2512 . . . . 5  class  { p  e.  ( Atoms `  l )  |  E. q  e.  m  E. r  e.  n  p ( le `  l ) ( q ( join `  l
) r ) }
2812, 27cun 3076 . . . 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 5712 . . 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 3974 . 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 1619 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  28675
  Copyright terms: Public domain W3C validator