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

Definition df-dib 31329
Description: Isomorphism B is isomorphism A extended with an extra dimension set to the zero vector component i.e. the zero endormorphism. Its domain is lattice elements less than or equal to the fiducial co-atom  w. (Contributed by NM, 8-Dec-2013.)
Assertion
Ref Expression
df-dib  |-  DIsoB  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( x  e.  dom  ( (
DIsoA `  k ) `  w )  |->  ( ( ( ( DIsoA `  k
) `  w ) `  x )  X.  {
( f  e.  ( ( LTrn `  k
) `  w )  |->  (  _I  |`  ( Base `  k ) ) ) } ) ) ) )
Distinct variable group:    w, k, x, f

Detailed syntax breakdown of Definition df-dib
StepHypRef Expression
1 cdib 31328 . 2  class  DIsoB
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
94cv 1622 . . . . . . 7  class  w
10 cdia 31218 . . . . . . . 8  class  DIsoA
115, 10cfv 5255 . . . . . . 7  class  ( DIsoA `  k )
129, 11cfv 5255 . . . . . 6  class  ( (
DIsoA `  k ) `  w )
1312cdm 4689 . . . . 5  class  dom  (
( DIsoA `  k ) `  w )
148cv 1622 . . . . . . 7  class  x
1514, 12cfv 5255 . . . . . 6  class  ( ( ( DIsoA `  k ) `  w ) `  x
)
16 vf . . . . . . . 8  set  f
17 cltrn 30290 . . . . . . . . . 10  class  LTrn
185, 17cfv 5255 . . . . . . . . 9  class  ( LTrn `  k )
199, 18cfv 5255 . . . . . . . 8  class  ( (
LTrn `  k ) `  w )
20 cid 4304 . . . . . . . . 9  class  _I
21 cbs 13148 . . . . . . . . . 10  class  Base
225, 21cfv 5255 . . . . . . . . 9  class  ( Base `  k )
2320, 22cres 4691 . . . . . . . 8  class  (  _I  |`  ( Base `  k
) )
2416, 19, 23cmpt 4077 . . . . . . 7  class  ( f  e.  ( ( LTrn `  k ) `  w
)  |->  (  _I  |`  ( Base `  k ) ) )
2524csn 3640 . . . . . 6  class  { ( f  e.  ( (
LTrn `  k ) `  w )  |->  (  _I  |`  ( Base `  k
) ) ) }
2615, 25cxp 4687 . . . . 5  class  ( ( ( ( DIsoA `  k
) `  w ) `  x )  X.  {
( f  e.  ( ( LTrn `  k
) `  w )  |->  (  _I  |`  ( Base `  k ) ) ) } )
278, 13, 26cmpt 4077 . . . 4  class  ( x  e.  dom  ( (
DIsoA `  k ) `  w )  |->  ( ( ( ( DIsoA `  k
) `  w ) `  x )  X.  {
( f  e.  ( ( LTrn `  k
) `  w )  |->  (  _I  |`  ( Base `  k ) ) ) } ) )
284, 7, 27cmpt 4077 . . 3  class  ( w  e.  ( LHyp `  k
)  |->  ( x  e. 
dom  ( ( DIsoA `  k ) `  w
)  |->  ( ( ( ( DIsoA `  k ) `  w ) `  x
)  X.  { ( f  e.  ( (
LTrn `  k ) `  w )  |->  (  _I  |`  ( Base `  k
) ) ) } ) ) )
292, 3, 28cmpt 4077 . 2  class  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k
)  |->  ( x  e. 
dom  ( ( DIsoA `  k ) `  w
)  |->  ( ( ( ( DIsoA `  k ) `  w ) `  x
)  X.  { ( f  e.  ( (
LTrn `  k ) `  w )  |->  (  _I  |`  ( Base `  k
) ) ) } ) ) ) )
301, 29wceq 1623 1  wff  DIsoB  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( x  e.  dom  ( (
DIsoA `  k ) `  w )  |->  ( ( ( ( DIsoA `  k
) `  w ) `  x )  X.  {
( f  e.  ( ( LTrn `  k
) `  w )  |->  (  _I  |`  ( Base `  k ) ) ) } ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  dibffval  31330
  Copyright terms: Public domain W3C validator