Theorem ovnn0val

Description: The value of a (multidimensional) Lebesgue outer measure, defined on a nonzero-dimensional space of reals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	ovnn0val.1	|- ( ph -> X e. Fin )
	ovnn0val.2	|- ( ph -> X =/= (/) )
	ovnn0val.3	|- ( ph -> A C_ ( RR ^m X ) )
	ovnn0val.4	|- M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }
Assertion	ovnn0val	|- ( ph -> ( ( voln* ` X ) ` A ) = inf ( M , RR* , < ) )

Proof

Step	Hyp	Ref	Expression
1		ovnn0val.1	|- ( ph -> X e. Fin )
2		ovnn0val.2	|- ( ph -> X =/= (/) )
3		ovnn0val.3	|- ( ph -> A C_ ( RR ^m X ) )
4		ovnn0val.4	|- M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }
5	1 3 4	ovnval2	|- ( ph -> ( ( voln* ` X ) ` A ) = if ( X = (/) , 0 , inf ( M , RR* , < ) ) )
6	2	neneqd	|- ( ph -> -. X = (/) )
7	6	iffalsed	|- ( ph -> if ( X = (/) , 0 , inf ( M , RR* , < ) ) = inf ( M , RR* , < ) )
8	5 7	eqtrd	|- ( ph -> ( ( voln* ` X ) ` A ) = inf ( M , RR* , < ) )