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 30530
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 30529 . 2  class  + P
2 vl . . 3  set  l
3 cvv 2948 . . 3  class  _V
4 vm . . . 4  set  m
5 vn . . . 4  set  n
62cv 1651 . . . . . 6  class  l
7 catm 29998 . . . . . 6  class  Atoms
86, 7cfv 5446 . . . . 5  class  ( Atoms `  l )
98cpw 3791 . . . 4  class  ~P ( Atoms `  l )
104cv 1651 . . . . . 6  class  m
115cv 1651 . . . . . 6  class  n
1210, 11cun 3310 . . . . 5  class  ( m  u.  n )
13 vp . . . . . . . . . 10  set  p
1413cv 1651 . . . . . . . . 9  class  p
15 vq . . . . . . . . . . 11  set  q
1615cv 1651 . . . . . . . . . 10  class  q
17 vr . . . . . . . . . . 11  set  r
1817cv 1651 . . . . . . . . . 10  class  r
19 cjn 14393 . . . . . . . . . . 11  class  join
206, 19cfv 5446 . . . . . . . . . 10  class  ( join `  l )
2116, 18, 20co 6073 . . . . . . . . 9  class  ( q ( join `  l
) r )
22 cple 13528 . . . . . . . . . 10  class  le
236, 22cfv 5446 . . . . . . . . 9  class  ( le
`  l )
2414, 21, 23wbr 4204 . . . . . . . 8  wff  p ( le `  l ) ( q ( join `  l ) r )
2524, 17, 11wrex 2698 . . . . . . 7  wff  E. r  e.  n  p ( le `  l ) ( q ( join `  l
) r )
2625, 15, 10wrex 2698 . . . . . 6  wff  E. q  e.  m  E. r  e.  n  p ( le `  l ) ( q ( join `  l
) r )
2726, 13, 8crab 2701 . . . . 5  class  { p  e.  ( Atoms `  l )  |  E. q  e.  m  E. r  e.  n  p ( le `  l ) ( q ( join `  l
) r ) }
2812, 27cun 3310 . . . 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 6075 . . 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 4258 . 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 1652 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  30531
  Copyright terms: Public domain W3C validator