Metamath Proof Explorer

Theorem hoiprodp1

Description: The dimensional volume of a half-open interval with dimension n + 1 . Used in the first equality of step (e) of Lemma 115B of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoiprodp1.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 ) ) ) ) ) )
hoiprodp1.y 
|- ( ph -> Y e. Fin )
hoiprodp1.3 
|- ( ph -> Z e. V )
hoiprodp1.z 
|- ( ph -> -. Z e. Y )
hoiprodp1.x 
|- X = ( Y u. { Z } )
hoiprodp1.a 
|- ( ph -> A : X --> RR )
hoiprodp1.b 
|- ( ph -> B : X --> RR )
hoiprodp1.g 
|- G = prod_ k e. Y ( vol ` ( ( A ` k ) [,) ( B ` k ) ) )
Assertion hoiprodp1 
|- ( ph -> ( A ( L ` X ) B ) = ( G x. ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hoiprodp1.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 hoiprodp1.y 
 |-  ( ph -> Y e. Fin )
3 hoiprodp1.3 
 |-  ( ph -> Z e. V )
4 hoiprodp1.z 
 |-  ( ph -> -. Z e. Y )
5 hoiprodp1.x 
 |-  X = ( Y u. { Z } )
6 hoiprodp1.a 
 |-  ( ph -> A : X --> RR )
7 hoiprodp1.b 
 |-  ( ph -> B : X --> RR )
8 hoiprodp1.g 
 |-  G = prod_ k e. Y ( vol ` ( ( A ` k ) [,) ( B ` k ) ) )
9 snfi 
 |-  { Z } e. Fin
10 9 a1i 
 |-  ( ph -> { Z } e. Fin )
11 unfi 
 |-  ( ( Y e. Fin /\ { Z } e. Fin ) -> ( Y u. { Z } ) e. Fin )
12 2 10 11 syl2anc 
 |-  ( ph -> ( Y u. { Z } ) e. Fin )
13 5 12 eqeltrid 
 |-  ( ph -> X e. Fin )
14 snidg 
 |-  ( Z e. V -> Z e. { Z } )
15 3 14 syl 
 |-  ( ph -> Z e. { Z } )
16 elun2 
 |-  ( Z e. { Z } -> Z e. ( Y u. { Z } ) )
17 15 16 syl 
 |-  ( ph -> Z e. ( Y u. { Z } ) )
18 17 5 eleqtrrdi 
 |-  ( ph -> Z e. X )
19 18 ne0d 
 |-  ( ph -> X =/= (/) )
20 1 13 19 6 7 hoidmvn0val 
 |-  ( ph -> ( A ( L ` X ) B ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
21 6 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR )
22 7 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) e. RR )
23 volicore 
 |-  ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR )
24 21 22 23 syl2anc 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR )
25 24 recnd 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. CC )
26 fveq2 
 |-  ( k = Z -> ( A ` k ) = ( A ` Z ) )
27 fveq2 
 |-  ( k = Z -> ( B ` k ) = ( B ` Z ) )
28 26 27 oveq12d 
 |-  ( k = Z -> ( ( A ` k ) [,) ( B ` k ) ) = ( ( A ` Z ) [,) ( B ` Z ) ) )
29 28 fveq2d 
 |-  ( k = Z -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) )
30 29 adantl 
 |-  ( ( ph /\ k = Z ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) )
31 13 25 18 30 fprodsplit1 
 |-  ( ph -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) x. prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) )
32 5 difeq1i 
 |-  ( X \ { Z } ) = ( ( Y u. { Z } ) \ { Z } )
33 32 a1i 
 |-  ( ph -> ( X \ { Z } ) = ( ( Y u. { Z } ) \ { Z } ) )
34 difun2 
 |-  ( ( Y u. { Z } ) \ { Z } ) = ( Y \ { Z } )
35 34 a1i 
 |-  ( ph -> ( ( Y u. { Z } ) \ { Z } ) = ( Y \ { Z } ) )
36 difsn 
 |-  ( -. Z e. Y -> ( Y \ { Z } ) = Y )
37 4 36 syl 
 |-  ( ph -> ( Y \ { Z } ) = Y )
38 33 35 37 3eqtrd 
 |-  ( ph -> ( X \ { Z } ) = Y )
39 38 prodeq1d 
 |-  ( ph -> prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = prod_ k e. Y ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
40 8 eqcomi 
 |-  prod_ k e. Y ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = G
41 40 a1i 
 |-  ( ph -> prod_ k e. Y ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = G )
42 39 41 eqtrd 
 |-  ( ph -> prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = G )
43 42 oveq2d 
 |-  ( ph -> ( ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) x. prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) = ( ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) x. G ) )
44 6 18 ffvelrnd 
 |-  ( ph -> ( A ` Z ) e. RR )
45 7 18 ffvelrnd 
 |-  ( ph -> ( B ` Z ) e. RR )
46 volicore 
 |-  ( ( ( A ` Z ) e. RR /\ ( B ` Z ) e. RR ) -> ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) e. RR )
47 44 45 46 syl2anc 
 |-  ( ph -> ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) e. RR )
48 47 recnd 
 |-  ( ph -> ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) e. CC )
49 6 adantr 
 |-  ( ( ph /\ k e. Y ) -> A : X --> RR )
50 ssun1 
 |-  Y C_ ( Y u. { Z } )
51 50 5 sseqtrri 
 |-  Y C_ X
52 id 
 |-  ( k e. Y -> k e. Y )
53 51 52 sselid 
 |-  ( k e. Y -> k e. X )
54 53 adantl 
 |-  ( ( ph /\ k e. Y ) -> k e. X )
55 49 54 ffvelrnd 
 |-  ( ( ph /\ k e. Y ) -> ( A ` k ) e. RR )
56 7 adantr 
 |-  ( ( ph /\ k e. Y ) -> B : X --> RR )
57 56 54 ffvelrnd 
 |-  ( ( ph /\ k e. Y ) -> ( B ` k ) e. RR )
58 55 57 23 syl2anc 
 |-  ( ( ph /\ k e. Y ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR )
59 2 58 fprodrecl 
 |-  ( ph -> prod_ k e. Y ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR )
60 8 59 eqeltrid 
 |-  ( ph -> G e. RR )
61 60 recnd 
 |-  ( ph -> G e. CC )
62 48 61 mulcomd 
 |-  ( ph -> ( ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) x. G ) = ( G x. ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) ) )
63 43 62 eqtrd 
 |-  ( ph -> ( ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) x. prod_ k e. ( X \ { Z } ) ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) = ( G x. ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) ) )
64 20 31 63 3eqtrd 
 |-  ( ph -> ( A ( L ` X ) B ) = ( G x. ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) ) )