df-dpj

Description: Define the projection operator for a direct product. (Contributed by Mario Carneiro, 21-Apr-2016)

		Ref	Expression
	Assertion	df-dpj	$⊢ dProj = (g \in Grp, s \in dom DProd [\{g\}] ⟼ (i \in dom s ⟼ s (i) {proj}_{1} (g) (g DProd ({s ↾}_{(dom s ∖ \{i\})}))))$

Step	Hyp	Ref	Expression
0		cdpj	$class dProj$
1		vg	$setvar g$
2		cgrp	$class Grp$
3		vs	$setvar s$
4		cdprd	$class DProd$
5	4	cdm	$class dom DProd$
6	1	cv	$setvar g$
7	6	csn	$class \{g\}$
8	5 7	cima	$class dom DProd [\{g\}]$
9		vi	$setvar i$
10	3	cv	$setvar s$
11	10	cdm	$class dom s$
12	9	cv	$setvar i$
13	12 10	cfv	$class s (i)$
14		cpj1	$class {proj}_{1}$
15	6 14	cfv	$class {proj}_{1} (g)$
16	12	csn	$class \{i\}$
17	11 16	cdif	$class (dom s ∖ \{i\})$
18	10 17	cres	$class ({s ↾}_{(dom s ∖ \{i\})})$
19	6 18 4	co	$class (g DProd ({s ↾}_{(dom s ∖ \{i\})}))$
20	13 19 15	co	$class (s (i) {proj}_{1} (g) (g DProd ({s ↾}_{(dom s ∖ \{i\})})))$
21	9 11 20	cmpt	$class (i \in dom s ⟼ s (i) {proj}_{1} (g) (g DProd ({s ↾}_{(dom s ∖ \{i\})})))$
22	1 3 2 8 21	cmpo	$class (g \in Grp, s \in dom DProd [\{g\}] ⟼ (i \in dom s ⟼ s (i) {proj}_{1} (g) (g DProd ({s ↾}_{(dom s ∖ \{i\})}))))$
23	0 22	wceq	$wff dProj = (g \in Grp, s \in dom DProd [\{g\}] ⟼ (i \in dom s ⟼ s (i) {proj}_{1} (g) (g DProd ({s ↾}_{(dom s ∖ \{i\})}))))$

Metamath Proof Explorer