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	|- ( ph -> G dom DProd S )
	dpjfval.2	|- ( ph -> dom S = I )
	dpjfval.p	|- P = ( G dProj S )
	dpjfval.q	|- Q = ( proj1 ` G )
	dpjval.3	|- ( ph -> X e. I )
Assertion	dpjval	|- ( ph -> ( P ` X ) = ( ( S ` X ) Q ( G DProd ( S |` ( I \ { X } ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dpjfval.1	|- ( ph -> G dom DProd S )
2		dpjfval.2	|- ( ph -> dom S = I )
3		dpjfval.p	|- P = ( G dProj S )
4		dpjfval.q	|- Q = ( proj1 ` G )
5		dpjval.3	|- ( ph -> X e. I )
6	1 2 3 4	dpjfval	|- ( ph -> P = ( x e. I |-> ( ( S ` x ) Q ( G DProd ( S |` ( I \ { x } ) ) ) ) ) )
7		simpr	|- ( ( ph /\ x = X ) -> x = X )
8	7	fveq2d	|- ( ( ph /\ x = X ) -> ( S ` x ) = ( S ` X ) )
9	7	sneqd	|- ( ( ph /\ x = X ) -> { x } = { X } )
10	9	difeq2d	|- ( ( ph /\ x = X ) -> ( I \ { x } ) = ( I \ { X } ) )
11	10	reseq2d	|- ( ( ph /\ x = X ) -> ( S |` ( I \ { x } ) ) = ( S |` ( I \ { X } ) ) )
12	11	oveq2d	|- ( ( ph /\ x = X ) -> ( G DProd ( S |` ( I \ { x } ) ) ) = ( G DProd ( S |` ( I \ { X } ) ) ) )
13	8 12	oveq12d	|- ( ( ph /\ x = X ) -> ( ( S ` x ) Q ( G DProd ( S |` ( I \ { x } ) ) ) ) = ( ( S ` X ) Q ( G DProd ( S |` ( I \ { X } ) ) ) ) )
14		ovexd	|- ( ph -> ( ( S ` X ) Q ( G DProd ( S |` ( I \ { X } ) ) ) ) e. _V )
15	6 13 5 14	fvmptd	|- ( ph -> ( P ` X ) = ( ( S ` X ) Q ( G DProd ( S |` ( I \ { X } ) ) ) ) )