Theorem itgsubnc

Description: Choice-free analogue of itgsub . (Contributed by Brendan Leahy, 11-Nov-2017)

	Ref	Expression
Hypotheses	ibladdnc.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
	ibladdnc.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
	ibladdnc.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
	ibladdnc.4	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
	iblsubnc.m	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 − 𝐶 ) ) ∈ MblFn )
Assertion	itgsubnc	⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 − 𝐶 ) d 𝑥 = ( ∫ 𝐴 𝐵 d 𝑥 − ∫ 𝐴 𝐶 d 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		ibladdnc.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2		ibladdnc.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
3		ibladdnc.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
4		ibladdnc.4	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
5		iblsubnc.m	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 − 𝐶 ) ) ∈ MblFn )
6		iblmbf	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
7	2 6	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
8	7 1	mbfmptcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
9		iblmbf	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
10	4 9	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
11	10 3	mbfmptcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
12	11	negcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐶 ∈ ℂ )
13	3 4	iblneg	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - 𝐶 ) ∈ 𝐿1 )
14	8 11	negsubd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + - 𝐶 ) = ( 𝐵 − 𝐶 ) )
15	14	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + - 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 − 𝐶 ) ) )
16	15 5	eqeltrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + - 𝐶 ) ) ∈ MblFn )
17	8 2 12 13 16	itgaddnc	⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 + - 𝐶 ) d 𝑥 = ( ∫ 𝐴 𝐵 d 𝑥 + ∫ 𝐴 - 𝐶 d 𝑥 ) )
18	3 4	itgneg	⊢ ( 𝜑 → - ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐴 - 𝐶 d 𝑥 )
19	18	oveq2d	⊢ ( 𝜑 → ( ∫ 𝐴 𝐵 d 𝑥 + - ∫ 𝐴 𝐶 d 𝑥 ) = ( ∫ 𝐴 𝐵 d 𝑥 + ∫ 𝐴 - 𝐶 d 𝑥 ) )
20	17 19	eqtr4d	⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 + - 𝐶 ) d 𝑥 = ( ∫ 𝐴 𝐵 d 𝑥 + - ∫ 𝐴 𝐶 d 𝑥 ) )
21	14	itgeq2dv	⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 + - 𝐶 ) d 𝑥 = ∫ 𝐴 ( 𝐵 − 𝐶 ) d 𝑥 )
22	1 2	itgcl	⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 ∈ ℂ )
23	3 4	itgcl	⊢ ( 𝜑 → ∫ 𝐴 𝐶 d 𝑥 ∈ ℂ )
24	22 23	negsubd	⊢ ( 𝜑 → ( ∫ 𝐴 𝐵 d 𝑥 + - ∫ 𝐴 𝐶 d 𝑥 ) = ( ∫ 𝐴 𝐵 d 𝑥 − ∫ 𝐴 𝐶 d 𝑥 ) )
25	20 21 24	3eqtr3d	⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 − 𝐶 ) d 𝑥 = ( ∫ 𝐴 𝐵 d 𝑥 − ∫ 𝐴 𝐶 d 𝑥 ) )