Definition df-dpj

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

	Ref	Expression
Assertion	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 } ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdpj	|- dProj
1		vg	|- g
2		cgrp	|- Grp
3		vs	|- s
4		cdprd	|- DProd
5	4	cdm	|- dom DProd
6	1	cv	|- g
7	6	csn	|- { g }
8	5 7	cima	|- ( dom DProd " { g } )
9		vi	|- i
10	3	cv	|- s
11	10	cdm	|- dom s
12	9	cv	|- i
13	12 10	cfv	|- ( s ` i )
14		cpj1	|- proj1
15	6 14	cfv	|- ( proj1 ` g )
16	12	csn	|- { i }
17	11 16	cdif	|- ( dom s \ { i } )
18	10 17	cres	|- ( s |` ( dom s \ { i } ) )
19	6 18 4	co	|- ( g DProd ( s |` ( dom s \ { i } ) ) )
20	13 19 15	co	|- ( ( s ` i ) ( proj1 ` g ) ( g DProd ( s |` ( dom s \ { i } ) ) ) )
21	9 11 20	cmpt	|- ( i e. dom s |-> ( ( s ` i ) ( proj1 ` g ) ( g DProd ( s |` ( dom s \ { i } ) ) ) ) )
22	1 3 2 8 21	cmpo	|- ( g e. Grp , s e. ( dom DProd " { g } ) |-> ( i e. dom s |-> ( ( s ` i ) ( proj1 ` g ) ( g DProd ( s |` ( dom s \ { i } ) ) ) ) ) )
23	0 22	wceq	|- dProj = ( g e. Grp , s e. ( dom DProd " { g } ) |-> ( i e. dom s |-> ( ( s ` i ) ( proj1 ` g ) ( g DProd ( s |` ( dom s \ { i } ) ) ) ) ) )