Metamath Proof Explorer


Theorem itg1addlem1

Description: Decompose a preimage, which is always a disjoint union. (Contributed by Mario Carneiro, 25-Jun-2014) (Proof shortened by Mario Carneiro, 11-Dec-2016)

Ref Expression
Hypotheses itg1addlem.1
|- ( ph -> F : X --> Y )
itg1addlem.2
|- ( ph -> A e. Fin )
itg1addlem.3
|- ( ( ph /\ k e. A ) -> B C_ ( `' F " { k } ) )
itg1addlem.4
|- ( ( ph /\ k e. A ) -> B e. dom vol )
itg1addlem.5
|- ( ( ph /\ k e. A ) -> ( vol ` B ) e. RR )
Assertion itg1addlem1
|- ( ph -> ( vol ` U_ k e. A B ) = sum_ k e. A ( vol ` B ) )

Proof

Step Hyp Ref Expression
1 itg1addlem.1
 |-  ( ph -> F : X --> Y )
2 itg1addlem.2
 |-  ( ph -> A e. Fin )
3 itg1addlem.3
 |-  ( ( ph /\ k e. A ) -> B C_ ( `' F " { k } ) )
4 itg1addlem.4
 |-  ( ( ph /\ k e. A ) -> B e. dom vol )
5 itg1addlem.5
 |-  ( ( ph /\ k e. A ) -> ( vol ` B ) e. RR )
6 4 5 jca
 |-  ( ( ph /\ k e. A ) -> ( B e. dom vol /\ ( vol ` B ) e. RR ) )
7 6 ralrimiva
 |-  ( ph -> A. k e. A ( B e. dom vol /\ ( vol ` B ) e. RR ) )
8 3 adantrr
 |-  ( ( ph /\ ( k e. A /\ x e. B ) ) -> B C_ ( `' F " { k } ) )
9 simprr
 |-  ( ( ph /\ ( k e. A /\ x e. B ) ) -> x e. B )
10 8 9 sseldd
 |-  ( ( ph /\ ( k e. A /\ x e. B ) ) -> x e. ( `' F " { k } ) )
11 1 ffnd
 |-  ( ph -> F Fn X )
12 11 adantr
 |-  ( ( ph /\ ( k e. A /\ x e. B ) ) -> F Fn X )
13 fniniseg
 |-  ( F Fn X -> ( x e. ( `' F " { k } ) <-> ( x e. X /\ ( F ` x ) = k ) ) )
14 12 13 syl
 |-  ( ( ph /\ ( k e. A /\ x e. B ) ) -> ( x e. ( `' F " { k } ) <-> ( x e. X /\ ( F ` x ) = k ) ) )
15 10 14 mpbid
 |-  ( ( ph /\ ( k e. A /\ x e. B ) ) -> ( x e. X /\ ( F ` x ) = k ) )
16 15 simprd
 |-  ( ( ph /\ ( k e. A /\ x e. B ) ) -> ( F ` x ) = k )
17 16 ralrimivva
 |-  ( ph -> A. k e. A A. x e. B ( F ` x ) = k )
18 invdisj
 |-  ( A. k e. A A. x e. B ( F ` x ) = k -> Disj_ k e. A B )
19 17 18 syl
 |-  ( ph -> Disj_ k e. A B )
20 volfiniun
 |-  ( ( A e. Fin /\ A. k e. A ( B e. dom vol /\ ( vol ` B ) e. RR ) /\ Disj_ k e. A B ) -> ( vol ` U_ k e. A B ) = sum_ k e. A ( vol ` B ) )
21 2 7 19 20 syl3anc
 |-  ( ph -> ( vol ` U_ k e. A B ) = sum_ k e. A ( vol ` B ) )