Metamath Proof Explorer


Theorem fimaproj

Description: Image of a cartesian product for 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=xA,yBFxGy
fimaproj.f φFFnA
fimaproj.g φGFnB
fimaproj.x φXA
fimaproj.y φYB
Assertion fimaproj φHX×Y=FX×GY

Proof

Step Hyp Ref Expression
1 fvproj.h H=xA,yBFxGy
2 fimaproj.f φFFnA
3 fimaproj.g φGFnB
4 fimaproj.x φXA
5 fimaproj.y φYB
6 opex F1stzG2ndzV
7 vex xV
8 vex yV
9 7 8 op1std z=xy1stz=x
10 9 fveq2d z=xyF1stz=Fx
11 7 8 op2ndd z=xy2ndz=y
12 11 fveq2d z=xyG2ndz=Gy
13 10 12 opeq12d z=xyF1stzG2ndz=FxGy
14 13 mpompt zA×BF1stzG2ndz=xA,yBFxGy
15 1 14 eqtr4i H=zA×BF1stzG2ndz
16 6 15 fnmpti HFnA×B
17 xpss12 XAYBX×YA×B
18 4 5 17 syl2anc φX×YA×B
19 fvelimab HFnA×BX×YA×BcHX×YzX×YHz=c
20 16 18 19 sylancr φcHX×YzX×YHz=c
21 simp-4r φcFX×GYaXFa=1stcbYGb=2ndcaX
22 simplr φcFX×GYaXFa=1stcbYGb=2ndcbY
23 opelxpi aXbYabX×Y
24 21 22 23 syl2anc φcFX×GYaXFa=1stcbYGb=2ndcabX×Y
25 simpllr φcFX×GYaXFa=1stcbYGb=2ndcFa=1stc
26 simpr φcFX×GYaXFa=1stcbYGb=2ndcGb=2ndc
27 25 26 opeq12d φcFX×GYaXFa=1stcbYGb=2ndcFaGb=1stc2ndc
28 4 ad5antr φcFX×GYaXFa=1stcbYGb=2ndcXA
29 28 21 sseldd φcFX×GYaXFa=1stcbYGb=2ndcaA
30 5 ad5antr φcFX×GYaXFa=1stcbYGb=2ndcYB
31 30 22 sseldd φcFX×GYaXFa=1stcbYGb=2ndcbB
32 1 29 31 fvproj φcFX×GYaXFa=1stcbYGb=2ndcHab=FaGb
33 1st2nd2 cFX×GYc=1stc2ndc
34 33 ad5antlr φcFX×GYaXFa=1stcbYGb=2ndcc=1stc2ndc
35 27 32 34 3eqtr4d φcFX×GYaXFa=1stcbYGb=2ndcHab=c
36 fveqeq2 z=abHz=cHab=c
37 36 rspcev abX×YHab=czX×YHz=c
38 24 35 37 syl2anc φcFX×GYaXFa=1stcbYGb=2ndczX×YHz=c
39 3 ad3antrrr φcFX×GYaXFa=1stcGFnB
40 fnfun GFnBFunG
41 39 40 syl φcFX×GYaXFa=1stcFunG
42 xp2nd cFX×GY2ndcGY
43 42 ad3antlr φcFX×GYaXFa=1stc2ndcGY
44 fvelima FunG2ndcGYbYGb=2ndc
45 41 43 44 syl2anc φcFX×GYaXFa=1stcbYGb=2ndc
46 38 45 r19.29a φcFX×GYaXFa=1stczX×YHz=c
47 2 adantr φcFX×GYFFnA
48 fnfun FFnAFunF
49 47 48 syl φcFX×GYFunF
50 xp1st cFX×GY1stcFX
51 50 adantl φcFX×GY1stcFX
52 fvelima FunF1stcFXaXFa=1stc
53 49 51 52 syl2anc φcFX×GYaXFa=1stc
54 46 53 r19.29a φcFX×GYzX×YHz=c
55 simpr φzX×YHz=cHz=c
56 18 ad2antrr φzX×YHz=cX×YA×B
57 simplr φzX×YHz=czX×Y
58 56 57 sseldd φzX×YHz=czA×B
59 15 fvmpt2 zA×BF1stzG2ndzVHz=F1stzG2ndz
60 58 6 59 sylancl φzX×YHz=cHz=F1stzG2ndz
61 2 ad2antrr φzX×YHz=cFFnA
62 4 ad2antrr φzX×YHz=cXA
63 xp1st zX×Y1stzX
64 57 63 syl φzX×YHz=c1stzX
65 fnfvima FFnAXA1stzXF1stzFX
66 61 62 64 65 syl3anc φzX×YHz=cF1stzFX
67 3 ad2antrr φzX×YHz=cGFnB
68 5 ad2antrr φzX×YHz=cYB
69 xp2nd zX×Y2ndzY
70 57 69 syl φzX×YHz=c2ndzY
71 fnfvima GFnBYB2ndzYG2ndzGY
72 67 68 70 71 syl3anc φzX×YHz=cG2ndzGY
73 opelxpi F1stzFXG2ndzGYF1stzG2ndzFX×GY
74 66 72 73 syl2anc φzX×YHz=cF1stzG2ndzFX×GY
75 60 74 eqeltrd φzX×YHz=cHzFX×GY
76 55 75 eqeltrrd φzX×YHz=ccFX×GY
77 76 r19.29an φzX×YHz=ccFX×GY
78 54 77 impbida φcFX×GYzX×YHz=c
79 20 78 bitr4d φcHX×YcFX×GY
80 79 eqrdv φHX×Y=FX×GY