Theorem pcoval2 22040

Description: Evaluate the concatenation of two paths on the second half. (Contributed by Jeff Madsen, 15-Jun-2010.) (Proof shortened by Mario Carneiro, 7-Jun-2014.)

Hypotheses

Ref	Expression
pcoval.2	|- ( ph -> F e. ( II Cn J ) )
pcoval.3	|- ( ph -> G e. ( II Cn J ) )
pcoval2.4	|- ( ph -> ( F ` 1 ) = ( G ` 0 ) )

Assertion

Ref	Expression
pcoval2	|- ( ( ph /\ X e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( F ( *p ` J ) G ) ` X ) = ( G ` ( ( 2 x. X ) - 1 ) ) )

Proof of Theorem pcoval2

Step	Hyp	Ref	Expression
1		0re 9640	. . . . 5 |- 0 e. RR
2		1re 9639	. . . . 5 |- 1 e. RR
3		halfre 10825	. . . . . 6 |- ( 1 / 2 ) e. RR
4		halfgt0 10827	. . . . . 6 |- 0 < ( 1 / 2 )
5	1, 3, 4	ltleii 9754	. . . . 5 |- 0 <_ ( 1 / 2 )
6		1le1 10237	. . . . 5 |- 1 <_ 1
7		iccss 11699	. . . . 5 |- ( ( ( 0 e. RR /\ 1 e. RR ) /\ ( 0 <_ ( 1 / 2 ) /\ 1 <_ 1 ) ) -> ( ( 1 / 2 ) [,] 1 ) C_ ( 0 [,] 1 ) )
8	1, 2, 5, 6, 7	mp4an 678	. . . 4 |- ( ( 1 / 2 ) [,] 1 ) C_ ( 0 [,] 1 )
9	8	sseli 3427	. . 3 |- ( X e. ( ( 1 / 2 ) [,] 1 ) -> X e. ( 0 [,] 1 ) )
10		pcoval.2	. . . 4 |- ( ph -> F e. ( II Cn J ) )
11		pcoval.3	. . . 4 |- ( ph -> G e. ( II Cn J ) )
12	10, 11	pcovalg 22036	. . 3 |- ( ( ph /\ X e. ( 0 [,] 1 ) ) -> ( ( F ( *p ` J ) G ) ` X ) = if ( X <_ ( 1 / 2 ) , ( F ` ( 2 x. X ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) )
13	9, 12	sylan2 477	. 2 |- ( ( ph /\ X e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( F ( *p ` J ) G ) ` X ) = if ( X <_ ( 1 / 2 ) , ( F ` ( 2 x. X ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) )
14		pcoval2.4	. . . . . . . 8 |- ( ph -> ( F ` 1 ) = ( G ` 0 ) )
15	14	adantr 467	. . . . . . 7 |- ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> ( F ` 1 ) = ( G ` 0 ) )
16		simprr 765	. . . . . . . . . . 11 |- ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> X <_ ( 1 / 2 ) )
17	3, 2	elicc2i 11697	. . . . . . . . . . . . 13 |- ( X e. ( ( 1 / 2 ) [,] 1 ) <-> ( X e. RR /\ ( 1 / 2 ) <_ X /\ X <_ 1 ) )
18	17	simp2bi 1023	. . . . . . . . . . . 12 |- ( X e. ( ( 1 / 2 ) [,] 1 ) -> ( 1 / 2 ) <_ X )
19	18	ad2antrl 733	. . . . . . . . . . 11 |- ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> ( 1 / 2 ) <_ X )
20	17	simp1bi 1022	. . . . . . . . . . . . 13 |- ( X e. ( ( 1 / 2 ) [,] 1 ) -> X e. RR )
21	20	ad2antrl 733	. . . . . . . . . . . 12 |- ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> X e. RR )
22		letri3 9716	. . . . . . . . . . . 12 |- ( ( X e. RR /\ ( 1 / 2 ) e. RR ) -> ( X = ( 1 / 2 ) <-> ( X <_ ( 1 / 2 ) /\ ( 1 / 2 ) <_ X ) ) )
23	21, 3, 22	sylancl 667	. . . . . . . . . . 11 |- ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> ( X = ( 1 / 2 ) <-> ( X <_ ( 1 / 2 ) /\ ( 1 / 2 ) <_ X ) ) )
24	16, 19, 23	mpbir2and 932	. . . . . . . . . 10 |- ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> X = ( 1 / 2 ) )
25	24	oveq2d 6304	. . . . . . . . 9 |- ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> ( 2 x. X ) = ( 2 x. ( 1 / 2 ) ) )
26		2cn 10677	. . . . . . . . . 10 |- 2 e. CC
27		2ne0 10699	. . . . . . . . . 10 |- 2 =/= 0
28	26, 27	recidi 10335	. . . . . . . . 9 |- ( 2 x. ( 1 / 2 ) ) = 1
29	25, 28	syl6eq 2500	. . . . . . . 8 |- ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> ( 2 x. X ) = 1 )
30	29	fveq2d 5867	. . . . . . 7 |- ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> ( F ` ( 2 x. X ) ) = ( F ` 1 ) )
31	29	oveq1d 6303	. . . . . . . . 9 |- ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> ( ( 2 x. X ) - 1 ) = ( 1 - 1 ) )
32		1m1e0 10675	. . . . . . . . 9 |- ( 1 - 1 ) = 0
33	31, 32	syl6eq 2500	. . . . . . . 8 |- ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> ( ( 2 x. X ) - 1 ) = 0 )
34	33	fveq2d 5867	. . . . . . 7 |- ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> ( G ` ( ( 2 x. X ) - 1 ) ) = ( G ` 0 ) )
35	15, 30, 34	3eqtr4d 2494	. . . . . 6 |- ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> ( F ` ( 2 x. X ) ) = ( G ` ( ( 2 x. X ) - 1 ) ) )
36	35	ifeq1d 3898	. . . . 5 |- ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> if ( X <_ ( 1 / 2 ) , ( F ` ( 2 x. X ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) = if ( X <_ ( 1 / 2 ) , ( G ` ( ( 2 x. X ) - 1 ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) )
37		ifid 3917	. . . . 5 |- if ( X <_ ( 1 / 2 ) , ( G ` ( ( 2 x. X ) - 1 ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) = ( G ` ( ( 2 x. X ) - 1 ) )
38	36, 37	syl6eq 2500	. . . 4 |- ( ( ph /\ ( X e. ( ( 1 / 2 ) [,] 1 ) /\ X <_ ( 1 / 2 ) ) ) -> if ( X <_ ( 1 / 2 ) , ( F ` ( 2 x. X ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) = ( G ` ( ( 2 x. X ) - 1 ) ) )
39	38	expr 619	. . 3 |- ( ( ph /\ X e. ( ( 1 / 2 ) [,] 1 ) ) -> ( X <_ ( 1 / 2 ) -> if ( X <_ ( 1 / 2 ) , ( F ` ( 2 x. X ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) = ( G ` ( ( 2 x. X ) - 1 ) ) ) )
40		iffalse 3889	. . 3 |- ( -. X <_ ( 1 / 2 ) -> if ( X <_ ( 1 / 2 ) , ( F ` ( 2 x. X ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) = ( G ` ( ( 2 x. X ) - 1 ) ) )
41	39, 40	pm2.61d1 163	. 2 |- ( ( ph /\ X e. ( ( 1 / 2 ) [,] 1 ) ) -> if ( X <_ ( 1 / 2 ) , ( F ` ( 2 x. X ) ) , ( G ` ( ( 2 x. X ) - 1 ) ) ) = ( G ` ( ( 2 x. X ) - 1 ) ) )
42	13, 41	eqtrd 2484	1 |- ( ( ph /\ X e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( F ( *p ` J ) G ) ` X ) = ( G ` ( ( 2 x. X ) - 1 ) ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   = wceq 1443   e. wcel 1886   C_ wss 3403   ifcif 3880   class class class wbr 4401   ` cfv 5581  (class class class)co 6288   RRcr 9535   0cc0 9536   1c1 9537   x. cmul 9541   <_ cle 9673   - cmin 9857   / cdiv 10266   2c2 10656   [,]cicc 11635   Cn ccn 20233   IIcii 21900   *pcpco 22024

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-cnex 9592  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  df-po 4754  df-so 4755  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-1st 6790  df-2nd 6791  df-er 7360  df-map 7471  df-en 7567  df-dom 7568  df-sdom 7569  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-sub 9859  df-neg 9860  df-div 10267  df-2 10665  df-icc 11639  df-top 19914  df-topon 19916  df-cn 20236  df-pco 22029

This theorem is referenced by:  pcoass  22048  pcorevlem  22050