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

Definition df-dib 34880
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 34879 . 2  class  DIsoB
2 vk . . 3  setvar  k
3 cvv 2993 . . 3  class  _V
4 vw . . . 4  setvar  w
52cv 1368 . . . . 5  class  k
6 clh 33724 . . . . 5  class  LHyp
75, 6cfv 5439 . . . 4  class  ( LHyp `  k )
8 vx . . . . 5  setvar  x
94cv 1368 . . . . . . 7  class  w
10 cdia 34769 . . . . . . . 8  class  DIsoA
115, 10cfv 5439 . . . . . . 7  class  ( DIsoA `  k )
129, 11cfv 5439 . . . . . 6  class  ( (
DIsoA `  k ) `  w )
1312cdm 4861 . . . . 5  class  dom  (
( DIsoA `  k ) `  w )
148cv 1368 . . . . . . 7  class  x
1514, 12cfv 5439 . . . . . 6  class  ( ( ( DIsoA `  k ) `  w ) `  x
)
16 vf . . . . . . . 8  setvar  f
17 cltrn 33841 . . . . . . . . . 10  class  LTrn
185, 17cfv 5439 . . . . . . . . 9  class  ( LTrn `  k )
199, 18cfv 5439 . . . . . . . 8  class  ( (
LTrn `  k ) `  w )
20 cid 4652 . . . . . . . . 9  class  _I
21 cbs 14195 . . . . . . . . . 10  class  Base
225, 21cfv 5439 . . . . . . . . 9  class  ( Base `  k )
2320, 22cres 4863 . . . . . . . 8  class  (  _I  |`  ( Base `  k
) )
2416, 19, 23cmpt 4371 . . . . . . 7  class  ( f  e.  ( ( LTrn `  k ) `  w
)  |->  (  _I  |`  ( Base `  k ) ) )
2524csn 3898 . . . . . 6  class  { ( f  e.  ( (
LTrn `  k ) `  w )  |->  (  _I  |`  ( Base `  k
) ) ) }
2615, 25cxp 4859 . . . . 5  class  ( ( ( ( DIsoA `  k
) `  w ) `  x )  X.  {
( f  e.  ( ( LTrn `  k
) `  w )  |->  (  _I  |`  ( Base `  k ) ) ) } )
278, 13, 26cmpt 4371 . . . 4  class  ( x  e.  dom  ( (
DIsoA `  k ) `  w )  |->  ( ( ( ( DIsoA `  k
) `  w ) `  x )  X.  {
( f  e.  ( ( LTrn `  k
) `  w )  |->  (  _I  |`  ( Base `  k ) ) ) } ) )
284, 7, 27cmpt 4371 . . 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 4371 . 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 1369 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 setvar class
This definition is referenced by:  dibffval  34881
  Copyright terms: Public domain W3C validator