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 = ( 𝑔 ∈ Grp , 𝑠 ∈ ( dom DProd “ { 𝑔 } ) ↦ ( 𝑖 ∈ dom 𝑠 ↦ ( ( 𝑠𝑖 ) ( proj1𝑔 ) ( 𝑔 DProd ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) ) ) ) )

Detailed syntax breakdown

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 proj1
15 6 14 cfv ( proj1𝑔 )
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 ( ( 𝑠𝑖 ) ( proj1𝑔 ) ( 𝑔 DProd ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) ) )
21 9 11 20 cmpt ( 𝑖 ∈ dom 𝑠 ↦ ( ( 𝑠𝑖 ) ( proj1𝑔 ) ( 𝑔 DProd ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) ) ) )
22 1 3 2 8 21 cmpo ( 𝑔 ∈ Grp , 𝑠 ∈ ( dom DProd “ { 𝑔 } ) ↦ ( 𝑖 ∈ dom 𝑠 ↦ ( ( 𝑠𝑖 ) ( proj1𝑔 ) ( 𝑔 DProd ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) ) ) ) )
23 0 22 wceq dProj = ( 𝑔 ∈ Grp , 𝑠 ∈ ( dom DProd “ { 𝑔 } ) ↦ ( 𝑖 ∈ dom 𝑠 ↦ ( ( 𝑠𝑖 ) ( proj1𝑔 ) ( 𝑔 DProd ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) ) ) ) )