Theorem ovnovol

Description: The 1-dimensional Lebesgue outer measure agrees with the Lebesgue outer measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ovnovol.a	|- ( ph -> A e. V )
	ovnovol.b	|- ( ph -> B C_ RR )
Assertion	ovnovol	|- ( ph -> ( ( voln* ` { A } ) ` ( B ^m { A } ) ) = ( vol* ` B ) )

Proof

Step	Hyp	Ref	Expression
1		ovnovol.a	|- ( ph -> A e. V )
2		ovnovol.b	|- ( ph -> B C_ RR )
3		eqid	|- { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m { A } ) ^m NN ) ( ( B ^m { A } ) C_ U_ j e. NN X_ k e. { A } ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m { A } ) ^m NN ) ( ( B ^m { A } ) C_ U_ j e. NN X_ k e. { A } ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. { A } ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }
4		eqeq1	|- ( w = z -> ( w = ( sum^ ` ( ( vol o. [,) ) o. f ) ) <-> z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) )
5	4	anbi2d	|- ( w = z -> ( ( B C_ U. ran ( [,) o. f ) /\ w = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) <-> ( B C_ U. ran ( [,) o. f ) /\ z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) ) )
6	5	rexbidv	|- ( w = z -> ( E. f e. ( ( RR X. RR ) ^m NN ) ( B C_ U. ran ( [,) o. f ) /\ w = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) <-> E. f e. ( ( RR X. RR ) ^m NN ) ( B C_ U. ran ( [,) o. f ) /\ z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) ) )
7	6	cbvrabv	|- { w e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( B C_ U. ran ( [,) o. f ) /\ w = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) } = { z e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( B C_ U. ran ( [,) o. f ) /\ z = ( sum^ ` ( ( vol o. [,) ) o. f ) ) ) }
8	1 2 3 7	ovnovollem3	|- ( ph -> ( ( voln* ` { A } ) ` ( B ^m { A } ) ) = ( vol* ` B ) )