Metamath Proof Explorer


Theorem hash2iun1dif1

Description: The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022)

Ref Expression
Hypotheses hash2iun1dif1.a
|- ( ph -> A e. Fin )
hash2iun1dif1.b
|- B = ( A \ { x } )
hash2iun1dif1.c
|- ( ( ph /\ x e. A /\ y e. B ) -> C e. Fin )
hash2iun1dif1.da
|- ( ph -> Disj_ x e. A U_ y e. B C )
hash2iun1dif1.db
|- ( ( ph /\ x e. A ) -> Disj_ y e. B C )
hash2iun1dif1.1
|- ( ( ph /\ x e. A /\ y e. B ) -> ( # ` C ) = 1 )
Assertion hash2iun1dif1
|- ( ph -> ( # ` U_ x e. A U_ y e. B C ) = ( ( # ` A ) x. ( ( # ` A ) - 1 ) ) )

Proof

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 ) ) )