Step |
Hyp |
Ref |
Expression |
1 |
|
simp1 |
|- ( ( Fun A /\ A e. Fin /\ B C_ dom A ) -> Fun A ) |
2 |
|
hashfun |
|- ( A e. Fin -> ( Fun A <-> ( # ` A ) = ( # ` dom A ) ) ) |
3 |
2
|
3ad2ant2 |
|- ( ( Fun A /\ A e. Fin /\ B C_ dom A ) -> ( Fun A <-> ( # ` A ) = ( # ` dom A ) ) ) |
4 |
1 3
|
mpbid |
|- ( ( Fun A /\ A e. Fin /\ B C_ dom A ) -> ( # ` A ) = ( # ` dom A ) ) |
5 |
|
dmfi |
|- ( A e. Fin -> dom A e. Fin ) |
6 |
5
|
anim1i |
|- ( ( A e. Fin /\ B C_ dom A ) -> ( dom A e. Fin /\ B C_ dom A ) ) |
7 |
6
|
3adant1 |
|- ( ( Fun A /\ A e. Fin /\ B C_ dom A ) -> ( dom A e. Fin /\ B C_ dom A ) ) |
8 |
|
hashssdif |
|- ( ( dom A e. Fin /\ B C_ dom A ) -> ( # ` ( dom A \ B ) ) = ( ( # ` dom A ) - ( # ` B ) ) ) |
9 |
7 8
|
syl |
|- ( ( Fun A /\ A e. Fin /\ B C_ dom A ) -> ( # ` ( dom A \ B ) ) = ( ( # ` dom A ) - ( # ` B ) ) ) |
10 |
9
|
oveq2d |
|- ( ( Fun A /\ A e. Fin /\ B C_ dom A ) -> ( ( # ` B ) + ( # ` ( dom A \ B ) ) ) = ( ( # ` B ) + ( ( # ` dom A ) - ( # ` B ) ) ) ) |
11 |
|
ssfi |
|- ( ( dom A e. Fin /\ B C_ dom A ) -> B e. Fin ) |
12 |
11
|
ex |
|- ( dom A e. Fin -> ( B C_ dom A -> B e. Fin ) ) |
13 |
|
hashcl |
|- ( B e. Fin -> ( # ` B ) e. NN0 ) |
14 |
13
|
nn0cnd |
|- ( B e. Fin -> ( # ` B ) e. CC ) |
15 |
12 14
|
syl6 |
|- ( dom A e. Fin -> ( B C_ dom A -> ( # ` B ) e. CC ) ) |
16 |
5 15
|
syl |
|- ( A e. Fin -> ( B C_ dom A -> ( # ` B ) e. CC ) ) |
17 |
16
|
imp |
|- ( ( A e. Fin /\ B C_ dom A ) -> ( # ` B ) e. CC ) |
18 |
|
hashcl |
|- ( dom A e. Fin -> ( # ` dom A ) e. NN0 ) |
19 |
5 18
|
syl |
|- ( A e. Fin -> ( # ` dom A ) e. NN0 ) |
20 |
19
|
nn0cnd |
|- ( A e. Fin -> ( # ` dom A ) e. CC ) |
21 |
20
|
adantr |
|- ( ( A e. Fin /\ B C_ dom A ) -> ( # ` dom A ) e. CC ) |
22 |
17 21
|
jca |
|- ( ( A e. Fin /\ B C_ dom A ) -> ( ( # ` B ) e. CC /\ ( # ` dom A ) e. CC ) ) |
23 |
22
|
3adant1 |
|- ( ( Fun A /\ A e. Fin /\ B C_ dom A ) -> ( ( # ` B ) e. CC /\ ( # ` dom A ) e. CC ) ) |
24 |
|
pncan3 |
|- ( ( ( # ` B ) e. CC /\ ( # ` dom A ) e. CC ) -> ( ( # ` B ) + ( ( # ` dom A ) - ( # ` B ) ) ) = ( # ` dom A ) ) |
25 |
23 24
|
syl |
|- ( ( Fun A /\ A e. Fin /\ B C_ dom A ) -> ( ( # ` B ) + ( ( # ` dom A ) - ( # ` B ) ) ) = ( # ` dom A ) ) |
26 |
10 25
|
eqtr2d |
|- ( ( Fun A /\ A e. Fin /\ B C_ dom A ) -> ( # ` dom A ) = ( ( # ` B ) + ( # ` ( dom A \ B ) ) ) ) |
27 |
|
hashres |
|- ( ( Fun A /\ A e. Fin /\ B C_ dom A ) -> ( # ` ( A |` B ) ) = ( # ` B ) ) |
28 |
27
|
eqcomd |
|- ( ( Fun A /\ A e. Fin /\ B C_ dom A ) -> ( # ` B ) = ( # ` ( A |` B ) ) ) |
29 |
28
|
oveq1d |
|- ( ( Fun A /\ A e. Fin /\ B C_ dom A ) -> ( ( # ` B ) + ( # ` ( dom A \ B ) ) ) = ( ( # ` ( A |` B ) ) + ( # ` ( dom A \ B ) ) ) ) |
30 |
4 26 29
|
3eqtrd |
|- ( ( Fun A /\ A e. Fin /\ B C_ dom A ) -> ( # ` A ) = ( ( # ` ( A |` B ) ) + ( # ` ( dom A \ B ) ) ) ) |