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

Definition df-psubsp 28942
Description: Define set of all projective subspaces. Based on definition of subspace in [Holland95] p. 212. (Contributed by NM, 2-Oct-2011.)
Assertion
Ref Expression
df-psubsp  |-  PSubSp  =  ( k  e.  _V  |->  { s  |  ( s 
C_  ( Atoms `  k
)  /\  A. p  e.  s  A. q  e.  s  A. r  e.  ( Atoms `  k )
( r ( le
`  k ) ( p ( join `  k
) q )  -> 
r  e.  s ) ) } )
Distinct variable group:    k, p, q, r, s

Detailed syntax breakdown of Definition df-psubsp
StepHypRef Expression
1 cpsubsp 28935 . 2  class  PSubSp
2 vk . . 3  set  k
3 cvv 2763 . . 3  class  _V
4 vs . . . . . . 7  set  s
54cv 1618 . . . . . 6  class  s
62cv 1618 . . . . . . 7  class  k
7 catm 28703 . . . . . . 7  class  Atoms
86, 7cfv 4673 . . . . . 6  class  ( Atoms `  k )
95, 8wss 3127 . . . . 5  wff  s  C_  ( Atoms `  k )
10 vr . . . . . . . . . . 11  set  r
1110cv 1618 . . . . . . . . . 10  class  r
12 vp . . . . . . . . . . . 12  set  p
1312cv 1618 . . . . . . . . . . 11  class  p
14 vq . . . . . . . . . . . 12  set  q
1514cv 1618 . . . . . . . . . . 11  class  q
16 cjn 14041 . . . . . . . . . . . 12  class  join
176, 16cfv 4673 . . . . . . . . . . 11  class  ( join `  k )
1813, 15, 17co 5792 . . . . . . . . . 10  class  ( p ( join `  k
) q )
19 cple 13178 . . . . . . . . . . 11  class  le
206, 19cfv 4673 . . . . . . . . . 10  class  ( le
`  k )
2111, 18, 20wbr 3997 . . . . . . . . 9  wff  r ( le `  k ) ( p ( join `  k ) q )
2210, 4wel 1622 . . . . . . . . 9  wff  r  e.  s
2321, 22wi 6 . . . . . . . 8  wff  ( r ( le `  k
) ( p (
join `  k )
q )  ->  r  e.  s )
2423, 10, 8wral 2518 . . . . . . 7  wff  A. r  e.  ( Atoms `  k )
( r ( le
`  k ) ( p ( join `  k
) q )  -> 
r  e.  s )
2524, 14, 5wral 2518 . . . . . 6  wff  A. q  e.  s  A. r  e.  ( Atoms `  k )
( r ( le
`  k ) ( p ( join `  k
) q )  -> 
r  e.  s )
2625, 12, 5wral 2518 . . . . 5  wff  A. p  e.  s  A. q  e.  s  A. r  e.  ( Atoms `  k )
( r ( le
`  k ) ( p ( join `  k
) q )  -> 
r  e.  s )
279, 26wa 360 . . . 4  wff  ( s 
C_  ( Atoms `  k
)  /\  A. p  e.  s  A. q  e.  s  A. r  e.  ( Atoms `  k )
( r ( le
`  k ) ( p ( join `  k
) q )  -> 
r  e.  s ) )
2827, 4cab 2244 . . 3  class  { s  |  ( s  C_  ( Atoms `  k )  /\  A. p  e.  s 
A. q  e.  s 
A. r  e.  (
Atoms `  k ) ( r ( le `  k ) ( p ( join `  k
) q )  -> 
r  e.  s ) ) }
292, 3, 28cmpt 4051 . 2  class  ( k  e.  _V  |->  { s  |  ( s  C_  ( Atoms `  k )  /\  A. p  e.  s 
A. q  e.  s 
A. r  e.  (
Atoms `  k ) ( r ( le `  k ) ( p ( join `  k
) q )  -> 
r  e.  s ) ) } )
301, 29wceq 1619 1  wff  PSubSp  =  ( k  e.  _V  |->  { s  |  ( s 
C_  ( Atoms `  k
)  /\  A. p  e.  s  A. q  e.  s  A. r  e.  ( Atoms `  k )
( r ( le
`  k ) ( p ( join `  k
) q )  -> 
r  e.  s ) ) } )
Colors of variables: wff set class
This definition is referenced by:  psubspset  29183
  Copyright terms: Public domain W3C validator