MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-dpj Unicode version

Definition df-dpj 15234
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 ) (
proj 1 `  g ) ( g DProd  ( s  |`  ( dom  s  \  { i } ) ) ) ) ) )
Distinct variable group:    g, i, s

Detailed syntax breakdown of Definition df-dpj
StepHypRef Expression
1 cdpj 15232 . 2  class dProj
2 vg . . 3  set  g
3 vs . . 3  set  s
4 cgrp 14362 . . 3  class  Grp
5 cdprd 15231 . . . . 5  class DProd
65cdm 4689 . . . 4  class  dom DProd
72cv 1622 . . . . 5  class  g
87csn 3640 . . . 4  class  { g }
96, 8cima 4692 . . 3  class  ( dom DProd  " { g } )
10 vi . . . 4  set  i
113cv 1622 . . . . 5  class  s
1211cdm 4689 . . . 4  class  dom  s
1310cv 1622 . . . . . 6  class  i
1413, 11cfv 5255 . . . . 5  class  ( s `
 i )
1513csn 3640 . . . . . . . 8  class  { i }
1612, 15cdif 3149 . . . . . . 7  class  ( dom  s  \  { i } )
1711, 16cres 4691 . . . . . 6  class  ( s  |`  ( dom  s  \  { i } ) )
187, 17, 5co 5858 . . . . 5  class  ( g DProd 
( s  |`  ( dom  s  \  { i } ) ) )
19 cpj1 14946 . . . . . 6  class  proj 1
207, 19cfv 5255 . . . . 5  class  ( proj
1 `  g )
2114, 18, 20co 5858 . . . 4  class  ( ( s `  i ) ( proj 1 `  g ) ( g DProd 
( s  |`  ( dom  s  \  { i } ) ) ) )
2210, 12, 21cmpt 4077 . . 3  class  ( i  e.  dom  s  |->  ( ( s `  i
) ( proj 1 `  g ) ( g DProd 
( s  |`  ( dom  s  \  { i } ) ) ) ) )
232, 3, 4, 9, 22cmpt2 5860 . 2  class  ( g  e.  Grp ,  s  e.  ( dom DProd  " {
g } )  |->  ( i  e.  dom  s  |->  ( ( s `  i ) ( proj
1 `  g )
( g DProd  ( s  |`  ( dom  s  \  { i } ) ) ) ) ) )
241, 23wceq 1623 1  wff dProj  =  ( g  e.  Grp , 
s  e.  ( dom DProd  " { g } ) 
|->  ( i  e.  dom  s  |->  ( ( s `
 i ) (
proj 1 `  g ) ( g DProd  ( s  |`  ( dom  s  \  { i } ) ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  dpjfval  15290
  Copyright terms: Public domain W3C validator