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

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