Metamath Proof Explorer

Definition df-dib

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)

Ref Expression
Assertion 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 ) ) ) } ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdib 
 |-  DIsoB
1 vk 
 |-  k
2 cvv 
 |-  _V
3 vw 
 |-  w
4 clh 
 |-  LHyp
5 1 cv 
 |-  k
6 5 4 cfv 
 |-  ( LHyp ` k )
7 vx 
 |-  x
8 cdia 
 |-  DIsoA
9 5 8 cfv 
 |-  ( DIsoA ` k )
10 3 cv 
 |-  w
11 10 9 cfv 
 |-  ( ( DIsoA ` k ) ` w )
12 11 cdm 
 |-  dom ( ( DIsoA ` k ) ` w )
13 7 cv 
 |-  x
14 13 11 cfv 
 |-  ( ( ( DIsoA ` k ) ` w ) ` x )
15 vf 
 |-  f
16 cltrn 
 |-  LTrn
17 5 16 cfv 
 |-  ( LTrn ` k )
18 10 17 cfv 
 |-  ( ( LTrn ` k ) ` w )
19 cid 
 |-  _I
20 cbs 
 |-  Base
21 5 20 cfv 
 |-  ( Base ` k )
22 19 21 cres 
 |-  ( _I |` ( Base ` k ) )
23 15 18 22 cmpt 
 |-  ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) )
24 23 csn 
 |-  { ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) ) }
25 14 24 cxp 
 |-  ( ( ( ( DIsoA ` k ) ` w ) ` x ) X. { ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) ) } )
26 7 12 25 cmpt 
 |-  ( x e. dom ( ( DIsoA ` k ) ` w ) |-> ( ( ( ( DIsoA ` k ) ` w ) ` x ) X. { ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) ) } ) )
27 3 6 26 cmpt 
 |-  ( w e. ( LHyp ` k ) |-> ( x e. dom ( ( DIsoA ` k ) ` w ) |-> ( ( ( ( DIsoA ` k ) ` w ) ` x ) X. { ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) ) } ) ) )
28 1 2 27 cmpt 
 |-  ( 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 ) ) ) } ) ) ) )
29 0 28 wceq 
 |-  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 ) ) ) } ) ) ) )