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

Definition df-dpj 17563
 Description: Define the projection operator for a direct product. (Contributed by Mario Carneiro, 21-Apr-2016.)
Assertion
Ref Expression
df-dpj dProj DProd DProd
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-dpj
StepHypRef Expression
1 cdpj 17561 . 2 dProj
2 vg . . 3
3 vs . . 3
4 cgrp 16620 . . 3
5 cdprd 17560 . . . . 5 DProd
65cdm 4854 . . . 4 DProd
72cv 1436 . . . . 5
87csn 4002 . . . 4
96, 8cima 4857 . . 3 DProd
10 vi . . . 4
113cv 1436 . . . . 5
1211cdm 4854 . . . 4
1310cv 1436 . . . . . 6
1413, 11cfv 5601 . . . . 5
1513csn 4002 . . . . . . . 8
1612, 15cdif 3439 . . . . . . 7
1711, 16cres 4856 . . . . . 6
187, 17, 5co 6305 . . . . 5 DProd
19 cpj1 17222 . . . . . 6
207, 19cfv 5601 . . . . 5
2114, 18, 20co 6305 . . . 4 DProd
2210, 12, 21cmpt 4484 . . 3 DProd
232, 3, 4, 9, 22cmpt2 6307 . 2 DProd DProd
241, 23wceq 1437 1 dProj DProd DProd
 Colors of variables: wff setvar class This definition is referenced by:  dpjfval  17623
 Copyright terms: Public domain W3C validator