itgsubstlem

	Ref	Expression
Hypotheses	itgsubst.x	\|- ( ph -> X e. RR )
	itgsubst.y	\|- ( ph -> Y e. RR )
	itgsubst.le	\|- ( ph -> X <_ Y )
	itgsubst.z	\|- ( ph -> Z e. RR* )
	itgsubst.w	\|- ( ph -> W e. RR* )
	itgsubst.a	\|- ( ph -> ( x e. ( X [,] Y ) \|-> A ) e. ( ( X [,] Y ) -cn-> ( Z (,) W ) ) )
	itgsubst.b	\|- ( ph -> ( x e. ( X (,) Y ) \|-> B ) e. ( ( ( X (,) Y ) -cn-> CC ) i^i L^1 ) )
	itgsubst.c	\|- ( ph -> ( u e. ( Z (,) W ) \|-> C ) e. ( ( Z (,) W ) -cn-> CC ) )
	itgsubst.da	\|- ( ph -> ( RR _D ( x e. ( X [,] Y ) \|-> A ) ) = ( x e. ( X (,) Y ) \|-> B ) )
	itgsubst.e	\|- ( u = A -> C = E )
	itgsubst.k	\|- ( x = X -> A = K )
	itgsubst.l	\|- ( x = Y -> A = L )
	itgsubst.m	\|- ( ph -> M e. ( Z (,) W ) )
	itgsubst.n	\|- ( ph -> N e. ( Z (,) W ) )
	itgsubst.cl2	\|- ( ( ph /\ x e. ( X [,] Y ) ) -> A e. ( M (,) N ) )
Assertion	itgsubstlem	\|- ( ph -> S_ [ K -> L ] C _d u = S_ [ X -> Y ] ( E x. B ) _d x )

Proof

Step	Hyp	Ref	Expression
1		itgsubst.x	\|- ( ph -> X e. RR )
2		itgsubst.y	\|- ( ph -> Y e. RR )
3		itgsubst.le	\|- ( ph -> X <_ Y )
4		itgsubst.z	\|- ( ph -> Z e. RR* )
5		itgsubst.w	\|- ( ph -> W e. RR* )
6		itgsubst.a	\|- ( ph -> ( x e. ( X [,] Y ) \|-> A ) e. ( ( X [,] Y ) -cn-> ( Z (,) W ) ) )
7		itgsubst.b	\|- ( ph -> ( x e. ( X (,) Y ) \|-> B ) e. ( ( ( X (,) Y ) -cn-> CC ) i^i L^1 ) )
8		itgsubst.c	\|- ( ph -> ( u e. ( Z (,) W ) \|-> C ) e. ( ( Z (,) W ) -cn-> CC ) )
9		itgsubst.da	\|- ( ph -> ( RR _D ( x e. ( X [,] Y ) \|-> A ) ) = ( x e. ( X (,) Y ) \|-> B ) )
10		itgsubst.e	\|- ( u = A -> C = E )
11		itgsubst.k	\|- ( x = X -> A = K )
12		itgsubst.l	\|- ( x = Y -> A = L )
13		itgsubst.m	\|- ( ph -> M e. ( Z (,) W ) )
14		itgsubst.n	\|- ( ph -> N e. ( Z (,) W ) )
15		itgsubst.cl2	\|- ( ( ph /\ x e. ( X [,] Y ) ) -> A e. ( M (,) N ) )
16	3	ditgpos	\|- ( ph -> S_ [ X -> Y ] ( E x. B ) _d x = S. ( X (,) Y ) ( E x. B ) _d x )
17		ax-resscn	\|- RR C_ CC
18	17	a1i	\|- ( ph -> RR C_ CC )
19		iccssre	\|- ( ( X e. RR /\ Y e. RR ) -> ( X [,] Y ) C_ RR )
20	1 2 19	syl2anc	\|- ( ph -> ( X [,] Y ) C_ RR )
21		eqidd	\|- ( ph -> ( x e. ( X [,] Y ) \|-> A ) = ( x e. ( X [,] Y ) \|-> A ) )
22		eqidd	\|- ( ph -> ( v e. ( M (,) N ) \|-> S. ( M (,) v ) C _d u ) = ( v e. ( M (,) N ) \|-> S. ( M (,) v ) C _d u ) )
23		oveq2	\|- ( v = A -> ( M (,) v ) = ( M (,) A ) )
24		itgeq1	\|- ( ( M (,) v ) = ( M (,) A ) -> S. ( M (,) v ) C _d u = S. ( M (,) A ) C _d u )
25	23 24	syl	\|- ( v = A -> S. ( M (,) v ) C _d u = S. ( M (,) A ) C _d u )
26	15 21 22 25	fmptco	\|- ( ph -> ( ( v e. ( M (,) N ) \|-> S. ( M (,) v ) C _d u ) o. ( x e. ( X [,] Y ) \|-> A ) ) = ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) )
27	15	fmpttd	\|- ( ph -> ( x e. ( X [,] Y ) \|-> A ) : ( X [,] Y ) --> ( M (,) N ) )
28		ioossicc	\|- ( M (,) N ) C_ ( M [,] N )
29		eliooord	\|- ( M e. ( Z (,) W ) -> ( Z < M /\ M < W ) )
30	13 29	syl	\|- ( ph -> ( Z < M /\ M < W ) )
31	30	simpld	\|- ( ph -> Z < M )
32		eliooord	\|- ( N e. ( Z (,) W ) -> ( Z < N /\ N < W ) )
33	14 32	syl	\|- ( ph -> ( Z < N /\ N < W ) )
34	33	simprd	\|- ( ph -> N < W )
35		iccssioo	\|- ( ( ( Z e. RR* /\ W e. RR* ) /\ ( Z < M /\ N < W ) ) -> ( M [,] N ) C_ ( Z (,) W ) )
36	4 5 31 34 35	syl22anc	\|- ( ph -> ( M [,] N ) C_ ( Z (,) W ) )
37	28 36	sstrid	\|- ( ph -> ( M (,) N ) C_ ( Z (,) W ) )
38		ioossre	\|- ( Z (,) W ) C_ RR
39	38	a1i	\|- ( ph -> ( Z (,) W ) C_ RR )
40	39 17	sstrdi	\|- ( ph -> ( Z (,) W ) C_ CC )
41	37 40	sstrd	\|- ( ph -> ( M (,) N ) C_ CC )
42		cncfcdm	\|- ( ( ( M (,) N ) C_ CC /\ ( x e. ( X [,] Y ) \|-> A ) e. ( ( X [,] Y ) -cn-> ( Z (,) W ) ) ) -> ( ( x e. ( X [,] Y ) \|-> A ) e. ( ( X [,] Y ) -cn-> ( M (,) N ) ) <-> ( x e. ( X [,] Y ) \|-> A ) : ( X [,] Y ) --> ( M (,) N ) ) )
43	41 6 42	syl2anc	\|- ( ph -> ( ( x e. ( X [,] Y ) \|-> A ) e. ( ( X [,] Y ) -cn-> ( M (,) N ) ) <-> ( x e. ( X [,] Y ) \|-> A ) : ( X [,] Y ) --> ( M (,) N ) ) )
44	27 43	mpbird	\|- ( ph -> ( x e. ( X [,] Y ) \|-> A ) e. ( ( X [,] Y ) -cn-> ( M (,) N ) ) )
45	28	sseli	\|- ( v e. ( M (,) N ) -> v e. ( M [,] N ) )
46	38 14	sselid	\|- ( ph -> N e. RR )
47	46	rexrd	\|- ( ph -> N e. RR* )
48	47	adantr	\|- ( ( ph /\ v e. ( M [,] N ) ) -> N e. RR* )
49	38 13	sselid	\|- ( ph -> M e. RR )
50		elicc2	\|- ( ( M e. RR /\ N e. RR ) -> ( v e. ( M [,] N ) <-> ( v e. RR /\ M <_ v /\ v <_ N ) ) )
51	49 46 50	syl2anc	\|- ( ph -> ( v e. ( M [,] N ) <-> ( v e. RR /\ M <_ v /\ v <_ N ) ) )
52	51	biimpa	\|- ( ( ph /\ v e. ( M [,] N ) ) -> ( v e. RR /\ M <_ v /\ v <_ N ) )
53	52	simp3d	\|- ( ( ph /\ v e. ( M [,] N ) ) -> v <_ N )
54		iooss2	\|- ( ( N e. RR* /\ v <_ N ) -> ( M (,) v ) C_ ( M (,) N ) )
55	48 53 54	syl2anc	\|- ( ( ph /\ v e. ( M [,] N ) ) -> ( M (,) v ) C_ ( M (,) N ) )
56	55	sselda	\|- ( ( ( ph /\ v e. ( M [,] N ) ) /\ u e. ( M (,) v ) ) -> u e. ( M (,) N ) )
57	37	sselda	\|- ( ( ph /\ u e. ( M (,) N ) ) -> u e. ( Z (,) W ) )
58		cncff	\|- ( ( u e. ( Z (,) W ) \|-> C ) e. ( ( Z (,) W ) -cn-> CC ) -> ( u e. ( Z (,) W ) \|-> C ) : ( Z (,) W ) --> CC )
59	8 58	syl	\|- ( ph -> ( u e. ( Z (,) W ) \|-> C ) : ( Z (,) W ) --> CC )
60	59	fvmptelcdm	\|- ( ( ph /\ u e. ( Z (,) W ) ) -> C e. CC )
61	57 60	syldan	\|- ( ( ph /\ u e. ( M (,) N ) ) -> C e. CC )
62	61	adantlr	\|- ( ( ( ph /\ v e. ( M [,] N ) ) /\ u e. ( M (,) N ) ) -> C e. CC )
63	56 62	syldan	\|- ( ( ( ph /\ v e. ( M [,] N ) ) /\ u e. ( M (,) v ) ) -> C e. CC )
64		ioombl	\|- ( M (,) v ) e. dom vol
65	64	a1i	\|- ( ( ph /\ v e. ( M [,] N ) ) -> ( M (,) v ) e. dom vol )
66	28	a1i	\|- ( ph -> ( M (,) N ) C_ ( M [,] N ) )
67		ioombl	\|- ( M (,) N ) e. dom vol
68	67	a1i	\|- ( ph -> ( M (,) N ) e. dom vol )
69	36	sselda	\|- ( ( ph /\ u e. ( M [,] N ) ) -> u e. ( Z (,) W ) )
70	69 60	syldan	\|- ( ( ph /\ u e. ( M [,] N ) ) -> C e. CC )
71	36	resmptd	\|- ( ph -> ( ( u e. ( Z (,) W ) \|-> C ) \|` ( M [,] N ) ) = ( u e. ( M [,] N ) \|-> C ) )
72		rescncf	\|- ( ( M [,] N ) C_ ( Z (,) W ) -> ( ( u e. ( Z (,) W ) \|-> C ) e. ( ( Z (,) W ) -cn-> CC ) -> ( ( u e. ( Z (,) W ) \|-> C ) \|` ( M [,] N ) ) e. ( ( M [,] N ) -cn-> CC ) ) )
73	36 8 72	sylc	\|- ( ph -> ( ( u e. ( Z (,) W ) \|-> C ) \|` ( M [,] N ) ) e. ( ( M [,] N ) -cn-> CC ) )
74	71 73	eqeltrrd	\|- ( ph -> ( u e. ( M [,] N ) \|-> C ) e. ( ( M [,] N ) -cn-> CC ) )
75		cniccibl	\|- ( ( M e. RR /\ N e. RR /\ ( u e. ( M [,] N ) \|-> C ) e. ( ( M [,] N ) -cn-> CC ) ) -> ( u e. ( M [,] N ) \|-> C ) e. L^1 )
76	49 46 74 75	syl3anc	\|- ( ph -> ( u e. ( M [,] N ) \|-> C ) e. L^1 )
77	66 68 70 76	iblss	\|- ( ph -> ( u e. ( M (,) N ) \|-> C ) e. L^1 )
78	77	adantr	\|- ( ( ph /\ v e. ( M [,] N ) ) -> ( u e. ( M (,) N ) \|-> C ) e. L^1 )
79	55 65 62 78	iblss	\|- ( ( ph /\ v e. ( M [,] N ) ) -> ( u e. ( M (,) v ) \|-> C ) e. L^1 )
80	63 79	itgcl	\|- ( ( ph /\ v e. ( M [,] N ) ) -> S. ( M (,) v ) C _d u e. CC )
81	45 80	sylan2	\|- ( ( ph /\ v e. ( M (,) N ) ) -> S. ( M (,) v ) C _d u e. CC )
82	81	fmpttd	\|- ( ph -> ( v e. ( M (,) N ) \|-> S. ( M (,) v ) C _d u ) : ( M (,) N ) --> CC )
83	37 38	sstrdi	\|- ( ph -> ( M (,) N ) C_ RR )
84		fveq2	\|- ( t = u -> ( ( u e. ( M (,) N ) \|-> C ) ` t ) = ( ( u e. ( M (,) N ) \|-> C ) ` u ) )
85		nffvmpt1	\|- F/_ u ( ( u e. ( M (,) N ) \|-> C ) ` t )
86		nfcv	\|- F/_ t ( ( u e. ( M (,) N ) \|-> C ) ` u )
87	84 85 86	cbvitg	\|- S. ( M (,) v ) ( ( u e. ( M (,) N ) \|-> C ) ` t ) _d t = S. ( M (,) v ) ( ( u e. ( M (,) N ) \|-> C ) ` u ) _d u
88		eqid	\|- ( u e. ( M (,) N ) \|-> C ) = ( u e. ( M (,) N ) \|-> C )
89	88	fvmpt2	\|- ( ( u e. ( M (,) N ) /\ C e. CC ) -> ( ( u e. ( M (,) N ) \|-> C ) ` u ) = C )
90	56 63 89	syl2anc	\|- ( ( ( ph /\ v e. ( M [,] N ) ) /\ u e. ( M (,) v ) ) -> ( ( u e. ( M (,) N ) \|-> C ) ` u ) = C )
91	90	itgeq2dv	\|- ( ( ph /\ v e. ( M [,] N ) ) -> S. ( M (,) v ) ( ( u e. ( M (,) N ) \|-> C ) ` u ) _d u = S. ( M (,) v ) C _d u )
92	87 91	eqtrid	\|- ( ( ph /\ v e. ( M [,] N ) ) -> S. ( M (,) v ) ( ( u e. ( M (,) N ) \|-> C ) ` t ) _d t = S. ( M (,) v ) C _d u )
93	92	mpteq2dva	\|- ( ph -> ( v e. ( M [,] N ) \|-> S. ( M (,) v ) ( ( u e. ( M (,) N ) \|-> C ) ` t ) _d t ) = ( v e. ( M [,] N ) \|-> S. ( M (,) v ) C _d u ) )
94	93	oveq2d	\|- ( ph -> ( RR _D ( v e. ( M [,] N ) \|-> S. ( M (,) v ) ( ( u e. ( M (,) N ) \|-> C ) ` t ) _d t ) ) = ( RR _D ( v e. ( M [,] N ) \|-> S. ( M (,) v ) C _d u ) ) )
95		eqid	\|- ( v e. ( M [,] N ) \|-> S. ( M (,) v ) ( ( u e. ( M (,) N ) \|-> C ) ` t ) _d t ) = ( v e. ( M [,] N ) \|-> S. ( M (,) v ) ( ( u e. ( M (,) N ) \|-> C ) ` t ) _d t )
96	1	rexrd	\|- ( ph -> X e. RR* )
97	2	rexrd	\|- ( ph -> Y e. RR* )
98		lbicc2	\|- ( ( X e. RR* /\ Y e. RR* /\ X <_ Y ) -> X e. ( X [,] Y ) )
99	96 97 3 98	syl3anc	\|- ( ph -> X e. ( X [,] Y ) )
100		n0i	\|- ( X e. ( X [,] Y ) -> -. ( X [,] Y ) = (/) )
101	99 100	syl	\|- ( ph -> -. ( X [,] Y ) = (/) )
102		feq3	\|- ( ( M (,) N ) = (/) -> ( ( x e. ( X [,] Y ) \|-> A ) : ( X [,] Y ) --> ( M (,) N ) <-> ( x e. ( X [,] Y ) \|-> A ) : ( X [,] Y ) --> (/) ) )
103	27 102	syl5ibcom	\|- ( ph -> ( ( M (,) N ) = (/) -> ( x e. ( X [,] Y ) \|-> A ) : ( X [,] Y ) --> (/) ) )
104		f00	\|- ( ( x e. ( X [,] Y ) \|-> A ) : ( X [,] Y ) --> (/) <-> ( ( x e. ( X [,] Y ) \|-> A ) = (/) /\ ( X [,] Y ) = (/) ) )
105	104	simprbi	\|- ( ( x e. ( X [,] Y ) \|-> A ) : ( X [,] Y ) --> (/) -> ( X [,] Y ) = (/) )
106	103 105	syl6	\|- ( ph -> ( ( M (,) N ) = (/) -> ( X [,] Y ) = (/) ) )
107	101 106	mtod	\|- ( ph -> -. ( M (,) N ) = (/) )
108	49	rexrd	\|- ( ph -> M e. RR* )
109		ioo0	\|- ( ( M e. RR* /\ N e. RR* ) -> ( ( M (,) N ) = (/) <-> N <_ M ) )
110	108 47 109	syl2anc	\|- ( ph -> ( ( M (,) N ) = (/) <-> N <_ M ) )
111	107 110	mtbid	\|- ( ph -> -. N <_ M )
112	46 49	letrid	\|- ( ph -> ( N <_ M \/ M <_ N ) )
113	112	ord	\|- ( ph -> ( -. N <_ M -> M <_ N ) )
114	111 113	mpd	\|- ( ph -> M <_ N )
115		resmpt	\|- ( ( M (,) N ) C_ ( M [,] N ) -> ( ( u e. ( M [,] N ) \|-> C ) \|` ( M (,) N ) ) = ( u e. ( M (,) N ) \|-> C ) )
116	28 115	ax-mp	\|- ( ( u e. ( M [,] N ) \|-> C ) \|` ( M (,) N ) ) = ( u e. ( M (,) N ) \|-> C )
117		rescncf	\|- ( ( M (,) N ) C_ ( M [,] N ) -> ( ( u e. ( M [,] N ) \|-> C ) e. ( ( M [,] N ) -cn-> CC ) -> ( ( u e. ( M [,] N ) \|-> C ) \|` ( M (,) N ) ) e. ( ( M (,) N ) -cn-> CC ) ) )
118	28 74 117	mpsyl	\|- ( ph -> ( ( u e. ( M [,] N ) \|-> C ) \|` ( M (,) N ) ) e. ( ( M (,) N ) -cn-> CC ) )
119	116 118	eqeltrrid	\|- ( ph -> ( u e. ( M (,) N ) \|-> C ) e. ( ( M (,) N ) -cn-> CC ) )
120	95 49 46 114 119 77	ftc1cn	\|- ( ph -> ( RR _D ( v e. ( M [,] N ) \|-> S. ( M (,) v ) ( ( u e. ( M (,) N ) \|-> C ) ` t ) _d t ) ) = ( u e. ( M (,) N ) \|-> C ) )
121	36 38	sstrdi	\|- ( ph -> ( M [,] N ) C_ RR )
122		tgioo4	\|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) \|`t RR )
123		eqid	\|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
124		iccntr	\|- ( ( M e. RR /\ N e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( M [,] N ) ) = ( M (,) N ) )
125	49 46 124	syl2anc	\|- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( M [,] N ) ) = ( M (,) N ) )
126	18 121 80 122 123 125	dvmptntr	\|- ( ph -> ( RR _D ( v e. ( M [,] N ) \|-> S. ( M (,) v ) C _d u ) ) = ( RR _D ( v e. ( M (,) N ) \|-> S. ( M (,) v ) C _d u ) ) )
127	94 120 126	3eqtr3rd	\|- ( ph -> ( RR _D ( v e. ( M (,) N ) \|-> S. ( M (,) v ) C _d u ) ) = ( u e. ( M (,) N ) \|-> C ) )
128	127	dmeqd	\|- ( ph -> dom ( RR _D ( v e. ( M (,) N ) \|-> S. ( M (,) v ) C _d u ) ) = dom ( u e. ( M (,) N ) \|-> C ) )
129	88 61	dmmptd	\|- ( ph -> dom ( u e. ( M (,) N ) \|-> C ) = ( M (,) N ) )
130	128 129	eqtrd	\|- ( ph -> dom ( RR _D ( v e. ( M (,) N ) \|-> S. ( M (,) v ) C _d u ) ) = ( M (,) N ) )
131		dvcn	\|- ( ( ( RR C_ CC /\ ( v e. ( M (,) N ) \|-> S. ( M (,) v ) C _d u ) : ( M (,) N ) --> CC /\ ( M (,) N ) C_ RR ) /\ dom ( RR _D ( v e. ( M (,) N ) \|-> S. ( M (,) v ) C _d u ) ) = ( M (,) N ) ) -> ( v e. ( M (,) N ) \|-> S. ( M (,) v ) C _d u ) e. ( ( M (,) N ) -cn-> CC ) )
132	18 82 83 130 131	syl31anc	\|- ( ph -> ( v e. ( M (,) N ) \|-> S. ( M (,) v ) C _d u ) e. ( ( M (,) N ) -cn-> CC ) )
133	44 132	cncfco	\|- ( ph -> ( ( v e. ( M (,) N ) \|-> S. ( M (,) v ) C _d u ) o. ( x e. ( X [,] Y ) \|-> A ) ) e. ( ( X [,] Y ) -cn-> CC ) )
134	26 133	eqeltrrd	\|- ( ph -> ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) e. ( ( X [,] Y ) -cn-> CC ) )
135		cncff	\|- ( ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) e. ( ( X [,] Y ) -cn-> CC ) -> ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) : ( X [,] Y ) --> CC )
136	134 135	syl	\|- ( ph -> ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) : ( X [,] Y ) --> CC )
137	136	fvmptelcdm	\|- ( ( ph /\ x e. ( X [,] Y ) ) -> S. ( M (,) A ) C _d u e. CC )
138		iccntr	\|- ( ( X e. RR /\ Y e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( X [,] Y ) ) = ( X (,) Y ) )
139	1 2 138	syl2anc	\|- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( X [,] Y ) ) = ( X (,) Y ) )
140	18 20 137 122 123 139	dvmptntr	\|- ( ph -> ( RR _D ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ) = ( RR _D ( x e. ( X (,) Y ) \|-> S. ( M (,) A ) C _d u ) ) )
141		reelprrecn	\|- RR e. { RR , CC }
142	141	a1i	\|- ( ph -> RR e. { RR , CC } )
143		ioossicc	\|- ( X (,) Y ) C_ ( X [,] Y )
144	143	sseli	\|- ( x e. ( X (,) Y ) -> x e. ( X [,] Y ) )
145	144 15	sylan2	\|- ( ( ph /\ x e. ( X (,) Y ) ) -> A e. ( M (,) N ) )
146		elin	\|- ( ( x e. ( X (,) Y ) \|-> B ) e. ( ( ( X (,) Y ) -cn-> CC ) i^i L^1 ) <-> ( ( x e. ( X (,) Y ) \|-> B ) e. ( ( X (,) Y ) -cn-> CC ) /\ ( x e. ( X (,) Y ) \|-> B ) e. L^1 ) )
147	7 146	sylib	\|- ( ph -> ( ( x e. ( X (,) Y ) \|-> B ) e. ( ( X (,) Y ) -cn-> CC ) /\ ( x e. ( X (,) Y ) \|-> B ) e. L^1 ) )
148	147	simpld	\|- ( ph -> ( x e. ( X (,) Y ) \|-> B ) e. ( ( X (,) Y ) -cn-> CC ) )
149		cncff	\|- ( ( x e. ( X (,) Y ) \|-> B ) e. ( ( X (,) Y ) -cn-> CC ) -> ( x e. ( X (,) Y ) \|-> B ) : ( X (,) Y ) --> CC )
150	148 149	syl	\|- ( ph -> ( x e. ( X (,) Y ) \|-> B ) : ( X (,) Y ) --> CC )
151	150	fvmptelcdm	\|- ( ( ph /\ x e. ( X (,) Y ) ) -> B e. CC )
152	61	fmpttd	\|- ( ph -> ( u e. ( M (,) N ) \|-> C ) : ( M (,) N ) --> CC )
153		nfcv	\|- F/_ v C
154		nfcsb1v	\|- F/_ u [_ v / u ]_ C
155		csbeq1a	\|- ( u = v -> C = [_ v / u ]_ C )
156	153 154 155	cbvmpt	\|- ( u e. ( M (,) N ) \|-> C ) = ( v e. ( M (,) N ) \|-> [_ v / u ]_ C )
157	156	fmpt	\|- ( A. v e. ( M (,) N ) [_ v / u ]_ C e. CC <-> ( u e. ( M (,) N ) \|-> C ) : ( M (,) N ) --> CC )
158	152 157	sylibr	\|- ( ph -> A. v e. ( M (,) N ) [_ v / u ]_ C e. CC )
159	158	r19.21bi	\|- ( ( ph /\ v e. ( M (,) N ) ) -> [_ v / u ]_ C e. CC )
160	38 17	sstri	\|- ( Z (,) W ) C_ CC
161		cncff	\|- ( ( x e. ( X [,] Y ) \|-> A ) e. ( ( X [,] Y ) -cn-> ( Z (,) W ) ) -> ( x e. ( X [,] Y ) \|-> A ) : ( X [,] Y ) --> ( Z (,) W ) )
162	6 161	syl	\|- ( ph -> ( x e. ( X [,] Y ) \|-> A ) : ( X [,] Y ) --> ( Z (,) W ) )
163	162	fvmptelcdm	\|- ( ( ph /\ x e. ( X [,] Y ) ) -> A e. ( Z (,) W ) )
164	160 163	sselid	\|- ( ( ph /\ x e. ( X [,] Y ) ) -> A e. CC )
165	18 20 164 122 123 139	dvmptntr	\|- ( ph -> ( RR _D ( x e. ( X [,] Y ) \|-> A ) ) = ( RR _D ( x e. ( X (,) Y ) \|-> A ) ) )
166	165 9	eqtr3d	\|- ( ph -> ( RR _D ( x e. ( X (,) Y ) \|-> A ) ) = ( x e. ( X (,) Y ) \|-> B ) )
167	127 156	eqtrdi	\|- ( ph -> ( RR _D ( v e. ( M (,) N ) \|-> S. ( M (,) v ) C _d u ) ) = ( v e. ( M (,) N ) \|-> [_ v / u ]_ C ) )
168		csbeq1	\|- ( v = A -> [_ v / u ]_ C = [_ A / u ]_ C )
169	142 142 145 151 81 159 166 167 25 168	dvmptco	\|- ( ph -> ( RR _D ( x e. ( X (,) Y ) \|-> S. ( M (,) A ) C _d u ) ) = ( x e. ( X (,) Y ) \|-> ( [_ A / u ]_ C x. B ) ) )
170		nfcvd	\|- ( A e. ( M (,) N ) -> F/_ u E )
171	170 10	csbiegf	\|- ( A e. ( M (,) N ) -> [_ A / u ]_ C = E )
172	145 171	syl	\|- ( ( ph /\ x e. ( X (,) Y ) ) -> [_ A / u ]_ C = E )
173	172	oveq1d	\|- ( ( ph /\ x e. ( X (,) Y ) ) -> ( [_ A / u ]_ C x. B ) = ( E x. B ) )
174	173	mpteq2dva	\|- ( ph -> ( x e. ( X (,) Y ) \|-> ( [_ A / u ]_ C x. B ) ) = ( x e. ( X (,) Y ) \|-> ( E x. B ) ) )
175	140 169 174	3eqtrd	\|- ( ph -> ( RR _D ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ) = ( x e. ( X (,) Y ) \|-> ( E x. B ) ) )
176		resmpt	\|- ( ( X (,) Y ) C_ ( X [,] Y ) -> ( ( x e. ( X [,] Y ) \|-> E ) \|` ( X (,) Y ) ) = ( x e. ( X (,) Y ) \|-> E ) )
177	143 176	ax-mp	\|- ( ( x e. ( X [,] Y ) \|-> E ) \|` ( X (,) Y ) ) = ( x e. ( X (,) Y ) \|-> E )
178		eqidd	\|- ( ph -> ( u e. ( Z (,) W ) \|-> C ) = ( u e. ( Z (,) W ) \|-> C ) )
179	163 21 178 10	fmptco	\|- ( ph -> ( ( u e. ( Z (,) W ) \|-> C ) o. ( x e. ( X [,] Y ) \|-> A ) ) = ( x e. ( X [,] Y ) \|-> E ) )
180	6 8	cncfco	\|- ( ph -> ( ( u e. ( Z (,) W ) \|-> C ) o. ( x e. ( X [,] Y ) \|-> A ) ) e. ( ( X [,] Y ) -cn-> CC ) )
181	179 180	eqeltrrd	\|- ( ph -> ( x e. ( X [,] Y ) \|-> E ) e. ( ( X [,] Y ) -cn-> CC ) )
182		rescncf	\|- ( ( X (,) Y ) C_ ( X [,] Y ) -> ( ( x e. ( X [,] Y ) \|-> E ) e. ( ( X [,] Y ) -cn-> CC ) -> ( ( x e. ( X [,] Y ) \|-> E ) \|` ( X (,) Y ) ) e. ( ( X (,) Y ) -cn-> CC ) ) )
183	143 181 182	mpsyl	\|- ( ph -> ( ( x e. ( X [,] Y ) \|-> E ) \|` ( X (,) Y ) ) e. ( ( X (,) Y ) -cn-> CC ) )
184	177 183	eqeltrrid	\|- ( ph -> ( x e. ( X (,) Y ) \|-> E ) e. ( ( X (,) Y ) -cn-> CC ) )
185	184 148	mulcncf	\|- ( ph -> ( x e. ( X (,) Y ) \|-> ( E x. B ) ) e. ( ( X (,) Y ) -cn-> CC ) )
186	175 185	eqeltrd	\|- ( ph -> ( RR _D ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ) e. ( ( X (,) Y ) -cn-> CC ) )
187		ioombl	\|- ( X (,) Y ) e. dom vol
188	187	a1i	\|- ( ph -> ( X (,) Y ) e. dom vol )
189		fco	\|- ( ( ( u e. ( Z (,) W ) \|-> C ) : ( Z (,) W ) --> CC /\ ( x e. ( X [,] Y ) \|-> A ) : ( X [,] Y ) --> ( Z (,) W ) ) -> ( ( u e. ( Z (,) W ) \|-> C ) o. ( x e. ( X [,] Y ) \|-> A ) ) : ( X [,] Y ) --> CC )
190	59 162 189	syl2anc	\|- ( ph -> ( ( u e. ( Z (,) W ) \|-> C ) o. ( x e. ( X [,] Y ) \|-> A ) ) : ( X [,] Y ) --> CC )
191	179	feq1d	\|- ( ph -> ( ( ( u e. ( Z (,) W ) \|-> C ) o. ( x e. ( X [,] Y ) \|-> A ) ) : ( X [,] Y ) --> CC <-> ( x e. ( X [,] Y ) \|-> E ) : ( X [,] Y ) --> CC ) )
192	190 191	mpbid	\|- ( ph -> ( x e. ( X [,] Y ) \|-> E ) : ( X [,] Y ) --> CC )
193	192	fvmptelcdm	\|- ( ( ph /\ x e. ( X [,] Y ) ) -> E e. CC )
194	144 193	sylan2	\|- ( ( ph /\ x e. ( X (,) Y ) ) -> E e. CC )
195		eqidd	\|- ( ph -> ( x e. ( X (,) Y ) \|-> E ) = ( x e. ( X (,) Y ) \|-> E ) )
196		eqidd	\|- ( ph -> ( x e. ( X (,) Y ) \|-> B ) = ( x e. ( X (,) Y ) \|-> B ) )
197	188 194 151 195 196	offval2	\|- ( ph -> ( ( x e. ( X (,) Y ) \|-> E ) oF x. ( x e. ( X (,) Y ) \|-> B ) ) = ( x e. ( X (,) Y ) \|-> ( E x. B ) ) )
198	175 197	eqtr4d	\|- ( ph -> ( RR _D ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ) = ( ( x e. ( X (,) Y ) \|-> E ) oF x. ( x e. ( X (,) Y ) \|-> B ) ) )
199	143	a1i	\|- ( ph -> ( X (,) Y ) C_ ( X [,] Y ) )
200		cniccibl	\|- ( ( X e. RR /\ Y e. RR /\ ( x e. ( X [,] Y ) \|-> E ) e. ( ( X [,] Y ) -cn-> CC ) ) -> ( x e. ( X [,] Y ) \|-> E ) e. L^1 )
201	1 2 181 200	syl3anc	\|- ( ph -> ( x e. ( X [,] Y ) \|-> E ) e. L^1 )
202	199 188 193 201	iblss	\|- ( ph -> ( x e. ( X (,) Y ) \|-> E ) e. L^1 )
203		iblmbf	\|- ( ( x e. ( X (,) Y ) \|-> E ) e. L^1 -> ( x e. ( X (,) Y ) \|-> E ) e. MblFn )
204	202 203	syl	\|- ( ph -> ( x e. ( X (,) Y ) \|-> E ) e. MblFn )
205	147	simprd	\|- ( ph -> ( x e. ( X (,) Y ) \|-> B ) e. L^1 )
206		cniccbdd	\|- ( ( X e. RR /\ Y e. RR /\ ( x e. ( X [,] Y ) \|-> E ) e. ( ( X [,] Y ) -cn-> CC ) ) -> E. y e. RR A. z e. ( X [,] Y ) ( abs ` ( ( x e. ( X [,] Y ) \|-> E ) ` z ) ) <_ y )
207	1 2 181 206	syl3anc	\|- ( ph -> E. y e. RR A. z e. ( X [,] Y ) ( abs ` ( ( x e. ( X [,] Y ) \|-> E ) ` z ) ) <_ y )
208		ssralv	\|- ( ( X (,) Y ) C_ ( X [,] Y ) -> ( A. z e. ( X [,] Y ) ( abs ` ( ( x e. ( X [,] Y ) \|-> E ) ` z ) ) <_ y -> A. z e. ( X (,) Y ) ( abs ` ( ( x e. ( X [,] Y ) \|-> E ) ` z ) ) <_ y ) )
209	143 208	ax-mp	\|- ( A. z e. ( X [,] Y ) ( abs ` ( ( x e. ( X [,] Y ) \|-> E ) ` z ) ) <_ y -> A. z e. ( X (,) Y ) ( abs ` ( ( x e. ( X [,] Y ) \|-> E ) ` z ) ) <_ y )
210		eqid	\|- ( x e. ( X (,) Y ) \|-> E ) = ( x e. ( X (,) Y ) \|-> E )
211	210 194	dmmptd	\|- ( ph -> dom ( x e. ( X (,) Y ) \|-> E ) = ( X (,) Y ) )
212	211	raleqdv	\|- ( ph -> ( A. z e. dom ( x e. ( X (,) Y ) \|-> E ) ( abs ` ( ( x e. ( X (,) Y ) \|-> E ) ` z ) ) <_ y <-> A. z e. ( X (,) Y ) ( abs ` ( ( x e. ( X (,) Y ) \|-> E ) ` z ) ) <_ y ) )
213	177	fveq1i	\|- ( ( ( x e. ( X [,] Y ) \|-> E ) \|` ( X (,) Y ) ) ` z ) = ( ( x e. ( X (,) Y ) \|-> E ) ` z )
214		fvres	\|- ( z e. ( X (,) Y ) -> ( ( ( x e. ( X [,] Y ) \|-> E ) \|` ( X (,) Y ) ) ` z ) = ( ( x e. ( X [,] Y ) \|-> E ) ` z ) )
215	213 214	eqtr3id	\|- ( z e. ( X (,) Y ) -> ( ( x e. ( X (,) Y ) \|-> E ) ` z ) = ( ( x e. ( X [,] Y ) \|-> E ) ` z ) )
216	215	fveq2d	\|- ( z e. ( X (,) Y ) -> ( abs ` ( ( x e. ( X (,) Y ) \|-> E ) ` z ) ) = ( abs ` ( ( x e. ( X [,] Y ) \|-> E ) ` z ) ) )
217	216	breq1d	\|- ( z e. ( X (,) Y ) -> ( ( abs ` ( ( x e. ( X (,) Y ) \|-> E ) ` z ) ) <_ y <-> ( abs ` ( ( x e. ( X [,] Y ) \|-> E ) ` z ) ) <_ y ) )
218	217	ralbiia	\|- ( A. z e. ( X (,) Y ) ( abs ` ( ( x e. ( X (,) Y ) \|-> E ) ` z ) ) <_ y <-> A. z e. ( X (,) Y ) ( abs ` ( ( x e. ( X [,] Y ) \|-> E ) ` z ) ) <_ y )
219	212 218	bitr2di	\|- ( ph -> ( A. z e. ( X (,) Y ) ( abs ` ( ( x e. ( X [,] Y ) \|-> E ) ` z ) ) <_ y <-> A. z e. dom ( x e. ( X (,) Y ) \|-> E ) ( abs ` ( ( x e. ( X (,) Y ) \|-> E ) ` z ) ) <_ y ) )
220	209 219	imbitrid	\|- ( ph -> ( A. z e. ( X [,] Y ) ( abs ` ( ( x e. ( X [,] Y ) \|-> E ) ` z ) ) <_ y -> A. z e. dom ( x e. ( X (,) Y ) \|-> E ) ( abs ` ( ( x e. ( X (,) Y ) \|-> E ) ` z ) ) <_ y ) )
221	220	reximdv	\|- ( ph -> ( E. y e. RR A. z e. ( X [,] Y ) ( abs ` ( ( x e. ( X [,] Y ) \|-> E ) ` z ) ) <_ y -> E. y e. RR A. z e. dom ( x e. ( X (,) Y ) \|-> E ) ( abs ` ( ( x e. ( X (,) Y ) \|-> E ) ` z ) ) <_ y ) )
222	207 221	mpd	\|- ( ph -> E. y e. RR A. z e. dom ( x e. ( X (,) Y ) \|-> E ) ( abs ` ( ( x e. ( X (,) Y ) \|-> E ) ` z ) ) <_ y )
223		bddmulibl	\|- ( ( ( x e. ( X (,) Y ) \|-> E ) e. MblFn /\ ( x e. ( X (,) Y ) \|-> B ) e. L^1 /\ E. y e. RR A. z e. dom ( x e. ( X (,) Y ) \|-> E ) ( abs ` ( ( x e. ( X (,) Y ) \|-> E ) ` z ) ) <_ y ) -> ( ( x e. ( X (,) Y ) \|-> E ) oF x. ( x e. ( X (,) Y ) \|-> B ) ) e. L^1 )
224	204 205 222 223	syl3anc	\|- ( ph -> ( ( x e. ( X (,) Y ) \|-> E ) oF x. ( x e. ( X (,) Y ) \|-> B ) ) e. L^1 )
225	198 224	eqeltrd	\|- ( ph -> ( RR _D ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ) e. L^1 )
226	1 2 3 186 225 134	ftc2	\|- ( ph -> S. ( X (,) Y ) ( ( RR _D ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ) ` t ) _d t = ( ( ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ` Y ) - ( ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ` X ) ) )
227		fveq2	\|- ( t = x -> ( ( RR _D ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ) ` t ) = ( ( RR _D ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ) ` x ) )
228		nfcv	\|- F/_ x RR
229		nfcv	\|- F/_ x _D
230		nfmpt1	\|- F/_ x ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u )
231	228 229 230	nfov	\|- F/_ x ( RR _D ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) )
232		nfcv	\|- F/_ x t
233	231 232	nffv	\|- F/_ x ( ( RR _D ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ) ` t )
234		nfcv	\|- F/_ t ( ( RR _D ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ) ` x )
235	227 233 234	cbvitg	\|- S. ( X (,) Y ) ( ( RR _D ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ) ` t ) _d t = S. ( X (,) Y ) ( ( RR _D ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ) ` x ) _d x
236	175	fveq1d	\|- ( ph -> ( ( RR _D ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ) ` x ) = ( ( x e. ( X (,) Y ) \|-> ( E x. B ) ) ` x ) )
237		ovex	\|- ( E x. B ) e. _V
238		eqid	\|- ( x e. ( X (,) Y ) \|-> ( E x. B ) ) = ( x e. ( X (,) Y ) \|-> ( E x. B ) )
239	238	fvmpt2	\|- ( ( x e. ( X (,) Y ) /\ ( E x. B ) e. _V ) -> ( ( x e. ( X (,) Y ) \|-> ( E x. B ) ) ` x ) = ( E x. B ) )
240	237 239	mpan2	\|- ( x e. ( X (,) Y ) -> ( ( x e. ( X (,) Y ) \|-> ( E x. B ) ) ` x ) = ( E x. B ) )
241	236 240	sylan9eq	\|- ( ( ph /\ x e. ( X (,) Y ) ) -> ( ( RR _D ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ) ` x ) = ( E x. B ) )
242	241	itgeq2dv	\|- ( ph -> S. ( X (,) Y ) ( ( RR _D ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ) ` x ) _d x = S. ( X (,) Y ) ( E x. B ) _d x )
243	235 242	eqtrid	\|- ( ph -> S. ( X (,) Y ) ( ( RR _D ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ) ` t ) _d t = S. ( X (,) Y ) ( E x. B ) _d x )
244	28 15	sselid	\|- ( ( ph /\ x e. ( X [,] Y ) ) -> A e. ( M [,] N ) )
245		elicc2	\|- ( ( M e. RR /\ N e. RR ) -> ( A e. ( M [,] N ) <-> ( A e. RR /\ M <_ A /\ A <_ N ) ) )
246	49 46 245	syl2anc	\|- ( ph -> ( A e. ( M [,] N ) <-> ( A e. RR /\ M <_ A /\ A <_ N ) ) )
247	246	adantr	\|- ( ( ph /\ x e. ( X [,] Y ) ) -> ( A e. ( M [,] N ) <-> ( A e. RR /\ M <_ A /\ A <_ N ) ) )
248	244 247	mpbid	\|- ( ( ph /\ x e. ( X [,] Y ) ) -> ( A e. RR /\ M <_ A /\ A <_ N ) )
249	248	simp2d	\|- ( ( ph /\ x e. ( X [,] Y ) ) -> M <_ A )
250	249	ditgpos	\|- ( ( ph /\ x e. ( X [,] Y ) ) -> S_ [ M -> A ] C _d u = S. ( M (,) A ) C _d u )
251	250	mpteq2dva	\|- ( ph -> ( x e. ( X [,] Y ) \|-> S_ [ M -> A ] C _d u ) = ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) )
252	251	fveq1d	\|- ( ph -> ( ( x e. ( X [,] Y ) \|-> S_ [ M -> A ] C _d u ) ` Y ) = ( ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ` Y ) )
253		ubicc2	\|- ( ( X e. RR* /\ Y e. RR* /\ X <_ Y ) -> Y e. ( X [,] Y ) )
254	96 97 3 253	syl3anc	\|- ( ph -> Y e. ( X [,] Y ) )
255		ditgeq2	\|- ( A = L -> S_ [ M -> A ] C _d u = S_ [ M -> L ] C _d u )
256	12 255	syl	\|- ( x = Y -> S_ [ M -> A ] C _d u = S_ [ M -> L ] C _d u )
257		eqid	\|- ( x e. ( X [,] Y ) \|-> S_ [ M -> A ] C _d u ) = ( x e. ( X [,] Y ) \|-> S_ [ M -> A ] C _d u )
258		ditgex	\|- S_ [ M -> L ] C _d u e. _V
259	256 257 258	fvmpt	\|- ( Y e. ( X [,] Y ) -> ( ( x e. ( X [,] Y ) \|-> S_ [ M -> A ] C _d u ) ` Y ) = S_ [ M -> L ] C _d u )
260	254 259	syl	\|- ( ph -> ( ( x e. ( X [,] Y ) \|-> S_ [ M -> A ] C _d u ) ` Y ) = S_ [ M -> L ] C _d u )
261	252 260	eqtr3d	\|- ( ph -> ( ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ` Y ) = S_ [ M -> L ] C _d u )
262	251	fveq1d	\|- ( ph -> ( ( x e. ( X [,] Y ) \|-> S_ [ M -> A ] C _d u ) ` X ) = ( ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ` X ) )
263		ditgeq2	\|- ( A = K -> S_ [ M -> A ] C _d u = S_ [ M -> K ] C _d u )
264	11 263	syl	\|- ( x = X -> S_ [ M -> A ] C _d u = S_ [ M -> K ] C _d u )
265		ditgex	\|- S_ [ M -> K ] C _d u e. _V
266	264 257 265	fvmpt	\|- ( X e. ( X [,] Y ) -> ( ( x e. ( X [,] Y ) \|-> S_ [ M -> A ] C _d u ) ` X ) = S_ [ M -> K ] C _d u )
267	99 266	syl	\|- ( ph -> ( ( x e. ( X [,] Y ) \|-> S_ [ M -> A ] C _d u ) ` X ) = S_ [ M -> K ] C _d u )
268	262 267	eqtr3d	\|- ( ph -> ( ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ` X ) = S_ [ M -> K ] C _d u )
269	261 268	oveq12d	\|- ( ph -> ( ( ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ` Y ) - ( ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ` X ) ) = ( S_ [ M -> L ] C _d u - S_ [ M -> K ] C _d u ) )
270		lbicc2	\|- ( ( M e. RR* /\ N e. RR* /\ M <_ N ) -> M e. ( M [,] N ) )
271	108 47 114 270	syl3anc	\|- ( ph -> M e. ( M [,] N ) )
272	11	eleq1d	\|- ( x = X -> ( A e. ( M [,] N ) <-> K e. ( M [,] N ) ) )
273	244	ralrimiva	\|- ( ph -> A. x e. ( X [,] Y ) A e. ( M [,] N ) )
274	272 273 99	rspcdva	\|- ( ph -> K e. ( M [,] N ) )
275	12	eleq1d	\|- ( x = Y -> ( A e. ( M [,] N ) <-> L e. ( M [,] N ) ) )
276	275 273 254	rspcdva	\|- ( ph -> L e. ( M [,] N ) )
277	49 46 271 274 276 61 77	ditgsplit	\|- ( ph -> S_ [ M -> L ] C _d u = ( S_ [ M -> K ] C _d u + S_ [ K -> L ] C _d u ) )
278	277	oveq1d	\|- ( ph -> ( S_ [ M -> L ] C _d u - S_ [ M -> K ] C _d u ) = ( ( S_ [ M -> K ] C _d u + S_ [ K -> L ] C _d u ) - S_ [ M -> K ] C _d u ) )
279	49 46 271 274 61 77	ditgcl	\|- ( ph -> S_ [ M -> K ] C _d u e. CC )
280	49 46 274 276 61 77	ditgcl	\|- ( ph -> S_ [ K -> L ] C _d u e. CC )
281	279 280	pncan2d	\|- ( ph -> ( ( S_ [ M -> K ] C _d u + S_ [ K -> L ] C _d u ) - S_ [ M -> K ] C _d u ) = S_ [ K -> L ] C _d u )
282	269 278 281	3eqtrd	\|- ( ph -> ( ( ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ` Y ) - ( ( x e. ( X [,] Y ) \|-> S. ( M (,) A ) C _d u ) ` X ) ) = S_ [ K -> L ] C _d u )
283	226 243 282	3eqtr3d	\|- ( ph -> S. ( X (,) Y ) ( E x. B ) _d x = S_ [ K -> L ] C _d u )
284	16 283	eqtr2d	\|- ( ph -> S_ [ K -> L ] C _d u = S_ [ X -> Y ] ( E x. B ) _d x )

Metamath Proof Explorer

Theorem itgsubstlem

Proof