Theorem pcoass 20618

Description: Order of concatenation does not affect homotopy class. (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof shortened by Mario Carneiro, 8-Jun-2014.)

Hypotheses

Ref	Expression
pcoass.2	|- ( ph -> F e. ( II Cn J ) )
pcoass.3	|- ( ph -> G e. ( II Cn J ) )
pcoass.4	|- ( ph -> H e. ( II Cn J ) )
pcoass.5	|- ( ph -> ( F ` 1 ) = ( G ` 0 ) )
pcoass.6	|- ( ph -> ( G ` 1 ) = ( H ` 0 ) )
pcoass.7	|- P = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) )

Assertion

Ref	Expression
pcoass	|- ( ph -> ( ( F ( *p ` J ) G ) ( *p ` J ) H ) ( ~=ph ` J ) ( F ( *p ` J ) ( G ( *p ` J ) H ) ) )

Distinct variable groups:   x, F   x, G   x, H   x, J   ph, x

Allowed substitution hint:   P( x)

Proof of Theorem pcoass

Dummy variables y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iftrue 3818	. . . . . . . . . . 11 |- ( x <_ ( 1 / 4 ) -> if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) = ( 2 x. x ) )
2	1	fveq2d 5716	. . . . . . . . . 10 |- ( x <_ ( 1 / 4 ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) ) = ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( 2 x. x ) ) )
3	2	adantl 466	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 4 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) ) = ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( 2 x. x ) ) )
4		2cn 10413	. . . . . . . . . . . . 13 |- 2 e. CC
5		0re 9407	. . . . . . . . . . . . . . . . 17 |- 0 e. RR
6		1re 9406	. . . . . . . . . . . . . . . . 17 |- 1 e. RR
7	5, 6	elicc2i 11382	. . . . . . . . . . . . . . . 16 |- ( x e. ( 0 [,] 1 ) <-> ( x e. RR /\ 0 <_ x /\ x <_ 1 ) )
8	7	simp1bi 1003	. . . . . . . . . . . . . . 15 |- ( x e. ( 0 [,] 1 ) -> x e. RR )
9	8	adantr 465	. . . . . . . . . . . . . 14 |- ( ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 4 ) ) -> x e. RR )
10	9	recnd 9433	. . . . . . . . . . . . 13 |- ( ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 4 ) ) -> x e. CC )
11		mulcom 9389	. . . . . . . . . . . . 13 |- ( ( 2 e. CC /\ x e. CC ) -> ( 2 x. x ) = ( x x. 2 ) )
12	4, 10, 11	sylancr 663	. . . . . . . . . . . 12 |- ( ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 4 ) ) -> ( 2 x. x ) = ( x x. 2 ) )
13	7	simp2bi 1004	. . . . . . . . . . . . . . 15 |- ( x e. ( 0 [,] 1 ) -> 0 <_ x )
14	13	adantr 465	. . . . . . . . . . . . . 14 |- ( ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 4 ) ) -> 0 <_ x )
15		simpr 461	. . . . . . . . . . . . . 14 |- ( ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 4 ) ) -> x <_ ( 1 / 4 ) )
16		4nn 10502	. . . . . . . . . . . . . . . 16 |- 4 e. NN
17		nnrecre 10379	. . . . . . . . . . . . . . . 16 |- ( 4 e. NN -> ( 1 / 4 ) e. RR )
18	16, 17	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( 1 / 4 ) e. RR
19	5, 18	elicc2i 11382	. . . . . . . . . . . . . 14 |- ( x e. ( 0 [,] ( 1 / 4 ) ) <-> ( x e. RR /\ 0 <_ x /\ x <_ ( 1 / 4 ) ) )
20	9, 14, 15, 19	syl3anbrc 1172	. . . . . . . . . . . . 13 |- ( ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 4 ) ) -> x e. ( 0 [,] ( 1 / 4 ) ) )
21		2rp 11017	. . . . . . . . . . . . . 14 |- 2 e. RR+
22	4	mul02i 9579	. . . . . . . . . . . . . 14 |- ( 0 x. 2 ) = 0
23	18	recni 9419	. . . . . . . . . . . . . . 15 |- ( 1 / 4 ) e. CC
24	23	2timesi 10463	. . . . . . . . . . . . . . . 16 |- ( 2 x. ( 1 / 4 ) ) = ( ( 1 / 4 ) + ( 1 / 4 ) )
25		2ne0 10435	. . . . . . . . . . . . . . . . . . . 20 |- 2 =/= 0
26		recdiv2 10065	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( 1 / 2 ) / 2 ) = ( 1 / ( 2 x. 2 ) ) )
27	4, 25, 4, 25, 26	mp4an 673	. . . . . . . . . . . . . . . . . . 19 |- ( ( 1 / 2 ) / 2 ) = ( 1 / ( 2 x. 2 ) )
28		2t2e4 10492	. . . . . . . . . . . . . . . . . . . 20 |- ( 2 x. 2 ) = 4
29	28	oveq2i 6123	. . . . . . . . . . . . . . . . . . 19 |- ( 1 / ( 2 x. 2 ) ) = ( 1 / 4 )
30	27, 29	eqtri 2463	. . . . . . . . . . . . . . . . . 18 |- ( ( 1 / 2 ) / 2 ) = ( 1 / 4 )
31	30, 30	oveq12i 6124	. . . . . . . . . . . . . . . . 17 |- ( ( ( 1 / 2 ) / 2 ) + ( ( 1 / 2 ) / 2 ) ) = ( ( 1 / 4 ) + ( 1 / 4 ) )
32		halfcn 10562	. . . . . . . . . . . . . . . . . 18 |- ( 1 / 2 ) e. CC
33		2halves 10574	. . . . . . . . . . . . . . . . . 18 |- ( ( 1 / 2 ) e. CC -> ( ( ( 1 / 2 ) / 2 ) + ( ( 1 / 2 ) / 2 ) ) = ( 1 / 2 ) )
34	32, 33	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( ( ( 1 / 2 ) / 2 ) + ( ( 1 / 2 ) / 2 ) ) = ( 1 / 2 )
35	31, 34	eqtr3i 2465	. . . . . . . . . . . . . . . 16 |- ( ( 1 / 4 ) + ( 1 / 4 ) ) = ( 1 / 2 )
36	24, 35	eqtri 2463	. . . . . . . . . . . . . . 15 |- ( 2 x. ( 1 / 4 ) ) = ( 1 / 2 )
37	4, 23, 36	mulcomli 9414	. . . . . . . . . . . . . 14 |- ( ( 1 / 4 ) x. 2 ) = ( 1 / 2 )
38	5, 18, 21, 22, 37	iccdili 11445	. . . . . . . . . . . . 13 |- ( x e. ( 0 [,] ( 1 / 4 ) ) -> ( x x. 2 ) e. ( 0 [,] ( 1 / 2 ) ) )
39	20, 38	syl 16	. . . . . . . . . . . 12 |- ( ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 4 ) ) -> ( x x. 2 ) e. ( 0 [,] ( 1 / 2 ) ) )
40	12, 39	eqeltrd 2517	. . . . . . . . . . 11 |- ( ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 4 ) ) -> ( 2 x. x ) e. ( 0 [,] ( 1 / 2 ) ) )
41		pcoass.2	. . . . . . . . . . . . 13 |- ( ph -> F e. ( II Cn J ) )
42		pcoass.3	. . . . . . . . . . . . . 14 |- ( ph -> G e. ( II Cn J ) )
43		pcoass.4	. . . . . . . . . . . . . 14 |- ( ph -> H e. ( II Cn J ) )
44		pcoass.6	. . . . . . . . . . . . . 14 |- ( ph -> ( G ` 1 ) = ( H ` 0 ) )
45	42, 43, 44	pcocn 20611	. . . . . . . . . . . . 13 |- ( ph -> ( G ( *p ` J ) H ) e. ( II Cn J ) )
46	41, 45	pcoval1 20607	. . . . . . . . . . . 12 |- ( ( ph /\ ( 2 x. x ) e. ( 0 [,] ( 1 / 2 ) ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( 2 x. x ) ) = ( F ` ( 2 x. ( 2 x. x ) ) ) )
47	41, 42	pcoval1 20607	. . . . . . . . . . . 12 |- ( ( ph /\ ( 2 x. x ) e. ( 0 [,] ( 1 / 2 ) ) ) -> ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) = ( F ` ( 2 x. ( 2 x. x ) ) ) )
48	46, 47	eqtr4d 2478	. . . . . . . . . . 11 |- ( ( ph /\ ( 2 x. x ) e. ( 0 [,] ( 1 / 2 ) ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( 2 x. x ) ) = ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) )
49	40, 48	sylan2 474	. . . . . . . . . 10 |- ( ( ph /\ ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 4 ) ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( 2 x. x ) ) = ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) )
50	49	anassrs 648	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 4 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( 2 x. x ) ) = ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) )
51	3, 50	eqtrd 2475	. . . . . . . 8 |- ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 4 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) ) = ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) )
52	51	adantlr 714	. . . . . . 7 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ x <_ ( 1 / 4 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) ) = ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) )
53		simplll 757	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ph )
54	8	ad2antlr 726	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) -> x e. RR )
55	54	adantr 465	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> x e. RR )
56		letric 9496	. . . . . . . . . . . . . 14 |- ( ( x e. RR /\ ( 1 / 4 ) e. RR ) -> ( x <_ ( 1 / 4 ) \/ ( 1 / 4 ) <_ x ) )
57	54, 18, 56	sylancl 662	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) -> ( x <_ ( 1 / 4 ) \/ ( 1 / 4 ) <_ x ) )
58	57	orcanai 904	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 1 / 4 ) <_ x )
59		simplr 754	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> x <_ ( 1 / 2 ) )
60		halfre 10561	. . . . . . . . . . . . 13 |- ( 1 / 2 ) e. RR
61	18, 60	elicc2i 11382	. . . . . . . . . . . 12 |- ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) <-> ( x e. RR /\ ( 1 / 4 ) <_ x /\ x <_ ( 1 / 2 ) ) )
62	55, 58, 59, 61	syl3anbrc 1172	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) )
63	61	simp1bi 1003	. . . . . . . . . . . . 13 |- ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> x e. RR )
64		readdcl 9386	. . . . . . . . . . . . 13 |- ( ( x e. RR /\ ( 1 / 4 ) e. RR ) -> ( x + ( 1 / 4 ) ) e. RR )
65	63, 18, 64	sylancl 662	. . . . . . . . . . . 12 |- ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( x + ( 1 / 4 ) ) e. RR )
66	18	a1i 11	. . . . . . . . . . . . . 14 |- ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( 1 / 4 ) e. RR )
67	61	simp2bi 1004	. . . . . . . . . . . . . 14 |- ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( 1 / 4 ) <_ x )
68	66, 63, 66, 67	leadd1dd 9974	. . . . . . . . . . . . 13 |- ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( ( 1 / 4 ) + ( 1 / 4 ) ) <_ ( x + ( 1 / 4 ) ) )
69	35, 68	syl5eqbrr 4347	. . . . . . . . . . . 12 |- ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( 1 / 2 ) <_ ( x + ( 1 / 4 ) ) )
70	60	a1i 11	. . . . . . . . . . . . . 14 |- ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( 1 / 2 ) e. RR )
71	61	simp3bi 1005	. . . . . . . . . . . . . 14 |- ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> x <_ ( 1 / 2 ) )
72		2lt4 10513	. . . . . . . . . . . . . . . . 17 |- 2 < 4
73		2re 10412	. . . . . . . . . . . . . . . . . 18 |- 2 e. RR
74		4re 10419	. . . . . . . . . . . . . . . . . 18 |- 4 e. RR
75		2pos 10434	. . . . . . . . . . . . . . . . . 18 |- 0 < 2
76		4pos 10438	. . . . . . . . . . . . . . . . . 18 |- 0 < 4
77	73, 74, 75, 76	ltrecii 10270	. . . . . . . . . . . . . . . . 17 |- ( 2 < 4 <-> ( 1 / 4 ) < ( 1 / 2 ) )
78	72, 77	mpbi 208	. . . . . . . . . . . . . . . 16 |- ( 1 / 4 ) < ( 1 / 2 )
79	18, 60, 78	ltleii 9518	. . . . . . . . . . . . . . 15 |- ( 1 / 4 ) <_ ( 1 / 2 )
80	79	a1i 11	. . . . . . . . . . . . . 14 |- ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( 1 / 4 ) <_ ( 1 / 2 ) )
81	63, 66, 70, 70, 71, 80	le2addd 9978	. . . . . . . . . . . . 13 |- ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( x + ( 1 / 4 ) ) <_ ( ( 1 / 2 ) + ( 1 / 2 ) ) )
82		ax-1cn 9361	. . . . . . . . . . . . . 14 |- 1 e. CC
83		2halves 10574	. . . . . . . . . . . . . 14 |- ( 1 e. CC -> ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 )
84	82, 83	ax-mp 5	. . . . . . . . . . . . 13 |- ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1
85	81, 84	syl6breq 4352	. . . . . . . . . . . 12 |- ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( x + ( 1 / 4 ) ) <_ 1 )
86	60, 6	elicc2i 11382	. . . . . . . . . . . 12 |- ( ( x + ( 1 / 4 ) ) e. ( ( 1 / 2 ) [,] 1 ) <-> ( ( x + ( 1 / 4 ) ) e. RR /\ ( 1 / 2 ) <_ ( x + ( 1 / 4 ) ) /\ ( x + ( 1 / 4 ) ) <_ 1 ) )
87	65, 69, 85, 86	syl3anbrc 1172	. . . . . . . . . . 11 |- ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( x + ( 1 / 4 ) ) e. ( ( 1 / 2 ) [,] 1 ) )
88	62, 87	syl 16	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( x + ( 1 / 4 ) ) e. ( ( 1 / 2 ) [,] 1 ) )
89		pcoass.5	. . . . . . . . . . . 12 |- ( ph -> ( F ` 1 ) = ( G ` 0 ) )
90	42, 43	pco0 20608	. . . . . . . . . . . 12 |- ( ph -> ( ( G ( *p ` J ) H ) ` 0 ) = ( G ` 0 ) )
91	89, 90	eqtr4d 2478	. . . . . . . . . . 11 |- ( ph -> ( F ` 1 ) = ( ( G ( *p ` J ) H ) ` 0 ) )
92	41, 45, 91	pcoval2 20610	. . . . . . . . . 10 |- ( ( ph /\ ( x + ( 1 / 4 ) ) e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( x + ( 1 / 4 ) ) ) = ( ( G ( *p ` J ) H ) ` ( ( 2 x. ( x + ( 1 / 4 ) ) ) - 1 ) ) )
93	53, 88, 92	syl2anc 661	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( x + ( 1 / 4 ) ) ) = ( ( G ( *p ` J ) H ) ` ( ( 2 x. ( x + ( 1 / 4 ) ) ) - 1 ) ) )
94	84	oveq2i 6123	. . . . . . . . . . . 12 |- ( ( 2 x. ( x + ( 1 / 4 ) ) ) - ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( 2 x. ( x + ( 1 / 4 ) ) ) - 1 )
95		2cnd 10415	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> 2 e. CC )
96	55	recnd 9433	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> x e. CC )
97	23	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 1 / 4 ) e. CC )
98	95, 96, 97	adddid 9431	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 2 x. ( x + ( 1 / 4 ) ) ) = ( ( 2 x. x ) + ( 2 x. ( 1 / 4 ) ) ) )
99	36	oveq2i 6123	. . . . . . . . . . . . . 14 |- ( ( 2 x. x ) + ( 2 x. ( 1 / 4 ) ) ) = ( ( 2 x. x ) + ( 1 / 2 ) )
100	98, 99	syl6eq 2491	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 2 x. ( x + ( 1 / 4 ) ) ) = ( ( 2 x. x ) + ( 1 / 2 ) ) )
101	100	oveq1d 6127	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( 2 x. ( x + ( 1 / 4 ) ) ) - ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( ( 2 x. x ) + ( 1 / 2 ) ) - ( ( 1 / 2 ) + ( 1 / 2 ) ) ) )
102	94, 101	syl5eqr 2489	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( 2 x. ( x + ( 1 / 4 ) ) ) - 1 ) = ( ( ( 2 x. x ) + ( 1 / 2 ) ) - ( ( 1 / 2 ) + ( 1 / 2 ) ) ) )
103		remulcl 9388	. . . . . . . . . . . . . 14 |- ( ( 2 e. RR /\ x e. RR ) -> ( 2 x. x ) e. RR )
104	73, 55, 103	sylancr 663	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 2 x. x ) e. RR )
105	104	recnd 9433	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 2 x. x ) e. CC )
106	32	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 1 / 2 ) e. CC )
107	105, 106, 106	pnpcan2d 9778	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( ( 2 x. x ) + ( 1 / 2 ) ) - ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( 2 x. x ) - ( 1 / 2 ) ) )
108	102, 107	eqtrd 2475	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( 2 x. ( x + ( 1 / 4 ) ) ) - 1 ) = ( ( 2 x. x ) - ( 1 / 2 ) ) )
109	108	fveq2d 5716	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( G ( *p ` J ) H ) ` ( ( 2 x. ( x + ( 1 / 4 ) ) ) - 1 ) ) = ( ( G ( *p ` J ) H ) ` ( ( 2 x. x ) - ( 1 / 2 ) ) ) )
110	4, 96, 11	sylancr 663	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 2 x. x ) = ( x x. 2 ) )
111	82, 4, 25	divcan1i 10096	. . . . . . . . . . . . . . 15 |- ( ( 1 / 2 ) x. 2 ) = 1
112	18, 60, 21, 37, 111	iccdili 11445	. . . . . . . . . . . . . 14 |- ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( x x. 2 ) e. ( ( 1 / 2 ) [,] 1 ) )
113	62, 112	syl 16	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( x x. 2 ) e. ( ( 1 / 2 ) [,] 1 ) )
114	110, 113	eqeltrd 2517	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 2 x. x ) e. ( ( 1 / 2 ) [,] 1 ) )
115	32	subidi 9700	. . . . . . . . . . . . 13 |- ( ( 1 / 2 ) - ( 1 / 2 ) ) = 0
116		1mhlfehlf 10565	. . . . . . . . . . . . 13 |- ( 1 - ( 1 / 2 ) ) = ( 1 / 2 )
117	60, 6, 60, 115, 116	iccshftli 11443	. . . . . . . . . . . 12 |- ( ( 2 x. x ) e. ( ( 1 / 2 ) [,] 1 ) -> ( ( 2 x. x ) - ( 1 / 2 ) ) e. ( 0 [,] ( 1 / 2 ) ) )
118	114, 117	syl 16	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( 2 x. x ) - ( 1 / 2 ) ) e. ( 0 [,] ( 1 / 2 ) ) )
119	42, 43	pcoval1 20607	. . . . . . . . . . 11 |- ( ( ph /\ ( ( 2 x. x ) - ( 1 / 2 ) ) e. ( 0 [,] ( 1 / 2 ) ) ) -> ( ( G ( *p ` J ) H ) ` ( ( 2 x. x ) - ( 1 / 2 ) ) ) = ( G ` ( 2 x. ( ( 2 x. x ) - ( 1 / 2 ) ) ) ) )
120	53, 118, 119	syl2anc 661	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( G ( *p ` J ) H ) ` ( ( 2 x. x ) - ( 1 / 2 ) ) ) = ( G ` ( 2 x. ( ( 2 x. x ) - ( 1 / 2 ) ) ) ) )
121	95, 105, 106	subdid 9821	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 2 x. ( ( 2 x. x ) - ( 1 / 2 ) ) ) = ( ( 2 x. ( 2 x. x ) ) - ( 2 x. ( 1 / 2 ) ) ) )
122	4, 25	recidi 10083	. . . . . . . . . . . . 13 |- ( 2 x. ( 1 / 2 ) ) = 1
123	122	oveq2i 6123	. . . . . . . . . . . 12 |- ( ( 2 x. ( 2 x. x ) ) - ( 2 x. ( 1 / 2 ) ) ) = ( ( 2 x. ( 2 x. x ) ) - 1 )
124	121, 123	syl6eq 2491	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 2 x. ( ( 2 x. x ) - ( 1 / 2 ) ) ) = ( ( 2 x. ( 2 x. x ) ) - 1 ) )
125	124	fveq2d 5716	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( G ` ( 2 x. ( ( 2 x. x ) - ( 1 / 2 ) ) ) ) = ( G ` ( ( 2 x. ( 2 x. x ) ) - 1 ) ) )
126	120, 125	eqtrd 2475	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( G ( *p ` J ) H ) ` ( ( 2 x. x ) - ( 1 / 2 ) ) ) = ( G ` ( ( 2 x. ( 2 x. x ) ) - 1 ) ) )
127	93, 109, 126	3eqtrd 2479	. . . . . . . 8 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( x + ( 1 / 4 ) ) ) = ( G ` ( ( 2 x. ( 2 x. x ) ) - 1 ) ) )
128		iffalse 3820	. . . . . . . . . 10 |- ( -. x <_ ( 1 / 4 ) -> if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) = ( x + ( 1 / 4 ) ) )
129	128	fveq2d 5716	. . . . . . . . 9 |- ( -. x <_ ( 1 / 4 ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) ) = ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( x + ( 1 / 4 ) ) ) )
130	129	adantl 466	. . . . . . . 8 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) ) = ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( x + ( 1 / 4 ) ) ) )
131	41, 42, 89	pcoval2 20610	. . . . . . . . 9 |- ( ( ph /\ ( 2 x. x ) e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) = ( G ` ( ( 2 x. ( 2 x. x ) ) - 1 ) ) )
132	53, 114, 131	syl2anc 661	. . . . . . . 8 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) = ( G ` ( ( 2 x. ( 2 x. x ) ) - 1 ) ) )
133	127, 130, 132	3eqtr4d 2485	. . . . . . 7 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) ) = ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) )
134	52, 133	pm2.61dan 789	. . . . . 6 |- ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) ) = ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) )
135		iftrue 3818	. . . . . . . 8 |- ( x <_ ( 1 / 2 ) -> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) = if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) )
136	135	fveq2d 5716	. . . . . . 7 |- ( x <_ ( 1 / 2 ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) = ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) ) )
137	136	adantl 466	. . . . . 6 |- ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) = ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) ) )
138		iftrue 3818	. . . . . . 7 |- ( x <_ ( 1 / 2 ) -> if ( x <_ ( 1 / 2 ) , ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) , ( H ` ( ( 2 x. x ) - 1 ) ) ) = ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) )
139	138	adantl 466	. . . . . 6 |- ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) -> if ( x <_ ( 1 / 2 ) , ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) , ( H ` ( ( 2 x. x ) - 1 ) ) ) = ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) )
140	134, 137, 139	3eqtr4d 2485	. . . . 5 |- ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) = if ( x <_ ( 1 / 2 ) , ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) , ( H ` ( ( 2 x. x ) - 1 ) ) ) )
141		elii2 20530	. . . . . . . 8 |- ( ( x e. ( 0 [,] 1 ) /\ -. x <_ ( 1 / 2 ) ) -> x e. ( ( 1 / 2 ) [,] 1 ) )
142		halfgt0 10563	. . . . . . . . . . . . . . 15 |- 0 < ( 1 / 2 )
143	5, 60, 142	ltleii 9518	. . . . . . . . . . . . . 14 |- 0 <_ ( 1 / 2 )
144		halflt1 10564	. . . . . . . . . . . . . . 15 |- ( 1 / 2 ) < 1
145	60, 6, 144	ltleii 9518	. . . . . . . . . . . . . 14 |- ( 1 / 2 ) <_ 1
146	5, 6	elicc2i 11382	. . . . . . . . . . . . . 14 |- ( ( 1 / 2 ) e. ( 0 [,] 1 ) <-> ( ( 1 / 2 ) e. RR /\ 0 <_ ( 1 / 2 ) /\ ( 1 / 2 ) <_ 1 ) )
147	60, 143, 145, 146	mpbir3an 1170	. . . . . . . . . . . . 13 |- ( 1 / 2 ) e. ( 0 [,] 1 )
148		1elunit 11425	. . . . . . . . . . . . 13 |- 1 e. ( 0 [,] 1 )
149		iccss2 11387	. . . . . . . . . . . . 13 |- ( ( ( 1 / 2 ) e. ( 0 [,] 1 ) /\ 1 e. ( 0 [,] 1 ) ) -> ( ( 1 / 2 ) [,] 1 ) C_ ( 0 [,] 1 ) )
150	147, 148, 149	mp2an 672	. . . . . . . . . . . 12 |- ( ( 1 / 2 ) [,] 1 ) C_ ( 0 [,] 1 )
151	150	sseli 3373	. . . . . . . . . . 11 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> x e. ( 0 [,] 1 ) )
152	4, 25	div0i 10086	. . . . . . . . . . . 12 |- ( 0 / 2 ) = 0
153		eqid 2443	. . . . . . . . . . . 12 |- ( 1 / 2 ) = ( 1 / 2 )
154	5, 6, 21, 152, 153	icccntri 11447	. . . . . . . . . . 11 |- ( x e. ( 0 [,] 1 ) -> ( x / 2 ) e. ( 0 [,] ( 1 / 2 ) ) )
155	32	addid2i 9578	. . . . . . . . . . . 12 |- ( 0 + ( 1 / 2 ) ) = ( 1 / 2 )
156	5, 60, 60, 155, 84	iccshftri 11441	. . . . . . . . . . 11 |- ( ( x / 2 ) e. ( 0 [,] ( 1 / 2 ) ) -> ( ( x / 2 ) + ( 1 / 2 ) ) e. ( ( 1 / 2 ) [,] 1 ) )
157	151, 154, 156	3syl 20	. . . . . . . . . 10 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( ( x / 2 ) + ( 1 / 2 ) ) e. ( ( 1 / 2 ) [,] 1 ) )
158	41, 45, 91	pcoval2 20610	. . . . . . . . . 10 |- ( ( ph /\ ( ( x / 2 ) + ( 1 / 2 ) ) e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( ( x / 2 ) + ( 1 / 2 ) ) ) = ( ( G ( *p ` J ) H ) ` ( ( 2 x. ( ( x / 2 ) + ( 1 / 2 ) ) ) - 1 ) ) )
159	157, 158	sylan2 474	. . . . . . . . 9 |- ( ( ph /\ x e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( ( x / 2 ) + ( 1 / 2 ) ) ) = ( ( G ( *p ` J ) H ) ` ( ( 2 x. ( ( x / 2 ) + ( 1 / 2 ) ) ) - 1 ) ) )
160	60, 6	elicc2i 11382	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( ( 1 / 2 ) [,] 1 ) <-> ( x e. RR /\ ( 1 / 2 ) <_ x /\ x <_ 1 ) )
161	160	simp1bi 1003	. . . . . . . . . . . . . . . . 17 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> x e. RR )
162	161	recnd 9433	. . . . . . . . . . . . . . . 16 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> x e. CC )
163	82	a1i 11	. . . . . . . . . . . . . . . 16 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> 1 e. CC )
164		2cnd 10415	. . . . . . . . . . . . . . . 16 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> 2 e. CC )
165	25	a1i 11	. . . . . . . . . . . . . . . 16 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> 2 =/= 0 )
166	162, 163, 164, 165	divdird 10166	. . . . . . . . . . . . . . 15 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( ( x + 1 ) / 2 ) = ( ( x / 2 ) + ( 1 / 2 ) ) )
167	166	oveq2d 6128	. . . . . . . . . . . . . 14 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( 2 x. ( ( x + 1 ) / 2 ) ) = ( 2 x. ( ( x / 2 ) + ( 1 / 2 ) ) ) )
168		peano2cn 9562	. . . . . . . . . . . . . . . 16 |- ( x e. CC -> ( x + 1 ) e. CC )
169	162, 168	syl 16	. . . . . . . . . . . . . . 15 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( x + 1 ) e. CC )
170	169, 164, 165	divcan2d 10130	. . . . . . . . . . . . . 14 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( 2 x. ( ( x + 1 ) / 2 ) ) = ( x + 1 ) )
171	167, 170	eqtr3d 2477	. . . . . . . . . . . . 13 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( 2 x. ( ( x / 2 ) + ( 1 / 2 ) ) ) = ( x + 1 ) )
172	171	oveq1d 6127	. . . . . . . . . . . 12 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( ( 2 x. ( ( x / 2 ) + ( 1 / 2 ) ) ) - 1 ) = ( ( x + 1 ) - 1 ) )
173		pncan 9637	. . . . . . . . . . . . 13 |- ( ( x e. CC /\ 1 e. CC ) -> ( ( x + 1 ) - 1 ) = x )
174	162, 82, 173	sylancl 662	. . . . . . . . . . . 12 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( ( x + 1 ) - 1 ) = x )
175	172, 174	eqtrd 2475	. . . . . . . . . . 11 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( ( 2 x. ( ( x / 2 ) + ( 1 / 2 ) ) ) - 1 ) = x )
176	175	fveq2d 5716	. . . . . . . . . 10 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( ( G ( *p ` J ) H ) ` ( ( 2 x. ( ( x / 2 ) + ( 1 / 2 ) ) ) - 1 ) ) = ( ( G ( *p ` J ) H ) ` x ) )
177	176	adantl 466	. . . . . . . . 9 |- ( ( ph /\ x e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( G ( *p ` J ) H ) ` ( ( 2 x. ( ( x / 2 ) + ( 1 / 2 ) ) ) - 1 ) ) = ( ( G ( *p ` J ) H ) ` x ) )
178	42, 43, 44	pcoval2 20610	. . . . . . . . 9 |- ( ( ph /\ x e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( G ( *p ` J ) H ) ` x ) = ( H ` ( ( 2 x. x ) - 1 ) ) )
179	159, 177, 178	3eqtrd 2479	. . . . . . . 8 |- ( ( ph /\ x e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( ( x / 2 ) + ( 1 / 2 ) ) ) = ( H ` ( ( 2 x. x ) - 1 ) ) )
180	141, 179	sylan2 474	. . . . . . 7 |- ( ( ph /\ ( x e. ( 0 [,] 1 ) /\ -. x <_ ( 1 / 2 ) ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( ( x / 2 ) + ( 1 / 2 ) ) ) = ( H ` ( ( 2 x. x ) - 1 ) ) )
181	180	anassrs 648	. . . . . 6 |- ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ -. x <_ ( 1 / 2 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( ( x / 2 ) + ( 1 / 2 ) ) ) = ( H ` ( ( 2 x. x ) - 1 ) ) )
182		iffalse 3820	. . . . . . . 8 |- ( -. x <_ ( 1 / 2 ) -> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) = ( ( x / 2 ) + ( 1 / 2 ) ) )
183	182	fveq2d 5716	. . . . . . 7 |- ( -. x <_ ( 1 / 2 ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) = ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( ( x / 2 ) + ( 1 / 2 ) ) ) )
184	183	adantl 466	. . . . . 6 |- ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ -. x <_ ( 1 / 2 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) = ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` ( ( x / 2 ) + ( 1 / 2 ) ) ) )
185		iffalse 3820	. . . . . . 7 |- ( -. x <_ ( 1 / 2 ) -> if ( x <_ ( 1 / 2 ) , ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) , ( H ` ( ( 2 x. x ) - 1 ) ) ) = ( H ` ( ( 2 x. x ) - 1 ) ) )
186	185	adantl 466	. . . . . 6 |- ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ -. x <_ ( 1 / 2 ) ) -> if ( x <_ ( 1 / 2 ) , ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) , ( H ` ( ( 2 x. x ) - 1 ) ) ) = ( H ` ( ( 2 x. x ) - 1 ) ) )
187	181, 184, 186	3eqtr4d 2485	. . . . 5 |- ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ -. x <_ ( 1 / 2 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) = if ( x <_ ( 1 / 2 ) , ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) , ( H ` ( ( 2 x. x ) - 1 ) ) ) )
188	140, 187	pm2.61dan 789	. . . 4 |- ( ( ph /\ x e. ( 0 [,] 1 ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) = if ( x <_ ( 1 / 2 ) , ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) , ( H ` ( ( 2 x. x ) - 1 ) ) ) )
189	188	mpteq2dva 4399	. . 3 |- ( ph -> ( x e. ( 0 [,] 1 ) |-> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) ) = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) , ( H ` ( ( 2 x. x ) - 1 ) ) ) ) )
190		pcoass.7	. . . . . . 7 |- P = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) )
191		iitopon 20477	. . . . . . . . 9 |- II e. (TopOn ` ( 0 [,] 1 ) )
192	191	a1i 11	. . . . . . . 8 |- ( ph -> II e. (TopOn ` ( 0 [,] 1 ) ) )
193	192	cnmptid 19256	. . . . . . . 8 |- ( ph -> ( x e. ( 0 [,] 1 ) |-> x ) e. ( II Cn II ) )
194		0elunit 11424	. . . . . . . . . 10 |- 0 e. ( 0 [,] 1 )
195	194	a1i 11	. . . . . . . . 9 |- ( ph -> 0 e. ( 0 [,] 1 ) )
196	192, 192, 195	cnmptc 19257	. . . . . . . 8 |- ( ph -> ( x e. ( 0 [,] 1 ) |-> 0 ) e. ( II Cn II ) )
197		eqid 2443	. . . . . . . . 9 |- ( topGen ` ran (,) ) = ( topGen ` ran (,) )
198		eqid 2443	. . . . . . . . 9 |- ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) = ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) )
199		eqid 2443	. . . . . . . . 9 |- ( ( topGen ` ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) = ( ( topGen ` ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) )
200		dfii2 20480	. . . . . . . . 9 |- II = ( ( topGen ` ran (,) ) ↾t ( 0 [,] 1 ) )
201		0red 9408	. . . . . . . . 9 |- ( ph -> 0 e. RR )
202		1red 9422	. . . . . . . . 9 |- ( ph -> 1 e. RR )
203	147	a1i 11	. . . . . . . . 9 |- ( ph -> ( 1 / 2 ) e. ( 0 [,] 1 ) )
204		simprl 755	. . . . . . . . . . . 12 |- ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> y = ( 1 / 2 ) )
205	204	oveq1d 6127	. . . . . . . . . . 11 |- ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( y + ( 1 / 4 ) ) = ( ( 1 / 2 ) + ( 1 / 4 ) ) )
206	32, 23	addcomi 9581	. . . . . . . . . . 11 |- ( ( 1 / 2 ) + ( 1 / 4 ) ) = ( ( 1 / 4 ) + ( 1 / 2 ) )
207	205, 206	syl6eq 2491	. . . . . . . . . 10 |- ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( y + ( 1 / 4 ) ) = ( ( 1 / 4 ) + ( 1 / 2 ) ) )
208	18, 60	ltnlei 9516	. . . . . . . . . . . . 13 |- ( ( 1 / 4 ) < ( 1 / 2 ) <-> -. ( 1 / 2 ) <_ ( 1 / 4 ) )
209	78, 208	mpbi 208	. . . . . . . . . . . 12 |- -. ( 1 / 2 ) <_ ( 1 / 4 )
210	204	breq1d 4323	. . . . . . . . . . . 12 |- ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( y <_ ( 1 / 4 ) <-> ( 1 / 2 ) <_ ( 1 / 4 ) ) )
211	209, 210	mtbiri 303	. . . . . . . . . . 11 |- ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> -. y <_ ( 1 / 4 ) )
212		iffalse 3820	. . . . . . . . . . 11 |- ( -. y <_ ( 1 / 4 ) -> if ( y <_ ( 1 / 4 ) , ( 2 x. y ) , ( y + ( 1 / 4 ) ) ) = ( y + ( 1 / 4 ) ) )
213	211, 212	syl 16	. . . . . . . . . 10 |- ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> if ( y <_ ( 1 / 4 ) , ( 2 x. y ) , ( y + ( 1 / 4 ) ) ) = ( y + ( 1 / 4 ) ) )
214	204	oveq1d 6127	. . . . . . . . . . . 12 |- ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( y / 2 ) = ( ( 1 / 2 ) / 2 ) )
215	214, 30	syl6eq 2491	. . . . . . . . . . 11 |- ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( y / 2 ) = ( 1 / 4 ) )
216	215	oveq1d 6127	. . . . . . . . . 10 |- ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( ( y / 2 ) + ( 1 / 2 ) ) = ( ( 1 / 4 ) + ( 1 / 2 ) ) )
217	207, 213, 216	3eqtr4d 2485	. . . . . . . . 9 |- ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> if ( y <_ ( 1 / 4 ) , ( 2 x. y ) , ( y + ( 1 / 4 ) ) ) = ( ( y / 2 ) + ( 1 / 2 ) ) )
218		eqid 2443	. . . . . . . . . 10 |- ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) = ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) )
219		eqid 2443	. . . . . . . . . 10 |- ( ( topGen ` ran (,) ) ↾t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) = ( ( topGen ` ran (,) ) ↾t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) )
220	60	a1i 11	. . . . . . . . . 10 |- ( ph -> ( 1 / 2 ) e. RR )
221	74, 76	recgt0ii 10259	. . . . . . . . . . . . 13 |- 0 < ( 1 / 4 )
222	5, 18, 221	ltleii 9518	. . . . . . . . . . . 12 |- 0 <_ ( 1 / 4 )
223	5, 60	elicc2i 11382	. . . . . . . . . . . 12 |- ( ( 1 / 4 ) e. ( 0 [,] ( 1 / 2 ) ) <-> ( ( 1 / 4 ) e. RR /\ 0 <_ ( 1 / 4 ) /\ ( 1 / 4 ) <_ ( 1 / 2 ) ) )
224	18, 222, 79, 223	mpbir3an 1170	. . . . . . . . . . 11 |- ( 1 / 4 ) e. ( 0 [,] ( 1 / 2 ) )
225	224	a1i 11	. . . . . . . . . 10 |- ( ph -> ( 1 / 4 ) e. ( 0 [,] ( 1 / 2 ) ) )
226		simprl 755	. . . . . . . . . . . 12 |- ( ( ph /\ ( y = ( 1 / 4 ) /\ z e. ( 0 [,] 1 ) ) ) -> y = ( 1 / 4 ) )
227	226	oveq2d 6128	. . . . . . . . . . 11 |- ( ( ph /\ ( y = ( 1 / 4 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( 2 x. y ) = ( 2 x. ( 1 / 4 ) ) )
228	226	oveq1d 6127	. . . . . . . . . . 11 |- ( ( ph /\ ( y = ( 1 / 4 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( y + ( 1 / 4 ) ) = ( ( 1 / 4 ) + ( 1 / 4 ) ) )
229	24, 227, 228	3eqtr4a 2501	. . . . . . . . . 10 |- ( ( ph /\ ( y = ( 1 / 4 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( 2 x. y ) = ( y + ( 1 / 4 ) ) )
230		retopon 20364	. . . . . . . . . . . . 13 |- ( topGen ` ran (,) ) e. (TopOn ` RR )
231		0xr 9451	. . . . . . . . . . . . . . . 16 |- 0 e. RR*
232	60	rexri 9457	. . . . . . . . . . . . . . . 16 |- ( 1 / 2 ) e. RR*
233		lbicc2 11422	. . . . . . . . . . . . . . . 16 |- ( ( 0 e. RR* /\ ( 1 / 2 ) e. RR* /\ 0 <_ ( 1 / 2 ) ) -> 0 e. ( 0 [,] ( 1 / 2 ) ) )
234	231, 232, 143, 233	mp3an 1314	. . . . . . . . . . . . . . 15 |- 0 e. ( 0 [,] ( 1 / 2 ) )
235		iccss2 11387	. . . . . . . . . . . . . . 15 |- ( ( 0 e. ( 0 [,] ( 1 / 2 ) ) /\ ( 1 / 4 ) e. ( 0 [,] ( 1 / 2 ) ) ) -> ( 0 [,] ( 1 / 4 ) ) C_ ( 0 [,] ( 1 / 2 ) ) )
236	234, 224, 235	mp2an 672	. . . . . . . . . . . . . 14 |- ( 0 [,] ( 1 / 4 ) ) C_ ( 0 [,] ( 1 / 2 ) )
237		iccssre 11398	. . . . . . . . . . . . . . 15 |- ( ( 0 e. RR /\ ( 1 / 2 ) e. RR ) -> ( 0 [,] ( 1 / 2 ) ) C_ RR )
238	5, 60, 237	mp2an 672	. . . . . . . . . . . . . 14 |- ( 0 [,] ( 1 / 2 ) ) C_ RR
239	236, 238	sstri 3386	. . . . . . . . . . . . 13 |- ( 0 [,] ( 1 / 4 ) ) C_ RR
240		resttopon 18787	. . . . . . . . . . . . 13 |- ( ( ( topGen ` ran (,) ) e. (TopOn ` RR ) /\ ( 0 [,] ( 1 / 4 ) ) C_ RR ) -> ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) e. (TopOn ` ( 0 [,] ( 1 / 4 ) ) ) )
241	230, 239, 240	mp2an 672	. . . . . . . . . . . 12 |- ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) e. (TopOn ` ( 0 [,] ( 1 / 4 ) ) )
242	241	a1i 11	. . . . . . . . . . 11 |- ( ph -> ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) e. (TopOn ` ( 0 [,] ( 1 / 4 ) ) ) )
243	242, 192	cnmpt1st 19263	. . . . . . . . . . 11 |- ( ph -> ( y e. ( 0 [,] ( 1 / 4 ) ) , z e. ( 0 [,] 1 ) |-> y ) e. ( ( ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) tX II ) Cn ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) ) )
244		retop 20362	. . . . . . . . . . . . . 14 |- ( topGen ` ran (,) ) e. Top
245		ovex 6137	. . . . . . . . . . . . . 14 |- ( 0 [,] ( 1 / 2 ) ) e. _V
246		restabs 18791	. . . . . . . . . . . . . 14 |- ( ( ( topGen ` ran (,) ) e. Top /\ ( 0 [,] ( 1 / 4 ) ) C_ ( 0 [,] ( 1 / 2 ) ) /\ ( 0 [,] ( 1 / 2 ) ) e. _V ) -> ( ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) = ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) )
247	244, 236, 245, 246	mp3an 1314	. . . . . . . . . . . . 13 |- ( ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) = ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) )
248	247	eqcomi 2447	. . . . . . . . . . . 12 |- ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) = ( ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ↾t ( 0 [,] ( 1 / 4 ) ) )
249		resttopon 18787	. . . . . . . . . . . . . 14 |- ( ( ( topGen ` ran (,) ) e. (TopOn ` RR ) /\ ( 0 [,] ( 1 / 2 ) ) C_ RR ) -> ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) e. (TopOn ` ( 0 [,] ( 1 / 2 ) ) ) )
250	230, 238, 249	mp2an 672	. . . . . . . . . . . . 13 |- ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) e. (TopOn ` ( 0 [,] ( 1 / 2 ) ) )
251	250	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) e. (TopOn ` ( 0 [,] ( 1 / 2 ) ) ) )
252	236	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( 0 [,] ( 1 / 4 ) ) C_ ( 0 [,] ( 1 / 2 ) ) )
253	198	iihalf1cn 20526	. . . . . . . . . . . . 13 |- ( x e. ( 0 [,] ( 1 / 2 ) ) |-> ( 2 x. x ) ) e. ( ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) Cn II )
254	253	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( x e. ( 0 [,] ( 1 / 2 ) ) |-> ( 2 x. x ) ) e. ( ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) Cn II ) )
255	248, 251, 252, 254	cnmpt1res 19271	. . . . . . . . . . 11 |- ( ph -> ( x e. ( 0 [,] ( 1 / 4 ) ) |-> ( 2 x. x ) ) e. ( ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) Cn II ) )
256		oveq2 6120	. . . . . . . . . . 11 |- ( x = y -> ( 2 x. x ) = ( 2 x. y ) )
257	242, 192, 243, 242, 255, 256	cnmpt21 19266	. . . . . . . . . 10 |- ( ph -> ( y e. ( 0 [,] ( 1 / 4 ) ) , z e. ( 0 [,] 1 ) |-> ( 2 x. y ) ) e. ( ( ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) tX II ) Cn II ) )
258		iccssre 11398	. . . . . . . . . . . . . 14 |- ( ( ( 1 / 4 ) e. RR /\ ( 1 / 2 ) e. RR ) -> ( ( 1 / 4 ) [,] ( 1 / 2 ) ) C_ RR )
259	18, 60, 258	mp2an 672	. . . . . . . . . . . . 13 |- ( ( 1 / 4 ) [,] ( 1 / 2 ) ) C_ RR
260		resttopon 18787	. . . . . . . . . . . . 13 |- ( ( ( topGen ` ran (,) ) e. (TopOn ` RR ) /\ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) C_ RR ) -> ( ( topGen ` ran (,) ) ↾t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) e. (TopOn ` ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) )
261	230, 259, 260	mp2an 672	. . . . . . . . . . . 12 |- ( ( topGen ` ran (,) ) ↾t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) e. (TopOn ` ( ( 1 / 4 ) [,] ( 1 / 2 ) ) )
262	261	a1i 11	. . . . . . . . . . 11 |- ( ph -> ( ( topGen ` ran (,) ) ↾t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) e. (TopOn ` ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) )
263	262, 192	cnmpt1st 19263	. . . . . . . . . . 11 |- ( ph -> ( y e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) , z e. ( 0 [,] 1 ) |-> y ) e. ( ( ( ( topGen ` ran (,) ) ↾t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) tX II ) Cn ( ( topGen ` ran (,) ) ↾t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) ) )
264		eqid 2443	. . . . . . . . . . . 12 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
265	259	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( ( 1 / 4 ) [,] ( 1 / 2 ) ) C_ RR )
266		unitssre 11453	. . . . . . . . . . . . 13 |- ( 0 [,] 1 ) C_ RR
267	266	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( 0 [,] 1 ) C_ RR )
268	150, 87	sseldi 3375	. . . . . . . . . . . . 13 |- ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( x + ( 1 / 4 ) ) e. ( 0 [,] 1 ) )
269	268	adantl 466	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) -> ( x + ( 1 / 4 ) ) e. ( 0 [,] 1 ) )
270	264	cnfldtopon 20384	. . . . . . . . . . . . . 14 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
271	270	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> ( TopOpen ` ℂfld ) e. (TopOn ` CC ) )
272	271	cnmptid 19256	. . . . . . . . . . . . 13 |- ( ph -> ( x e. CC |-> x ) e. ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) ) )
273	18	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1 / 4 ) e. RR )
274	273	recnd 9433	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 / 4 ) e. CC )
275	271, 271, 274	cnmptc 19257	. . . . . . . . . . . . 13 |- ( ph -> ( x e. CC |-> ( 1 / 4 ) ) e. ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) ) )
276	264	addcn 20463	. . . . . . . . . . . . . 14 |- + e. ( ( ( TopOpen ` ℂfld ) tX ( TopOpen ` ℂfld ) ) Cn ( TopOpen ` ℂfld ) )
277	276	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> + e. ( ( ( TopOpen ` ℂfld ) tX ( TopOpen ` ℂfld ) ) Cn ( TopOpen ` ℂfld ) ) )
278	271, 272, 275, 277	cnmpt12f 19261	. . . . . . . . . . . 12 |- ( ph -> ( x e. CC |-> ( x + ( 1 / 4 ) ) ) e. ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) ) )
279	264, 219, 200, 265, 267, 269, 278	cnmptre 20521	. . . . . . . . . . 11 |- ( ph -> ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) |-> ( x + ( 1 / 4 ) ) ) e. ( ( ( topGen ` ran (,) ) ↾t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) Cn II ) )
280		oveq1 6119	. . . . . . . . . . 11 |- ( x = y -> ( x + ( 1 / 4 ) ) = ( y + ( 1 / 4 ) ) )
281	262, 192, 263, 262, 279, 280	cnmpt21 19266	. . . . . . . . . 10 |- ( ph -> ( y e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) , z e. ( 0 [,] 1 ) |-> ( y + ( 1 / 4 ) ) ) e. ( ( ( ( topGen ` ran (,) ) ↾t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) tX II ) Cn II ) )
282	197, 218, 219, 198, 201, 220, 225, 192, 229, 257, 281	cnmpt2pc 20522	. . . . . . . . 9 |- ( ph -> ( y e. ( 0 [,] ( 1 / 2 ) ) , z e. ( 0 [,] 1 ) |-> if ( y <_ ( 1 / 4 ) , ( 2 x. y ) , ( y + ( 1 / 4 ) ) ) ) e. ( ( ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) tX II ) Cn II ) )
283		iccssre 11398	. . . . . . . . . . . . 13 |- ( ( ( 1 / 2 ) e. RR /\ 1 e. RR ) -> ( ( 1 / 2 ) [,] 1 ) C_ RR )
284	60, 6, 283	mp2an 672	. . . . . . . . . . . 12 |- ( ( 1 / 2 ) [,] 1 ) C_ RR
285		resttopon 18787	. . . . . . . . . . . 12 |- ( ( ( topGen ` ran (,) ) e. (TopOn ` RR ) /\ ( ( 1 / 2 ) [,] 1 ) C_ RR ) -> ( ( topGen ` ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) e. (TopOn ` ( ( 1 / 2 ) [,] 1 ) ) )
286	230, 284, 285	mp2an 672	. . . . . . . . . . 11 |- ( ( topGen ` ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) e. (TopOn ` ( ( 1 / 2 ) [,] 1 ) )
287	286	a1i 11	. . . . . . . . . 10 |- ( ph -> ( ( topGen ` ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) e. (TopOn ` ( ( 1 / 2 ) [,] 1 ) ) )
288	287, 192	cnmpt1st 19263	. . . . . . . . . 10 |- ( ph -> ( y e. ( ( 1 / 2 ) [,] 1 ) , z e. ( 0 [,] 1 ) |-> y ) e. ( ( ( ( topGen ` ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) tX II ) Cn ( ( topGen ` ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) ) )
289	284	a1i 11	. . . . . . . . . . 11 |- ( ph -> ( ( 1 / 2 ) [,] 1 ) C_ RR )
290	150, 157	sseldi 3375	. . . . . . . . . . . 12 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( ( x / 2 ) + ( 1 / 2 ) ) e. ( 0 [,] 1 ) )
291	290	adantl 466	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( x / 2 ) + ( 1 / 2 ) ) e. ( 0 [,] 1 ) )
292	264	divccn 20471	. . . . . . . . . . . . . 14 |- ( ( 2 e. CC /\ 2 =/= 0 ) -> ( x e. CC |-> ( x / 2 ) ) e. ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) ) )
293	4, 25, 292	mp2an 672	. . . . . . . . . . . . 13 |- ( x e. CC |-> ( x / 2 ) ) e. ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) )
294	293	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( x e. CC |-> ( x / 2 ) ) e. ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) ) )
295	32	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> ( 1 / 2 ) e. CC )
296	271, 271, 295	cnmptc 19257	. . . . . . . . . . . 12 |- ( ph -> ( x e. CC |-> ( 1 / 2 ) ) e. ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) ) )
297	271, 294, 296, 277	cnmpt12f 19261	. . . . . . . . . . 11 |- ( ph -> ( x e. CC |-> ( ( x / 2 ) + ( 1 / 2 ) ) ) e. ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) ) )
298	264, 199, 200, 289, 267, 291, 297	cnmptre 20521	. . . . . . . . . 10 |- ( ph -> ( x e. ( ( 1 / 2 ) [,] 1 ) |-> ( ( x / 2 ) + ( 1 / 2 ) ) ) e. ( ( ( topGen ` ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) Cn II ) )
299		oveq1 6119	. . . . . . . . . . 11 |- ( x = y -> ( x / 2 ) = ( y / 2 ) )
300	299	oveq1d 6127	. . . . . . . . . 10 |- ( x = y -> ( ( x / 2 ) + ( 1 / 2 ) ) = ( ( y / 2 ) + ( 1 / 2 ) ) )
301	287, 192, 288, 287, 298, 300	cnmpt21 19266	. . . . . . . . 9 |- ( ph -> ( y e. ( ( 1 / 2 ) [,] 1 ) , z e. ( 0 [,] 1 ) |-> ( ( y / 2 ) + ( 1 / 2 ) ) ) e. ( ( ( ( topGen ` ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) tX II ) Cn II ) )
302	197, 198, 199, 200, 201, 202, 203, 192, 217, 282, 301	cnmpt2pc 20522	. . . . . . . 8 |- ( ph -> ( y e. ( 0 [,] 1 ) , z e. ( 0 [,] 1 ) |-> if ( y <_ ( 1 / 2 ) , if ( y <_ ( 1 / 4 ) , ( 2 x. y ) , ( y + ( 1 / 4 ) ) ) , ( ( y / 2 ) + ( 1 / 2 ) ) ) ) e. ( ( II tX II ) Cn II ) )
303		breq1 4316	. . . . . . . . . . . 12 |- ( x = y -> ( x <_ ( 1 / 2 ) <-> y <_ ( 1 / 2 ) ) )
304		breq1 4316	. . . . . . . . . . . . 13 |- ( x = y -> ( x <_ ( 1 / 4 ) <-> y <_ ( 1 / 4 ) ) )
305	304, 256, 280	ifbieq12d 3837	. . . . . . . . . . . 12 |- ( x = y -> if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) = if ( y <_ ( 1 / 4 ) , ( 2 x. y ) , ( y + ( 1 / 4 ) ) ) )
306	303, 305, 300	ifbieq12d 3837	. . . . . . . . . . 11 |- ( x = y -> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) = if ( y <_ ( 1 / 2 ) , if ( y <_ ( 1 / 4 ) , ( 2 x. y ) , ( y + ( 1 / 4 ) ) ) , ( ( y / 2 ) + ( 1 / 2 ) ) ) )
307	306	equcoms 1733	. . . . . . . . . 10 |- ( y = x -> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) = if ( y <_ ( 1 / 2 ) , if ( y <_ ( 1 / 4 ) , ( 2 x. y ) , ( y + ( 1 / 4 ) ) ) , ( ( y / 2 ) + ( 1 / 2 ) ) ) )
308	307	adantr 465	. . . . . . . . 9 |- ( ( y = x /\ z = 0 ) -> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) = if ( y <_ ( 1 / 2 ) , if ( y <_ ( 1 / 4 ) , ( 2 x. y ) , ( y + ( 1 / 4 ) ) ) , ( ( y / 2 ) + ( 1 / 2 ) ) ) )
309	308	eqcomd 2448	. . . . . . . 8 |- ( ( y = x /\ z = 0 ) -> if ( y <_ ( 1 / 2 ) , if ( y <_ ( 1 / 4 ) , ( 2 x. y ) , ( y + ( 1 / 4 ) ) ) , ( ( y / 2 ) + ( 1 / 2 ) ) ) = if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) )
310	192, 193, 196, 192, 192, 302, 309	cnmpt12 19262	. . . . . . 7 |- ( ph -> ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) e. ( II Cn II ) )
311	190, 310	syl5eqel 2527	. . . . . 6 |- ( ph -> P e. ( II Cn II ) )
312		iiuni 20479	. . . . . . 7 |- ( 0 [,] 1 ) = U. II
313	312, 312	cnf 18872	. . . . . 6 |- ( P e. ( II Cn II ) -> P : ( 0 [,] 1 ) --> ( 0 [,] 1 ) )
314	311, 313	syl 16	. . . . 5 |- ( ph -> P : ( 0 [,] 1 ) --> ( 0 [,] 1 ) )
315	190	fmpt 5885	. . . . 5 |- ( A. x e. ( 0 [,] 1 ) if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) e. ( 0 [,] 1 ) <-> P : ( 0 [,] 1 ) --> ( 0 [,] 1 ) )
316	314, 315	sylibr 212	. . . 4 |- ( ph -> A. x e. ( 0 [,] 1 ) if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) e. ( 0 [,] 1 ) )
317	190	a1i 11	. . . 4 |- ( ph -> P = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) )
318	41, 45, 91	pcocn 20611	. . . . . 6 |- ( ph -> ( F ( *p ` J ) ( G ( *p ` J ) H ) ) e. ( II Cn J ) )
319		eqid 2443	. . . . . . 7 |- U. J = U. J
320	312, 319	cnf 18872	. . . . . 6 |- ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) e. ( II Cn J ) -> ( F ( *p ` J ) ( G ( *p ` J ) H ) ) : ( 0 [,] 1 ) --> U. J )
321	318, 320	syl 16	. . . . 5 |- ( ph -> ( F ( *p ` J ) ( G ( *p ` J ) H ) ) : ( 0 [,] 1 ) --> U. J )
322	321	feqmptd 5765	. . . 4 |- ( ph -> ( F ( *p ` J ) ( G ( *p ` J ) H ) ) = ( y e. ( 0 [,] 1 ) |-> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` y ) ) )
323		fveq2 5712	. . . 4 |- ( y = if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` y ) = ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) )
324	316, 317, 322, 323	fmptcof 5898	. . 3 |- ( ph -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) o. P ) = ( x e. ( 0 [,] 1 ) |-> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) ) ) )
325	41, 42, 89	pcocn 20611	. . . 4 |- ( ph -> ( F ( *p ` J ) G ) e. ( II Cn J ) )
326	325, 43	pcoval 20605	. . 3 |- ( ph -> ( ( F ( *p ` J ) G ) ( *p ` J ) H ) = ( x e. ( 0 [,] 1 ) |-> if ( x <_ ( 1 / 2 ) , ( ( F ( *p ` J ) G ) ` ( 2 x. x ) ) , ( H ` ( ( 2 x. x ) - 1 ) ) ) ) )
327	189, 324, 326	3eqtr4rd 2486	. 2 |- ( ph -> ( ( F ( *p ` J ) G ) ( *p ` J ) H ) = ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) o. P ) )
328		id 22	. . . . . . . 8 |- ( x = 0 -> x = 0 )
329	328, 143	syl6eqbr 4350	. . . . . . 7 |- ( x = 0 -> x <_ ( 1 / 2 ) )
330	329, 135	syl 16	. . . . . 6 |- ( x = 0 -> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) = if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) )
331	328, 222	syl6eqbr 4350	. . . . . . 7 |- ( x = 0 -> x <_ ( 1 / 4 ) )
332	331, 1	syl 16	. . . . . 6 |- ( x = 0 -> if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) = ( 2 x. x ) )
333		oveq2 6120	. . . . . . 7 |- ( x = 0 -> ( 2 x. x ) = ( 2 x. 0 ) )
334		2t0e0 10498	. . . . . . 7 |- ( 2 x. 0 ) = 0
335	333, 334	syl6eq 2491	. . . . . 6 |- ( x = 0 -> ( 2 x. x ) = 0 )
336	330, 332, 335	3eqtrd 2479	. . . . 5 |- ( x = 0 -> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) = 0 )
337		c0ex 9401	. . . . 5 |- 0 e. _V
338	336, 190, 337	fvmpt 5795	. . . 4 |- ( 0 e. ( 0 [,] 1 ) -> ( P ` 0 ) = 0 )
339	195, 338	syl 16	. . 3 |- ( ph -> ( P ` 0 ) = 0 )
340	148	a1i 11	. . . 4 |- ( ph -> 1 e. ( 0 [,] 1 ) )
341	60, 6	ltnlei 9516	. . . . . . . . 9 |- ( ( 1 / 2 ) < 1 <-> -. 1 <_ ( 1 / 2 ) )
342	144, 341	mpbi 208	. . . . . . . 8 |- -. 1 <_ ( 1 / 2 )
343		breq1 4316	. . . . . . . 8 |- ( x = 1 -> ( x <_ ( 1 / 2 ) <-> 1 <_ ( 1 / 2 ) ) )
344	342, 343	mtbiri 303	. . . . . . 7 |- ( x = 1 -> -. x <_ ( 1 / 2 ) )
345	344, 182	syl 16	. . . . . 6 |- ( x = 1 -> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) = ( ( x / 2 ) + ( 1 / 2 ) ) )
346		oveq1 6119	. . . . . . . 8 |- ( x = 1 -> ( x / 2 ) = ( 1 / 2 ) )
347	346	oveq1d 6127	. . . . . . 7 |- ( x = 1 -> ( ( x / 2 ) + ( 1 / 2 ) ) = ( ( 1 / 2 ) + ( 1 / 2 ) ) )
348	347, 84	syl6eq 2491	. . . . . 6 |- ( x = 1 -> ( ( x / 2 ) + ( 1 / 2 ) ) = 1 )
349	345, 348	eqtrd 2475	. . . . 5 |- ( x = 1 -> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) = 1 )
350		1ex 9402	. . . . 5 |- 1 e. _V
351	349, 190, 350	fvmpt 5795	. . . 4 |- ( 1 e. ( 0 [,] 1 ) -> ( P ` 1 ) = 1 )
352	340, 351	syl 16	. . 3 |- ( ph -> ( P ` 1 ) = 1 )
353	318, 311, 339, 352	reparpht 20592	. 2 |- ( ph -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) o. P ) ( ~=ph ` J ) ( F ( *p ` J ) ( G ( *p ` J ) H ) ) )
354	327, 353	eqbrtrd 4333	1 |- ( ph -> ( ( F ( *p ` J ) G ) ( *p ` J ) H ) ( ~=ph ` J ) ( F ( *p ` J ) ( G ( *p ` J ) H ) ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 368   /\ wa 369   = wceq 1369   e. wcel 1756   =/= wne 2620   A.wral 2736   _Vcvv 2993   C_ wss 3349   ifcif 3812   U.cuni 4112   class class class wbr 4313   e. cmpt 4371   ran crn 4862   o. ccom 4865   -->wf 5435   ` cfv 5439  (class class class)co 6112   CCcc 9301   RRcr 9302   0cc0 9303   1c1 9304   + caddc 9306   x. cmul 9308   RR*cxr 9438   < clt 9439   <_ cle 9440   - cmin 9616   / cdiv 10014   NNcn 10343   2c2 10392   4c4 10394   (,)cioo 11321   [,]cicc 11324   ↾_t crest 14380   TopOpenctopn 14381   topGenctg 14397  ℂ_fldccnfld 17840   Topctop 18520  TopOnctopon 18521   Cn ccn 18850   tX ctx 19155   IIcii 20473   ~=ph cphtpc 20563   *pcpco 20594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4424  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393  ax-inf2 7868  ax-cnex 9359  ax-resscn 9360  ax-1cn 9361  ax-icn 9362  ax-addcl 9363  ax-addrcl 9364  ax-mulcl 9365  ax-mulrcl 9366  ax-mulcom 9367  ax-addass 9368  ax-mulass 9369  ax-distr 9370  ax-i2m1 9371  ax-1ne0 9372  ax-1rid 9373  ax-rnegex 9374  ax-rrecex 9375  ax-cnre 9376  ax-pre-lttri 9377  ax-pre-lttrn 9378  ax-pre-ltadd 9379  ax-pre-mulgt0 9380  ax-pre-sup 9381  ax-addf 9382  ax-mulf 9383

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-int 4150  df-iun 4194  df-iin 4195  df-br 4314  df-opab 4372  df-mpt 4373  df-tr 4407  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-se 4701  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-isom 5448  df-riota 6073  df-ov 6115  df-oprab 6116  df-mpt2 6117  df-of 6341  df-om 6498  df-1st 6598  df-2nd 6599  df-supp 6712  df-recs 6853  df-rdg 6887  df-1o 6941  df-2o 6942  df-oadd 6945  df-er 7122  df-map 7237  df-ixp 7285  df-en 7332  df-dom 7333  df-sdom 7334  df-fin 7335  df-fsupp 7642  df-fi 7682  df-sup 7712  df-oi 7745  df-card 8130  df-cda 8358  df-pnf 9441  df-mnf 9442  df-xr 9443  df-ltxr 9444  df-le 9445  df-sub 9618  df-neg 9619  df-div 10015  df-nn 10344  df-2 10401  df-3 10402  df-4 10403  df-5 10404  df-6 10405  df-7 10406  df-8 10407  df-9 10408  df-10 10409  df-n0 10601  df-z 10668  df-dec 10777  df-uz 10883  df-q 10975  df-rp 11013  df-xneg 11110  df-xadd 11111  df-xmul 11112  df-ioo 11325  df-icc 11328  df-fz 11459  df-fzo 11570  df-seq 11828  df-exp 11887  df-hash 12125  df-cj 12609  df-re 12610  df-im 12611  df-sqr 12745  df-abs 12746  df-struct 14197  df-ndx 14198  df-slot 14199  df-base 14200  df-sets 14201  df-ress 14202  df-plusg 14272  df-mulr 14273  df-starv 14274  df-sca 14275  df-vsca 14276  df-ip 14277  df-tset 14278  df-ple 14279  df-ds 14281  df-unif 14282  df-hom 14283  df-cco 14284  df-rest 14382  df-topn 14383  df-0g 14401  df-gsum 14402  df-topgen 14403  df-pt 14404  df-prds 14407  df-xrs 14461  df-qtop 14466  df-imas 14467  df-xps 14469  df-mre 14545  df-mrc 14546  df-acs 14548  df-mnd 15436  df-submnd 15486  df-mulg 15569  df-cntz 15856  df-cmn 16300  df-psmet 17831  df-xmet 17832  df-met 17833  df-bl 17834  df-mopn 17835  df-cnfld 17841  df-top 18525  df-bases 18527  df-topon 18528  df-topsp 18529  df-cld 18645  df-cn 18853  df-cnp 18854  df-tx 19157  df-hmeo 19350  df-xms 19917  df-ms 19918  df-tms 19919  df-ii 20475  df-htpy 20564  df-phtpy 20565  df-phtpc 20586  df-pco 20599

This theorem is referenced by:  pcophtb  20623  pi1grplem  20643  pi1xfr  20649  pi1xfrcnvlem  20650