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 18609
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 18607 . 2 class dProj
2 vg . . 3 setvar 𝑔
3 vs . . 3 setvar 𝑠
4 cgrp 17636 . . 3 class Grp
5 cdprd 18606 . . . . 5 class DProd
65cdm 5248 . . . 4 class dom DProd
72cv 1628 . . . . 5 class 𝑔
87csn 4313 . . . 4 class {𝑔}
96, 8cima 5251 . . 3 class (dom DProd “ {𝑔})
10 vi . . . 4 setvar 𝑖
113cv 1628 . . . . 5 class 𝑠
1211cdm 5248 . . . 4 class dom 𝑠
1310cv 1628 . . . . . 6 class 𝑖
1413, 11cfv 6030 . . . . 5 class (𝑠𝑖)
1513csn 4313 . . . . . . . 8 class {𝑖}
1612, 15cdif 3717 . . . . . . 7 class (dom 𝑠 ∖ {𝑖})
1711, 16cres 5250 . . . . . 6 class (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))
187, 17, 5co 6791 . . . . 5 class (𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖})))
19 cpj1 18263 . . . . . 6 class proj1
207, 19cfv 6030 . . . . 5 class (proj1𝑔)
2114, 18, 20co 6791 . . . 4 class ((𝑠𝑖)(proj1𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))))
2210, 12, 21cmpt 4860 . . 3 class (𝑖 ∈ dom 𝑠 ↦ ((𝑠𝑖)(proj1𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖})))))
232, 3, 4, 9, 22cmpt2 6793 . 2 class (𝑔 ∈ Grp, 𝑠 ∈ (dom DProd “ {𝑔}) ↦ (𝑖 ∈ dom 𝑠 ↦ ((𝑠𝑖)(proj1𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))))))
241, 23wceq 1629 1 wff dProj = (𝑔 ∈ Grp, 𝑠 ∈ (dom DProd “ {𝑔}) ↦ (𝑖 ∈ dom 𝑠 ↦ ((𝑠𝑖)(proj1𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))))))
Colors of variables: wff setvar class
This definition is referenced by:  dpjfval  18668
  Copyright terms: Public domain W3C validator