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 A , y B F x G y
fvproj.x φ X A
fvproj.y φ Y B
Assertion fvproj φ H X Y = F X G Y

Proof

Step Hyp Ref Expression
1 fvproj.h H = x A , y B F x G y
2 fvproj.x φ X A
3 fvproj.y φ Y 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 A , y B F x G y = a A , b B F a G b
14 1 13 eqtri H = a A , b B F a G b
15 opex F X G Y V
16 6 8 14 15 ovmpo X A Y B X H Y = F X G Y
17 2 3 16 syl2anc φ X H Y = F X G Y
18 4 17 eqtr3id φ H X Y = F X G Y