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	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
	dpjfval.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
	dpjfval.p	⊢ 𝑃 = ( 𝐺 dProj 𝑆 )
	dpjfval.q	⊢ 𝑄 = ( proj1 ‘ 𝐺 )
Assertion	dpjfval	⊢ ( 𝜑 → 𝑃 = ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑆 ‘ 𝑖 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑖 } ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dpjfval.1	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2		dpjfval.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3		dpjfval.p	⊢ 𝑃 = ( 𝐺 dProj 𝑆 )
4		dpjfval.q	⊢ 𝑄 = ( proj1 ‘ 𝐺 )
5		df-dpj	⊢ dProj = ( 𝑔 ∈ Grp , 𝑠 ∈ ( dom DProd “ { 𝑔 } ) ↦ ( 𝑖 ∈ dom 𝑠 ↦ ( ( 𝑠 ‘ 𝑖 ) ( proj1 ‘ 𝑔 ) ( 𝑔 DProd ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) ) ) ) )
6	5	a1i	⊢ ( 𝜑 → dProj = ( 𝑔 ∈ Grp , 𝑠 ∈ ( dom DProd “ { 𝑔 } ) ↦ ( 𝑖 ∈ dom 𝑠 ↦ ( ( 𝑠 ‘ 𝑖 ) ( proj1 ‘ 𝑔 ) ( 𝑔 DProd ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) ) ) ) ) )
7		simprr	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → 𝑠 = 𝑆 )
8	7	dmeqd	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → dom 𝑠 = dom 𝑆 )
9	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → dom 𝑆 = 𝐼 )
10	8 9	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → dom 𝑠 = 𝐼 )
11		simprl	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → 𝑔 = 𝐺 )
12	11	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → ( proj1 ‘ 𝑔 ) = ( proj1 ‘ 𝐺 ) )
13	12 4	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → ( proj1 ‘ 𝑔 ) = 𝑄 )
14	7	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → ( 𝑠 ‘ 𝑖 ) = ( 𝑆 ‘ 𝑖 ) )
15	10	difeq1d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → ( dom 𝑠 ∖ { 𝑖 } ) = ( 𝐼 ∖ { 𝑖 } ) )
16	7 15	reseq12d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) = ( 𝑆 ↾ ( 𝐼 ∖ { 𝑖 } ) ) )
17	11 16	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → ( 𝑔 DProd ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) ) = ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑖 } ) ) ) )
18	13 14 17	oveq123d	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → ( ( 𝑠 ‘ 𝑖 ) ( proj1 ‘ 𝑔 ) ( 𝑔 DProd ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) ) ) = ( ( 𝑆 ‘ 𝑖 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑖 } ) ) ) ) )
19	10 18	mpteq12dv	⊢ ( ( 𝜑 ∧ ( 𝑔 = 𝐺 ∧ 𝑠 = 𝑆 ) ) → ( 𝑖 ∈ dom 𝑠 ↦ ( ( 𝑠 ‘ 𝑖 ) ( proj1 ‘ 𝑔 ) ( 𝑔 DProd ( 𝑠 ↾ ( dom 𝑠 ∖ { 𝑖 } ) ) ) ) ) = ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑆 ‘ 𝑖 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑖 } ) ) ) ) ) )
20		simpr	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
21	20	sneqd	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → { 𝑔 } = { 𝐺 } )
22	21	imaeq2d	⊢ ( ( 𝜑 ∧ 𝑔 = 𝐺 ) → ( dom DProd “ { 𝑔 } ) = ( dom DProd “ { 𝐺 } ) )
23		dprdgrp	⊢ ( 𝐺 dom DProd 𝑆 → 𝐺 ∈ Grp )
24	1 23	syl	⊢ ( 𝜑 → 𝐺 ∈ Grp )
25		reldmdprd	⊢ Rel dom DProd
26		elrelimasn	⊢ ( Rel dom DProd → ( 𝑆 ∈ ( dom DProd “ { 𝐺 } ) ↔ 𝐺 dom DProd 𝑆 ) )
27	25 26	ax-mp	⊢ ( 𝑆 ∈ ( dom DProd “ { 𝐺 } ) ↔ 𝐺 dom DProd 𝑆 )
28	1 27	sylibr	⊢ ( 𝜑 → 𝑆 ∈ ( dom DProd “ { 𝐺 } ) )
29	1 2	dprddomcld	⊢ ( 𝜑 → 𝐼 ∈ V )
30	29	mptexd	⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑆 ‘ 𝑖 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑖 } ) ) ) ) ) ∈ V )
31	6 19 22 24 28 30	ovmpodx	⊢ ( 𝜑 → ( 𝐺 dProj 𝑆 ) = ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑆 ‘ 𝑖 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑖 } ) ) ) ) ) )
32	3 31	syl5eq	⊢ ( 𝜑 → 𝑃 = ( 𝑖 ∈ 𝐼 ↦ ( ( 𝑆 ‘ 𝑖 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑖 } ) ) ) ) ) )