Metamath Proof Explorer

Theorem hashmap

Description: The size of the set exponential of two finite sets is the exponential of their sizes. (This is the original motivation behind the notation for set exponentiation.) (Contributed by Mario Carneiro, 5-Aug-2014) (Proof shortened by AV, 18-Jul-2022)

Ref Expression
Assertion hashmap 
|- ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( A ^m B ) ) = ( ( # ` A ) ^ ( # ` B ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = (/) -> ( A ^m x ) = ( A ^m (/) ) )
2 1 fveq2d 
 |-  ( x = (/) -> ( # ` ( A ^m x ) ) = ( # ` ( A ^m (/) ) ) )
3 fveq2 
 |-  ( x = (/) -> ( # ` x ) = ( # ` (/) ) )
4 3 oveq2d 
 |-  ( x = (/) -> ( ( # ` A ) ^ ( # ` x ) ) = ( ( # ` A ) ^ ( # ` (/) ) ) )
5 2 4 eqeq12d 
 |-  ( x = (/) -> ( ( # ` ( A ^m x ) ) = ( ( # ` A ) ^ ( # ` x ) ) <-> ( # ` ( A ^m (/) ) ) = ( ( # ` A ) ^ ( # ` (/) ) ) ) )
6 5 imbi2d 
 |-  ( x = (/) -> ( ( A e. Fin -> ( # ` ( A ^m x ) ) = ( ( # ` A ) ^ ( # ` x ) ) ) <-> ( A e. Fin -> ( # ` ( A ^m (/) ) ) = ( ( # ` A ) ^ ( # ` (/) ) ) ) ) )
7 oveq2 
 |-  ( x = y -> ( A ^m x ) = ( A ^m y ) )
8 7 fveq2d 
 |-  ( x = y -> ( # ` ( A ^m x ) ) = ( # ` ( A ^m y ) ) )
9 fveq2 
 |-  ( x = y -> ( # ` x ) = ( # ` y ) )
10 9 oveq2d 
 |-  ( x = y -> ( ( # ` A ) ^ ( # ` x ) ) = ( ( # ` A ) ^ ( # ` y ) ) )
11 8 10 eqeq12d 
 |-  ( x = y -> ( ( # ` ( A ^m x ) ) = ( ( # ` A ) ^ ( # ` x ) ) <-> ( # ` ( A ^m y ) ) = ( ( # ` A ) ^ ( # ` y ) ) ) )
12 11 imbi2d 
 |-  ( x = y -> ( ( A e. Fin -> ( # ` ( A ^m x ) ) = ( ( # ` A ) ^ ( # ` x ) ) ) <-> ( A e. Fin -> ( # ` ( A ^m y ) ) = ( ( # ` A ) ^ ( # ` y ) ) ) ) )
13 oveq2 
 |-  ( x = ( y u. { z } ) -> ( A ^m x ) = ( A ^m ( y u. { z } ) ) )
14 13 fveq2d 
 |-  ( x = ( y u. { z } ) -> ( # ` ( A ^m x ) ) = ( # ` ( A ^m ( y u. { z } ) ) ) )
15 fveq2 
 |-  ( x = ( y u. { z } ) -> ( # ` x ) = ( # ` ( y u. { z } ) ) )
16 15 oveq2d 
 |-  ( x = ( y u. { z } ) -> ( ( # ` A ) ^ ( # ` x ) ) = ( ( # ` A ) ^ ( # ` ( y u. { z } ) ) ) )
17 14 16 eqeq12d 
 |-  ( x = ( y u. { z } ) -> ( ( # ` ( A ^m x ) ) = ( ( # ` A ) ^ ( # ` x ) ) <-> ( # ` ( A ^m ( y u. { z } ) ) ) = ( ( # ` A ) ^ ( # ` ( y u. { z } ) ) ) ) )
18 17 imbi2d 
 |-  ( x = ( y u. { z } ) -> ( ( A e. Fin -> ( # ` ( A ^m x ) ) = ( ( # ` A ) ^ ( # ` x ) ) ) <-> ( A e. Fin -> ( # ` ( A ^m ( y u. { z } ) ) ) = ( ( # ` A ) ^ ( # ` ( y u. { z } ) ) ) ) ) )
19 oveq2 
 |-  ( x = B -> ( A ^m x ) = ( A ^m B ) )
20 19 fveq2d 
 |-  ( x = B -> ( # ` ( A ^m x ) ) = ( # ` ( A ^m B ) ) )
21 fveq2 
 |-  ( x = B -> ( # ` x ) = ( # ` B ) )
22 21 oveq2d 
 |-  ( x = B -> ( ( # ` A ) ^ ( # ` x ) ) = ( ( # ` A ) ^ ( # ` B ) ) )
23 20 22 eqeq12d 
 |-  ( x = B -> ( ( # ` ( A ^m x ) ) = ( ( # ` A ) ^ ( # ` x ) ) <-> ( # ` ( A ^m B ) ) = ( ( # ` A ) ^ ( # ` B ) ) ) )
24 23 imbi2d 
 |-  ( x = B -> ( ( A e. Fin -> ( # ` ( A ^m x ) ) = ( ( # ` A ) ^ ( # ` x ) ) ) <-> ( A e. Fin -> ( # ` ( A ^m B ) ) = ( ( # ` A ) ^ ( # ` B ) ) ) ) )
25 hashcl 
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
26 25 nn0cnd 
 |-  ( A e. Fin -> ( # ` A ) e. CC )
27 26 exp0d 
 |-  ( A e. Fin -> ( ( # ` A ) ^ 0 ) = 1 )
28 hash0 
 |-  ( # ` (/) ) = 0
29 28 oveq2i 
 |-  ( ( # ` A ) ^ ( # ` (/) ) ) = ( ( # ` A ) ^ 0 )
30 29 a1i 
 |-  ( A e. Fin -> ( ( # ` A ) ^ ( # ` (/) ) ) = ( ( # ` A ) ^ 0 ) )
31 mapdm0 
 |-  ( A e. Fin -> ( A ^m (/) ) = { (/) } )
32 31 fveq2d 
 |-  ( A e. Fin -> ( # ` ( A ^m (/) ) ) = ( # ` { (/) } ) )
33 0ex 
 |-  (/) e. _V
34 hashsng 
 |-  ( (/) e. _V -> ( # ` { (/) } ) = 1 )
35 33 34 mp1i 
 |-  ( A e. Fin -> ( # ` { (/) } ) = 1 )
36 32 35 eqtrd 
 |-  ( A e. Fin -> ( # ` ( A ^m (/) ) ) = 1 )
37 27 30 36 3eqtr4rd 
 |-  ( A e. Fin -> ( # ` ( A ^m (/) ) ) = ( ( # ` A ) ^ ( # ` (/) ) ) )
38 oveq1 
 |-  ( ( # ` ( A ^m y ) ) = ( ( # ` A ) ^ ( # ` y ) ) -> ( ( # ` ( A ^m y ) ) x. ( # ` A ) ) = ( ( ( # ` A ) ^ ( # ` y ) ) x. ( # ` A ) ) )
39 vex 
 |-  y e. _V
40 39 a1i 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> y e. _V )
41 snex 
 |-  { z } e. _V
42 41 a1i 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> { z } e. _V )
43 elex 
 |-  ( A e. Fin -> A e. _V )
44 43 adantr 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> A e. _V )
45 simprr 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> -. z e. y )
46 disjsn 
 |-  ( ( y i^i { z } ) = (/) <-> -. z e. y )
47 45 46 sylibr 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( y i^i { z } ) = (/) )
48 mapunen 
 |-  ( ( ( y e. _V /\ { z } e. _V /\ A e. _V ) /\ ( y i^i { z } ) = (/) ) -> ( A ^m ( y u. { z } ) ) ~~ ( ( A ^m y ) X. ( A ^m { z } ) ) )
49 40 42 44 47 48 syl31anc 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( A ^m ( y u. { z } ) ) ~~ ( ( A ^m y ) X. ( A ^m { z } ) ) )
50 simpl 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> A e. Fin )
51 simprl 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> y e. Fin )
52 snfi 
 |-  { z } e. Fin
53 unfi 
 |-  ( ( y e. Fin /\ { z } e. Fin ) -> ( y u. { z } ) e. Fin )
54 51 52 53 sylancl 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( y u. { z } ) e. Fin )
55 mapfi 
 |-  ( ( A e. Fin /\ ( y u. { z } ) e. Fin ) -> ( A ^m ( y u. { z } ) ) e. Fin )
56 50 54 55 syl2anc 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( A ^m ( y u. { z } ) ) e. Fin )
57 mapfi 
 |-  ( ( A e. Fin /\ y e. Fin ) -> ( A ^m y ) e. Fin )
58 57 adantrr 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( A ^m y ) e. Fin )
59 mapfi 
 |-  ( ( A e. Fin /\ { z } e. Fin ) -> ( A ^m { z } ) e. Fin )
60 50 52 59 sylancl 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( A ^m { z } ) e. Fin )
61 xpfi 
 |-  ( ( ( A ^m y ) e. Fin /\ ( A ^m { z } ) e. Fin ) -> ( ( A ^m y ) X. ( A ^m { z } ) ) e. Fin )
62 58 60 61 syl2anc 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( A ^m y ) X. ( A ^m { z } ) ) e. Fin )
63 hashen 
 |-  ( ( ( A ^m ( y u. { z } ) ) e. Fin /\ ( ( A ^m y ) X. ( A ^m { z } ) ) e. Fin ) -> ( ( # ` ( A ^m ( y u. { z } ) ) ) = ( # ` ( ( A ^m y ) X. ( A ^m { z } ) ) ) <-> ( A ^m ( y u. { z } ) ) ~~ ( ( A ^m y ) X. ( A ^m { z } ) ) ) )
64 56 62 63 syl2anc 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( # ` ( A ^m ( y u. { z } ) ) ) = ( # ` ( ( A ^m y ) X. ( A ^m { z } ) ) ) <-> ( A ^m ( y u. { z } ) ) ~~ ( ( A ^m y ) X. ( A ^m { z } ) ) ) )
65 49 64 mpbird 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( # ` ( A ^m ( y u. { z } ) ) ) = ( # ` ( ( A ^m y ) X. ( A ^m { z } ) ) ) )
66 hashxp 
 |-  ( ( ( A ^m y ) e. Fin /\ ( A ^m { z } ) e. Fin ) -> ( # ` ( ( A ^m y ) X. ( A ^m { z } ) ) ) = ( ( # ` ( A ^m y ) ) x. ( # ` ( A ^m { z } ) ) ) )
67 58 60 66 syl2anc 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( # ` ( ( A ^m y ) X. ( A ^m { z } ) ) ) = ( ( # ` ( A ^m y ) ) x. ( # ` ( A ^m { z } ) ) ) )
68 vex 
 |-  z e. _V
69 68 a1i 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> z e. _V )
70 50 69 mapsnend 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( A ^m { z } ) ~~ A )
71 hashen 
 |-  ( ( ( A ^m { z } ) e. Fin /\ A e. Fin ) -> ( ( # ` ( A ^m { z } ) ) = ( # ` A ) <-> ( A ^m { z } ) ~~ A ) )
72 60 50 71 syl2anc 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( # ` ( A ^m { z } ) ) = ( # ` A ) <-> ( A ^m { z } ) ~~ A ) )
73 70 72 mpbird 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( # ` ( A ^m { z } ) ) = ( # ` A ) )
74 73 oveq2d 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( # ` ( A ^m y ) ) x. ( # ` ( A ^m { z } ) ) ) = ( ( # ` ( A ^m y ) ) x. ( # ` A ) ) )
75 65 67 74 3eqtrd 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( # ` ( A ^m ( y u. { z } ) ) ) = ( ( # ` ( A ^m y ) ) x. ( # ` A ) ) )
76 hashunsng 
 |-  ( z e. _V -> ( ( y e. Fin /\ -. z e. y ) -> ( # ` ( y u. { z } ) ) = ( ( # ` y ) + 1 ) ) )
77 76 elv 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( # ` ( y u. { z } ) ) = ( ( # ` y ) + 1 ) )
78 77 adantl 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( # ` ( y u. { z } ) ) = ( ( # ` y ) + 1 ) )
79 78 oveq2d 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( # ` A ) ^ ( # ` ( y u. { z } ) ) ) = ( ( # ` A ) ^ ( ( # ` y ) + 1 ) ) )
80 26 adantr 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( # ` A ) e. CC )
81 hashcl 
 |-  ( y e. Fin -> ( # ` y ) e. NN0 )
82 81 ad2antrl 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( # ` y ) e. NN0 )
83 80 82 expp1d 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( # ` A ) ^ ( ( # ` y ) + 1 ) ) = ( ( ( # ` A ) ^ ( # ` y ) ) x. ( # ` A ) ) )
84 79 83 eqtrd 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( # ` A ) ^ ( # ` ( y u. { z } ) ) ) = ( ( ( # ` A ) ^ ( # ` y ) ) x. ( # ` A ) ) )
85 75 84 eqeq12d 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( # ` ( A ^m ( y u. { z } ) ) ) = ( ( # ` A ) ^ ( # ` ( y u. { z } ) ) ) <-> ( ( # ` ( A ^m y ) ) x. ( # ` A ) ) = ( ( ( # ` A ) ^ ( # ` y ) ) x. ( # ` A ) ) ) )
86 38 85 syl5ibr 
 |-  ( ( A e. Fin /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( # ` ( A ^m y ) ) = ( ( # ` A ) ^ ( # ` y ) ) -> ( # ` ( A ^m ( y u. { z } ) ) ) = ( ( # ` A ) ^ ( # ` ( y u. { z } ) ) ) ) )
87 86 expcom 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( A e. Fin -> ( ( # ` ( A ^m y ) ) = ( ( # ` A ) ^ ( # ` y ) ) -> ( # ` ( A ^m ( y u. { z } ) ) ) = ( ( # ` A ) ^ ( # ` ( y u. { z } ) ) ) ) ) )
88 87 a2d 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( A e. Fin -> ( # ` ( A ^m y ) ) = ( ( # ` A ) ^ ( # ` y ) ) ) -> ( A e. Fin -> ( # ` ( A ^m ( y u. { z } ) ) ) = ( ( # ` A ) ^ ( # ` ( y u. { z } ) ) ) ) ) )
89 6 12 18 24 37 88 findcard2s 
 |-  ( B e. Fin -> ( A e. Fin -> ( # ` ( A ^m B ) ) = ( ( # ` A ) ^ ( # ` B ) ) ) )
90 89 impcom 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( A ^m B ) ) = ( ( # ` A ) ^ ( # ` B ) ) )