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 e. NN0 /\ N e. NN0 ) /\ ( F : ( 0 ..^ M ) --> X /\ P : ( 0 ..^ N ) --> Y ) ) -> ( F = P <-> ( M = N /\ A. i e. ( 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 e. ZZ
8 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
9 8 adantl 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> N e. ZZ )
10 fzon 
 |-  ( ( 0 e. ZZ /\ N e. ZZ ) -> ( N <_ 0 <-> ( 0 ..^ N ) = (/) ) )
11 7 9 10 sylancr 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( N <_ 0 <-> ( 0 ..^ N ) = (/) ) )
12 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
13 0red 
 |-  ( N e. NN0 -> 0 e. RR )
14 nn0re 
 |-  ( N e. NN0 -> N e. RR )
15 13 14 letri3d 
 |-  ( N e. NN0 -> ( 0 = N <-> ( 0 <_ N /\ N <_ 0 ) ) )
16 15 biimprd 
 |-  ( N e. NN0 -> ( ( 0 <_ N /\ N <_ 0 ) -> 0 = N ) )
17 12 16 mpand 
 |-  ( N e. NN0 -> ( N <_ 0 -> 0 = N ) )
18 17 adantl 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( N <_ 0 -> 0 = N ) )
19 11 18 sylbird 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( 0 ..^ N ) = (/) -> 0 = N ) )
20 6 19 syl5com 
 |-  ( ( P Fn ( 0 ..^ N ) /\ P Fn (/) ) -> ( ( M e. NN0 /\ N e. NN0 ) -> 0 = N ) )
21 20 ex 
 |-  ( P Fn ( 0 ..^ N ) -> ( P Fn (/) -> ( ( M e. NN0 /\ N e. NN0 ) -> 0 = N ) ) )
22 4 5 21 syl2imc 
 |-  ( P : (/) --> Y -> ( P : ( 0 ..^ N ) --> Y -> ( ( M e. NN0 /\ N e. NN0 ) -> 0 = N ) ) )
23 3 22 sylbir 
 |-  ( P = (/) -> ( P : ( 0 ..^ N ) --> Y -> ( ( M e. NN0 /\ N e. NN0 ) -> 0 = N ) ) )
24 23 imp 
 |-  ( ( P = (/) /\ P : ( 0 ..^ N ) --> Y ) -> ( ( M e. NN0 /\ N e. NN0 ) -> 0 = N ) )
25 2 24 biimtrdi 
 |-  ( F = P -> ( ( F = (/) /\ P : ( 0 ..^ N ) --> Y ) -> ( ( M e. NN0 /\ N e. NN0 ) -> 0 = N ) ) )
26 25 com3l 
 |-  ( ( F = (/) /\ P : ( 0 ..^ N ) --> Y ) -> ( ( M e. NN0 /\ N e. NN0 ) -> ( F = P -> 0 = N ) ) )
27 26 a1i 
 |-  ( M = 0 -> ( ( F = (/) /\ P : ( 0 ..^ N ) --> Y ) -> ( ( M e. NN0 /\ N e. NN0 ) -> ( 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 e. NN0 /\ N e. NN0 ) -> ( F = P -> M = N ) ) <-> ( ( M e. NN0 /\ N e. NN0 ) -> ( F = P -> 0 = N ) ) ) )
38 27 34 37 3imtr4d 
 |-  ( M = 0 -> ( ( F : ( 0 ..^ M ) --> X /\ P : ( 0 ..^ N ) --> Y ) -> ( ( M e. NN0 /\ N e. NN0 ) -> ( F = P -> M = N ) ) ) )
39 38 com3l 
 |-  ( ( F : ( 0 ..^ M ) --> X /\ P : ( 0 ..^ N ) --> Y ) -> ( ( M e. NN0 /\ N e. NN0 ) -> ( M = 0 -> ( F = P -> M = N ) ) ) )
40 39 impcom 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( F : ( 0 ..^ M ) --> X /\ P : ( 0 ..^ N ) --> Y ) ) -> ( M = 0 -> ( F = P -> M = N ) ) )
41 40 impcom 
 |-  ( ( M = 0 /\ ( ( M e. NN0 /\ N e. NN0 ) /\ ( 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 biimtrdi 
 |-  ( ( 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 e. NN0 /\ N e. NN0 ) /\ ( F : ( 0 ..^ M ) --> X /\ P : ( 0 ..^ N ) --> Y ) ) -> ( M = 0 -> ( M = N -> F = P ) ) )
61 60 impcom 
 |-  ( ( M = 0 /\ ( ( M e. NN0 /\ N e. NN0 ) /\ ( F : ( 0 ..^ M ) --> X /\ P : ( 0 ..^ N ) --> Y ) ) ) -> ( M = N -> F = P ) )
62 41 61 impbid 
 |-  ( ( M = 0 /\ ( ( M e. NN0 /\ N e. NN0 ) /\ ( F : ( 0 ..^ M ) --> X /\ P : ( 0 ..^ N ) --> Y ) ) ) -> ( F = P <-> M = N ) )
63 ral0 
 |-  A. i e. (/) ( F ` i ) = ( P ` i )
64 30 raleqdv 
 |-  ( M = 0 -> ( A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) <-> A. i e. (/) ( F ` i ) = ( P ` i ) ) )
65 63 64 mpbiri 
 |-  ( M = 0 -> A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) )
66 65 biantrud 
 |-  ( M = 0 -> ( M = N <-> ( M = N /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) ) )
67 66 adantr 
 |-  ( ( M = 0 /\ ( ( M e. NN0 /\ N e. NN0 ) /\ ( F : ( 0 ..^ M ) --> X /\ P : ( 0 ..^ N ) --> Y ) ) ) -> ( M = N <-> ( M = N /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) ) )
68 62 67 bitrd 
 |-  ( ( M = 0 /\ ( ( M e. NN0 /\ N e. NN0 ) /\ ( F : ( 0 ..^ M ) --> X /\ P : ( 0 ..^ N ) --> Y ) ) ) -> ( F = P <-> ( M = N /\ A. i e. ( 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 e. NN0 /\ N e. NN0 ) /\ ( F : ( 0 ..^ M ) --> X /\ P : ( 0 ..^ N ) --> Y ) ) -> ( F Fn ( 0 ..^ M ) /\ P Fn ( 0 ..^ N ) ) )
72 71 adantl 
 |-  ( ( -. M = 0 /\ ( ( M e. NN0 /\ N e. NN0 ) /\ ( 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 ) /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) ) )
74 72 73 syl 
 |-  ( ( -. M = 0 /\ ( ( M e. NN0 /\ N e. NN0 ) /\ ( F : ( 0 ..^ M ) --> X /\ P : ( 0 ..^ N ) --> Y ) ) ) -> ( F = P <-> ( ( 0 ..^ M ) = ( 0 ..^ N ) /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) ) )
75 df-ne 
 |-  ( M =/= 0 <-> -. M = 0 )
76 elnnne0 
 |-  ( M e. NN <-> ( M e. NN0 /\ M =/= 0 ) )
77 0zd 
 |-  ( M e. NN -> 0 e. ZZ )
78 nnz 
 |-  ( M e. NN -> M e. ZZ )
79 nngt0 
 |-  ( M e. NN -> 0 < M )
80 77 78 79 3jca 
 |-  ( M e. NN -> ( 0 e. ZZ /\ M e. ZZ /\ 0 < M ) )
81 80 adantr 
 |-  ( ( M e. NN /\ N e. NN0 ) -> ( 0 e. ZZ /\ M e. ZZ /\ 0 < M ) )
82 fzoopth 
 |-  ( ( 0 e. ZZ /\ M e. ZZ /\ 0 < M ) -> ( ( 0 ..^ M ) = ( 0 ..^ N ) <-> ( 0 = 0 /\ M = N ) ) )
83 81 82 syl 
 |-  ( ( M e. NN /\ N e. NN0 ) -> ( ( 0 ..^ M ) = ( 0 ..^ N ) <-> ( 0 = 0 /\ M = N ) ) )
84 simpr 
 |-  ( ( 0 = 0 /\ M = N ) -> M = N )
85 83 84 biimtrdi 
 |-  ( ( M e. NN /\ N e. NN0 ) -> ( ( 0 ..^ M ) = ( 0 ..^ N ) -> M = N ) )
86 85 anim1d 
 |-  ( ( M e. NN /\ N e. NN0 ) -> ( ( ( 0 ..^ M ) = ( 0 ..^ N ) /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) -> ( M = N /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) ) )
87 oveq2 
 |-  ( M = N -> ( 0 ..^ M ) = ( 0 ..^ N ) )
88 87 anim1i 
 |-  ( ( M = N /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) -> ( ( 0 ..^ M ) = ( 0 ..^ N ) /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) )
89 86 88 impbid1 
 |-  ( ( M e. NN /\ N e. NN0 ) -> ( ( ( 0 ..^ M ) = ( 0 ..^ N ) /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) <-> ( M = N /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) ) )
90 89 ex 
 |-  ( M e. NN -> ( N e. NN0 -> ( ( ( 0 ..^ M ) = ( 0 ..^ N ) /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) <-> ( M = N /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) ) ) )
91 76 90 sylbir 
 |-  ( ( M e. NN0 /\ M =/= 0 ) -> ( N e. NN0 -> ( ( ( 0 ..^ M ) = ( 0 ..^ N ) /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) <-> ( M = N /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) ) ) )
92 91 impancom 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M =/= 0 -> ( ( ( 0 ..^ M ) = ( 0 ..^ N ) /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) <-> ( M = N /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) ) ) )
93 75 92 biimtrrid 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( -. M = 0 -> ( ( ( 0 ..^ M ) = ( 0 ..^ N ) /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) <-> ( M = N /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) ) ) )
94 93 adantr 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( F : ( 0 ..^ M ) --> X /\ P : ( 0 ..^ N ) --> Y ) ) -> ( -. M = 0 -> ( ( ( 0 ..^ M ) = ( 0 ..^ N ) /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) <-> ( M = N /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) ) ) )
95 94 impcom 
 |-  ( ( -. M = 0 /\ ( ( M e. NN0 /\ N e. NN0 ) /\ ( F : ( 0 ..^ M ) --> X /\ P : ( 0 ..^ N ) --> Y ) ) ) -> ( ( ( 0 ..^ M ) = ( 0 ..^ N ) /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) <-> ( M = N /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) ) )
96 74 95 bitrd 
 |-  ( ( -. M = 0 /\ ( ( M e. NN0 /\ N e. NN0 ) /\ ( F : ( 0 ..^ M ) --> X /\ P : ( 0 ..^ N ) --> Y ) ) ) -> ( F = P <-> ( M = N /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) ) )
97 68 96 pm2.61ian 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( F : ( 0 ..^ M ) --> X /\ P : ( 0 ..^ N ) --> Y ) ) -> ( F = P <-> ( M = N /\ A. i e. ( 0 ..^ M ) ( F ` i ) = ( P ` i ) ) ) )