Theorem iblsubnc

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

	Ref	Expression
Hypotheses	ibladdnc.1	|- ( ( ph /\ x e. A ) -> B e. V )
	ibladdnc.2	|- ( ph -> ( x e. A |-> B ) e. L^1 )
	ibladdnc.3	|- ( ( ph /\ x e. A ) -> C e. V )
	ibladdnc.4	|- ( ph -> ( x e. A |-> C ) e. L^1 )
	iblsubnc.m	|- ( ph -> ( x e. A |-> ( B - C ) ) e. MblFn )
Assertion	iblsubnc	|- ( ph -> ( x e. A |-> ( B - C ) ) e. L^1 )

Proof

Step	Hyp	Ref	Expression
1		ibladdnc.1	|- ( ( ph /\ x e. A ) -> B e. V )
2		ibladdnc.2	|- ( ph -> ( x e. A |-> B ) e. L^1 )
3		ibladdnc.3	|- ( ( ph /\ x e. A ) -> C e. V )
4		ibladdnc.4	|- ( ph -> ( x e. A |-> C ) e. L^1 )
5		iblsubnc.m	|- ( ph -> ( x e. A |-> ( B - C ) ) e. MblFn )
6		iblmbf	|- ( ( x e. A |-> B ) e. L^1 -> ( x e. A |-> B ) e. MblFn )
7	2 6	syl	|- ( ph -> ( x e. A |-> B ) e. MblFn )
8	7 1	mbfmptcl	|- ( ( ph /\ x e. A ) -> B e. CC )
9		iblmbf	|- ( ( x e. A |-> C ) e. L^1 -> ( x e. A |-> C ) e. MblFn )
10	4 9	syl	|- ( ph -> ( x e. A |-> C ) e. MblFn )
11	10 3	mbfmptcl	|- ( ( ph /\ x e. A ) -> C e. CC )
12	8 11	negsubd	|- ( ( ph /\ x e. A ) -> ( B + -u C ) = ( B - C ) )
13	12	mpteq2dva	|- ( ph -> ( x e. A |-> ( B + -u C ) ) = ( x e. A |-> ( B - C ) ) )
14	11	negcld	|- ( ( ph /\ x e. A ) -> -u C e. CC )
15	3 4	iblneg	|- ( ph -> ( x e. A |-> -u C ) e. L^1 )
16	13 5	eqeltrd	|- ( ph -> ( x e. A |-> ( B + -u C ) ) e. MblFn )
17	8 2 14 15 16	ibladdnc	|- ( ph -> ( x e. A |-> ( B + -u C ) ) e. L^1 )
18	13 17	eqeltrrd	|- ( ph -> ( x e. A |-> ( B - C ) ) e. L^1 )