Metamath Proof Explorer

Theorem hoidmvval0

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 hoidmvval0.p 
|- F/ j ph
hoidmvval0.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 ) ) ) ) ) )
hoidmvval0.x 
|- ( ph -> X e. Fin )
hoidmvval0.a 
|- ( ph -> A : X --> RR )
hoidmvval0.b 
|- ( ph -> B : X --> RR )
hoidmvval0.j 
|- ( ph -> E. j e. X ( B ` j ) <_ ( A ` j ) )
Assertion hoidmvval0 
|- ( ph -> ( A ( L ` X ) B ) = 0 )

Proof

Step Hyp Ref Expression
1 hoidmvval0.p 
 |-  F/ j ph
2 hoidmvval0.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 ) ) ) ) ) )
3 hoidmvval0.x 
 |-  ( ph -> X e. Fin )
4 hoidmvval0.a 
 |-  ( ph -> A : X --> RR )
5 hoidmvval0.b 
 |-  ( ph -> B : X --> RR )
6 hoidmvval0.j 
 |-  ( ph -> E. j e. X ( B ` j ) <_ ( A ` j ) )
7 id 
 |-  ( ph -> ph )
8 fveq2 
 |-  ( k = j -> ( B ` k ) = ( B ` j ) )
9 fveq2 
 |-  ( k = j -> ( A ` k ) = ( A ` j ) )
10 8 9 breq12d 
 |-  ( k = j -> ( ( B ` k ) <_ ( A ` k ) <-> ( B ` j ) <_ ( A ` j ) ) )
11 10 cbvrexvw 
 |-  ( E. k e. X ( B ` k ) <_ ( A ` k ) <-> E. j e. X ( B ` j ) <_ ( A ` j ) )
12 rexn0 
 |-  ( E. k e. X ( B ` k ) <_ ( A ` k ) -> X =/= (/) )
13 11 12 sylbir 
 |-  ( E. j e. X ( B ` j ) <_ ( A ` j ) -> X =/= (/) )
14 6 13 syl 
 |-  ( ph -> X =/= (/) )
15 3 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> X e. Fin )
16 simpr 
 |-  ( ( ph /\ X =/= (/) ) -> X =/= (/) )
17 4 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> A : X --> RR )
18 5 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> B : X --> RR )
19 2 15 16 17 18 hoidmvn0val 
 |-  ( ( ph /\ X =/= (/) ) -> ( A ( L ` X ) B ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
20 6 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> E. j e. X ( B ` j ) <_ ( A ` j ) )
21 nfv 
 |-  F/ j X =/= (/)
22 1 21 nfan 
 |-  F/ j ( ph /\ X =/= (/) )
23 nfv 
 |-  F/ j prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = 0
24 nfv 
 |-  F/ k ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) )
25 nfcv 
 |-  F/_ k ( vol ` ( ( A ` j ) [,) ( B ` j ) ) )
26 3 3ad2ant1 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> X e. Fin )
27 4 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR )
28 5 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) e. RR )
29 volicore 
 |-  ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR )
30 27 28 29 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR )
31 30 recnd 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. CC )
32 31 3ad2antl1 
 |-  ( ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. CC )
33 9 8 oveq12d 
 |-  ( k = j -> ( ( A ` k ) [,) ( B ` k ) ) = ( ( A ` j ) [,) ( B ` j ) ) )
34 33 fveq2d 
 |-  ( k = j -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( vol ` ( ( A ` j ) [,) ( B ` j ) ) ) )
35 simp2 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> j e. X )
36 4 ffvelrnda 
 |-  ( ( ph /\ j e. X ) -> ( A ` j ) e. RR )
37 36 3adant3 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> ( A ` j ) e. RR )
38 5 ffvelrnda 
 |-  ( ( ph /\ j e. X ) -> ( B ` j ) e. RR )
39 38 3adant3 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> ( B ` j ) e. RR )
40 volico 
 |-  ( ( ( A ` j ) e. RR /\ ( B ` j ) e. RR ) -> ( vol ` ( ( A ` j ) [,) ( B ` j ) ) ) = if ( ( A ` j ) < ( B ` j ) , ( ( B ` j ) - ( A ` j ) ) , 0 ) )
41 37 39 40 syl2anc 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> ( vol ` ( ( A ` j ) [,) ( B ` j ) ) ) = if ( ( A ` j ) < ( B ` j ) , ( ( B ` j ) - ( A ` j ) ) , 0 ) )
42 simp3 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> ( B ` j ) <_ ( A ` j ) )
43 39 37 lenltd 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> ( ( B ` j ) <_ ( A ` j ) <-> -. ( A ` j ) < ( B ` j ) ) )
44 42 43 mpbid 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> -. ( A ` j ) < ( B ` j ) )
45 44 iffalsed 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> if ( ( A ` j ) < ( B ` j ) , ( ( B ` j ) - ( A ` j ) ) , 0 ) = 0 )
46 41 45 eqtrd 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> ( vol ` ( ( A ` j ) [,) ( B ` j ) ) ) = 0 )
47 24 25 26 32 34 35 46 fprod0 
 |-  ( ( ph /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = 0 )
48 47 3adant1r 
 |-  ( ( ( ph /\ X =/= (/) ) /\ j e. X /\ ( B ` j ) <_ ( A ` j ) ) -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = 0 )
49 48 3exp 
 |-  ( ( ph /\ X =/= (/) ) -> ( j e. X -> ( ( B ` j ) <_ ( A ` j ) -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = 0 ) ) )
50 22 23 49 rexlimd 
 |-  ( ( ph /\ X =/= (/) ) -> ( E. j e. X ( B ` j ) <_ ( A ` j ) -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = 0 ) )
51 20 50 mpd 
 |-  ( ( ph /\ X =/= (/) ) -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = 0 )
52 eqidd 
 |-  ( ( ph /\ X =/= (/) ) -> 0 = 0 )
53 19 51 52 3eqtrd 
 |-  ( ( ph /\ X =/= (/) ) -> ( A ( L ` X ) B ) = 0 )
54 7 14 53 syl2anc 
 |-  ( ph -> ( A ( L ` X ) B ) = 0 )