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