Metamath Proof Explorer

Theorem hashxplem

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

Ref Expression
Hypothesis hashxplem.1 ⊢ 𝐵 ∈ Fin
Assertion hashxplem ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 hashxplem.1 ⊢ 𝐵 ∈ Fin
2 xpeq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 × 𝐵 ) = ( ∅ × 𝐵 ) )
3 2 fveq2d ⊢ ( 𝑥 = ∅ → ( ♯ ‘ ( 𝑥 × 𝐵 ) ) = ( ♯ ‘ ( ∅ × 𝐵 ) ) )
4 fveq2 ⊢ ( 𝑥 = ∅ → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ ∅ ) )
5 4 oveq1d ⊢ ( 𝑥 = ∅ → ( ( ♯ ‘ 𝑥 ) · ( ♯ ‘ 𝐵 ) ) = ( ( ♯ ‘ ∅ ) · ( ♯ ‘ 𝐵 ) ) )
6 3 5 eqeq12d ⊢ ( 𝑥 = ∅ → ( ( ♯ ‘ ( 𝑥 × 𝐵 ) ) = ( ( ♯ ‘ 𝑥 ) · ( ♯ ‘ 𝐵 ) ) ↔ ( ♯ ‘ ( ∅ × 𝐵 ) ) = ( ( ♯ ‘ ∅ ) · ( ♯ ‘ 𝐵 ) ) ) )
7 xpeq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 × 𝐵 ) = ( 𝑦 × 𝐵 ) )
8 7 fveq2d ⊢ ( 𝑥 = 𝑦 → ( ♯ ‘ ( 𝑥 × 𝐵 ) ) = ( ♯ ‘ ( 𝑦 × 𝐵 ) ) )
9 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) )
10 9 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ( ♯ ‘ 𝑥 ) · ( ♯ ‘ 𝐵 ) ) = ( ( ♯ ‘ 𝑦 ) · ( ♯ ‘ 𝐵 ) ) )
11 8 10 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( ♯ ‘ ( 𝑥 × 𝐵 ) ) = ( ( ♯ ‘ 𝑥 ) · ( ♯ ‘ 𝐵 ) ) ↔ ( ♯ ‘ ( 𝑦 × 𝐵 ) ) = ( ( ♯ ‘ 𝑦 ) · ( ♯ ‘ 𝐵 ) ) ) )
12 xpeq1 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑥 × 𝐵 ) = ( ( 𝑦 ∪ { 𝑧 } ) × 𝐵 ) )
13 12 fveq2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ♯ ‘ ( 𝑥 × 𝐵 ) ) = ( ♯ ‘ ( ( 𝑦 ∪ { 𝑧 } ) × 𝐵 ) ) )
14 fveq2 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) )
15 14 oveq1d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ♯ ‘ 𝑥 ) · ( ♯ ‘ 𝐵 ) ) = ( ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) · ( ♯ ‘ 𝐵 ) ) )
16 13 15 eqeq12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ♯ ‘ ( 𝑥 × 𝐵 ) ) = ( ( ♯ ‘ 𝑥 ) · ( ♯ ‘ 𝐵 ) ) ↔ ( ♯ ‘ ( ( 𝑦 ∪ { 𝑧 } ) × 𝐵 ) ) = ( ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) · ( ♯ ‘ 𝐵 ) ) ) )
17 xpeq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 × 𝐵 ) = ( 𝐴 × 𝐵 ) )
18 17 fveq2d ⊢ ( 𝑥 = 𝐴 → ( ♯ ‘ ( 𝑥 × 𝐵 ) ) = ( ♯ ‘ ( 𝐴 × 𝐵 ) ) )
19 fveq2 ⊢ ( 𝑥 = 𝐴 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝐴 ) )
20 19 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( ♯ ‘ 𝑥 ) · ( ♯ ‘ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ 𝐵 ) ) )
21 18 20 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( ♯ ‘ ( 𝑥 × 𝐵 ) ) = ( ( ♯ ‘ 𝑥 ) · ( ♯ ‘ 𝐵 ) ) ↔ ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ 𝐵 ) ) ) )
22 hashcl ⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
23 22 nn0cnd ⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℂ )
24 23 mul02d ⊢ ( 𝐵 ∈ Fin → ( 0 · ( ♯ ‘ 𝐵 ) ) = 0 )
25 1 24 ax-mp ⊢ ( 0 · ( ♯ ‘ 𝐵 ) ) = 0
26 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
27 26 oveq1i ⊢ ( ( ♯ ‘ ∅ ) · ( ♯ ‘ 𝐵 ) ) = ( 0 · ( ♯ ‘ 𝐵 ) )
28 0xp ⊢ ( ∅ × 𝐵 ) = ∅
29 28 fveq2i ⊢ ( ♯ ‘ ( ∅ × 𝐵 ) ) = ( ♯ ‘ ∅ )
30 29 26 eqtri ⊢ ( ♯ ‘ ( ∅ × 𝐵 ) ) = 0
31 25 27 30 3eqtr4ri ⊢ ( ♯ ‘ ( ∅ × 𝐵 ) ) = ( ( ♯ ‘ ∅ ) · ( ♯ ‘ 𝐵 ) )
32 oveq1 ⊢ ( ( ♯ ‘ ( 𝑦 × 𝐵 ) ) = ( ( ♯ ‘ 𝑦 ) · ( ♯ ‘ 𝐵 ) ) → ( ( ♯ ‘ ( 𝑦 × 𝐵 ) ) + ( ♯ ‘ 𝐵 ) ) = ( ( ( ♯ ‘ 𝑦 ) · ( ♯ ‘ 𝐵 ) ) + ( ♯ ‘ 𝐵 ) ) )
33 32 adantl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ♯ ‘ ( 𝑦 × 𝐵 ) ) = ( ( ♯ ‘ 𝑦 ) · ( ♯ ‘ 𝐵 ) ) ) → ( ( ♯ ‘ ( 𝑦 × 𝐵 ) ) + ( ♯ ‘ 𝐵 ) ) = ( ( ( ♯ ‘ 𝑦 ) · ( ♯ ‘ 𝐵 ) ) + ( ♯ ‘ 𝐵 ) ) )
34 xpundir ⊢ ( ( 𝑦 ∪ { 𝑧 } ) × 𝐵 ) = ( ( 𝑦 × 𝐵 ) ∪ ( { 𝑧 } × 𝐵 ) )
35 34 fveq2i ⊢ ( ♯ ‘ ( ( 𝑦 ∪ { 𝑧 } ) × 𝐵 ) ) = ( ♯ ‘ ( ( 𝑦 × 𝐵 ) ∪ ( { 𝑧 } × 𝐵 ) ) )
36 xpfi ⊢ ( ( 𝑦 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝑦 × 𝐵 ) ∈ Fin )
37 1 36 mpan2 ⊢ ( 𝑦 ∈ Fin → ( 𝑦 × 𝐵 ) ∈ Fin )
38 inxp ⊢ ( ( 𝑦 × 𝐵 ) ∩ ( { 𝑧 } × 𝐵 ) ) = ( ( 𝑦 ∩ { 𝑧 } ) × ( 𝐵 ∩ 𝐵 ) )
39 disjsn ⊢ ( ( 𝑦 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ 𝑦 )
40 39 biimpri ⊢ ( ¬ 𝑧 ∈ 𝑦 → ( 𝑦 ∩ { 𝑧 } ) = ∅ )
41 40 xpeq1d ⊢ ( ¬ 𝑧 ∈ 𝑦 → ( ( 𝑦 ∩ { 𝑧 } ) × ( 𝐵 ∩ 𝐵 ) ) = ( ∅ × ( 𝐵 ∩ 𝐵 ) ) )
42 0xp ⊢ ( ∅ × ( 𝐵 ∩ 𝐵 ) ) = ∅
43 41 42 eqtrdi ⊢ ( ¬ 𝑧 ∈ 𝑦 → ( ( 𝑦 ∩ { 𝑧 } ) × ( 𝐵 ∩ 𝐵 ) ) = ∅ )
44 38 43 syl5eq ⊢ ( ¬ 𝑧 ∈ 𝑦 → ( ( 𝑦 × 𝐵 ) ∩ ( { 𝑧 } × 𝐵 ) ) = ∅ )
45 snfi ⊢ { 𝑧 } ∈ Fin
46 xpfi ⊢ ( ( { 𝑧 } ∈ Fin ∧ 𝐵 ∈ Fin ) → ( { 𝑧 } × 𝐵 ) ∈ Fin )
47 45 1 46 mp2an ⊢ ( { 𝑧 } × 𝐵 ) ∈ Fin
48 hashun ⊢ ( ( ( 𝑦 × 𝐵 ) ∈ Fin ∧ ( { 𝑧 } × 𝐵 ) ∈ Fin ∧ ( ( 𝑦 × 𝐵 ) ∩ ( { 𝑧 } × 𝐵 ) ) = ∅ ) → ( ♯ ‘ ( ( 𝑦 × 𝐵 ) ∪ ( { 𝑧 } × 𝐵 ) ) ) = ( ( ♯ ‘ ( 𝑦 × 𝐵 ) ) + ( ♯ ‘ ( { 𝑧 } × 𝐵 ) ) ) )
49 47 48 mp3an2 ⊢ ( ( ( 𝑦 × 𝐵 ) ∈ Fin ∧ ( ( 𝑦 × 𝐵 ) ∩ ( { 𝑧 } × 𝐵 ) ) = ∅ ) → ( ♯ ‘ ( ( 𝑦 × 𝐵 ) ∪ ( { 𝑧 } × 𝐵 ) ) ) = ( ( ♯ ‘ ( 𝑦 × 𝐵 ) ) + ( ♯ ‘ ( { 𝑧 } × 𝐵 ) ) ) )
50 37 44 49 syl2an ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ♯ ‘ ( ( 𝑦 × 𝐵 ) ∪ ( { 𝑧 } × 𝐵 ) ) ) = ( ( ♯ ‘ ( 𝑦 × 𝐵 ) ) + ( ♯ ‘ ( { 𝑧 } × 𝐵 ) ) ) )
51 snex ⊢ { 𝑧 } ∈ V
52 1 elexi ⊢ 𝐵 ∈ V
53 51 52 xpcomen ⊢ ( { 𝑧 } × 𝐵 ) ≈ ( 𝐵 × { 𝑧 } )
54 vex ⊢ 𝑧 ∈ V
55 52 54 xpsnen ⊢ ( 𝐵 × { 𝑧 } ) ≈ 𝐵
56 53 55 entri ⊢ ( { 𝑧 } × 𝐵 ) ≈ 𝐵
57 hashen ⊢ ( ( ( { 𝑧 } × 𝐵 ) ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ ( { 𝑧 } × 𝐵 ) ) = ( ♯ ‘ 𝐵 ) ↔ ( { 𝑧 } × 𝐵 ) ≈ 𝐵 ) )
58 47 1 57 mp2an ⊢ ( ( ♯ ‘ ( { 𝑧 } × 𝐵 ) ) = ( ♯ ‘ 𝐵 ) ↔ ( { 𝑧 } × 𝐵 ) ≈ 𝐵 )
59 56 58 mpbir ⊢ ( ♯ ‘ ( { 𝑧 } × 𝐵 ) ) = ( ♯ ‘ 𝐵 )
60 59 oveq2i ⊢ ( ( ♯ ‘ ( 𝑦 × 𝐵 ) ) + ( ♯ ‘ ( { 𝑧 } × 𝐵 ) ) ) = ( ( ♯ ‘ ( 𝑦 × 𝐵 ) ) + ( ♯ ‘ 𝐵 ) )
61 50 60 eqtrdi ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ♯ ‘ ( ( 𝑦 × 𝐵 ) ∪ ( { 𝑧 } × 𝐵 ) ) ) = ( ( ♯ ‘ ( 𝑦 × 𝐵 ) ) + ( ♯ ‘ 𝐵 ) ) )
62 35 61 syl5eq ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ♯ ‘ ( ( 𝑦 ∪ { 𝑧 } ) × 𝐵 ) ) = ( ( ♯ ‘ ( 𝑦 × 𝐵 ) ) + ( ♯ ‘ 𝐵 ) ) )
63 62 adantr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ♯ ‘ ( 𝑦 × 𝐵 ) ) = ( ( ♯ ‘ 𝑦 ) · ( ♯ ‘ 𝐵 ) ) ) → ( ♯ ‘ ( ( 𝑦 ∪ { 𝑧 } ) × 𝐵 ) ) = ( ( ♯ ‘ ( 𝑦 × 𝐵 ) ) + ( ♯ ‘ 𝐵 ) ) )
64 hashunsng ⊢ ( 𝑧 ∈ V → ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝑦 ) + 1 ) ) )
65 54 64 ax-mp ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( ♯ ‘ 𝑦 ) + 1 ) )
66 65 oveq1d ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) · ( ♯ ‘ 𝐵 ) ) = ( ( ( ♯ ‘ 𝑦 ) + 1 ) · ( ♯ ‘ 𝐵 ) ) )
67 hashcl ⊢ ( 𝑦 ∈ Fin → ( ♯ ‘ 𝑦 ) ∈ ℕ0 )
68 67 nn0cnd ⊢ ( 𝑦 ∈ Fin → ( ♯ ‘ 𝑦 ) ∈ ℂ )
69 ax-1cn ⊢ 1 ∈ ℂ
70 nn0cn ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℕ0 → ( ♯ ‘ 𝐵 ) ∈ ℂ )
71 1 22 70 mp2b ⊢ ( ♯ ‘ 𝐵 ) ∈ ℂ
72 adddir ⊢ ( ( ( ♯ ‘ 𝑦 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( ♯ ‘ 𝐵 ) ∈ ℂ ) → ( ( ( ♯ ‘ 𝑦 ) + 1 ) · ( ♯ ‘ 𝐵 ) ) = ( ( ( ♯ ‘ 𝑦 ) · ( ♯ ‘ 𝐵 ) ) + ( 1 · ( ♯ ‘ 𝐵 ) ) ) )
73 69 71 72 mp3an23 ⊢ ( ( ♯ ‘ 𝑦 ) ∈ ℂ → ( ( ( ♯ ‘ 𝑦 ) + 1 ) · ( ♯ ‘ 𝐵 ) ) = ( ( ( ♯ ‘ 𝑦 ) · ( ♯ ‘ 𝐵 ) ) + ( 1 · ( ♯ ‘ 𝐵 ) ) ) )
74 68 73 syl ⊢ ( 𝑦 ∈ Fin → ( ( ( ♯ ‘ 𝑦 ) + 1 ) · ( ♯ ‘ 𝐵 ) ) = ( ( ( ♯ ‘ 𝑦 ) · ( ♯ ‘ 𝐵 ) ) + ( 1 · ( ♯ ‘ 𝐵 ) ) ) )
75 71 mulid2i ⊢ ( 1 · ( ♯ ‘ 𝐵 ) ) = ( ♯ ‘ 𝐵 )
76 75 oveq2i ⊢ ( ( ( ♯ ‘ 𝑦 ) · ( ♯ ‘ 𝐵 ) ) + ( 1 · ( ♯ ‘ 𝐵 ) ) ) = ( ( ( ♯ ‘ 𝑦 ) · ( ♯ ‘ 𝐵 ) ) + ( ♯ ‘ 𝐵 ) )
77 74 76 eqtrdi ⊢ ( 𝑦 ∈ Fin → ( ( ( ♯ ‘ 𝑦 ) + 1 ) · ( ♯ ‘ 𝐵 ) ) = ( ( ( ♯ ‘ 𝑦 ) · ( ♯ ‘ 𝐵 ) ) + ( ♯ ‘ 𝐵 ) ) )
78 77 adantr ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ( ♯ ‘ 𝑦 ) + 1 ) · ( ♯ ‘ 𝐵 ) ) = ( ( ( ♯ ‘ 𝑦 ) · ( ♯ ‘ 𝐵 ) ) + ( ♯ ‘ 𝐵 ) ) )
79 66 78 eqtrd ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) · ( ♯ ‘ 𝐵 ) ) = ( ( ( ♯ ‘ 𝑦 ) · ( ♯ ‘ 𝐵 ) ) + ( ♯ ‘ 𝐵 ) ) )
80 79 adantr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ♯ ‘ ( 𝑦 × 𝐵 ) ) = ( ( ♯ ‘ 𝑦 ) · ( ♯ ‘ 𝐵 ) ) ) → ( ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) · ( ♯ ‘ 𝐵 ) ) = ( ( ( ♯ ‘ 𝑦 ) · ( ♯ ‘ 𝐵 ) ) + ( ♯ ‘ 𝐵 ) ) )
81 33 63 80 3eqtr4d ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( ♯ ‘ ( 𝑦 × 𝐵 ) ) = ( ( ♯ ‘ 𝑦 ) · ( ♯ ‘ 𝐵 ) ) ) → ( ♯ ‘ ( ( 𝑦 ∪ { 𝑧 } ) × 𝐵 ) ) = ( ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) · ( ♯ ‘ 𝐵 ) ) )
82 81 ex ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ♯ ‘ ( 𝑦 × 𝐵 ) ) = ( ( ♯ ‘ 𝑦 ) · ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ ( ( 𝑦 ∪ { 𝑧 } ) × 𝐵 ) ) = ( ( ♯ ‘ ( 𝑦 ∪ { 𝑧 } ) ) · ( ♯ ‘ 𝐵 ) ) ) )
83 6 11 16 21 31 82 findcard2s ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ 𝐵 ) ) )