Metamath Proof Explorer

Theorem hoidmvval

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

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

Proof

Step Hyp Ref Expression
1 hoidmvval.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 hoidmvval.a 
 |-  ( ph -> A : X --> RR )
3 hoidmvval.b 
 |-  ( ph -> B : X --> RR )
4 hoidmvval.x 
 |-  ( ph -> X e. Fin )
5 oveq2 
 |-  ( x = X -> ( RR ^m x ) = ( RR ^m X ) )
6 eqeq1 
 |-  ( x = X -> ( x = (/) <-> X = (/) ) )
7 prodeq1 
 |-  ( x = X -> prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) = prod_ k e. X ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) )
8 6 7 ifbieq2d 
 |-  ( x = X -> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) = if ( X = (/) , 0 , prod_ k e. X ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) )
9 5 5 8 mpoeq123dv 
 |-  ( x = X -> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) = ( a e. ( RR ^m X ) , b e. ( RR ^m X ) |-> if ( X = (/) , 0 , prod_ k e. X ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )
10 ovex 
 |-  ( RR ^m X ) e. _V
11 10 10 mpoex 
 |-  ( a e. ( RR ^m X ) , b e. ( RR ^m X ) |-> if ( X = (/) , 0 , prod_ k e. X ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) e. _V
12 11 a1i 
 |-  ( ph -> ( a e. ( RR ^m X ) , b e. ( RR ^m X ) |-> if ( X = (/) , 0 , prod_ k e. X ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) e. _V )
13 1 9 4 12 fvmptd3 
 |-  ( ph -> ( L ` X ) = ( a e. ( RR ^m X ) , b e. ( RR ^m X ) |-> if ( X = (/) , 0 , prod_ k e. X ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )
14 fveq1 
 |-  ( a = A -> ( a ` k ) = ( A ` k ) )
15 14 adantr 
 |-  ( ( a = A /\ b = B ) -> ( a ` k ) = ( A ` k ) )
16 fveq1 
 |-  ( b = B -> ( b ` k ) = ( B ` k ) )
17 16 adantl 
 |-  ( ( a = A /\ b = B ) -> ( b ` k ) = ( B ` k ) )
18 15 17 oveq12d 
 |-  ( ( a = A /\ b = B ) -> ( ( a ` k ) [,) ( b ` k ) ) = ( ( A ` k ) [,) ( B ` k ) ) )
19 18 fveq2d 
 |-  ( ( a = A /\ b = B ) -> ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) = ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
20 19 prodeq2ad 
 |-  ( ( a = A /\ b = B ) -> prod_ k e. X ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
21 20 ifeq2d 
 |-  ( ( a = A /\ b = B ) -> if ( X = (/) , 0 , prod_ k e. X ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) = if ( X = (/) , 0 , prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) )
22 21 adantl 
 |-  ( ( ph /\ ( a = A /\ b = B ) ) -> if ( X = (/) , 0 , prod_ k e. X ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) = if ( X = (/) , 0 , prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) )
23 reex 
 |-  RR e. _V
24 23 a1i 
 |-  ( ph -> RR e. _V )
25 elmapg 
 |-  ( ( RR e. _V /\ X e. Fin ) -> ( A e. ( RR ^m X ) <-> A : X --> RR ) )
26 24 4 25 syl2anc 
 |-  ( ph -> ( A e. ( RR ^m X ) <-> A : X --> RR ) )
27 2 26 mpbird 
 |-  ( ph -> A e. ( RR ^m X ) )
28 elmapg 
 |-  ( ( RR e. _V /\ X e. Fin ) -> ( B e. ( RR ^m X ) <-> B : X --> RR ) )
29 24 4 28 syl2anc 
 |-  ( ph -> ( B e. ( RR ^m X ) <-> B : X --> RR ) )
30 3 29 mpbird 
 |-  ( ph -> B e. ( RR ^m X ) )
31 c0ex 
 |-  0 e. _V
32 prodex 
 |-  prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. _V
33 31 32 ifex 
 |-  if ( X = (/) , 0 , prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) e. _V
34 33 a1i 
 |-  ( ph -> if ( X = (/) , 0 , prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) e. _V )
35 13 22 27 30 34 ovmpod 
 |-  ( ph -> ( A ( L ` X ) B ) = if ( X = (/) , 0 , prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) )