Definition df-dib 35954

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

Step	Hyp	Ref	Expression
1		cdib 35953	. 2 class DIsoB
2		vk	. . 3 setvar k
3		cvv 3113	. . 3 class _V
4		vw	. . . 4 setvar w
5	2	cv 1378	. . . . 5 class k
6		clh 34798	. . . . 5 class LHyp
7	5, 6	cfv 5588	. . . 4 class ( LHyp ` k )
8		vx	. . . . 5 setvar x
9	4	cv 1378	. . . . . . 7 class w
10		cdia 35843	. . . . . . . 8 class DIsoA
11	5, 10	cfv 5588	. . . . . . 7 class ( DIsoA ` k )
12	9, 11	cfv 5588	. . . . . 6 class ( ( DIsoA ` k ) ` w )
13	12	cdm 4999	. . . . 5 class dom ( ( DIsoA ` k ) ` w )
14	8	cv 1378	. . . . . . 7 class x
15	14, 12	cfv 5588	. . . . . 6 class ( ( ( DIsoA ` k ) ` w ) ` x )
16		vf	. . . . . . . 8 setvar f
17		cltrn 34915	. . . . . . . . . 10 class LTrn
18	5, 17	cfv 5588	. . . . . . . . 9 class ( LTrn ` k )
19	9, 18	cfv 5588	. . . . . . . 8 class ( ( LTrn ` k ) ` w )
20		cid 4790	. . . . . . . . 9 class _I
21		cbs 14490	. . . . . . . . . 10 class Base
22	5, 21	cfv 5588	. . . . . . . . 9 class ( Base ` k )
23	20, 22	cres 5001	. . . . . . . 8 class ( _I |` ( Base ` k ) )
24	16, 19, 23	cmpt 4505	. . . . . . 7 class ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) )
25	24	csn 4027	. . . . . 6 class { ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) ) }
26	15, 25	cxp 4997	. . . . 5 class ( ( ( ( DIsoA ` k ) ` w ) ` x ) X. { ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) ) } )
27	8, 13, 26	cmpt 4505	. . . 4 class ( x e. dom ( ( DIsoA ` k ) ` w ) |-> ( ( ( ( DIsoA ` k ) ` w ) ` x ) X. { ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) ) } ) )
28	4, 7, 27	cmpt 4505	. . 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 ) ) ) } ) ) )
29	2, 3, 28	cmpt 4505	. 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 ) ) ) } ) ) ) )
30	1, 29	wceq 1379	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 ) ) ) } ) ) ) )

This definition is referenced by:  dibffval  35955