Metamath Proof Explorer

Theorem hsphoif

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 hsphoif.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 ) ) ) ) )
hsphoif.a 
|- ( ph -> A e. RR )
hsphoif.x 
|- ( ph -> X e. V )
hsphoif.b 
|- ( ph -> B : X --> RR )
Assertion hsphoif 
|- ( ph -> ( ( H ` A ) ` B ) : X --> RR )

Proof

Step Hyp Ref Expression
1 hsphoif.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 hsphoif.a 
 |-  ( ph -> A e. RR )
3 hsphoif.x 
 |-  ( ph -> X e. V )
4 hsphoif.b 
 |-  ( ph -> B : X --> RR )
5 4 ffvelrnda 
 |-  ( ( ph /\ j e. X ) -> ( B ` j ) e. RR )
6 2 adantr 
 |-  ( ( ph /\ j e. X ) -> A e. RR )
7 5 6 ifcld 
 |-  ( ( ph /\ j e. X ) -> if ( ( B ` j ) <_ A , ( B ` j ) , A ) e. RR )
8 5 7 ifcld 
 |-  ( ( ph /\ j e. X ) -> if ( j e. Y , ( B ` j ) , if ( ( B ` j ) <_ A , ( B ` j ) , A ) ) e. RR )
9 eqid 
 |-  ( j e. X |-> if ( j e. Y , ( B ` j ) , if ( ( B ` j ) <_ A , ( B ` j ) , A ) ) ) = ( j e. X |-> if ( j e. Y , ( B ` j ) , if ( ( B ` j ) <_ A , ( B ` j ) , A ) ) )
10 8 9 fmptd 
 |-  ( ph -> ( j e. X |-> if ( j e. Y , ( B ` j ) , if ( ( B ` j ) <_ A , ( B ` j ) , A ) ) ) : X --> RR )
11 breq2 
 |-  ( x = A -> ( ( a ` j ) <_ x <-> ( a ` j ) <_ A ) )
12 id 
 |-  ( x = A -> x = A )
13 11 12 ifbieq2d 
 |-  ( x = A -> if ( ( a ` j ) <_ x , ( a ` j ) , x ) = if ( ( a ` j ) <_ A , ( a ` j ) , A ) )
14 13 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 ) ) )
15 14 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 ) ) ) )
16 15 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 ) ) ) ) )
17 ovex 
 |-  ( RR ^m X ) e. _V
18 17 mptex 
 |-  ( a e. ( RR ^m X ) |-> ( j e. X |-> if ( j e. Y , ( a ` j ) , if ( ( a ` j ) <_ A , ( a ` j ) , A ) ) ) ) e. _V
19 18 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 )
20 1 16 2 19 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 ) ) ) ) )
21 fveq1 
 |-  ( a = B -> ( a ` j ) = ( B ` j ) )
22 21 breq1d 
 |-  ( a = B -> ( ( a ` j ) <_ A <-> ( B ` j ) <_ A ) )
23 22 21 ifbieq1d 
 |-  ( a = B -> if ( ( a ` j ) <_ A , ( a ` j ) , A ) = if ( ( B ` j ) <_ A , ( B ` j ) , A ) )
24 21 23 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 ) ) )
25 24 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 ) ) ) )
26 25 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 ) ) ) )
27 reex 
 |-  RR e. _V
28 27 a1i 
 |-  ( ph -> RR e. _V )
29 28 3 jca 
 |-  ( ph -> ( RR e. _V /\ X e. V ) )
30 elmapg 
 |-  ( ( RR e. _V /\ X e. V ) -> ( B e. ( RR ^m X ) <-> B : X --> RR ) )
31 29 30 syl 
 |-  ( ph -> ( B e. ( RR ^m X ) <-> B : X --> RR ) )
32 4 31 mpbird 
 |-  ( ph -> B e. ( RR ^m X ) )
33 mptexg 
 |-  ( X e. V -> ( j e. X |-> if ( j e. Y , ( B ` j ) , if ( ( B ` j ) <_ A , ( B ` j ) , A ) ) ) e. _V )
34 3 33 syl 
 |-  ( ph -> ( j e. X |-> if ( j e. Y , ( B ` j ) , if ( ( B ` j ) <_ A , ( B ` j ) , A ) ) ) e. _V )
35 20 26 32 34 fvmptd 
 |-  ( ph -> ( ( H ` A ) ` B ) = ( j e. X |-> if ( j e. Y , ( B ` j ) , if ( ( B ` j ) <_ A , ( B ` j ) , A ) ) ) )
36 35 feq1d 
 |-  ( ph -> ( ( ( H ` A ) ` B ) : X --> RR <-> ( j e. X |-> if ( j e. Y , ( B ` j ) , if ( ( B ` j ) <_ A , ( B ` j ) , A ) ) ) : X --> RR ) )
37 10 36 mpbird 
 |-  ( ph -> ( ( H ` A ) ` B ) : X --> RR )