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

Definition df-padd 30655
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 30654 . 2  class  + P
2 vl . . 3  set  l
3 cvv 2958 . . 3  class  _V
4 vm . . . 4  set  m
5 vn . . . 4  set  n
62cv 1652 . . . . . 6  class  l
7 catm 30123 . . . . . 6  class  Atoms
86, 7cfv 5456 . . . . 5  class  ( Atoms `  l )
98cpw 3801 . . . 4  class  ~P ( Atoms `  l )
104cv 1652 . . . . . 6  class  m
115cv 1652 . . . . . 6  class  n
1210, 11cun 3320 . . . . 5  class  ( m  u.  n )
13 vp . . . . . . . . . 10  set  p
1413cv 1652 . . . . . . . . 9  class  p
15 vq . . . . . . . . . . 11  set  q
1615cv 1652 . . . . . . . . . 10  class  q
17 vr . . . . . . . . . . 11  set  r
1817cv 1652 . . . . . . . . . 10  class  r
19 cjn 14403 . . . . . . . . . . 11  class  join
206, 19cfv 5456 . . . . . . . . . 10  class  ( join `  l )
2116, 18, 20co 6083 . . . . . . . . 9  class  ( q ( join `  l
) r )
22 cple 13538 . . . . . . . . . 10  class  le
236, 22cfv 5456 . . . . . . . . 9  class  ( le
`  l )
2414, 21, 23wbr 4214 . . . . . . . 8  wff  p ( le `  l ) ( q ( join `  l ) r )
2524, 17, 11wrex 2708 . . . . . . 7  wff  E. r  e.  n  p ( le `  l ) ( q ( join `  l
) r )
2625, 15, 10wrex 2708 . . . . . 6  wff  E. q  e.  m  E. r  e.  n  p ( le `  l ) ( q ( join `  l
) r )
2726, 13, 8crab 2711 . . . . 5  class  { p  e.  ( Atoms `  l )  |  E. q  e.  m  E. r  e.  n  p ( le `  l ) ( q ( join `  l
) r ) }
2812, 27cun 3320 . . . 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 6085 . . 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 4268 . 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 1653 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  30656
  Copyright terms: Public domain W3C validator