Metamath Proof Explorer

Theorem hsphoival

Description: H is a function (that returns the representation of the right side of a half-open interval intersected with a half-space). Step (b) in Lemma 115B of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hsphoival.h 
|- H = ( x e. RR |-> ( a e. ( RR ^m X ) |-> ( j e. X |-> if ( j e. Y , ( a ` j ) , if ( ( a ` j ) <_ x , ( a ` j ) , x ) ) ) ) )
hsphoival.a 
|- ( ph -> A e. RR )
hsphoival.x 
|- ( ph -> X e. V )
hsphoival.b 
|- ( ph -> B : X --> RR )
hsphoival.k 
|- ( ph -> K e. X )
Assertion hsphoival 
|- ( ph -> ( ( ( H ` A ) ` B ) ` K ) = if ( K e. Y , ( B ` K ) , if ( ( B ` K ) <_ A , ( B ` K ) , A ) ) )

Proof

Step Hyp Ref Expression
1 hsphoival.h 
 |-  H = ( x e. RR |-> ( a e. ( RR ^m X ) |-> ( j e. X |-> if ( j e. Y , ( a ` j ) , if ( ( a ` j ) <_ x , ( a ` j ) , x ) ) ) ) )
2 hsphoival.a 
 |-  ( ph -> A e. RR )
3 hsphoival.x 
 |-  ( ph -> X e. V )
4 hsphoival.b 
 |-  ( ph -> B : X --> RR )
5 hsphoival.k 
 |-  ( ph -> K e. X )
6 breq2 
 |-  ( x = A -> ( ( a ` j ) <_ x <-> ( a ` j ) <_ A ) )
7 id 
 |-  ( x = A -> x = A )
8 6 7 ifbieq2d 
 |-  ( x = A -> if ( ( a ` j ) <_ x , ( a ` j ) , x ) = if ( ( a ` j ) <_ A , ( a ` j ) , A ) )
9 8 ifeq2d 
 |-  ( x = A -> if ( j e. Y , ( a ` j ) , if ( ( a ` j ) <_ x , ( a ` j ) , x ) ) = if ( j e. Y , ( a ` j ) , if ( ( a ` j ) <_ A , ( a ` j ) , A ) ) )
10 9 mpteq2dv 
 |-  ( x = A -> ( j e. X |-> if ( j e. Y , ( a ` j ) , if ( ( a ` j ) <_ x , ( a ` j ) , x ) ) ) = ( j e. X |-> if ( j e. Y , ( a ` j ) , if ( ( a ` j ) <_ A , ( a ` j ) , A ) ) ) )
11 10 mpteq2dv 
 |-  ( x = A -> ( a e. ( RR ^m X ) |-> ( j e. X |-> if ( j e. Y , ( a ` j ) , if ( ( a ` j ) <_ x , ( a ` j ) , x ) ) ) ) = ( a e. ( RR ^m X ) |-> ( j e. X |-> if ( j e. Y , ( a ` j ) , if ( ( a ` j ) <_ A , ( a ` j ) , A ) ) ) ) )
12 ovex 
 |-  ( RR ^m X ) e. _V
13 12 mptex 
 |-  ( a e. ( RR ^m X ) |-> ( j e. X |-> if ( j e. Y , ( a ` j ) , if ( ( a ` j ) <_ A , ( a ` j ) , A ) ) ) ) e. _V
14 13 a1i 
 |-  ( ph -> ( a e. ( RR ^m X ) |-> ( j e. X |-> if ( j e. Y , ( a ` j ) , if ( ( a ` j ) <_ A , ( a ` j ) , A ) ) ) ) e. _V )
15 1 11 2 14 fvmptd3 
 |-  ( ph -> ( H ` A ) = ( a e. ( RR ^m X ) |-> ( j e. X |-> if ( j e. Y , ( a ` j ) , if ( ( a ` j ) <_ A , ( a ` j ) , A ) ) ) ) )
16 fveq1 
 |-  ( a = B -> ( a ` j ) = ( B ` j ) )
17 16 breq1d 
 |-  ( a = B -> ( ( a ` j ) <_ A <-> ( B ` j ) <_ A ) )
18 17 16 ifbieq1d 
 |-  ( a = B -> if ( ( a ` j ) <_ A , ( a ` j ) , A ) = if ( ( B ` j ) <_ A , ( B ` j ) , A ) )
19 16 18 ifeq12d 
 |-  ( a = B -> if ( j e. Y , ( a ` j ) , if ( ( a ` j ) <_ A , ( a ` j ) , A ) ) = if ( j e. Y , ( B ` j ) , if ( ( B ` j ) <_ A , ( B ` j ) , A ) ) )
20 19 mpteq2dv 
 |-  ( a = B -> ( j e. X |-> if ( j e. Y , ( a ` j ) , if ( ( a ` j ) <_ A , ( a ` j ) , A ) ) ) = ( j e. X |-> if ( j e. Y , ( B ` j ) , if ( ( B ` j ) <_ A , ( B ` j ) , A ) ) ) )
21 20 adantl 
 |-  ( ( ph /\ a = B ) -> ( j e. X |-> if ( j e. Y , ( a ` j ) , if ( ( a ` j ) <_ A , ( a ` j ) , A ) ) ) = ( j e. X |-> if ( j e. Y , ( B ` j ) , if ( ( B ` j ) <_ A , ( B ` j ) , A ) ) ) )
22 reex 
 |-  RR e. _V
23 22 a1i 
 |-  ( ph -> RR e. _V )
24 23 3 jca 
 |-  ( ph -> ( RR e. _V /\ X e. V ) )
25 elmapg 
 |-  ( ( RR e. _V /\ X e. V ) -> ( B e. ( RR ^m X ) <-> B : X --> RR ) )
26 24 25 syl 
 |-  ( ph -> ( B e. ( RR ^m X ) <-> B : X --> RR ) )
27 4 26 mpbird 
 |-  ( ph -> B e. ( RR ^m X ) )
28 mptexg 
 |-  ( X e. V -> ( j e. X |-> if ( j e. Y , ( B ` j ) , if ( ( B ` j ) <_ A , ( B ` j ) , A ) ) ) e. _V )
29 3 28 syl 
 |-  ( ph -> ( j e. X |-> if ( j e. Y , ( B ` j ) , if ( ( B ` j ) <_ A , ( B ` j ) , A ) ) ) e. _V )
30 15 21 27 29 fvmptd 
 |-  ( ph -> ( ( H ` A ) ` B ) = ( j e. X |-> if ( j e. Y , ( B ` j ) , if ( ( B ` j ) <_ A , ( B ` j ) , A ) ) ) )
31 eleq1 
 |-  ( j = K -> ( j e. Y <-> K e. Y ) )
32 fveq2 
 |-  ( j = K -> ( B ` j ) = ( B ` K ) )
33 32 breq1d 
 |-  ( j = K -> ( ( B ` j ) <_ A <-> ( B ` K ) <_ A ) )
34 33 32 ifbieq1d 
 |-  ( j = K -> if ( ( B ` j ) <_ A , ( B ` j ) , A ) = if ( ( B ` K ) <_ A , ( B ` K ) , A ) )
35 31 32 34 ifbieq12d 
 |-  ( j = K -> if ( j e. Y , ( B ` j ) , if ( ( B ` j ) <_ A , ( B ` j ) , A ) ) = if ( K e. Y , ( B ` K ) , if ( ( B ` K ) <_ A , ( B ` K ) , A ) ) )
36 35 adantl 
 |-  ( ( ph /\ j = K ) -> if ( j e. Y , ( B ` j ) , if ( ( B ` j ) <_ A , ( B ` j ) , A ) ) = if ( K e. Y , ( B ` K ) , if ( ( B ` K ) <_ A , ( B ` K ) , A ) ) )
37 4 5 ffvelcdmd 
 |-  ( ph -> ( B ` K ) e. RR )
38 37 2 ifcld 
 |-  ( ph -> if ( ( B ` K ) <_ A , ( B ` K ) , A ) e. RR )
39 37 38 ifexd 
 |-  ( ph -> if ( K e. Y , ( B ` K ) , if ( ( B ` K ) <_ A , ( B ` K ) , A ) ) e. _V )
40 30 36 5 39 fvmptd 
 |-  ( ph -> ( ( ( H ` A ) ` B ) ` K ) = if ( K e. Y , ( B ` K ) , if ( ( B ` K ) <_ A , ( B ` K ) , A ) ) )