Theorem dpjval

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 ‘ 𝐺 )
	dpjval.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
Assertion	dpjval	⊢ ( 𝜑 → ( 𝑃 ‘ 𝑋 ) = ( ( 𝑆 ‘ 𝑋 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dpjfval.1	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
2		dpjfval.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
3		dpjfval.p	⊢ 𝑃 = ( 𝐺 dProj 𝑆 )
4		dpjfval.q	⊢ 𝑄 = ( proj1 ‘ 𝐺 )
5		dpjval.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
6	1 2 3 4	dpjfval	⊢ ( 𝜑 → 𝑃 = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑆 ‘ 𝑥 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) ) )
7		simpr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
8	7	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑋 ) )
9	7	sneqd	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → { 𝑥 } = { 𝑋 } )
10	9	difeq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝐼 ∖ { 𝑥 } ) = ( 𝐼 ∖ { 𝑋 } ) )
11	10	reseq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) = ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) )
12	11	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) = ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) )
13	8 12	oveq12d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 𝑆 ‘ 𝑥 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑥 } ) ) ) ) = ( ( 𝑆 ‘ 𝑋 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) )
14		ovexd	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) ∈ V )
15	6 13 5 14	fvmptd	⊢ ( 𝜑 → ( 𝑃 ‘ 𝑋 ) = ( ( 𝑆 ‘ 𝑋 ) 𝑄 ( 𝐺 DProd ( 𝑆 ↾ ( 𝐼 ∖ { 𝑋 } ) ) ) ) )