Metamath Proof Explorer

Theorem hashreshashfun

Description: The number of elements of a finite function expressed by a restriction. (Contributed by AV, 15-Dec-2021)

Ref Expression
Assertion hashreshashfun ⊢ Fun ⁡ A ∧ A ∈ Fin ∧ B ⊆ dom ⁡ A → A = A ↾ B + dom ⁡ A ∖ B

Proof

Step Hyp Ref Expression
1 simp1 ⊢ Fun ⁡ A ∧ A ∈ Fin ∧ B ⊆ dom ⁡ A → Fun ⁡ A
2 hashfun ⊢ A ∈ Fin → Fun ⁡ A ↔ A = dom ⁡ A
3 2 3ad2ant2 ⊢ Fun ⁡ A ∧ A ∈ Fin ∧ B ⊆ dom ⁡ A → Fun ⁡ A ↔ A = dom ⁡ A
4 1 3 mpbid ⊢ Fun ⁡ A ∧ A ∈ Fin ∧ B ⊆ dom ⁡ A → A = dom ⁡ A
5 dmfi ⊢ A ∈ Fin → dom ⁡ A ∈ Fin
6 5 anim1i ⊢ A ∈ Fin ∧ B ⊆ dom ⁡ A → dom ⁡ A ∈ Fin ∧ B ⊆ dom ⁡ A
7 6 3adant1 ⊢ Fun ⁡ A ∧ A ∈ Fin ∧ B ⊆ dom ⁡ A → dom ⁡ A ∈ Fin ∧ B ⊆ dom ⁡ A
8 hashssdif ⊢ dom ⁡ A ∈ Fin ∧ B ⊆ dom ⁡ A → dom ⁡ A ∖ B = dom ⁡ A − B
9 7 8 syl ⊢ Fun ⁡ A ∧ A ∈ Fin ∧ B ⊆ dom ⁡ A → dom ⁡ A ∖ B = dom ⁡ A − B
10 9 oveq2d ⊢ Fun ⁡ A ∧ A ∈ Fin ∧ B ⊆ dom ⁡ A → B + dom ⁡ A ∖ B = B + dom ⁡ A - B
11 ssfi ⊢ dom ⁡ A ∈ Fin ∧ B ⊆ dom ⁡ A → B ∈ Fin
12 11 ex ⊢ dom ⁡ A ∈ Fin → B ⊆ dom ⁡ A → B ∈ Fin
13 hashcl ⊢ B ∈ Fin → B ∈ ℕ 0
14 13 nn0cnd ⊢ B ∈ Fin → B ∈ ℂ
15 12 14 syl6 ⊢ dom ⁡ A ∈ Fin → B ⊆ dom ⁡ A → B ∈ ℂ
16 5 15 syl ⊢ A ∈ Fin → B ⊆ dom ⁡ A → B ∈ ℂ
17 16 imp ⊢ A ∈ Fin ∧ B ⊆ dom ⁡ A → B ∈ ℂ
18 hashcl ⊢ dom ⁡ A ∈ Fin → dom ⁡ A ∈ ℕ 0
19 5 18 syl ⊢ A ∈ Fin → dom ⁡ A ∈ ℕ 0
20 19 nn0cnd ⊢ A ∈ Fin → dom ⁡ A ∈ ℂ
21 20 adantr ⊢ A ∈ Fin ∧ B ⊆ dom ⁡ A → dom ⁡ A ∈ ℂ
22 17 21 jca ⊢ A ∈ Fin ∧ B ⊆ dom ⁡ A → B ∈ ℂ ∧ dom ⁡ A ∈ ℂ
23 22 3adant1 ⊢ Fun ⁡ A ∧ A ∈ Fin ∧ B ⊆ dom ⁡ A → B ∈ ℂ ∧ dom ⁡ A ∈ ℂ
24 pncan3 ⊢ B ∈ ℂ ∧ dom ⁡ A ∈ ℂ → B + dom ⁡ A - B = dom ⁡ A
25 23 24 syl ⊢ Fun ⁡ A ∧ A ∈ Fin ∧ B ⊆ dom ⁡ A → B + dom ⁡ A - B = dom ⁡ A
26 10 25 eqtr2d ⊢ Fun ⁡ A ∧ A ∈ Fin ∧ B ⊆ dom ⁡ A → dom ⁡ A = B + dom ⁡ A ∖ B
27 hashres ⊢ Fun ⁡ A ∧ A ∈ Fin ∧ B ⊆ dom ⁡ A → A ↾ B = B
28 27 eqcomd ⊢ Fun ⁡ A ∧ A ∈ Fin ∧ B ⊆ dom ⁡ A → B = A ↾ B
29 28 oveq1d ⊢ Fun ⁡ A ∧ A ∈ Fin ∧ B ⊆ dom ⁡ A → B + dom ⁡ A ∖ B = A ↾ B + dom ⁡ A ∖ B
30 4 26 29 3eqtrd ⊢ Fun ⁡ A ∧ A ∈ Fin ∧ B ⊆ dom ⁡ A → A = A ↾ B + dom ⁡ A ∖ B