Metamath Proof Explorer

Theorem hoidmvn0val

Description: The dimensional volume of a non-0-dimensional half-open interval. Definition 115A (c) of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020)

		Ref	Expression
	Hypotheses	hoidmvn0val.l	\|- L = ( 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 ) ) ) ) ) )
		hoidmvn0val.x	\|- ( ph -> X e. Fin )
		hoidmvn0val.n	\|- ( ph -> X =/= (/) )
		hoidmvn0val.a	\|- ( ph -> A : X --> RR )
		hoidmvn0val.b	\|- ( ph -> B : X --> RR )
	Assertion	hoidmvn0val	\|- ( ph -> ( A ( L ` X ) B ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		hoidmvn0val.l	\|- L = ( 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 ) ) ) ) ) )
2		hoidmvn0val.x	\|- ( ph -> X e. Fin )
3		hoidmvn0val.n	\|- ( ph -> X =/= (/) )
4		hoidmvn0val.a	\|- ( ph -> A : X --> RR )
5		hoidmvn0val.b	\|- ( ph -> B : X --> RR )
6	1 4 5 2	hoidmvval	\|- ( ph -> ( A ( L ` X ) B ) = if ( X = (/) , 0 , prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) )
7	3	neneqd	\|- ( ph -> -. X = (/) )
8	7	iffalsed	\|- ( ph -> if ( X = (/) , 0 , prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
9	6 8	eqtrd	\|- ( ph -> ( A ( L ` X ) B ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )