Definition df-dpj 18395

Description: Define the projection operator for a direct product. (Contributed by Mario Carneiro, 21-Apr-2016.)

Assertion

Ref	Expression
df-dpj	|- dProj = ( g e. Grp , s e. ( dom DProd " { g } ) |-> ( i e. dom s |-> ( ( s ` i ) ( proj1 ` g ) ( g DProd ( s |` ( dom s \ { i } ) ) ) ) ) )

Distinct variable group:   g, i, s

Detailed syntax breakdown of Definition df-dpj

Step	Hyp	Ref	Expression
1		cdpj 18393	. 2 class dProj
2		vg	. . 3 setvar g
3		vs	. . 3 setvar s
4		cgrp 17422	. . 3 class Grp
5		cdprd 18392	. . . . 5 class DProd
6	5	cdm 5114	. . . 4 class dom DProd
7	2	cv 1482	. . . . 5 class g
8	7	csn 4177	. . . 4 class { g }
9	6, 8	cima 5117	. . 3 class ( dom DProd " { g } )
10		vi	. . . 4 setvar i
11	3	cv 1482	. . . . 5 class s
12	11	cdm 5114	. . . 4 class dom s
13	10	cv 1482	. . . . . 6 class i
14	13, 11	cfv 5888	. . . . 5 class ( s ` i )
15	13	csn 4177	. . . . . . . 8 class { i }
16	12, 15	cdif 3571	. . . . . . 7 class ( dom s \ { i } )
17	11, 16	cres 5116	. . . . . 6 class ( s |` ( dom s \ { i } ) )
18	7, 17, 5	co 6650	. . . . 5 class ( g DProd ( s |` ( dom s \ { i } ) ) )
19		cpj1 18050	. . . . . 6 class proj1
20	7, 19	cfv 5888	. . . . 5 class ( proj1 ` g )
21	14, 18, 20	co 6650	. . . 4 class ( ( s ` i ) ( proj1 ` g ) ( g DProd ( s |` ( dom s \ { i } ) ) ) )
22	10, 12, 21	cmpt 4729	. . 3 class ( i e. dom s |-> ( ( s ` i ) ( proj1 ` g ) ( g DProd ( s |` ( dom s \ { i } ) ) ) ) )
23	2, 3, 4, 9, 22	cmpt2 6652	. 2 class ( g e. Grp , s e. ( dom DProd " { g } ) |-> ( i e. dom s |-> ( ( s ` i ) ( proj1 ` g ) ( g DProd ( s |` ( dom s \ { i } ) ) ) ) ) )
24	1, 23	wceq 1483	1 wff dProj = ( g e. Grp , s e. ( dom DProd " { g } ) |-> ( i e. dom s |-> ( ( s ` i ) ( proj1 ` g ) ( g DProd ( s |` ( dom s \ { i } ) ) ) ) ) )

This definition is referenced by:  dpjfval  18454