Metamath Proof Explorer

Definition 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 ∈ Grp , s ∈ dom ⁡ DProd g ⟼ i ∈ dom ⁡ s ⟼ s ⁡ i proj 1 ⁡ g g DProd s ↾ dom ⁡ s ∖ i

Detailed syntax breakdown

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 ∈ dom ⁡ s ⟼ s ⁡ i proj 1 ⁡ g g DProd s ↾ dom ⁡ s ∖ i
22 1 3 2 8 21 cmpo class g ∈ Grp , s ∈ dom ⁡ DProd g ⟼ i ∈ dom ⁡ s ⟼ s ⁡ i proj 1 ⁡ g g DProd s ↾ dom ⁡ s ∖ i
23 0 22 wceq wff dProj = g ∈ Grp , s ∈ dom ⁡ DProd g ⟼ i ∈ dom ⁡ s ⟼ s ⁡ i proj 1 ⁡ g g DProd s ↾ dom ⁡ s ∖ i