Theorem hoidmv0val

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

	Ref	Expression
Hypotheses	hoidmv0val.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 ) ) ) ) ) )
	hoidmv0val.a	|- ( ph -> A : (/) --> RR )
	hoidmv0val.b	|- ( ph -> B : (/) --> RR )
Assertion	hoidmv0val	|- ( ph -> ( A ( L ` (/) ) B ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		hoidmv0val.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		hoidmv0val.a	|- ( ph -> A : (/) --> RR )
3		hoidmv0val.b	|- ( ph -> B : (/) --> RR )
4		0fin	|- (/) e. Fin
5	4	a1i	|- ( ph -> (/) e. Fin )
6	1 2 3 5	hoidmvval	|- ( ph -> ( A ( L ` (/) ) B ) = if ( (/) = (/) , 0 , prod_ k e. (/) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) )
7		eqid	|- (/) = (/)
8		iftrue	|- ( (/) = (/) -> if ( (/) = (/) , 0 , prod_ k e. (/) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) = 0 )
9	7 8	ax-mp	|- if ( (/) = (/) , 0 , prod_ k e. (/) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) = 0
10	9	a1i	|- ( ph -> if ( (/) = (/) , 0 , prod_ k e. (/) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) = 0 )
11	6 10	eqtrd	|- ( ph -> ( A ( L ` (/) ) B ) = 0 )