Definition df-dib 34752

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 34751	. 2 class DIsoB
2		vk	. . 3 setvar k
3		cvv 3057	. . 3 class _V
4		vw	. . . 4 setvar w
5	2	cv 1454	. . . . 5 class k
6		clh 33594	. . . . 5 class LHyp
7	5, 6	cfv 5601	. . . 4 class ( LHyp ` k )
8		vx	. . . . 5 setvar x
9	4	cv 1454	. . . . . . 7 class w
10		cdia 34641	. . . . . . . 8 class DIsoA
11	5, 10	cfv 5601	. . . . . . 7 class ( DIsoA ` k )
12	9, 11	cfv 5601	. . . . . 6 class ( ( DIsoA ` k ) ` w )
13	12	cdm 4853	. . . . 5 class dom ( ( DIsoA ` k ) ` w )
14	8	cv 1454	. . . . . . 7 class x
15	14, 12	cfv 5601	. . . . . 6 class ( ( ( DIsoA ` k ) ` w ) ` x )
16		vf	. . . . . . . 8 setvar f
17		cltrn 33711	. . . . . . . . . 10 class LTrn
18	5, 17	cfv 5601	. . . . . . . . 9 class ( LTrn ` k )
19	9, 18	cfv 5601	. . . . . . . 8 class ( ( LTrn ` k ) ` w )
20		cid 4763	. . . . . . . . 9 class _I
21		cbs 15170	. . . . . . . . . 10 class Base
22	5, 21	cfv 5601	. . . . . . . . 9 class ( Base ` k )
23	20, 22	cres 4855	. . . . . . . 8 class ( _I |` ( Base ` k ) )
24	16, 19, 23	cmpt 4475	. . . . . . 7 class ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) )
25	24	csn 3980	. . . . . 6 class { ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) ) }
26	15, 25	cxp 4851	. . . . 5 class ( ( ( ( DIsoA ` k ) ` w ) ` x ) X. { ( f e. ( ( LTrn ` k ) ` w ) |-> ( _I |` ( Base ` k ) ) ) } )
27	8, 13, 26	cmpt 4475	. . . 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 4475	. . 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 4475	. 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 1455	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  34753