Theorem sitmfval

Description: Value of the integral distance between two simple functions. (Contributed by Thierry Arnoux, 30-Jan-2018)

	Ref	Expression
Hypotheses	sitmval.d	|- D = ( dist ` W )
	sitmval.1	|- ( ph -> W e. V )
	sitmval.2	|- ( ph -> M e. U. ran measures )
	sitmfval.1	|- ( ph -> F e. dom ( W sitg M ) )
	sitmfval.2	|- ( ph -> G e. dom ( W sitg M ) )
Assertion	sitmfval	|- ( ph -> ( F ( W sitm M ) G ) = ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) ` ( F oF D G ) ) )

Proof

Step	Hyp	Ref	Expression
1		sitmval.d	|- D = ( dist ` W )
2		sitmval.1	|- ( ph -> W e. V )
3		sitmval.2	|- ( ph -> M e. U. ran measures )
4		sitmfval.1	|- ( ph -> F e. dom ( W sitg M ) )
5		sitmfval.2	|- ( ph -> G e. dom ( W sitg M ) )
6	1 2 3	sitmval	|- ( ph -> ( W sitm M ) = ( f e. dom ( W sitg M ) , g e. dom ( W sitg M ) |-> ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) ` ( f oF D g ) ) ) )
7		simprl	|- ( ( ph /\ ( f = F /\ g = G ) ) -> f = F )
8		simprr	|- ( ( ph /\ ( f = F /\ g = G ) ) -> g = G )
9	7 8	oveq12d	|- ( ( ph /\ ( f = F /\ g = G ) ) -> ( f oF D g ) = ( F oF D G ) )
10	9	fveq2d	|- ( ( ph /\ ( f = F /\ g = G ) ) -> ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) ` ( f oF D g ) ) = ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) ` ( F oF D G ) ) )
11		fvexd	|- ( ph -> ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) ` ( F oF D G ) ) e. _V )
12	6 10 4 5 11	ovmpod	|- ( ph -> ( F ( W sitm M ) G ) = ( ( ( RR*s |`s ( 0 [,] +oo ) ) sitg M ) ` ( F oF D G ) ) )