Metamath Proof Explorer


Definition df-padd

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)

Ref Expression
Assertion 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 ) } ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpadd
 |-  +P
1 vl
 |-  l
2 cvv
 |-  _V
3 vm
 |-  m
4 catm
 |-  Atoms
5 1 cv
 |-  l
6 5 4 cfv
 |-  ( Atoms ` l )
7 6 cpw
 |-  ~P ( Atoms ` l )
8 vn
 |-  n
9 3 cv
 |-  m
10 8 cv
 |-  n
11 9 10 cun
 |-  ( m u. n )
12 vp
 |-  p
13 vq
 |-  q
14 vr
 |-  r
15 12 cv
 |-  p
16 cple
 |-  le
17 5 16 cfv
 |-  ( le ` l )
18 13 cv
 |-  q
19 cjn
 |-  join
20 5 19 cfv
 |-  ( join ` l )
21 14 cv
 |-  r
22 18 21 20 co
 |-  ( q ( join ` l ) r )
23 15 22 17 wbr
 |-  p ( le ` l ) ( q ( join ` l ) r )
24 23 14 10 wrex
 |-  E. r e. n p ( le ` l ) ( q ( join ` l ) r )
25 24 13 9 wrex
 |-  E. q e. m E. r e. n p ( le ` l ) ( q ( join ` l ) r )
26 25 12 6 crab
 |-  { p e. ( Atoms ` l ) | E. q e. m E. r e. n p ( le ` l ) ( q ( join ` l ) r ) }
27 11 26 cun
 |-  ( ( m u. n ) u. { p e. ( Atoms ` l ) | E. q e. m E. r e. n p ( le ` l ) ( q ( join ` l ) r ) } )
28 3 8 7 7 27 cmpo
 |-  ( 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 ) } ) )
29 1 2 28 cmpt
 |-  ( 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 ) } ) ) )
30 0 29 wceq
 |-  +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 ) } ) ) )