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	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
	itg1addlem.2	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	itg1addlem.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ⊆ ( ◡ 𝐹 “ { 𝑘 } ) )
	itg1addlem.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ dom vol )
	itg1addlem.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( vol ‘ 𝐵 ) ∈ ℝ )
Assertion	itg1addlem1	⊢ ( 𝜑 → ( vol ‘ ∪ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( vol ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		itg1addlem.1	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
2		itg1addlem.2	⊢ ( 𝜑 → 𝐴 ∈ Fin )
3		itg1addlem.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ⊆ ( ◡ 𝐹 “ { 𝑘 } ) )
4		itg1addlem.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ dom vol )
5		itg1addlem.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( vol ‘ 𝐵 ) ∈ ℝ )
6	4 5	jca	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) )
7	6	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) )
8	3	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) → 𝐵 ⊆ ( ◡ 𝐹 “ { 𝑘 } ) )
9		simprr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
10	8 9	sseldd	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) → 𝑥 ∈ ( ◡ 𝐹 “ { 𝑘 } ) )
11	1	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
12	11	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) → 𝐹 Fn 𝑋 )
13		fniniseg	⊢ ( 𝐹 Fn 𝑋 → ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑘 } ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) )
14	12 13	syl	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑘 } ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) ) )
15	10 14	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑘 ) )
16	15	simprd	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) = 𝑘 )
17	16	ralrimivva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝑘 )
18		invdisj	⊢ ( ∀ 𝑘 ∈ 𝐴 ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝑘 → Disj 𝑘 ∈ 𝐴 𝐵 )
19	17 18	syl	⊢ ( 𝜑 → Disj 𝑘 ∈ 𝐴 𝐵 )
20		volfiniun	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑘 ∈ 𝐴 ( 𝐵 ∈ dom vol ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ∧ Disj 𝑘 ∈ 𝐴 𝐵 ) → ( vol ‘ ∪ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( vol ‘ 𝐵 ) )
21	2 7 19 20	syl3anc	⊢ ( 𝜑 → ( vol ‘ ∪ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( vol ‘ 𝐵 ) )