Definition df-dib 36428

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 36427	. 2 class DIsoB
2		vk	. . 3 setvar k
3		cvv 3200	. . 3 class _V
4		vw	. . . 4 setvar w
5	2	cv 1482	. . . . 5 class k
6		clh 35270	. . . . 5 class LHyp
7	5, 6	cfv 5888	. . . 4 class ( LHyp ` k )
8		vx	. . . . 5 setvar x
9	4	cv 1482	. . . . . . 7 class w
10		cdia 36317	. . . . . . . 8 class DIsoA
11	5, 10	cfv 5888	. . . . . . 7 class ( DIsoA ` k )
12	9, 11	cfv 5888	. . . . . 6 class ( ( DIsoA ` k ) ` w )
13	12	cdm 5114	. . . . 5 class dom ( ( DIsoA ` k ) ` w )
14	8	cv 1482	. . . . . . 7 class x
15	14, 12	cfv 5888	. . . . . 6 class ( ( ( DIsoA ` k ) ` w ) ` x )
16		vf	. . . . . . . 8 setvar f
17		cltrn 35387	. . . . . . . . . 10 class LTrn
18	5, 17	cfv 5888	. . . . . . . . 9 class ( LTrn ` k )
19	9, 18	cfv 5888	. . . . . . . 8 class ( ( LTrn ` k ) ` w )
20		cid 5023	. . . . . . . . 9 class _I
21		cbs 15857	. . . . . . . . . 10 class Base
22	5, 21	cfv 5888	. . . . . . . . 9 class ( Base ` k )
23	20, 22	cres 5116	. . . . . . . 8 class ( _I |` ( Base ` k ) )
24	16, 19, 23	cmpt 4729	. . . . . . 7 class ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) )
25	24	csn 4177	. . . . . 6 class { ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) ) }
26	15, 25	cxp 5112	. . . . 5 class ( ( ( ( DIsoA ` k ) ` w ) ` x ) X. { ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) ) } )
27	8, 13, 26	cmpt 4729	. . . 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 4729	. . 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 4729	. 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 1483	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  36429