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	$⊢ φ \to F : X ⟶ Y$
	itg1addlem.2	$⊢ φ \to A \in Fin$
	itg1addlem.3	$⊢ (φ \land k \in A) \to B \subseteq F^{-1} [\{k\}]$
	itg1addlem.4	$⊢ (φ \land k \in A) \to B \in dom vol$
	itg1addlem.5	$⊢ (φ \land k \in A) \to vol (B) \in ℝ$
Assertion	itg1addlem1	$⊢ φ \to vol (⋃_{k \in A} B) = \sum_{k \in A} vol (B)$

Proof

Step	Hyp	Ref	Expression
1		itg1addlem.1	$⊢ φ \to F : X ⟶ Y$
2		itg1addlem.2	$⊢ φ \to A \in Fin$
3		itg1addlem.3	$⊢ (φ \land k \in A) \to B \subseteq F^{-1} [\{k\}]$
4		itg1addlem.4	$⊢ (φ \land k \in A) \to B \in dom vol$
5		itg1addlem.5	$⊢ (φ \land k \in A) \to vol (B) \in ℝ$
6	4 5	jca	$⊢ (φ \land k \in A) \to (B \in dom vol \land vol (B) \in ℝ)$
7	6	ralrimiva	$⊢ φ \to \forall k \in A (B \in dom vol \land vol (B) \in ℝ)$
8	3	adantrr	$⊢ (φ \land (k \in A \land x \in B)) \to B \subseteq F^{-1} [\{k\}]$
9		simprr	$⊢ (φ \land (k \in A \land x \in B)) \to x \in B$
10	8 9	sseldd	$⊢ (φ \land (k \in A \land x \in B)) \to x \in F^{-1} [\{k\}]$
11	1	ffnd	$⊢ φ \to F Fn X$
12	11	adantr	$⊢ (φ \land (k \in A \land x \in B)) \to F Fn X$
13		fniniseg	$⊢ F Fn X \to (x \in F^{-1} [\{k\}] \leftrightarrow (x \in X \land F (x) = k))$
14	12 13	syl	$⊢ (φ \land (k \in A \land x \in B)) \to (x \in F^{-1} [\{k\}] \leftrightarrow (x \in X \land F (x) = k))$
15	10 14	mpbid	$⊢ (φ \land (k \in A \land x \in B)) \to (x \in X \land F (x) = k)$
16	15	simprd	$⊢ (φ \land (k \in A \land x \in B)) \to F (x) = k$
17	16	ralrimivva	$⊢ φ \to \forall k \in A \forall x \in B F (x) = k$
18		invdisj	$⊢ \forall k \in A \forall x \in B F (x) = k \to \underset{k \in A}{Disj} B$
19	17 18	syl	$⊢ φ \to \underset{k \in A}{Disj} B$
20		volfiniun	$⊢ (A \in Fin \land \forall k \in A (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in A}{Disj} B) \to vol (⋃_{k \in A} B) = \sum_{k \in A} vol (B)$
21	2 7 19 20	syl3anc	$⊢ φ \to vol (⋃_{k \in A} B) = \sum_{k \in A} vol (B)$

Metamath Proof Explorer

Theorem itg1addlem1

Proof