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

Definition df-dpj 15498
 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 15496 . 2 dProj
2 vg . . 3
3 vs . . 3
4 cgrp 14626 . . 3
5 cdprd 15495 . . . . 5 DProd
65cdm 4832 . . . 4 DProd
72cv 1648 . . . . 5
87csn 3771 . . . 4
96, 8cima 4835 . . 3 DProd
10 vi . . . 4
113cv 1648 . . . . 5
1211cdm 4832 . . . 4
1310cv 1648 . . . . . 6
1413, 11cfv 5408 . . . . 5
1513csn 3771 . . . . . . . 8
1612, 15cdif 3274 . . . . . . 7
1711, 16cres 4834 . . . . . 6
187, 17, 5co 6034 . . . . 5 DProd
19 cpj1 15210 . . . . . 6
207, 19cfv 5408 . . . . 5
2114, 18, 20co 6034 . . . 4 DProd
2210, 12, 21cmpt 4221 . . 3 DProd
232, 3, 4, 9, 22cmpt2 6036 . 2 DProd DProd
241, 23wceq 1649 1 dProj DProd DProd
 Colors of variables: wff set class This definition is referenced by:  dpjfval  15554
 Copyright terms: Public domain W3C validator