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	$⊢ φ \to G dom DProd S$
	dpjfval.2	$⊢ φ \to dom S = I$
	dpjfval.p	$⊢ P = G dProj S$
	dpjfval.q	$⊢ Q = {proj}_{1} (G)$
Assertion	dpjfval	$⊢ φ \to P = (i \in I ⟼ S (i) Q (G DProd ({S ↾}_{(I ∖ \{i\})})))$

Proof

Step	Hyp	Ref	Expression
1		dpjfval.1	$⊢ φ \to G dom DProd S$
2		dpjfval.2	$⊢ φ \to dom S = I$
3		dpjfval.p	$⊢ P = G dProj S$
4		dpjfval.q	$⊢ Q = {proj}_{1} (G)$
5		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\})}))))$
6	5	a1i	$⊢ φ \to dProj = (g \in Grp, s \in dom DProd [\{g\}] ⟼ (i \in dom s ⟼ s (i) {proj}_{1} (g) (g DProd ({s ↾}_{(dom s ∖ \{i\})}))))$
7		simprr	$⊢ (φ \land (g = G \land s = S)) \to s = S$
8	7	dmeqd	$⊢ (φ \land (g = G \land s = S)) \to dom s = dom S$
9	2	adantr	$⊢ (φ \land (g = G \land s = S)) \to dom S = I$
10	8 9	eqtrd	$⊢ (φ \land (g = G \land s = S)) \to dom s = I$
11		simprl	$⊢ (φ \land (g = G \land s = S)) \to g = G$
12	11	fveq2d	$⊢ (φ \land (g = G \land s = S)) \to {proj}_{1} (g) = {proj}_{1} (G)$
13	12 4	eqtr4di	$⊢ (φ \land (g = G \land s = S)) \to {proj}_{1} (g) = Q$
14	7	fveq1d	$⊢ (φ \land (g = G \land s = S)) \to s (i) = S (i)$
15	10	difeq1d	$⊢ (φ \land (g = G \land s = S)) \to dom s ∖ \{i\} = I ∖ \{i\}$
16	7 15	reseq12d	$⊢ (φ \land (g = G \land s = S)) \to {s ↾}_{(dom s ∖ \{i\})} = {S ↾}_{(I ∖ \{i\})}$
17	11 16	oveq12d	$⊢ (φ \land (g = G \land s = S)) \to g DProd ({s ↾}_{(dom s ∖ \{i\})}) = G DProd ({S ↾}_{(I ∖ \{i\})})$
18	13 14 17	oveq123d	$⊢ (φ \land (g = G \land s = S)) \to s (i) {proj}_{1} (g) (g DProd ({s ↾}_{(dom s ∖ \{i\})})) = S (i) Q (G DProd ({S ↾}_{(I ∖ \{i\})}))$
19	10 18	mpteq12dv	$⊢ (φ \land (g = G \land s = S)) \to (i \in dom s ⟼ s (i) {proj}_{1} (g) (g DProd ({s ↾}_{(dom s ∖ \{i\})}))) = (i \in I ⟼ S (i) Q (G DProd ({S ↾}_{(I ∖ \{i\})})))$
20		simpr	$⊢ (φ \land g = G) \to g = G$
21	20	sneqd	$⊢ (φ \land g = G) \to \{g\} = \{G\}$
22	21	imaeq2d	$⊢ (φ \land g = G) \to dom DProd [\{g\}] = dom DProd [\{G\}]$
23		dprdgrp	$⊢ G dom DProd S \to G \in Grp$
24	1 23	syl	$⊢ φ \to G \in Grp$
25		reldmdprd	$⊢ Rel dom DProd$
26		elrelimasn	$⊢ Rel dom DProd \to (S \in dom DProd [\{G\}] \leftrightarrow G dom DProd S)$
27	25 26	ax-mp	$⊢ S \in dom DProd [\{G\}] \leftrightarrow G dom DProd S$
28	1 27	sylibr	$⊢ φ \to S \in dom DProd [\{G\}]$
29	1 2	dprddomcld	$⊢ φ \to I \in V$
30	29	mptexd	$⊢ φ \to (i \in I ⟼ S (i) Q (G DProd ({S ↾}_{(I ∖ \{i\})}))) \in V$
31	6 19 22 24 28 30	ovmpodx	$⊢ φ \to G dProj S = (i \in I ⟼ S (i) Q (G DProd ({S ↾}_{(I ∖ \{i\})})))$
32	3 31	syl5eq	$⊢ φ \to P = (i \in I ⟼ S (i) Q (G DProd ({S ↾}_{(I ∖ \{i\})})))$

Metamath Proof Explorer

Theorem dpjfval

Proof