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