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