| Step | Hyp | Ref
| Expression |
| 1 | | xpeq1 5699 |
. . . 4
⊢ (𝑥 = ∅ → (𝑥 × 𝐵) = (∅ × 𝐵)) |
| 2 | 1 | fveq2d 6910 |
. . 3
⊢ (𝑥 = ∅ →
(♯‘(𝑥 ×
𝐵)) =
(♯‘(∅ × 𝐵))) |
| 3 | | fveq2 6906 |
. . . 4
⊢ (𝑥 = ∅ →
(♯‘𝑥) =
(♯‘∅)) |
| 4 | 3 | oveq1d 7446 |
. . 3
⊢ (𝑥 = ∅ →
((♯‘𝑥) ·
(♯‘𝐵)) =
((♯‘∅) · (♯‘𝐵))) |
| 5 | 2, 4 | eqeq12d 2753 |
. 2
⊢ (𝑥 = ∅ →
((♯‘(𝑥 ×
𝐵)) = ((♯‘𝑥) · (♯‘𝐵)) ↔
(♯‘(∅ × 𝐵)) = ((♯‘∅) ·
(♯‘𝐵)))) |
| 6 | | xpeq1 5699 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝑥 × 𝐵) = (𝑦 × 𝐵)) |
| 7 | 6 | fveq2d 6910 |
. . 3
⊢ (𝑥 = 𝑦 → (♯‘(𝑥 × 𝐵)) = (♯‘(𝑦 × 𝐵))) |
| 8 | | fveq2 6906 |
. . . 4
⊢ (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦)) |
| 9 | 8 | oveq1d 7446 |
. . 3
⊢ (𝑥 = 𝑦 → ((♯‘𝑥) · (♯‘𝐵)) = ((♯‘𝑦) · (♯‘𝐵))) |
| 10 | 7, 9 | eqeq12d 2753 |
. 2
⊢ (𝑥 = 𝑦 → ((♯‘(𝑥 × 𝐵)) = ((♯‘𝑥) · (♯‘𝐵)) ↔ (♯‘(𝑦 × 𝐵)) = ((♯‘𝑦) · (♯‘𝐵)))) |
| 11 | | xpeq1 5699 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑥 × 𝐵) = ((𝑦 ∪ {𝑧}) × 𝐵)) |
| 12 | 11 | fveq2d 6910 |
. . 3
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘(𝑥 × 𝐵)) = (♯‘((𝑦 ∪ {𝑧}) × 𝐵))) |
| 13 | | fveq2 6906 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘𝑥) = (♯‘(𝑦 ∪ {𝑧}))) |
| 14 | 13 | oveq1d 7446 |
. . 3
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘𝑥) · (♯‘𝐵)) = ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵))) |
| 15 | 12, 14 | eqeq12d 2753 |
. 2
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘(𝑥 × 𝐵)) = ((♯‘𝑥) · (♯‘𝐵)) ↔ (♯‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵)))) |
| 16 | | xpeq1 5699 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝑥 × 𝐵) = (𝐴 × 𝐵)) |
| 17 | 16 | fveq2d 6910 |
. . 3
⊢ (𝑥 = 𝐴 → (♯‘(𝑥 × 𝐵)) = (♯‘(𝐴 × 𝐵))) |
| 18 | | fveq2 6906 |
. . . 4
⊢ (𝑥 = 𝐴 → (♯‘𝑥) = (♯‘𝐴)) |
| 19 | 18 | oveq1d 7446 |
. . 3
⊢ (𝑥 = 𝐴 → ((♯‘𝑥) · (♯‘𝐵)) = ((♯‘𝐴) · (♯‘𝐵))) |
| 20 | 17, 19 | eqeq12d 2753 |
. 2
⊢ (𝑥 = 𝐴 → ((♯‘(𝑥 × 𝐵)) = ((♯‘𝑥) · (♯‘𝐵)) ↔ (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) · (♯‘𝐵)))) |
| 21 | | hashxplem.1 |
. . . 4
⊢ 𝐵 ∈ Fin |
| 22 | | hashcl 14395 |
. . . . . 6
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℕ0) |
| 23 | 22 | nn0cnd 12589 |
. . . . 5
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℂ) |
| 24 | 23 | mul02d 11459 |
. . . 4
⊢ (𝐵 ∈ Fin → (0 ·
(♯‘𝐵)) =
0) |
| 25 | 21, 24 | ax-mp 5 |
. . 3
⊢ (0
· (♯‘𝐵))
= 0 |
| 26 | | hash0 14406 |
. . . 4
⊢
(♯‘∅) = 0 |
| 27 | 26 | oveq1i 7441 |
. . 3
⊢
((♯‘∅) · (♯‘𝐵)) = (0 · (♯‘𝐵)) |
| 28 | | 0xp 5784 |
. . . . 5
⊢ (∅
× 𝐵) =
∅ |
| 29 | 28 | fveq2i 6909 |
. . . 4
⊢
(♯‘(∅ × 𝐵)) =
(♯‘∅) |
| 30 | 29, 26 | eqtri 2765 |
. . 3
⊢
(♯‘(∅ × 𝐵)) = 0 |
| 31 | 25, 27, 30 | 3eqtr4ri 2776 |
. 2
⊢
(♯‘(∅ × 𝐵)) = ((♯‘∅) ·
(♯‘𝐵)) |
| 32 | | oveq1 7438 |
. . . . 5
⊢
((♯‘(𝑦
× 𝐵)) =
((♯‘𝑦) ·
(♯‘𝐵)) →
((♯‘(𝑦 ×
𝐵)) + (♯‘𝐵)) = (((♯‘𝑦) · (♯‘𝐵)) + (♯‘𝐵))) |
| 33 | 32 | adantl 481 |
. . . 4
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (♯‘(𝑦 × 𝐵)) = ((♯‘𝑦) · (♯‘𝐵))) → ((♯‘(𝑦 × 𝐵)) + (♯‘𝐵)) = (((♯‘𝑦) · (♯‘𝐵)) + (♯‘𝐵))) |
| 34 | | xpundir 5755 |
. . . . . . 7
⊢ ((𝑦 ∪ {𝑧}) × 𝐵) = ((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵)) |
| 35 | 34 | fveq2i 6909 |
. . . . . 6
⊢
(♯‘((𝑦
∪ {𝑧}) × 𝐵)) = (♯‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))) |
| 36 | | xpfi 9358 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝑦 × 𝐵) ∈ Fin) |
| 37 | 21, 36 | mpan2 691 |
. . . . . . . 8
⊢ (𝑦 ∈ Fin → (𝑦 × 𝐵) ∈ Fin) |
| 38 | | inxp 5842 |
. . . . . . . . 9
⊢ ((𝑦 × 𝐵) ∩ ({𝑧} × 𝐵)) = ((𝑦 ∩ {𝑧}) × (𝐵 ∩ 𝐵)) |
| 39 | | disjsn 4711 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦) |
| 40 | 39 | biimpri 228 |
. . . . . . . . . . 11
⊢ (¬
𝑧 ∈ 𝑦 → (𝑦 ∩ {𝑧}) = ∅) |
| 41 | 40 | xpeq1d 5714 |
. . . . . . . . . 10
⊢ (¬
𝑧 ∈ 𝑦 → ((𝑦 ∩ {𝑧}) × (𝐵 ∩ 𝐵)) = (∅ × (𝐵 ∩ 𝐵))) |
| 42 | | 0xp 5784 |
. . . . . . . . . 10
⊢ (∅
× (𝐵 ∩ 𝐵)) = ∅ |
| 43 | 41, 42 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (¬
𝑧 ∈ 𝑦 → ((𝑦 ∩ {𝑧}) × (𝐵 ∩ 𝐵)) = ∅) |
| 44 | 38, 43 | eqtrid 2789 |
. . . . . . . 8
⊢ (¬
𝑧 ∈ 𝑦 → ((𝑦 × 𝐵) ∩ ({𝑧} × 𝐵)) = ∅) |
| 45 | | snfi 9083 |
. . . . . . . . . 10
⊢ {𝑧} ∈ Fin |
| 46 | | xpfi 9358 |
. . . . . . . . . 10
⊢ (({𝑧} ∈ Fin ∧ 𝐵 ∈ Fin) → ({𝑧} × 𝐵) ∈ Fin) |
| 47 | 45, 21, 46 | mp2an 692 |
. . . . . . . . 9
⊢ ({𝑧} × 𝐵) ∈ Fin |
| 48 | | hashun 14421 |
. . . . . . . . 9
⊢ (((𝑦 × 𝐵) ∈ Fin ∧ ({𝑧} × 𝐵) ∈ Fin ∧ ((𝑦 × 𝐵) ∩ ({𝑧} × 𝐵)) = ∅) → (♯‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))) = ((♯‘(𝑦 × 𝐵)) + (♯‘({𝑧} × 𝐵)))) |
| 49 | 47, 48 | mp3an2 1451 |
. . . . . . . 8
⊢ (((𝑦 × 𝐵) ∈ Fin ∧ ((𝑦 × 𝐵) ∩ ({𝑧} × 𝐵)) = ∅) → (♯‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))) = ((♯‘(𝑦 × 𝐵)) + (♯‘({𝑧} × 𝐵)))) |
| 50 | 37, 44, 49 | syl2an 596 |
. . . . . . 7
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (♯‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))) = ((♯‘(𝑦 × 𝐵)) + (♯‘({𝑧} × 𝐵)))) |
| 51 | | snex 5436 |
. . . . . . . . . . 11
⊢ {𝑧} ∈ V |
| 52 | 21 | elexi 3503 |
. . . . . . . . . . 11
⊢ 𝐵 ∈ V |
| 53 | 51, 52 | xpcomen 9103 |
. . . . . . . . . 10
⊢ ({𝑧} × 𝐵) ≈ (𝐵 × {𝑧}) |
| 54 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
| 55 | 52, 54 | xpsnen 9095 |
. . . . . . . . . 10
⊢ (𝐵 × {𝑧}) ≈ 𝐵 |
| 56 | 53, 55 | entri 9048 |
. . . . . . . . 9
⊢ ({𝑧} × 𝐵) ≈ 𝐵 |
| 57 | | hashen 14386 |
. . . . . . . . . 10
⊢ ((({𝑧} × 𝐵) ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘({𝑧} × 𝐵)) = (♯‘𝐵) ↔ ({𝑧} × 𝐵) ≈ 𝐵)) |
| 58 | 47, 21, 57 | mp2an 692 |
. . . . . . . . 9
⊢
((♯‘({𝑧}
× 𝐵)) =
(♯‘𝐵) ↔
({𝑧} × 𝐵) ≈ 𝐵) |
| 59 | 56, 58 | mpbir 231 |
. . . . . . . 8
⊢
(♯‘({𝑧}
× 𝐵)) =
(♯‘𝐵) |
| 60 | 59 | oveq2i 7442 |
. . . . . . 7
⊢
((♯‘(𝑦
× 𝐵)) +
(♯‘({𝑧} ×
𝐵))) =
((♯‘(𝑦 ×
𝐵)) + (♯‘𝐵)) |
| 61 | 50, 60 | eqtrdi 2793 |
. . . . . 6
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (♯‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))) = ((♯‘(𝑦 × 𝐵)) + (♯‘𝐵))) |
| 62 | 35, 61 | eqtrid 2789 |
. . . . 5
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (♯‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((♯‘(𝑦 × 𝐵)) + (♯‘𝐵))) |
| 63 | 62 | adantr 480 |
. . . 4
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (♯‘(𝑦 × 𝐵)) = ((♯‘𝑦) · (♯‘𝐵))) → (♯‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((♯‘(𝑦 × 𝐵)) + (♯‘𝐵))) |
| 64 | | hashunsng 14431 |
. . . . . . . 8
⊢ (𝑧 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))) |
| 65 | 54, 64 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)) |
| 66 | 65 | oveq1d 7446 |
. . . . . 6
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵)) = (((♯‘𝑦) + 1) · (♯‘𝐵))) |
| 67 | | hashcl 14395 |
. . . . . . . . . 10
⊢ (𝑦 ∈ Fin →
(♯‘𝑦) ∈
ℕ0) |
| 68 | 67 | nn0cnd 12589 |
. . . . . . . . 9
⊢ (𝑦 ∈ Fin →
(♯‘𝑦) ∈
ℂ) |
| 69 | | ax-1cn 11213 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
| 70 | | nn0cn 12536 |
. . . . . . . . . . 11
⊢
((♯‘𝐵)
∈ ℕ0 → (♯‘𝐵) ∈ ℂ) |
| 71 | 21, 22, 70 | mp2b 10 |
. . . . . . . . . 10
⊢
(♯‘𝐵)
∈ ℂ |
| 72 | | adddir 11252 |
. . . . . . . . . 10
⊢
(((♯‘𝑦)
∈ ℂ ∧ 1 ∈ ℂ ∧ (♯‘𝐵) ∈ ℂ) →
(((♯‘𝑦) + 1)
· (♯‘𝐵))
= (((♯‘𝑦)
· (♯‘𝐵))
+ (1 · (♯‘𝐵)))) |
| 73 | 69, 71, 72 | mp3an23 1455 |
. . . . . . . . 9
⊢
((♯‘𝑦)
∈ ℂ → (((♯‘𝑦) + 1) · (♯‘𝐵)) = (((♯‘𝑦) · (♯‘𝐵)) + (1 ·
(♯‘𝐵)))) |
| 74 | 68, 73 | syl 17 |
. . . . . . . 8
⊢ (𝑦 ∈ Fin →
(((♯‘𝑦) + 1)
· (♯‘𝐵))
= (((♯‘𝑦)
· (♯‘𝐵))
+ (1 · (♯‘𝐵)))) |
| 75 | 71 | mullidi 11266 |
. . . . . . . . 9
⊢ (1
· (♯‘𝐵))
= (♯‘𝐵) |
| 76 | 75 | oveq2i 7442 |
. . . . . . . 8
⊢
(((♯‘𝑦)
· (♯‘𝐵))
+ (1 · (♯‘𝐵))) = (((♯‘𝑦) · (♯‘𝐵)) + (♯‘𝐵)) |
| 77 | 74, 76 | eqtrdi 2793 |
. . . . . . 7
⊢ (𝑦 ∈ Fin →
(((♯‘𝑦) + 1)
· (♯‘𝐵))
= (((♯‘𝑦)
· (♯‘𝐵))
+ (♯‘𝐵))) |
| 78 | 77 | adantr 480 |
. . . . . 6
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (((♯‘𝑦) + 1) · (♯‘𝐵)) = (((♯‘𝑦) · (♯‘𝐵)) + (♯‘𝐵))) |
| 79 | 66, 78 | eqtrd 2777 |
. . . . 5
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵)) = (((♯‘𝑦) · (♯‘𝐵)) + (♯‘𝐵))) |
| 80 | 79 | adantr 480 |
. . . 4
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (♯‘(𝑦 × 𝐵)) = ((♯‘𝑦) · (♯‘𝐵))) → ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵)) = (((♯‘𝑦) · (♯‘𝐵)) + (♯‘𝐵))) |
| 81 | 33, 63, 80 | 3eqtr4d 2787 |
. . 3
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (♯‘(𝑦 × 𝐵)) = ((♯‘𝑦) · (♯‘𝐵))) → (♯‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵))) |
| 82 | 81 | ex 412 |
. 2
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((♯‘(𝑦 × 𝐵)) = ((♯‘𝑦) · (♯‘𝐵)) → (♯‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵)))) |
| 83 | 5, 10, 15, 20, 31, 82 | findcard2s 9205 |
1
⊢ (𝐴 ∈ Fin →
(♯‘(𝐴 ×
𝐵)) = ((♯‘𝐴) · (♯‘𝐵))) |