Metamath Proof Explorer


Theorem dpjfval

Description: Value of the direct product projection (defined in terms of binary projection). (Contributed by Mario Carneiro, 26-Apr-2016)

Ref Expression
Hypotheses dpjfval.1 φ G dom DProd S
dpjfval.2 φ dom S = I
dpjfval.p P = G dProj S
dpjfval.q Q = proj 1 G
Assertion dpjfval φ P = i I S i Q G DProd S I i

Proof

Step Hyp Ref Expression
1 dpjfval.1 φ G dom DProd S
2 dpjfval.2 φ dom S = I
3 dpjfval.p P = G dProj S
4 dpjfval.q Q = proj 1 G
5 df-dpj dProj = g Grp , s dom DProd g i dom s s i proj 1 g g DProd s dom s i
6 5 a1i φ dProj = g Grp , s dom DProd g i dom s s i proj 1 g g DProd s dom s i
7 simprr φ g = G s = S s = S
8 7 dmeqd φ g = G s = S dom s = dom S
9 2 adantr φ g = G s = S dom S = I
10 8 9 eqtrd φ g = G s = S dom s = I
11 simprl φ g = G s = S g = G
12 11 fveq2d φ g = G s = S proj 1 g = proj 1 G
13 12 4 eqtr4di φ g = G s = S proj 1 g = Q
14 7 fveq1d φ g = G s = S s i = S i
15 10 difeq1d φ g = G s = S dom s i = I i
16 7 15 reseq12d φ g = G s = S s dom s i = S I i
17 11 16 oveq12d φ g = G s = S g DProd s dom s i = G DProd S I i
18 13 14 17 oveq123d φ g = G s = S s i proj 1 g g DProd s dom s i = S i Q G DProd S I i
19 10 18 mpteq12dv φ g = G s = S i dom s s i proj 1 g g DProd s dom s i = i I S i Q G DProd S I i
20 simpr φ g = G g = G
21 20 sneqd φ g = G g = G
22 21 imaeq2d φ g = G dom DProd g = dom DProd G
23 dprdgrp G dom DProd S G Grp
24 1 23 syl φ G Grp
25 reldmdprd Rel dom DProd
26 elrelimasn Rel dom DProd S dom DProd G G dom DProd S
27 25 26 ax-mp S dom DProd G G dom DProd S
28 1 27 sylibr φ S dom DProd G
29 1 2 dprddomcld φ I V
30 29 mptexd φ i I S i Q G DProd S I i V
31 6 19 22 24 28 30 ovmpodx φ G dProj S = i I S i Q G DProd S I i
32 3 31 syl5eq φ P = i I S i Q G DProd S I i