This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } ) ) ) ) )