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 19047
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 19045 . 2 class dProj
2 vg . . 3 setvar 𝑔
3 vs . . 3 setvar 𝑠
4 cgrp 18041 . . 3 class Grp
5 cdprd 19044 . . . . 5 class DProd
65cdm 5548 . . . 4 class dom DProd
72cv 1527 . . . . 5 class 𝑔
87csn 4557 . . . 4 class {𝑔}
96, 8cima 5551 . . 3 class (dom DProd “ {𝑔})
10 vi . . . 4 setvar 𝑖
113cv 1527 . . . . 5 class 𝑠
1211cdm 5548 . . . 4 class dom 𝑠
1310cv 1527 . . . . . 6 class 𝑖
1413, 11cfv 6348 . . . . 5 class (𝑠𝑖)
1513csn 4557 . . . . . . . 8 class {𝑖}
1612, 15cdif 3930 . . . . . . 7 class (dom 𝑠 ∖ {𝑖})
1711, 16cres 5550 . . . . . 6 class (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))
187, 17, 5co 7145 . . . . 5 class (𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖})))
19 cpj1 18689 . . . . . 6 class proj1
207, 19cfv 6348 . . . . 5 class (proj1𝑔)
2114, 18, 20co 7145 . . . 4 class ((𝑠𝑖)(proj1𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))))
2210, 12, 21cmpt 5137 . . 3 class (𝑖 ∈ dom 𝑠 ↦ ((𝑠𝑖)(proj1𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖})))))
232, 3, 4, 9, 22cmpo 7147 . 2 class (𝑔 ∈ Grp, 𝑠 ∈ (dom DProd “ {𝑔}) ↦ (𝑖 ∈ dom 𝑠 ↦ ((𝑠𝑖)(proj1𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))))))
241, 23wceq 1528 1 wff dProj = (𝑔 ∈ Grp, 𝑠 ∈ (dom DProd “ {𝑔}) ↦ (𝑖 ∈ dom 𝑠 ↦ ((𝑠𝑖)(proj1𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))))))
Colors of variables: wff setvar class
This definition is referenced by:  dpjfval  19106
  Copyright terms: Public domain W3C validator