This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } ) ) ) ) ) )