This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐵 ⊆ dom 𝐴 ) → ( ♯ ‘ 𝐴 ) = ( ( ♯ ‘ ( 𝐴 ↾ 𝐵 ) ) + ( ♯ ‘ ( dom 𝐴 ∖ 𝐵 ) ) ) )

Proof

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