Theorem vonmea

Description: ( volnX ) is a measure on the space of multidimensional real numbers with dimension equal to the cardinality of the finite set X . Comments in Definition 115E of Fremlin1 p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypothesis	vonmea.1	$$⊢\phi \to X\in \mathrm{Fin}$$
Assertion	vonmea	$$⊢\phi \to \mathrm{voln}\left(X\right)\in \mathrm{Meas}$$

Proof

Step	Hyp	Ref	Expression
1		vonmea.1	$$⊢\phi \to X\in \mathrm{Fin}$$
2	1	vonval	$$⊢\phi \to \mathrm{voln}\left(X\right)={\mathrm{voln*}\left(X\right)\upharpoonright }_{\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)}$$
3	1	ovnome	$$⊢\phi \to \mathrm{voln*}\left(X\right)\in \mathrm{OutMeas}$$
4		eqid	$$⊢\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)=\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)$$
5	3 4	caratheodory	$$⊢\phi \to {\mathrm{voln*}\left(X\right)\upharpoonright }_{\mathrm{CaraGen}\left(\mathrm{voln*}\left(X\right)\right)}\in \mathrm{Meas}$$
6	2 5	eqeltrd	$$⊢\phi \to \mathrm{voln}\left(X\right)\in \mathrm{Meas}$$