Definition df-tendo 36043

Description: Define trace-preserving endomorphisms on the set of translations. (Contributed by NM, 8-Jun-2013.)

Assertion

Ref	Expression
df-tendo	|- TEndo = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { f | ( f : ( ( LTrn ` k ) ` w ) --> ( ( LTrn ` k ) ` w ) /\ A. x e. ( ( LTrn ` k ) ` w ) A. y e. ( ( LTrn ` k ) ` w ) ( f ` ( x o. y ) ) = ( ( f ` x ) o. ( f ` y ) ) /\ A. x e. ( ( LTrn ` k ) ` w ) ( ( ( trL ` k ) ` w ) ` ( f ` x ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` x ) ) } ) )

Distinct variable group:   w, k, f, x, y

Detailed syntax breakdown of Definition df-tendo

Step	Hyp	Ref	Expression
1		ctendo 36040	. 2 class TEndo
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	4	cv 1482	. . . . . . . 8 class w
9		cltrn 35387	. . . . . . . . 9 class LTrn
10	5, 9	cfv 5888	. . . . . . . 8 class ( LTrn ` k )
11	8, 10	cfv 5888	. . . . . . 7 class ( ( LTrn ` k ) ` w )
12		vf	. . . . . . . 8 setvar f
13	12	cv 1482	. . . . . . 7 class f
14	11, 11, 13	wf 5884	. . . . . 6 wff f : ( ( LTrn ` k ) ` w ) --> ( ( LTrn ` k ) ` w )
15		vx	. . . . . . . . . . . 12 setvar x
16	15	cv 1482	. . . . . . . . . . 11 class x
17		vy	. . . . . . . . . . . 12 setvar y
18	17	cv 1482	. . . . . . . . . . 11 class y
19	16, 18	ccom 5118	. . . . . . . . . 10 class ( x o. y )
20	19, 13	cfv 5888	. . . . . . . . 9 class ( f ` ( x o. y ) )
21	16, 13	cfv 5888	. . . . . . . . . 10 class ( f ` x )
22	18, 13	cfv 5888	. . . . . . . . . 10 class ( f ` y )
23	21, 22	ccom 5118	. . . . . . . . 9 class ( ( f ` x ) o. ( f ` y ) )
24	20, 23	wceq 1483	. . . . . . . 8 wff ( f ` ( x o. y ) ) = ( ( f ` x ) o. ( f ` y ) )
25	24, 17, 11	wral 2912	. . . . . . 7 wff A. y e. ( ( LTrn ` k ) ` w ) ( f ` ( x o. y ) ) = ( ( f ` x ) o. ( f ` y ) )
26	25, 15, 11	wral 2912	. . . . . 6 wff A. x e. ( ( LTrn ` k ) ` w ) A. y e. ( ( LTrn ` k ) ` w ) ( f ` ( x o. y ) ) = ( ( f ` x ) o. ( f ` y ) )
27		ctrl 35445	. . . . . . . . . . 11 class trL
28	5, 27	cfv 5888	. . . . . . . . . 10 class ( trL ` k )
29	8, 28	cfv 5888	. . . . . . . . 9 class ( ( trL ` k ) ` w )
30	21, 29	cfv 5888	. . . . . . . 8 class ( ( ( trL ` k ) ` w ) ` ( f ` x ) )
31	16, 29	cfv 5888	. . . . . . . 8 class ( ( ( trL ` k ) ` w ) ` x )
32		cple 15948	. . . . . . . . 9 class le
33	5, 32	cfv 5888	. . . . . . . 8 class ( le ` k )
34	30, 31, 33	wbr 4653	. . . . . . 7 wff ( ( ( trL ` k ) ` w ) ` ( f ` x ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` x )
35	34, 15, 11	wral 2912	. . . . . 6 wff A. x e. ( ( LTrn ` k ) ` w ) ( ( ( trL ` k ) ` w ) ` ( f ` x ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` x )
36	14, 26, 35	w3a 1037	. . . . 5 wff ( f : ( ( LTrn ` k ) ` w ) --> ( ( LTrn ` k ) ` w ) /\ A. x e. ( ( LTrn ` k ) ` w ) A. y e. ( ( LTrn ` k ) ` w ) ( f ` ( x o. y ) ) = ( ( f ` x ) o. ( f ` y ) ) /\ A. x e. ( ( LTrn ` k ) ` w ) ( ( ( trL ` k ) ` w ) ` ( f ` x ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` x ) )
37	36, 12	cab 2608	. . . 4 class { f | ( f : ( ( LTrn ` k ) ` w ) --> ( ( LTrn ` k ) ` w ) /\ A. x e. ( ( LTrn ` k ) ` w ) A. y e. ( ( LTrn ` k ) ` w ) ( f ` ( x o. y ) ) = ( ( f ` x ) o. ( f ` y ) ) /\ A. x e. ( ( LTrn ` k ) ` w ) ( ( ( trL ` k ) ` w ) ` ( f ` x ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` x ) ) }
38	4, 7, 37	cmpt 4729	. . 3 class ( w e. ( LHyp ` k ) |-> { f | ( f : ( ( LTrn ` k ) ` w ) --> ( ( LTrn ` k ) ` w ) /\ A. x e. ( ( LTrn ` k ) ` w ) A. y e. ( ( LTrn ` k ) ` w ) ( f ` ( x o. y ) ) = ( ( f ` x ) o. ( f ` y ) ) /\ A. x e. ( ( LTrn ` k ) ` w ) ( ( ( trL ` k ) ` w ) ` ( f ` x ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` x ) ) } )
39	2, 3, 38	cmpt 4729	. 2 class ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { f | ( f : ( ( LTrn ` k ) ` w ) --> ( ( LTrn ` k ) ` w ) /\ A. x e. ( ( LTrn ` k ) ` w ) A. y e. ( ( LTrn ` k ) ` w ) ( f ` ( x o. y ) ) = ( ( f ` x ) o. ( f ` y ) ) /\ A. x e. ( ( LTrn ` k ) ` w ) ( ( ( trL ` k ) ` w ) ` ( f ` x ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` x ) ) } ) )
40	1, 39	wceq 1483	1 wff TEndo = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { f | ( f : ( ( LTrn ` k ) ` w ) --> ( ( LTrn ` k ) ` w ) /\ A. x e. ( ( LTrn ` k ) ` w ) A. y e. ( ( LTrn ` k ) ` w ) ( f ` ( x o. y ) ) = ( ( f ` x ) o. ( f ` y ) ) /\ A. x e. ( ( LTrn ` k ) ` w ) ( ( ( trL ` k ) ` w ) ` ( f ` x ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` x ) ) } ) )

This definition is referenced by:  tendofset  36046