Metamath Proof Explorer

Theorem hashxplem

Description: Lemma for hashxp . (Contributed by Paul Chapman, 30-Nov-2012)

Ref Expression
Hypothesis hashxplem.1 
|- B e. Fin
Assertion hashxplem 
|- ( A e. Fin -> ( # ` ( A X. B ) ) = ( ( # ` A ) x. ( # ` B ) ) )

Proof

Step Hyp Ref Expression
1 hashxplem.1 
 |-  B e. Fin
2 xpeq1 
 |-  ( x = (/) -> ( x X. B ) = ( (/) X. B ) )
3 2 fveq2d 
 |-  ( x = (/) -> ( # ` ( x X. B ) ) = ( # ` ( (/) X. B ) ) )
4 fveq2 
 |-  ( x = (/) -> ( # ` x ) = ( # ` (/) ) )
5 4 oveq1d 
 |-  ( x = (/) -> ( ( # ` x ) x. ( # ` B ) ) = ( ( # ` (/) ) x. ( # ` B ) ) )
6 3 5 eqeq12d 
 |-  ( x = (/) -> ( ( # ` ( x X. B ) ) = ( ( # ` x ) x. ( # ` B ) ) <-> ( # ` ( (/) X. B ) ) = ( ( # ` (/) ) x. ( # ` B ) ) ) )
7 xpeq1 
 |-  ( x = y -> ( x X. B ) = ( y X. B ) )
8 7 fveq2d 
 |-  ( x = y -> ( # ` ( x X. B ) ) = ( # ` ( y X. B ) ) )
9 fveq2 
 |-  ( x = y -> ( # ` x ) = ( # ` y ) )
10 9 oveq1d 
 |-  ( x = y -> ( ( # ` x ) x. ( # ` B ) ) = ( ( # ` y ) x. ( # ` B ) ) )
11 8 10 eqeq12d 
 |-  ( x = y -> ( ( # ` ( x X. B ) ) = ( ( # ` x ) x. ( # ` B ) ) <-> ( # ` ( y X. B ) ) = ( ( # ` y ) x. ( # ` B ) ) ) )
12 xpeq1 
 |-  ( x = ( y u. { z } ) -> ( x X. B ) = ( ( y u. { z } ) X. B ) )
13 12 fveq2d 
 |-  ( x = ( y u. { z } ) -> ( # ` ( x X. B ) ) = ( # ` ( ( y u. { z } ) X. B ) ) )
14 fveq2 
 |-  ( x = ( y u. { z } ) -> ( # ` x ) = ( # ` ( y u. { z } ) ) )
15 14 oveq1d 
 |-  ( x = ( y u. { z } ) -> ( ( # ` x ) x. ( # ` B ) ) = ( ( # ` ( y u. { z } ) ) x. ( # ` B ) ) )
16 13 15 eqeq12d 
 |-  ( x = ( y u. { z } ) -> ( ( # ` ( x X. B ) ) = ( ( # ` x ) x. ( # ` B ) ) <-> ( # ` ( ( y u. { z } ) X. B ) ) = ( ( # ` ( y u. { z } ) ) x. ( # ` B ) ) ) )
17 xpeq1 
 |-  ( x = A -> ( x X. B ) = ( A X. B ) )
18 17 fveq2d 
 |-  ( x = A -> ( # ` ( x X. B ) ) = ( # ` ( A X. B ) ) )
19 fveq2 
 |-  ( x = A -> ( # ` x ) = ( # ` A ) )
20 19 oveq1d 
 |-  ( x = A -> ( ( # ` x ) x. ( # ` B ) ) = ( ( # ` A ) x. ( # ` B ) ) )
21 18 20 eqeq12d 
 |-  ( x = A -> ( ( # ` ( x X. B ) ) = ( ( # ` x ) x. ( # ` B ) ) <-> ( # ` ( A X. B ) ) = ( ( # ` A ) x. ( # ` B ) ) ) )
22 hashcl 
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
23 22 nn0cnd 
 |-  ( B e. Fin -> ( # ` B ) e. CC )
24 23 mul02d 
 |-  ( B e. Fin -> ( 0 x. ( # ` B ) ) = 0 )
25 1 24 ax-mp 
 |-  ( 0 x. ( # ` B ) ) = 0
26 hash0 
 |-  ( # ` (/) ) = 0
27 26 oveq1i 
 |-  ( ( # ` (/) ) x. ( # ` B ) ) = ( 0 x. ( # ` B ) )
28 0xp 
 |-  ( (/) X. B ) = (/)
29 28 fveq2i 
 |-  ( # ` ( (/) X. B ) ) = ( # ` (/) )
30 29 26 eqtri 
 |-  ( # ` ( (/) X. B ) ) = 0
31 25 27 30 3eqtr4ri 
 |-  ( # ` ( (/) X. B ) ) = ( ( # ` (/) ) x. ( # ` B ) )
32 oveq1 
 |-  ( ( # ` ( y X. B ) ) = ( ( # ` y ) x. ( # ` B ) ) -> ( ( # ` ( y X. B ) ) + ( # ` B ) ) = ( ( ( # ` y ) x. ( # ` B ) ) + ( # ` B ) ) )
33 32 adantl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( # ` ( y X. B ) ) = ( ( # ` y ) x. ( # ` B ) ) ) -> ( ( # ` ( y X. B ) ) + ( # ` B ) ) = ( ( ( # ` y ) x. ( # ` B ) ) + ( # ` B ) ) )
34 xpundir 
 |-  ( ( y u. { z } ) X. B ) = ( ( y X. B ) u. ( { z } X. B ) )
35 34 fveq2i 
 |-  ( # ` ( ( y u. { z } ) X. B ) ) = ( # ` ( ( y X. B ) u. ( { z } X. B ) ) )
36 xpfi 
 |-  ( ( y e. Fin /\ B e. Fin ) -> ( y X. B ) e. Fin )
37 1 36 mpan2 
 |-  ( y e. Fin -> ( y X. B ) e. Fin )
38 inxp 
 |-  ( ( y X. B ) i^i ( { z } X. B ) ) = ( ( y i^i { z } ) X. ( B i^i B ) )
39 disjsn 
 |-  ( ( y i^i { z } ) = (/) <-> -. z e. y )
40 39 biimpri 
 |-  ( -. z e. y -> ( y i^i { z } ) = (/) )
41 40 xpeq1d 
 |-  ( -. z e. y -> ( ( y i^i { z } ) X. ( B i^i B ) ) = ( (/) X. ( B i^i B ) ) )
42 0xp 
 |-  ( (/) X. ( B i^i B ) ) = (/)
43 41 42 eqtrdi 
 |-  ( -. z e. y -> ( ( y i^i { z } ) X. ( B i^i B ) ) = (/) )
44 38 43 eqtrid 
 |-  ( -. z e. y -> ( ( y X. B ) i^i ( { z } X. B ) ) = (/) )
45 snfi 
 |-  { z } e. Fin
46 xpfi 
 |-  ( ( { z } e. Fin /\ B e. Fin ) -> ( { z } X. B ) e. Fin )
47 45 1 46 mp2an 
 |-  ( { z } X. B ) e. Fin
48 hashun 
 |-  ( ( ( y X. B ) e. Fin /\ ( { z } X. B ) e. Fin /\ ( ( y X. B ) i^i ( { z } X. B ) ) = (/) ) -> ( # ` ( ( y X. B ) u. ( { z } X. B ) ) ) = ( ( # ` ( y X. B ) ) + ( # ` ( { z } X. B ) ) ) )
49 47 48 mp3an2 
 |-  ( ( ( y X. B ) e. Fin /\ ( ( y X. B ) i^i ( { z } X. B ) ) = (/) ) -> ( # ` ( ( y X. B ) u. ( { z } X. B ) ) ) = ( ( # ` ( y X. B ) ) + ( # ` ( { z } X. B ) ) ) )
50 37 44 49 syl2an 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( # ` ( ( y X. B ) u. ( { z } X. B ) ) ) = ( ( # ` ( y X. B ) ) + ( # ` ( { z } X. B ) ) ) )
51 snex 
 |-  { z } e. _V
52 1 elexi 
 |-  B e. _V
53 51 52 xpcomen 
 |-  ( { z } X. B ) ~~ ( B X. { z } )
54 vex 
 |-  z e. _V
55 52 54 xpsnen 
 |-  ( B X. { z } ) ~~ B
56 53 55 entri 
 |-  ( { z } X. B ) ~~ B
57 hashen 
 |-  ( ( ( { z } X. B ) e. Fin /\ B e. Fin ) -> ( ( # ` ( { z } X. B ) ) = ( # ` B ) <-> ( { z } X. B ) ~~ B ) )
58 47 1 57 mp2an 
 |-  ( ( # ` ( { z } X. B ) ) = ( # ` B ) <-> ( { z } X. B ) ~~ B )
59 56 58 mpbir 
 |-  ( # ` ( { z } X. B ) ) = ( # ` B )
60 59 oveq2i 
 |-  ( ( # ` ( y X. B ) ) + ( # ` ( { z } X. B ) ) ) = ( ( # ` ( y X. B ) ) + ( # ` B ) )
61 50 60 eqtrdi 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( # ` ( ( y X. B ) u. ( { z } X. B ) ) ) = ( ( # ` ( y X. B ) ) + ( # ` B ) ) )
62 35 61 eqtrid 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( # ` ( ( y u. { z } ) X. B ) ) = ( ( # ` ( y X. B ) ) + ( # ` B ) ) )
63 62 adantr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( # ` ( y X. B ) ) = ( ( # ` y ) x. ( # ` B ) ) ) -> ( # ` ( ( y u. { z } ) X. B ) ) = ( ( # ` ( y X. B ) ) + ( # ` B ) ) )
64 hashunsng 
 |-  ( z e. _V -> ( ( y e. Fin /\ -. z e. y ) -> ( # ` ( y u. { z } ) ) = ( ( # ` y ) + 1 ) ) )
65 54 64 ax-mp 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( # ` ( y u. { z } ) ) = ( ( # ` y ) + 1 ) )
66 65 oveq1d 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( # ` ( y u. { z } ) ) x. ( # ` B ) ) = ( ( ( # ` y ) + 1 ) x. ( # ` B ) ) )
67 hashcl 
 |-  ( y e. Fin -> ( # ` y ) e. NN0 )
68 67 nn0cnd 
 |-  ( y e. Fin -> ( # ` y ) e. CC )
69 ax-1cn 
 |-  1 e. CC
70 nn0cn 
 |-  ( ( # ` B ) e. NN0 -> ( # ` B ) e. CC )
71 1 22 70 mp2b 
 |-  ( # ` B ) e. CC
72 adddir 
 |-  ( ( ( # ` y ) e. CC /\ 1 e. CC /\ ( # ` B ) e. CC ) -> ( ( ( # ` y ) + 1 ) x. ( # ` B ) ) = ( ( ( # ` y ) x. ( # ` B ) ) + ( 1 x. ( # ` B ) ) ) )
73 69 71 72 mp3an23 
 |-  ( ( # ` y ) e. CC -> ( ( ( # ` y ) + 1 ) x. ( # ` B ) ) = ( ( ( # ` y ) x. ( # ` B ) ) + ( 1 x. ( # ` B ) ) ) )
74 68 73 syl 
 |-  ( y e. Fin -> ( ( ( # ` y ) + 1 ) x. ( # ` B ) ) = ( ( ( # ` y ) x. ( # ` B ) ) + ( 1 x. ( # ` B ) ) ) )
75 71 mulid2i 
 |-  ( 1 x. ( # ` B ) ) = ( # ` B )
76 75 oveq2i 
 |-  ( ( ( # ` y ) x. ( # ` B ) ) + ( 1 x. ( # ` B ) ) ) = ( ( ( # ` y ) x. ( # ` B ) ) + ( # ` B ) )
77 74 76 eqtrdi 
 |-  ( y e. Fin -> ( ( ( # ` y ) + 1 ) x. ( # ` B ) ) = ( ( ( # ` y ) x. ( # ` B ) ) + ( # ` B ) ) )
78 77 adantr 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( ( # ` y ) + 1 ) x. ( # ` B ) ) = ( ( ( # ` y ) x. ( # ` B ) ) + ( # ` B ) ) )
79 66 78 eqtrd 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( # ` ( y u. { z } ) ) x. ( # ` B ) ) = ( ( ( # ` y ) x. ( # ` B ) ) + ( # ` B ) ) )
80 79 adantr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( # ` ( y X. B ) ) = ( ( # ` y ) x. ( # ` B ) ) ) -> ( ( # ` ( y u. { z } ) ) x. ( # ` B ) ) = ( ( ( # ` y ) x. ( # ` B ) ) + ( # ` B ) ) )
81 33 63 80 3eqtr4d 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( # ` ( y X. B ) ) = ( ( # ` y ) x. ( # ` B ) ) ) -> ( # ` ( ( y u. { z } ) X. B ) ) = ( ( # ` ( y u. { z } ) ) x. ( # ` B ) ) )
82 81 ex 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( # ` ( y X. B ) ) = ( ( # ` y ) x. ( # ` B ) ) -> ( # ` ( ( y u. { z } ) X. B ) ) = ( ( # ` ( y u. { z } ) ) x. ( # ` B ) ) ) )
83 6 11 16 21 31 82 findcard2s 
 |-  ( A e. Fin -> ( # ` ( A X. B ) ) = ( ( # ` A ) x. ( # ` B ) ) )