Theorem hsphoif 38398

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.)

Hypotheses

Ref	Expression
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

Ref	Expression
hsphoif	|- ( ph -> ( ( H ` A ) ` B ) : X --> RR )

Distinct variable groups:   A, a, j, x   B, a, j   X, a, j, x   Y, a, x   ph, a, j, x

Allowed substitution hints:   B( x)   H( x, j, a)   V( x, j, a)   Y( j)

Proof of Theorem hsphoif

Step	Hyp	Ref	Expression
1		hsphoif.b	. . . . 5 |- ( ph -> B : X --> RR )
2	1	ffvelrnda 6022	. . . 4 |- ( ( ph /\ j e. X ) -> ( B ` j ) e. RR )
3		hsphoif.a	. . . . . 6 |- ( ph -> A e. RR )
4	3	adantr 467	. . . . 5 |- ( ( ph /\ j e. X ) -> A e. RR )
5	2, 4	ifcld 3924	. . . 4 |- ( ( ph /\ j e. X ) -> if ( ( B ` j ) <_ A , ( B ` j ) , A ) e. RR )
6	2, 5	ifcld 3924	. . 3 |- ( ( ph /\ j e. X ) -> if ( j e. Y , ( B ` j ) , if ( ( B ` j ) <_ A , ( B ` j ) , A ) ) e. RR )
7		eqid 2451	. . 3 |- ( 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 ) ) )
8	6, 7	fmptd 6046	. 2 |- ( ph -> ( j e. X |-> if ( j e. Y , ( B ` j ) , if ( ( B ` j ) <_ A , ( B ` j ) , A ) ) ) : X --> RR )
9		hsphoif.h	. . . . . 6 |- 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 ) ) ) ) )
10	9	a1i 11	. . . . 5 |- ( ph -> 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 ) ) ) ) ) )
11		breq2 4406	. . . . . . . . . 10 |- ( x = A -> ( ( a ` j ) <_ x <-> ( a ` j ) <_ A ) )
12		id 22	. . . . . . . . . 10 |- ( x = A -> x = A )
13	11, 12	ifbieq2d 3906	. . . . . . . . 9 |- ( x = A -> if ( ( a ` j ) <_ x , ( a ` j ) , x ) = if ( ( a ` j ) <_ A , ( a ` j ) , A ) )
14	13	ifeq2d 3900	. . . . . . . 8 |- ( 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 4490	. . . . . . 7 |- ( 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 4490	. . . . . 6 |- ( 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	16	adantl 468	. . . . 5 |- ( ( ph /\ 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 ) ) ) ) )
18		ovex 6318	. . . . . . 7 |- ( RR ^m X ) e. _V
19	18	mptex 6136	. . . . . 6 |- ( a e. ( RR ^m X ) |-> ( j e. X |-> if ( j e. Y , ( a ` j ) , if ( ( a ` j ) <_ A , ( a ` j ) , A ) ) ) ) e. _V
20	19	a1i 11	. . . . 5 |- ( ph -> ( a e. ( RR ^m X ) |-> ( j e. X |-> if ( j e. Y , ( a ` j ) , if ( ( a ` j ) <_ A , ( a ` j ) , A ) ) ) ) e. _V )
21	10, 17, 3, 20	fvmptd 5954	. . . 4 |- ( ph -> ( H ` A ) = ( a e. ( RR ^m X ) |-> ( j e. X |-> if ( j e. Y , ( a ` j ) , if ( ( a ` j ) <_ A , ( a ` j ) , A ) ) ) ) )
22		fveq1 5864	. . . . . . 7 |- ( a = B -> ( a ` j ) = ( B ` j ) )
23	22	breq1d 4412	. . . . . . . 8 |- ( a = B -> ( ( a ` j ) <_ A <-> ( B ` j ) <_ A ) )
24	23, 22	ifbieq1d 3904	. . . . . . 7 |- ( a = B -> if ( ( a ` j ) <_ A , ( a ` j ) , A ) = if ( ( B ` j ) <_ A , ( B ` j ) , A ) )
25	22, 24	ifeq12d 3901	. . . . . 6 |- ( 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 ) ) )
26	25	mpteq2dv 4490	. . . . 5 |- ( 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	26	adantl 468	. . . 4 |- ( ( 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 ) ) ) )
28		reex 9630	. . . . . . . 8 |- RR e. _V
29	28	a1i 11	. . . . . . 7 |- ( ph -> RR e. _V )
30		hsphoif.x	. . . . . . 7 |- ( ph -> X e. V )
31	29, 30	jca 535	. . . . . 6 |- ( ph -> ( RR e. _V /\ X e. V ) )
32		elmapg 7485	. . . . . 6 |- ( ( RR e. _V /\ X e. V ) -> ( B e. ( RR ^m X ) <-> B : X --> RR ) )
33	31, 32	syl 17	. . . . 5 |- ( ph -> ( B e. ( RR ^m X ) <-> B : X --> RR ) )
34	1, 33	mpbird 236	. . . 4 |- ( ph -> B e. ( RR ^m X ) )
35		mptexg 6135	. . . . 5 |- ( X e. V -> ( j e. X |-> if ( j e. Y , ( B ` j ) , if ( ( B ` j ) <_ A , ( B ` j ) , A ) ) ) e. _V )
36	30, 35	syl 17	. . . 4 |- ( ph -> ( j e. X |-> if ( j e. Y , ( B ` j ) , if ( ( B ` j ) <_ A , ( B ` j ) , A ) ) ) e. _V )
37	21, 27, 34, 36	fvmptd 5954	. . 3 |- ( ph -> ( ( H ` A ) ` B ) = ( j e. X |-> if ( j e. Y , ( B ` j ) , if ( ( B ` j ) <_ A , ( B ` j ) , A ) ) ) )
38	37	feq1d 5714	. 2 |- ( ph -> ( ( ( H ` A ) ` B ) : X --> RR <-> ( j e. X |-> if ( j e. Y , ( B ` j ) , if ( ( B ` j ) <_ A , ( B ` j ) , A ) ) ) : X --> RR ) )
39	8, 38	mpbird 236	1 |- ( ph -> ( ( H ` A ) ` B ) : X --> RR )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   = wceq 1444   e. wcel 1887   _Vcvv 3045   ifcif 3881   class class class wbr 4402   |-> cmpt 4461   -->wf 5578   ` cfv 5582  (class class class)co 6290   ^m cmap 7472   RRcr 9538   <_ cle 9676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-cnex 9595  ax-resscn 9596

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-map 7474

This theorem is referenced by:  hsphoidmvle2  38407  hsphoidmvle  38408  sge0hsphoire  38411  hoidmvlelem1  38417  hoidmvlelem2  38418  hoidmvlelem4  38420  hspmbllem1  38448  hspmbllem2  38449