Theorem vonn0hoi

Description: The Lebesgue outer measure of a multidimensional half-open interval when the dimension of the space is nonzero. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	vonn0hoi.x	|- ( ph -> X e. Fin )
	vonn0hoi.n	|- ( ph -> X =/= (/) )
	vonn0hoi.a	|- ( ph -> A : X --> RR )
	vonn0hoi.b	|- ( ph -> B : X --> RR )
	vonn0hoi.i	|- I = X_ k e. X ( ( A ` k ) [,) ( B ` k ) )
Assertion	vonn0hoi	|- ( ph -> ( ( voln ` X ) ` I ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		vonn0hoi.x	|- ( ph -> X e. Fin )
2		vonn0hoi.n	|- ( ph -> X =/= (/) )
3		vonn0hoi.a	|- ( ph -> A : X --> RR )
4		vonn0hoi.b	|- ( ph -> B : X --> RR )
5		vonn0hoi.i	|- I = X_ k e. X ( ( A ` k ) [,) ( B ` k ) )
6		eqid	|- ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) ) = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )
7	1 3 4 5 6	vonhoi	|- ( ph -> ( ( voln ` X ) ` I ) = ( A ( ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) ) ` X ) B ) )
8	6 1 2 3 4	hoidmvn0val	|- ( ph -> ( A ( ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) ) ` X ) B ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
9	7 8	eqtrd	|- ( ph -> ( ( voln ` X ) ` I ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )