Step |
Hyp |
Ref |
Expression |
1 |
|
hash2iun1dif1.a |
|- ( ph -> A e. Fin ) |
2 |
|
hash2iun1dif1.b |
|- B = ( A \ { x } ) |
3 |
|
hash2iun1dif1.c |
|- ( ( ph /\ x e. A /\ y e. B ) -> C e. Fin ) |
4 |
|
hash2iun1dif1.da |
|- ( ph -> Disj_ x e. A U_ y e. B C ) |
5 |
|
hash2iun1dif1.db |
|- ( ( ph /\ x e. A ) -> Disj_ y e. B C ) |
6 |
|
hash2iun1dif1.1 |
|- ( ( ph /\ x e. A /\ y e. B ) -> ( # ` C ) = 1 ) |
7 |
|
diffi |
|- ( A e. Fin -> ( A \ { x } ) e. Fin ) |
8 |
1 7
|
syl |
|- ( ph -> ( A \ { x } ) e. Fin ) |
9 |
8
|
adantr |
|- ( ( ph /\ x e. A ) -> ( A \ { x } ) e. Fin ) |
10 |
2 9
|
eqeltrid |
|- ( ( ph /\ x e. A ) -> B e. Fin ) |
11 |
1 10 3 4 5
|
hash2iun |
|- ( ph -> ( # ` U_ x e. A U_ y e. B C ) = sum_ x e. A sum_ y e. B ( # ` C ) ) |
12 |
6
|
2sumeq2dv |
|- ( ph -> sum_ x e. A sum_ y e. B ( # ` C ) = sum_ x e. A sum_ y e. B 1 ) |
13 |
|
1cnd |
|- ( ( ph /\ x e. A ) -> 1 e. CC ) |
14 |
|
fsumconst |
|- ( ( B e. Fin /\ 1 e. CC ) -> sum_ y e. B 1 = ( ( # ` B ) x. 1 ) ) |
15 |
10 13 14
|
syl2anc |
|- ( ( ph /\ x e. A ) -> sum_ y e. B 1 = ( ( # ` B ) x. 1 ) ) |
16 |
15
|
sumeq2dv |
|- ( ph -> sum_ x e. A sum_ y e. B 1 = sum_ x e. A ( ( # ` B ) x. 1 ) ) |
17 |
2
|
a1i |
|- ( ( ph /\ x e. A ) -> B = ( A \ { x } ) ) |
18 |
17
|
fveq2d |
|- ( ( ph /\ x e. A ) -> ( # ` B ) = ( # ` ( A \ { x } ) ) ) |
19 |
|
hashdifsn |
|- ( ( A e. Fin /\ x e. A ) -> ( # ` ( A \ { x } ) ) = ( ( # ` A ) - 1 ) ) |
20 |
1 19
|
sylan |
|- ( ( ph /\ x e. A ) -> ( # ` ( A \ { x } ) ) = ( ( # ` A ) - 1 ) ) |
21 |
18 20
|
eqtrd |
|- ( ( ph /\ x e. A ) -> ( # ` B ) = ( ( # ` A ) - 1 ) ) |
22 |
21
|
oveq1d |
|- ( ( ph /\ x e. A ) -> ( ( # ` B ) x. 1 ) = ( ( ( # ` A ) - 1 ) x. 1 ) ) |
23 |
22
|
sumeq2dv |
|- ( ph -> sum_ x e. A ( ( # ` B ) x. 1 ) = sum_ x e. A ( ( ( # ` A ) - 1 ) x. 1 ) ) |
24 |
|
hashcl |
|- ( A e. Fin -> ( # ` A ) e. NN0 ) |
25 |
1 24
|
syl |
|- ( ph -> ( # ` A ) e. NN0 ) |
26 |
25
|
nn0cnd |
|- ( ph -> ( # ` A ) e. CC ) |
27 |
|
peano2cnm |
|- ( ( # ` A ) e. CC -> ( ( # ` A ) - 1 ) e. CC ) |
28 |
26 27
|
syl |
|- ( ph -> ( ( # ` A ) - 1 ) e. CC ) |
29 |
28
|
mulid1d |
|- ( ph -> ( ( ( # ` A ) - 1 ) x. 1 ) = ( ( # ` A ) - 1 ) ) |
30 |
29
|
sumeq2sdv |
|- ( ph -> sum_ x e. A ( ( ( # ` A ) - 1 ) x. 1 ) = sum_ x e. A ( ( # ` A ) - 1 ) ) |
31 |
|
fsumconst |
|- ( ( A e. Fin /\ ( ( # ` A ) - 1 ) e. CC ) -> sum_ x e. A ( ( # ` A ) - 1 ) = ( ( # ` A ) x. ( ( # ` A ) - 1 ) ) ) |
32 |
1 28 31
|
syl2anc |
|- ( ph -> sum_ x e. A ( ( # ` A ) - 1 ) = ( ( # ` A ) x. ( ( # ` A ) - 1 ) ) ) |
33 |
30 32
|
eqtrd |
|- ( ph -> sum_ x e. A ( ( ( # ` A ) - 1 ) x. 1 ) = ( ( # ` A ) x. ( ( # ` A ) - 1 ) ) ) |
34 |
16 23 33
|
3eqtrd |
|- ( ph -> sum_ x e. A sum_ y e. B 1 = ( ( # ` A ) x. ( ( # ` A ) - 1 ) ) ) |
35 |
11 12 34
|
3eqtrd |
|- ( ph -> ( # ` U_ x e. A U_ y e. B C ) = ( ( # ` A ) x. ( ( # ` A ) - 1 ) ) ) |