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

Definition df-dpj 18218
Description: Define the projection operator for a direct product. (Contributed by Mario Carneiro, 21-Apr-2016.)
Assertion
Ref Expression
df-dpj dProj = (𝑔 ∈ Grp, 𝑠 ∈ (dom DProd “ {𝑔}) ↦ (𝑖 ∈ dom 𝑠 ↦ ((𝑠𝑖)(proj1𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))))))
Distinct variable group:   𝑔,𝑖,𝑠

Detailed syntax breakdown of Definition df-dpj
StepHypRef Expression
1 cdpj 18216 . 2 class dProj
2 vg . . 3 setvar 𝑔
3 vs . . 3 setvar 𝑠
4 cgrp 17245 . . 3 class Grp
5 cdprd 18215 . . . . 5 class DProd
65cdm 5038 . . . 4 class dom DProd
72cv 1474 . . . . 5 class 𝑔
87csn 4125 . . . 4 class {𝑔}
96, 8cima 5041 . . 3 class (dom DProd “ {𝑔})
10 vi . . . 4 setvar 𝑖
113cv 1474 . . . . 5 class 𝑠
1211cdm 5038 . . . 4 class dom 𝑠
1310cv 1474 . . . . . 6 class 𝑖
1413, 11cfv 5804 . . . . 5 class (𝑠𝑖)
1513csn 4125 . . . . . . . 8 class {𝑖}
1612, 15cdif 3537 . . . . . . 7 class (dom 𝑠 ∖ {𝑖})
1711, 16cres 5040 . . . . . 6 class (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))
187, 17, 5co 6549 . . . . 5 class (𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖})))
19 cpj1 17873 . . . . . 6 class proj1
207, 19cfv 5804 . . . . 5 class (proj1𝑔)
2114, 18, 20co 6549 . . . 4 class ((𝑠𝑖)(proj1𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))))
2210, 12, 21cmpt 4643 . . 3 class (𝑖 ∈ dom 𝑠 ↦ ((𝑠𝑖)(proj1𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖})))))
232, 3, 4, 9, 22cmpt2 6551 . 2 class (𝑔 ∈ Grp, 𝑠 ∈ (dom DProd “ {𝑔}) ↦ (𝑖 ∈ dom 𝑠 ↦ ((𝑠𝑖)(proj1𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))))))
241, 23wceq 1475 1 wff dProj = (𝑔 ∈ Grp, 𝑠 ∈ (dom DProd “ {𝑔}) ↦ (𝑖 ∈ dom 𝑠 ↦ ((𝑠𝑖)(proj1𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))))))
Colors of variables: wff setvar class
This definition is referenced by:  dpjfval  18277
  Copyright terms: Public domain W3C validator