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

Definition df-djh 31585
Description: Define (closed) subspace join for  DVecH vector space. (Contributed by NM, 19-Jul-2014.)
Assertion
Ref Expression
df-djh  |- joinH  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( x  e.  ~P ( Base `  ( ( DVecH `  k
) `  w )
) ,  y  e. 
~P ( Base `  (
( DVecH `  k ) `  w ) )  |->  ( ( ( ocH `  k
) `  w ) `  ( ( ( ( ocH `  k ) `
 w ) `  x )  i^i  (
( ( ocH `  k
) `  w ) `  y ) ) ) ) ) )
Distinct variable group:    w, k, x, y

Detailed syntax breakdown of Definition df-djh
StepHypRef Expression
1 cdjh 31584 . 2  class joinH
2 vk . . 3  set  k
3 cvv 2788 . . 3  class  _V
4 vw . . . 4  set  w
52cv 1622 . . . . 5  class  k
6 clh 30173 . . . . 5  class  LHyp
75, 6cfv 5255 . . . 4  class  ( LHyp `  k )
8 vx . . . . 5  set  x
9 vy . . . . 5  set  y
104cv 1622 . . . . . . . 8  class  w
11 cdvh 31268 . . . . . . . . 9  class  DVecH
125, 11cfv 5255 . . . . . . . 8  class  ( DVecH `  k )
1310, 12cfv 5255 . . . . . . 7  class  ( (
DVecH `  k ) `  w )
14 cbs 13148 . . . . . . 7  class  Base
1513, 14cfv 5255 . . . . . 6  class  ( Base `  ( ( DVecH `  k
) `  w )
)
1615cpw 3625 . . . . 5  class  ~P ( Base `  ( ( DVecH `  k ) `  w
) )
178cv 1622 . . . . . . . 8  class  x
18 coch 31537 . . . . . . . . . 10  class  ocH
195, 18cfv 5255 . . . . . . . . 9  class  ( ocH `  k )
2010, 19cfv 5255 . . . . . . . 8  class  ( ( ocH `  k ) `
 w )
2117, 20cfv 5255 . . . . . . 7  class  ( ( ( ocH `  k
) `  w ) `  x )
229cv 1622 . . . . . . . 8  class  y
2322, 20cfv 5255 . . . . . . 7  class  ( ( ( ocH `  k
) `  w ) `  y )
2421, 23cin 3151 . . . . . 6  class  ( ( ( ( ocH `  k
) `  w ) `  x )  i^i  (
( ( ocH `  k
) `  w ) `  y ) )
2524, 20cfv 5255 . . . . 5  class  ( ( ( ocH `  k
) `  w ) `  ( ( ( ( ocH `  k ) `
 w ) `  x )  i^i  (
( ( ocH `  k
) `  w ) `  y ) ) )
268, 9, 16, 16, 25cmpt2 5860 . . . 4  class  ( x  e.  ~P ( Base `  ( ( DVecH `  k
) `  w )
) ,  y  e. 
~P ( Base `  (
( DVecH `  k ) `  w ) )  |->  ( ( ( ocH `  k
) `  w ) `  ( ( ( ( ocH `  k ) `
 w ) `  x )  i^i  (
( ( ocH `  k
) `  w ) `  y ) ) ) )
274, 7, 26cmpt 4077 . . 3  class  ( w  e.  ( LHyp `  k
)  |->  ( x  e. 
~P ( Base `  (
( DVecH `  k ) `  w ) ) ,  y  e.  ~P ( Base `  ( ( DVecH `  k ) `  w
) )  |->  ( ( ( ocH `  k
) `  w ) `  ( ( ( ( ocH `  k ) `
 w ) `  x )  i^i  (
( ( ocH `  k
) `  w ) `  y ) ) ) ) )
282, 3, 27cmpt 4077 . 2  class  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k
)  |->  ( x  e. 
~P ( Base `  (
( DVecH `  k ) `  w ) ) ,  y  e.  ~P ( Base `  ( ( DVecH `  k ) `  w
) )  |->  ( ( ( ocH `  k
) `  w ) `  ( ( ( ( ocH `  k ) `
 w ) `  x )  i^i  (
( ( ocH `  k
) `  w ) `  y ) ) ) ) ) )
291, 28wceq 1623 1  wff joinH  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( x  e.  ~P ( Base `  ( ( DVecH `  k
) `  w )
) ,  y  e. 
~P ( Base `  (
( DVecH `  k ) `  w ) )  |->  ( ( ( ocH `  k
) `  w ) `  ( ( ( ( ocH `  k ) `
 w ) `  x )  i^i  (
( ( ocH `  k
) `  w ) `  y ) ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  djhffval  31586
  Copyright terms: Public domain W3C validator