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

Definition df-dih 31492
Description: Define isomorphism H. (Contributed by NM, 28-Jan-2014.)
Assertion
Ref Expression
df-dih  |-  DIsoH  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( x  e.  ( Base `  k
)  |->  if ( x ( le `  k
) w ,  ( ( ( DIsoB `  k
) `  w ) `  x ) ,  (
iota_ u  e.  ( LSubSp `
 ( ( DVecH `  k ) `  w
) ) A. q  e.  ( Atoms `  k )
( ( -.  q
( le `  k
) w  /\  (
q ( join `  k
) ( x (
meet `  k )
w ) )  =  x )  ->  u  =  ( ( ( ( DIsoC `  k ) `  w ) `  q
) ( LSSum `  (
( DVecH `  k ) `  w ) ) ( ( ( DIsoB `  k
) `  w ) `  ( x ( meet `  k ) w ) ) ) ) ) ) ) ) )
Distinct variable group:    k, q, w, u, x

Detailed syntax breakdown of Definition df-dih
StepHypRef Expression
1 cdih 31491 . 2  class  DIsoH
2 vk . . 3  set  k
3 cvv 2790 . . 3  class  _V
4 vw . . . 4  set  w
52cv 1624 . . . . 5  class  k
6 clh 30246 . . . . 5  class  LHyp
75, 6cfv 5257 . . . 4  class  ( LHyp `  k )
8 vx . . . . 5  set  x
9 cbs 13150 . . . . . 6  class  Base
105, 9cfv 5257 . . . . 5  class  ( Base `  k )
118cv 1624 . . . . . . 7  class  x
124cv 1624 . . . . . . 7  class  w
13 cple 13217 . . . . . . . 8  class  le
145, 13cfv 5257 . . . . . . 7  class  ( le
`  k )
1511, 12, 14wbr 4025 . . . . . 6  wff  x ( le `  k ) w
16 cdib 31401 . . . . . . . . 9  class  DIsoB
175, 16cfv 5257 . . . . . . . 8  class  ( DIsoB `  k )
1812, 17cfv 5257 . . . . . . 7  class  ( (
DIsoB `  k ) `  w )
1911, 18cfv 5257 . . . . . 6  class  ( ( ( DIsoB `  k ) `  w ) `  x
)
20 vq . . . . . . . . . . . . 13  set  q
2120cv 1624 . . . . . . . . . . . 12  class  q
2221, 12, 14wbr 4025 . . . . . . . . . . 11  wff  q ( le `  k ) w
2322wn 3 . . . . . . . . . 10  wff  -.  q
( le `  k
) w
24 cmee 14081 . . . . . . . . . . . . . 14  class  meet
255, 24cfv 5257 . . . . . . . . . . . . 13  class  ( meet `  k )
2611, 12, 25co 5860 . . . . . . . . . . . 12  class  ( x ( meet `  k
) w )
27 cjn 14080 . . . . . . . . . . . . 13  class  join
285, 27cfv 5257 . . . . . . . . . . . 12  class  ( join `  k )
2921, 26, 28co 5860 . . . . . . . . . . 11  class  ( q ( join `  k
) ( x (
meet `  k )
w ) )
3029, 11wceq 1625 . . . . . . . . . 10  wff  ( q ( join `  k
) ( x (
meet `  k )
w ) )  =  x
3123, 30wa 358 . . . . . . . . 9  wff  ( -.  q ( le `  k ) w  /\  ( q ( join `  k ) ( x ( meet `  k
) w ) )  =  x )
32 vu . . . . . . . . . . 11  set  u
3332cv 1624 . . . . . . . . . 10  class  u
34 cdic 31435 . . . . . . . . . . . . . 14  class  DIsoC
355, 34cfv 5257 . . . . . . . . . . . . 13  class  ( DIsoC `  k )
3612, 35cfv 5257 . . . . . . . . . . . 12  class  ( (
DIsoC `  k ) `  w )
3721, 36cfv 5257 . . . . . . . . . . 11  class  ( ( ( DIsoC `  k ) `  w ) `  q
)
3826, 18cfv 5257 . . . . . . . . . . 11  class  ( ( ( DIsoB `  k ) `  w ) `  (
x ( meet `  k
) w ) )
39 cdvh 31341 . . . . . . . . . . . . . 14  class  DVecH
405, 39cfv 5257 . . . . . . . . . . . . 13  class  ( DVecH `  k )
4112, 40cfv 5257 . . . . . . . . . . . 12  class  ( (
DVecH `  k ) `  w )
42 clsm 14947 . . . . . . . . . . . 12  class  LSSum
4341, 42cfv 5257 . . . . . . . . . . 11  class  ( LSSum `  ( ( DVecH `  k
) `  w )
)
4437, 38, 43co 5860 . . . . . . . . . 10  class  ( ( ( ( DIsoC `  k
) `  w ) `  q ) ( LSSum `  ( ( DVecH `  k
) `  w )
) ( ( (
DIsoB `  k ) `  w ) `  (
x ( meet `  k
) w ) ) )
4533, 44wceq 1625 . . . . . . . . 9  wff  u  =  ( ( ( (
DIsoC `  k ) `  w ) `  q
) ( LSSum `  (
( DVecH `  k ) `  w ) ) ( ( ( DIsoB `  k
) `  w ) `  ( x ( meet `  k ) w ) ) )
4631, 45wi 4 . . . . . . . 8  wff  ( ( -.  q ( le
`  k ) w  /\  ( q (
join `  k )
( x ( meet `  k ) w ) )  =  x )  ->  u  =  ( ( ( ( DIsoC `  k ) `  w
) `  q )
( LSSum `  ( ( DVecH `  k ) `  w ) ) ( ( ( DIsoB `  k
) `  w ) `  ( x ( meet `  k ) w ) ) ) )
47 catm 29526 . . . . . . . . 9  class  Atoms
485, 47cfv 5257 . . . . . . . 8  class  ( Atoms `  k )
4946, 20, 48wral 2545 . . . . . . 7  wff  A. q  e.  ( Atoms `  k )
( ( -.  q
( le `  k
) w  /\  (
q ( join `  k
) ( x (
meet `  k )
w ) )  =  x )  ->  u  =  ( ( ( ( DIsoC `  k ) `  w ) `  q
) ( LSSum `  (
( DVecH `  k ) `  w ) ) ( ( ( DIsoB `  k
) `  w ) `  ( x ( meet `  k ) w ) ) ) )
50 clss 15691 . . . . . . . 8  class  LSubSp
5141, 50cfv 5257 . . . . . . 7  class  ( LSubSp `  ( ( DVecH `  k
) `  w )
)
5249, 32, 51crio 6299 . . . . . 6  class  ( iota_ u  e.  ( LSubSp `  (
( DVecH `  k ) `  w ) ) A. q  e.  ( Atoms `  k ) ( ( -.  q ( le
`  k ) w  /\  ( q (
join `  k )
( x ( meet `  k ) w ) )  =  x )  ->  u  =  ( ( ( ( DIsoC `  k ) `  w
) `  q )
( LSSum `  ( ( DVecH `  k ) `  w ) ) ( ( ( DIsoB `  k
) `  w ) `  ( x ( meet `  k ) w ) ) ) ) )
5315, 19, 52cif 3567 . . . . 5  class  if ( x ( le `  k ) w ,  ( ( ( DIsoB `  k ) `  w
) `  x ) ,  ( iota_ u  e.  ( LSubSp `  ( ( DVecH `  k ) `  w ) ) A. q  e.  ( Atoms `  k ) ( ( -.  q ( le
`  k ) w  /\  ( q (
join `  k )
( x ( meet `  k ) w ) )  =  x )  ->  u  =  ( ( ( ( DIsoC `  k ) `  w
) `  q )
( LSSum `  ( ( DVecH `  k ) `  w ) ) ( ( ( DIsoB `  k
) `  w ) `  ( x ( meet `  k ) w ) ) ) ) ) )
548, 10, 53cmpt 4079 . . . 4  class  ( x  e.  ( Base `  k
)  |->  if ( x ( le `  k
) w ,  ( ( ( DIsoB `  k
) `  w ) `  x ) ,  (
iota_ u  e.  ( LSubSp `
 ( ( DVecH `  k ) `  w
) ) A. q  e.  ( Atoms `  k )
( ( -.  q
( le `  k
) w  /\  (
q ( join `  k
) ( x (
meet `  k )
w ) )  =  x )  ->  u  =  ( ( ( ( DIsoC `  k ) `  w ) `  q
) ( LSSum `  (
( DVecH `  k ) `  w ) ) ( ( ( DIsoB `  k
) `  w ) `  ( x ( meet `  k ) w ) ) ) ) ) ) )
554, 7, 54cmpt 4079 . . 3  class  ( w  e.  ( LHyp `  k
)  |->  ( x  e.  ( Base `  k
)  |->  if ( x ( le `  k
) w ,  ( ( ( DIsoB `  k
) `  w ) `  x ) ,  (
iota_ u  e.  ( LSubSp `
 ( ( DVecH `  k ) `  w
) ) A. q  e.  ( Atoms `  k )
( ( -.  q
( le `  k
) w  /\  (
q ( join `  k
) ( x (
meet `  k )
w ) )  =  x )  ->  u  =  ( ( ( ( DIsoC `  k ) `  w ) `  q
) ( LSSum `  (
( DVecH `  k ) `  w ) ) ( ( ( DIsoB `  k
) `  w ) `  ( x ( meet `  k ) w ) ) ) ) ) ) ) )
562, 3, 55cmpt 4079 . 2  class  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k
)  |->  ( x  e.  ( Base `  k
)  |->  if ( x ( le `  k
) w ,  ( ( ( DIsoB `  k
) `  w ) `  x ) ,  (
iota_ u  e.  ( LSubSp `
 ( ( DVecH `  k ) `  w
) ) A. q  e.  ( Atoms `  k )
( ( -.  q
( le `  k
) w  /\  (
q ( join `  k
) ( x (
meet `  k )
w ) )  =  x )  ->  u  =  ( ( ( ( DIsoC `  k ) `  w ) `  q
) ( LSSum `  (
( DVecH `  k ) `  w ) ) ( ( ( DIsoB `  k
) `  w ) `  ( x ( meet `  k ) w ) ) ) ) ) ) ) ) )
571, 56wceq 1625 1  wff  DIsoH  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( x  e.  ( Base `  k
)  |->  if ( x ( le `  k
) w ,  ( ( ( DIsoB `  k
) `  w ) `  x ) ,  (
iota_ u  e.  ( LSubSp `
 ( ( DVecH `  k ) `  w
) ) A. q  e.  ( Atoms `  k )
( ( -.  q
( le `  k
) w  /\  (
q ( join `  k
) ( x (
meet `  k )
w ) )  =  x )  ->  u  =  ( ( ( ( DIsoC `  k ) `  w ) `  q
) ( LSSum `  (
( DVecH `  k ) `  w ) ) ( ( ( DIsoB `  k
) `  w ) `  ( x ( meet `  k ) w ) ) ) ) ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  dihffval  31493
  Copyright terms: Public domain W3C validator