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

Metamath Proof Explorer

Theorem fvproj

Description: Value of a function on ordered pairs with values expressed as ordered pairs. Note that F and G are the projections of H to the first and second coordinate respectively. (Contributed by Thierry Arnoux, 30-Dec-2019)

Ref Expression
Hypotheses fvproj.h 
|- H = ( x e. A , y e. B |-> <. ( F ` x ) , ( G ` y ) >. )
fvproj.x 
|- ( ph -> X e. A )
fvproj.y 
|- ( ph -> Y e. B )
Assertion fvproj 
|- ( ph -> ( H ` <. X , Y >. ) = <. ( F ` X ) , ( G ` Y ) >. )

Proof

Step Hyp Ref Expression
1 fvproj.h 
 |-  H = ( x e. A , y e. B |-> <. ( F ` x ) , ( G ` y ) >. )
2 fvproj.x 
 |-  ( ph -> X e. A )
3 fvproj.y 
 |-  ( ph -> Y e. B )
4 df-ov 
 |-  ( X H Y ) = ( H ` <. X , Y >. )
5 fveq2 
 |-  ( a = X -> ( F ` a ) = ( F ` X ) )
6 5 opeq1d 
 |-  ( a = X -> <. ( F ` a ) , ( G ` b ) >. = <. ( F ` X ) , ( G ` b ) >. )
7 fveq2 
 |-  ( b = Y -> ( G ` b ) = ( G ` Y ) )
8 7 opeq2d 
 |-  ( b = Y -> <. ( F ` X ) , ( G ` b ) >. = <. ( F ` X ) , ( G ` Y ) >. )
9 fveq2 
 |-  ( x = a -> ( F ` x ) = ( F ` a ) )
10 9 opeq1d 
 |-  ( x = a -> <. ( F ` x ) , ( G ` y ) >. = <. ( F ` a ) , ( G ` y ) >. )
11 fveq2 
 |-  ( y = b -> ( G ` y ) = ( G ` b ) )
12 11 opeq2d 
 |-  ( y = b -> <. ( F ` a ) , ( G ` y ) >. = <. ( F ` a ) , ( G ` b ) >. )
13 10 12 cbvmpov 
 |-  ( x e. A , y e. B |-> <. ( F ` x ) , ( G ` y ) >. ) = ( a e. A , b e. B |-> <. ( F ` a ) , ( G ` b ) >. )
14 1 13 eqtri 
 |-  H = ( a e. A , b e. B |-> <. ( F ` a ) , ( G ` b ) >. )
15 opex 
 |-  <. ( F ` X ) , ( G ` Y ) >. e. _V
16 6 8 14 15 ovmpo 
 |-  ( ( X e. A /\ Y e. B ) -> ( X H Y ) = <. ( F ` X ) , ( G ` Y ) >. )
17 2 3 16 syl2anc 
 |-  ( ph -> ( X H Y ) = <. ( F ` X ) , ( G ` Y ) >. )
18 4 17 eqtr3id 
 |-  ( ph -> ( H ` <. X , Y >. ) = <. ( F ` X ) , ( G ` Y ) >. )