Definition df-dpj 20017

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

Step	Hyp	Ref	Expression
1		cdpj 20015	. 2 class dProj
2		vg	. . 3 setvar 𝑔
3		vs	. . 3 setvar 𝑠
4		cgrp 18952	. . 3 class Grp
5		cdprd 20014	. . . . 5 class DProd
6	5	cdm 5684	. . . 4 class dom DProd
7	2	cv 1538	. . . . 5 class 𝑔
8	7	csn 4625	. . . 4 class {𝑔}
9	6, 8	cima 5687	. . 3 class (dom DProd “ {𝑔})
10		vi	. . . 4 setvar 𝑖
11	3	cv 1538	. . . . 5 class 𝑠
12	11	cdm 5684	. . . 4 class dom 𝑠
13	10	cv 1538	. . . . . 6 class 𝑖
14	13, 11	cfv 6560	. . . . 5 class (𝑠‘𝑖)
15	13	csn 4625	. . . . . . . 8 class {𝑖}
16	12, 15	cdif 3947	. . . . . . 7 class (dom 𝑠 ∖ {𝑖})
17	11, 16	cres 5686	. . . . . 6 class (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))
18	7, 17, 5	co 7432	. . . . 5 class (𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖})))
19		cpj1 19654	. . . . . 6 class proj1
20	7, 19	cfv 6560	. . . . 5 class (proj1‘𝑔)
21	14, 18, 20	co 7432	. . . 4 class ((𝑠‘𝑖)(proj1‘𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))))
22	10, 12, 21	cmpt 5224	. . 3 class (𝑖 ∈ dom 𝑠 ↦ ((𝑠‘𝑖)(proj1‘𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖})))))
23	2, 3, 4, 9, 22	cmpo 7434	. 2 class (𝑔 ∈ Grp, 𝑠 ∈ (dom DProd “ {𝑔}) ↦ (𝑖 ∈ dom 𝑠 ↦ ((𝑠‘𝑖)(proj1‘𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))))))
24	1, 23	wceq 1539	1 wff dProj = (𝑔 ∈ Grp, 𝑠 ∈ (dom DProd “ {𝑔}) ↦ (𝑖 ∈ dom 𝑠 ↦ ((𝑠‘𝑖)(proj1‘𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖}))))))

This definition is referenced by:  dpjfval  20076