Metamath Proof Explorer

Theorem hashxplem

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

Ref Expression
Hypothesis hashxplem.1 ⊢ B ∈ Fin
Assertion hashxplem ⊢ A ∈ Fin → A × B = A ⁢ B

Proof

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