df-dpj

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

		Ref	Expression
	Assertion	df-dpj	⊢ dProj = ( 𝑔 ∈ Grp , 𝑠 ∈ ( dom DProd “ { 𝑔 } ) ↦ ( 𝑖 ∈ dom 𝑠 ↦ ( ( 𝑠 ‘ 𝑖 ) ( proj₁ ‘ 𝑔 ) ( 𝑔 DProd ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) ) ) ) )

Step	Hyp	Ref	Expression
0		cdpj	⊢ dProj
1		vg	⊢ 𝑔
2		cgrp	⊢ Grp
3		vs	⊢ 𝑠
4		cdprd	⊢ DProd
5	4	cdm	⊢ dom DProd
6	1	cv	⊢ 𝑔
7	6	csn	⊢ { 𝑔 }
8	5 7	cima	⊢ ( dom DProd “ { 𝑔 } )
9		vi	⊢ 𝑖
10	3	cv	⊢ 𝑠
11	10	cdm	⊢ dom 𝑠
12	9	cv	⊢ 𝑖
13	12 10	cfv	⊢ ( 𝑠 ‘ 𝑖 )
14		cpj1	⊢ proj₁
15	6 14	cfv	⊢ ( proj₁ ‘ 𝑔 )
16	12	csn	⊢ { 𝑖 }
17	11 16	cdif	⊢ ( dom 𝑠 ∖ { 𝑖 } )
18	10 17	cres	⊢ ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) )
19	6 18 4	co	⊢ ( 𝑔 DProd ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) )
20	13 19 15	co	⊢ ( ( 𝑠 ‘ 𝑖 ) ( proj₁ ‘ 𝑔 ) ( 𝑔 DProd ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) ) )
21	9 11 20	cmpt	⊢ ( 𝑖 ∈ dom 𝑠 ↦ ( ( 𝑠 ‘ 𝑖 ) ( proj₁ ‘ 𝑔 ) ( 𝑔 DProd ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) ) ) )
22	1 3 2 8 21	cmpo	⊢ ( 𝑔 ∈ Grp , 𝑠 ∈ ( dom DProd “ { 𝑔 } ) ↦ ( 𝑖 ∈ dom 𝑠 ↦ ( ( 𝑠 ‘ 𝑖 ) ( proj₁ ‘ 𝑔 ) ( 𝑔 DProd ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) ) ) ) )
23	0 22	wceq	⊢ dProj = ( 𝑔 ∈ Grp , 𝑠 ∈ ( dom DProd “ { 𝑔 } ) ↦ ( 𝑖 ∈ dom 𝑠 ↦ ( ( 𝑠 ‘ 𝑖 ) ( proj₁ ‘ 𝑔 ) ( 𝑔 DProd ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) ) ) ) )

Metamath Proof Explorer