Theorem ovnome

Description: ( voln*X ) is an outer measure on the space of multidimensional real numbers with dimension equal to the cardinality of the finite set X . Proposition 115D (a) of Fremlin1 p. 30 . (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypothesis	ovnome.1	|- ( ph -> X e. Fin )
Assertion	ovnome	|- ( ph -> ( voln* ` X ) e. OutMeas )

Proof

Step	Hyp	Ref	Expression
1		ovnome.1	|- ( ph -> X e. Fin )
2		ovexd	|- ( ph -> ( RR ^m X ) e. _V )
3	1	ovnf	|- ( ph -> ( voln* ` X ) : ~P ( RR ^m X ) --> ( 0 [,] +oo ) )
4	1	ovn0	|- ( ph -> ( ( voln* ` X ) ` (/) ) = 0 )
5	1	3ad2ant1	|- ( ( ph /\ x C_ ( RR ^m X ) /\ y C_ x ) -> X e. Fin )
6		simp3	|- ( ( ph /\ x C_ ( RR ^m X ) /\ y C_ x ) -> y C_ x )
7		simp2	|- ( ( ph /\ x C_ ( RR ^m X ) /\ y C_ x ) -> x C_ ( RR ^m X ) )
8	5 6 7	ovnssle	|- ( ( ph /\ x C_ ( RR ^m X ) /\ y C_ x ) -> ( ( voln* ` X ) ` y ) <_ ( ( voln* ` X ) ` x ) )
9	1	adantr	|- ( ( ph /\ a : NN --> ~P ( RR ^m X ) ) -> X e. Fin )
10		simpr	|- ( ( ph /\ a : NN --> ~P ( RR ^m X ) ) -> a : NN --> ~P ( RR ^m X ) )
11	9 10	ovnsubadd	|- ( ( ph /\ a : NN --> ~P ( RR ^m X ) ) -> ( ( voln* ` X ) ` U_ n e. NN ( a ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( ( voln* ` X ) ` ( a ` n ) ) ) ) )
12	2 3 4 8 11	isomennd	|- ( ph -> ( voln* ` X ) e. OutMeas )