Theorem iblsubnc

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

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

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	8 11	negsubd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + - 𝐶 ) = ( 𝐵 − 𝐶 ) )
13	12	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + - 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 − 𝐶 ) ) )
14	11	negcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐶 ∈ ℂ )
15	3 4	iblneg	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - 𝐶 ) ∈ 𝐿1 )
16	13 5	eqeltrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + - 𝐶 ) ) ∈ MblFn )
17	8 2 14 15 16	ibladdnc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + - 𝐶 ) ) ∈ 𝐿1 )
18	13 17	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 − 𝐶 ) ) ∈ 𝐿1 )