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

Definition df-dpj 19109
 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 19107 . 2 class dProj
2 vg . . 3 setvar 𝑔
3 vs . . 3 setvar 𝑠
4 cgrp 18094 . . 3 class Grp
5 cdprd 19106 . . . . 5 class DProd
65cdm 5532 . . . 4 class dom DProd
72cv 1537 . . . . 5 class 𝑔
87csn 4539 . . . 4 class {𝑔}
96, 8cima 5535 . . 3 class (dom DProd “ {𝑔})
10 vi . . . 4 setvar 𝑖
113cv 1537 . . . . 5 class 𝑠
1211cdm 5532 . . . 4 class dom 𝑠
1310cv 1537 . . . . . 6 class 𝑖
1413, 11cfv 6334 . . . . 5 class (𝑠𝑖)
1513csn 4539 . . . . . . . 8 class {𝑖}
1612, 15cdif 3905 . . . . . . 7 class (dom 𝑠 ∖ {𝑖})
1711, 16cres 5534 . . . . . 6 class (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))
187, 17, 5co 7140 . . . . 5 class (𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖})))
19 cpj1 18751 . . . . . 6 class proj1
207, 19cfv 6334 . . . . 5 class (proj1𝑔)
2114, 18, 20co 7140 . . . 4 class ((𝑠𝑖)(proj1𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))))
2210, 12, 21cmpt 5122 . . 3 class (𝑖 ∈ dom 𝑠 ↦ ((𝑠𝑖)(proj1𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖})))))
232, 3, 4, 9, 22cmpo 7142 . 2 class (𝑔 ∈ Grp, 𝑠 ∈ (dom DProd “ {𝑔}) ↦ (𝑖 ∈ dom 𝑠 ↦ ((𝑠𝑖)(proj1𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))))))
241, 23wceq 1538 1 wff dProj = (𝑔 ∈ Grp, 𝑠 ∈ (dom DProd “ {𝑔}) ↦ (𝑖 ∈ dom 𝑠 ↦ ((𝑠𝑖)(proj1𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))))))
 Colors of variables: wff setvar class This definition is referenced by:  dpjfval  19168
 Copyright terms: Public domain W3C validator