Metamath Proof Explorer

Theorem hoidmvval0b

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

Ref Expression
Hypotheses hoidmvval0b.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 ) ) ) ) ) )
hoidmvval0b.x 
|- ( ph -> X e. Fin )
hoidmvval0b.a 
|- ( ph -> A : X --> RR )
Assertion hoidmvval0b 
|- ( ph -> ( A ( L ` X ) A ) = 0 )

Proof

Step Hyp Ref Expression
1 hoidmvval0b.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 hoidmvval0b.x 
 |-  ( ph -> X e. Fin )
3 hoidmvval0b.a 
 |-  ( ph -> A : X --> RR )
4 fveq2 
 |-  ( X = (/) -> ( L ` X ) = ( L ` (/) ) )
5 4 oveqd 
 |-  ( X = (/) -> ( A ( L ` X ) A ) = ( A ( L ` (/) ) A ) )
6 5 adantl 
 |-  ( ( ph /\ X = (/) ) -> ( A ( L ` X ) A ) = ( A ( L ` (/) ) A ) )
7 3 adantr 
 |-  ( ( ph /\ X = (/) ) -> A : X --> RR )
8 feq2 
 |-  ( X = (/) -> ( A : X --> RR <-> A : (/) --> RR ) )
9 8 adantl 
 |-  ( ( ph /\ X = (/) ) -> ( A : X --> RR <-> A : (/) --> RR ) )
10 7 9 mpbid 
 |-  ( ( ph /\ X = (/) ) -> A : (/) --> RR )
11 1 10 10 hoidmv0val 
 |-  ( ( ph /\ X = (/) ) -> ( A ( L ` (/) ) A ) = 0 )
12 6 11 eqtrd 
 |-  ( ( ph /\ X = (/) ) -> ( A ( L ` X ) A ) = 0 )
13 nfv 
 |-  F/ j ( ph /\ -. X = (/) )
14 2 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> X e. Fin )
15 3 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> A : X --> RR )
16 neqne 
 |-  ( -. X = (/) -> X =/= (/) )
17 n0 
 |-  ( X =/= (/) <-> E. j j e. X )
18 16 17 sylib 
 |-  ( -. X = (/) -> E. j j e. X )
19 18 adantl 
 |-  ( ( ph /\ -. X = (/) ) -> E. j j e. X )
20 simpr 
 |-  ( ( ph /\ j e. X ) -> j e. X )
21 3 ffvelrnda 
 |-  ( ( ph /\ j e. X ) -> ( A ` j ) e. RR )
22 eqidd 
 |-  ( ( ph /\ j e. X ) -> ( A ` j ) = ( A ` j ) )
23 21 22 eqled 
 |-  ( ( ph /\ j e. X ) -> ( A ` j ) <_ ( A ` j ) )
24 20 23 jca 
 |-  ( ( ph /\ j e. X ) -> ( j e. X /\ ( A ` j ) <_ ( A ` j ) ) )
25 24 ex 
 |-  ( ph -> ( j e. X -> ( j e. X /\ ( A ` j ) <_ ( A ` j ) ) ) )
26 25 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> ( j e. X -> ( j e. X /\ ( A ` j ) <_ ( A ` j ) ) ) )
27 26 eximdv 
 |-  ( ( ph /\ -. X = (/) ) -> ( E. j j e. X -> E. j ( j e. X /\ ( A ` j ) <_ ( A ` j ) ) ) )
28 19 27 mpd 
 |-  ( ( ph /\ -. X = (/) ) -> E. j ( j e. X /\ ( A ` j ) <_ ( A ` j ) ) )
29 df-rex 
 |-  ( E. j e. X ( A ` j ) <_ ( A ` j ) <-> E. j ( j e. X /\ ( A ` j ) <_ ( A ` j ) ) )
30 28 29 sylibr 
 |-  ( ( ph /\ -. X = (/) ) -> E. j e. X ( A ` j ) <_ ( A ` j ) )
31 13 1 14 15 15 30 hoidmvval0 
 |-  ( ( ph /\ -. X = (/) ) -> ( A ( L ` X ) A ) = 0 )
32 12 31 pm2.61dan 
 |-  ( ph -> ( A ( L ` X ) A ) = 0 )