Metamath Proof Explorer


Theorem 2ffzoeq

Description: Two functions over a half-open range of nonnegative integers are equal if and only if their domains have the same length and the function values are the same at each position. (Contributed by Alexander van der Vekens, 1-Jul-2018)

Ref Expression
Assertion 2ffzoeq M 0 N 0 F : 0 ..^ M X P : 0 ..^ N Y F = P M = N i 0 ..^ M F i = P i

Proof

Step Hyp Ref Expression
1 eqeq1 F = P F = P =
2 1 anbi1d F = P F = P : 0 ..^ N Y P = P : 0 ..^ N Y
3 f0bi P : Y P =
4 ffn P : 0 ..^ N Y P Fn 0 ..^ N
5 ffn P : Y P Fn
6 fndmu P Fn 0 ..^ N P Fn 0 ..^ N =
7 0z 0
8 nn0z N 0 N
9 8 adantl M 0 N 0 N
10 fzon 0 N N 0 0 ..^ N =
11 7 9 10 sylancr M 0 N 0 N 0 0 ..^ N =
12 nn0ge0 N 0 0 N
13 0red N 0 0
14 nn0re N 0 N
15 13 14 letri3d N 0 0 = N 0 N N 0
16 15 biimprd N 0 0 N N 0 0 = N
17 12 16 mpand N 0 N 0 0 = N
18 17 adantl M 0 N 0 N 0 0 = N
19 11 18 sylbird M 0 N 0 0 ..^ N = 0 = N
20 6 19 syl5com P Fn 0 ..^ N P Fn M 0 N 0 0 = N
21 20 ex P Fn 0 ..^ N P Fn M 0 N 0 0 = N
22 4 5 21 syl2imc P : Y P : 0 ..^ N Y M 0 N 0 0 = N
23 3 22 sylbir P = P : 0 ..^ N Y M 0 N 0 0 = N
24 23 imp P = P : 0 ..^ N Y M 0 N 0 0 = N
25 2 24 syl6bi F = P F = P : 0 ..^ N Y M 0 N 0 0 = N
26 25 com3l F = P : 0 ..^ N Y M 0 N 0 F = P 0 = N
27 26 a1i M = 0 F = P : 0 ..^ N Y M 0 N 0 F = P 0 = N
28 oveq2 M = 0 0 ..^ M = 0 ..^ 0
29 fzo0 0 ..^ 0 =
30 28 29 eqtrdi M = 0 0 ..^ M =
31 30 feq2d M = 0 F : 0 ..^ M X F : X
32 f0bi F : X F =
33 31 32 bitrdi M = 0 F : 0 ..^ M X F =
34 33 anbi1d M = 0 F : 0 ..^ M X P : 0 ..^ N Y F = P : 0 ..^ N Y
35 eqeq1 M = 0 M = N 0 = N
36 35 imbi2d M = 0 F = P M = N F = P 0 = N
37 36 imbi2d M = 0 M 0 N 0 F = P M = N M 0 N 0 F = P 0 = N
38 27 34 37 3imtr4d M = 0 F : 0 ..^ M X P : 0 ..^ N Y M 0 N 0 F = P M = N
39 38 com3l F : 0 ..^ M X P : 0 ..^ N Y M 0 N 0 M = 0 F = P M = N
40 39 impcom M 0 N 0 F : 0 ..^ M X P : 0 ..^ N Y M = 0 F = P M = N
41 40 impcom M = 0 M 0 N 0 F : 0 ..^ M X P : 0 ..^ N Y F = P M = N
42 28 feq2d M = 0 F : 0 ..^ M X F : 0 ..^ 0 X
43 29 feq2i F : 0 ..^ 0 X F : X
44 43 32 bitri F : 0 ..^ 0 X F =
45 42 44 bitrdi M = 0 F : 0 ..^ M X F =
46 45 adantr M = 0 M = N F : 0 ..^ M X F =
47 eqeq1 M = N M = 0 N = 0
48 47 biimpac M = 0 M = N N = 0
49 oveq2 N = 0 0 ..^ N = 0 ..^ 0
50 49 feq2d N = 0 P : 0 ..^ N Y P : 0 ..^ 0 Y
51 29 feq2i P : 0 ..^ 0 Y P : Y
52 51 3 bitri P : 0 ..^ 0 Y P =
53 50 52 bitrdi N = 0 P : 0 ..^ N Y P =
54 48 53 syl M = 0 M = N P : 0 ..^ N Y P =
55 46 54 anbi12d M = 0 M = N F : 0 ..^ M X P : 0 ..^ N Y F = P =
56 eqtr3 F = P = F = P
57 55 56 syl6bi M = 0 M = N F : 0 ..^ M X P : 0 ..^ N Y F = P
58 57 com12 F : 0 ..^ M X P : 0 ..^ N Y M = 0 M = N F = P
59 58 expd F : 0 ..^ M X P : 0 ..^ N Y M = 0 M = N F = P
60 59 adantl M 0 N 0 F : 0 ..^ M X P : 0 ..^ N Y M = 0 M = N F = P
61 60 impcom M = 0 M 0 N 0 F : 0 ..^ M X P : 0 ..^ N Y M = N F = P
62 41 61 impbid M = 0 M 0 N 0 F : 0 ..^ M X P : 0 ..^ N Y F = P M = N
63 ral0 i F i = P i
64 30 raleqdv M = 0 i 0 ..^ M F i = P i i F i = P i
65 63 64 mpbiri M = 0 i 0 ..^ M F i = P i
66 65 biantrud M = 0 M = N M = N i 0 ..^ M F i = P i
67 66 adantr M = 0 M 0 N 0 F : 0 ..^ M X P : 0 ..^ N Y M = N M = N i 0 ..^ M F i = P i
68 62 67 bitrd M = 0 M 0 N 0 F : 0 ..^ M X P : 0 ..^ N Y F = P M = N i 0 ..^ M F i = P i
69 ffn F : 0 ..^ M X F Fn 0 ..^ M
70 69 4 anim12i F : 0 ..^ M X P : 0 ..^ N Y F Fn 0 ..^ M P Fn 0 ..^ N
71 70 adantl M 0 N 0 F : 0 ..^ M X P : 0 ..^ N Y F Fn 0 ..^ M P Fn 0 ..^ N
72 71 adantl ¬ M = 0 M 0 N 0 F : 0 ..^ M X P : 0 ..^ N Y F Fn 0 ..^ M P Fn 0 ..^ N
73 eqfnfv2 F Fn 0 ..^ M P Fn 0 ..^ N F = P 0 ..^ M = 0 ..^ N i 0 ..^ M F i = P i
74 72 73 syl ¬ M = 0 M 0 N 0 F : 0 ..^ M X P : 0 ..^ N Y F = P 0 ..^ M = 0 ..^ N i 0 ..^ M F i = P i
75 df-ne M 0 ¬ M = 0
76 elnnne0 M M 0 M 0
77 0zd M 0
78 nnz M M
79 nngt0 M 0 < M
80 77 78 79 3jca M 0 M 0 < M
81 80 adantr M N 0 0 M 0 < M
82 fzoopth 0 M 0 < M 0 ..^ M = 0 ..^ N 0 = 0 M = N
83 81 82 syl M N 0 0 ..^ M = 0 ..^ N 0 = 0 M = N
84 simpr 0 = 0 M = N M = N
85 83 84 syl6bi M N 0 0 ..^ M = 0 ..^ N M = N
86 85 anim1d M N 0 0 ..^ M = 0 ..^ N i 0 ..^ M F i = P i M = N i 0 ..^ M F i = P i
87 oveq2 M = N 0 ..^ M = 0 ..^ N
88 87 anim1i M = N i 0 ..^ M F i = P i 0 ..^ M = 0 ..^ N i 0 ..^ M F i = P i
89 86 88 impbid1 M N 0 0 ..^ M = 0 ..^ N i 0 ..^ M F i = P i M = N i 0 ..^ M F i = P i
90 89 ex M N 0 0 ..^ M = 0 ..^ N i 0 ..^ M F i = P i M = N i 0 ..^ M F i = P i
91 76 90 sylbir M 0 M 0 N 0 0 ..^ M = 0 ..^ N i 0 ..^ M F i = P i M = N i 0 ..^ M F i = P i
92 91 impancom M 0 N 0 M 0 0 ..^ M = 0 ..^ N i 0 ..^ M F i = P i M = N i 0 ..^ M F i = P i
93 75 92 syl5bir M 0 N 0 ¬ M = 0 0 ..^ M = 0 ..^ N i 0 ..^ M F i = P i M = N i 0 ..^ M F i = P i
94 93 adantr M 0 N 0 F : 0 ..^ M X P : 0 ..^ N Y ¬ M = 0 0 ..^ M = 0 ..^ N i 0 ..^ M F i = P i M = N i 0 ..^ M F i = P i
95 94 impcom ¬ M = 0 M 0 N 0 F : 0 ..^ M X P : 0 ..^ N Y 0 ..^ M = 0 ..^ N i 0 ..^ M F i = P i M = N i 0 ..^ M F i = P i
96 74 95 bitrd ¬ M = 0 M 0 N 0 F : 0 ..^ M X P : 0 ..^ N Y F = P M = N i 0 ..^ M F i = P i
97 68 96 pm2.61ian M 0 N 0 F : 0 ..^ M X P : 0 ..^ N Y F = P M = N i 0 ..^ M F i = P i