Theorem pcoass 21287

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 3945	. . . . . . . . . . 11 |- ( x <_ ( 1 / 4 ) -> if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) = ( 2 x. x ) )
2	1	fveq2d 5870	. . . . . . . . . 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 10606	. . . . . . . . . . . . 13 |- 2 e. CC
5		0re 9596	. . . . . . . . . . . . . . . . 17 |- 0 e. RR
6		1re 9595	. . . . . . . . . . . . . . . . 17 |- 1 e. RR
7	5, 6	elicc2i 11590	. . . . . . . . . . . . . . . 16 |- ( x e. ( 0 [,] 1 ) <-> ( x e. RR /\ 0 <_ x /\ x <_ 1 ) )
8	7	simp1bi 1011	. . . . . . . . . . . . . . 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 9622	. . . . . . . . . . . . 13 |- ( ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 4 ) ) -> x e. CC )
11		mulcom 9578	. . . . . . . . . . . . 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 1012	. . . . . . . . . . . . . . 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 10695	. . . . . . . . . . . . . . . 16 |- 4 e. NN
17		nnrecre 10572	. . . . . . . . . . . . . . . 16 |- ( 4 e. NN -> ( 1 / 4 ) e. RR )
18	16, 17	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( 1 / 4 ) e. RR
19	5, 18	elicc2i 11590	. . . . . . . . . . . . . 14 |- ( x e. ( 0 [,] ( 1 / 4 ) ) <-> ( x e. RR /\ 0 <_ x /\ x <_ ( 1 / 4 ) ) )
20	9, 14, 15, 19	syl3anbrc 1180	. . . . . . . . . . . . 13 |- ( ( x e. ( 0 [,] 1 ) /\ x <_ ( 1 / 4 ) ) -> x e. ( 0 [,] ( 1 / 4 ) ) )
21		2rp 11225	. . . . . . . . . . . . . 14 |- 2 e. RR+
22	4	mul02i 9768	. . . . . . . . . . . . . 14 |- ( 0 x. 2 ) = 0
23	18	recni 9608	. . . . . . . . . . . . . . 15 |- ( 1 / 4 ) e. CC
24	23	2timesi 10656	. . . . . . . . . . . . . . . 16 |- ( 2 x. ( 1 / 4 ) ) = ( ( 1 / 4 ) + ( 1 / 4 ) )
25		2ne0 10628	. . . . . . . . . . . . . . . . . . . 20 |- 2 =/= 0
26		recdiv2 10257	. . . . . . . . . . . . . . . . . . . 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 10685	. . . . . . . . . . . . . . . . . . . 20 |- ( 2 x. 2 ) = 4
29	28	oveq2i 6295	. . . . . . . . . . . . . . . . . . 19 |- ( 1 / ( 2 x. 2 ) ) = ( 1 / 4 )
30	27, 29	eqtri 2496	. . . . . . . . . . . . . . . . . 18 |- ( ( 1 / 2 ) / 2 ) = ( 1 / 4 )
31	30, 30	oveq12i 6296	. . . . . . . . . . . . . . . . 17 |- ( ( ( 1 / 2 ) / 2 ) + ( ( 1 / 2 ) / 2 ) ) = ( ( 1 / 4 ) + ( 1 / 4 ) )
32		halfcn 10755	. . . . . . . . . . . . . . . . . 18 |- ( 1 / 2 ) e. CC
33		2halves 10767	. . . . . . . . . . . . . . . . . 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 2498	. . . . . . . . . . . . . . . 16 |- ( ( 1 / 4 ) + ( 1 / 4 ) ) = ( 1 / 2 )
36	24, 35	eqtri 2496	. . . . . . . . . . . . . . 15 |- ( 2 x. ( 1 / 4 ) ) = ( 1 / 2 )
37	4, 23, 36	mulcomli 9603	. . . . . . . . . . . . . 14 |- ( ( 1 / 4 ) x. 2 ) = ( 1 / 2 )
38	5, 18, 21, 22, 37	iccdili 11659	. . . . . . . . . . . . 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 2555	. . . . . . . . . . 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 21280	. . . . . . . . . . . . 13 |- ( ph -> ( G ( *p ` J ) H ) e. ( II Cn J ) )
46	41, 45	pcoval1 21276	. . . . . . . . . . . 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 21276	. . . . . . . . . . . 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 2511	. . . . . . . . . . 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 2508	. . . . . . . 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 9685	. . . . . . . . . . . . . 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 911	. . . . . . . . . . . 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 10754	. . . . . . . . . . . . 13 |- ( 1 / 2 ) e. RR
61	18, 60	elicc2i 11590	. . . . . . . . . . . 12 |- ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) <-> ( x e. RR /\ ( 1 / 4 ) <_ x /\ x <_ ( 1 / 2 ) ) )
62	55, 58, 59, 61	syl3anbrc 1180	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) )
63	61	simp1bi 1011	. . . . . . . . . . . . 13 |- ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> x e. RR )
64		readdcl 9575	. . . . . . . . . . . . 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 1012	. . . . . . . . . . . . . 14 |- ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( 1 / 4 ) <_ x )
68	66, 63, 66, 67	leadd1dd 10166	. . . . . . . . . . . . 13 |- ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( ( 1 / 4 ) + ( 1 / 4 ) ) <_ ( x + ( 1 / 4 ) ) )
69	35, 68	syl5eqbrr 4481	. . . . . . . . . . . 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 1013	. . . . . . . . . . . . . 14 |- ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> x <_ ( 1 / 2 ) )
72		2lt4 10706	. . . . . . . . . . . . . . . . 17 |- 2 < 4
73		2re 10605	. . . . . . . . . . . . . . . . . 18 |- 2 e. RR
74		4re 10612	. . . . . . . . . . . . . . . . . 18 |- 4 e. RR
75		2pos 10627	. . . . . . . . . . . . . . . . . 18 |- 0 < 2
76		4pos 10631	. . . . . . . . . . . . . . . . . 18 |- 0 < 4
77	73, 74, 75, 76	ltrecii 10462	. . . . . . . . . . . . . . . . 17 |- ( 2 < 4 <-> ( 1 / 4 ) < ( 1 / 2 ) )
78	72, 77	mpbi 208	. . . . . . . . . . . . . . . 16 |- ( 1 / 4 ) < ( 1 / 2 )
79	18, 60, 78	ltleii 9707	. . . . . . . . . . . . . . 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 10170	. . . . . . . . . . . . 13 |- ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( x + ( 1 / 4 ) ) <_ ( ( 1 / 2 ) + ( 1 / 2 ) ) )
82		ax-1cn 9550	. . . . . . . . . . . . . 14 |- 1 e. CC
83		2halves 10767	. . . . . . . . . . . . . 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 4486	. . . . . . . . . . . 12 |- ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) -> ( x + ( 1 / 4 ) ) <_ 1 )
86	60, 6	elicc2i 11590	. . . . . . . . . . . 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 1180	. . . . . . . . . . 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 21277	. . . . . . . . . . . 12 |- ( ph -> ( ( G ( *p ` J ) H ) ` 0 ) = ( G ` 0 ) )
91	89, 90	eqtr4d 2511	. . . . . . . . . . 11 |- ( ph -> ( F ` 1 ) = ( ( G ( *p ` J ) H ) ` 0 ) )
92	41, 45, 91	pcoval2 21279	. . . . . . . . . 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 6295	. . . . . . . . . . . 12 |- ( ( 2 x. ( x + ( 1 / 4 ) ) ) - ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( 2 x. ( x + ( 1 / 4 ) ) ) - 1 )
95		2cnd 10608	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> 2 e. CC )
96	55	recnd 9622	. . . . . . . . . . . . . . 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 9620	. . . . . . . . . . . . . 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 6295	. . . . . . . . . . . . . 14 |- ( ( 2 x. x ) + ( 2 x. ( 1 / 4 ) ) ) = ( ( 2 x. x ) + ( 1 / 2 ) )
100	98, 99	syl6eq 2524	. . . . . . . . . . . . 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 6299	. . . . . . . . . . . 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 2522	. . . . . . . . . . 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 9577	. . . . . . . . . . . . . 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 9622	. . . . . . . . . . . 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 9968	. . . . . . . . . . 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 2508	. . . . . . . . . 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 5870	. . . . . . . . 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 10288	. . . . . . . . . . . . . . 15 |- ( ( 1 / 2 ) x. 2 ) = 1
112	18, 60, 21, 37, 111	iccdili 11659	. . . . . . . . . . . . . 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 2555	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. ( 0 [,] 1 ) ) /\ x <_ ( 1 / 2 ) ) /\ -. x <_ ( 1 / 4 ) ) -> ( 2 x. x ) e. ( ( 1 / 2 ) [,] 1 ) )
115	32	subidi 9890	. . . . . . . . . . . . 13 |- ( ( 1 / 2 ) - ( 1 / 2 ) ) = 0
116		1mhlfehlf 10758	. . . . . . . . . . . . 13 |- ( 1 - ( 1 / 2 ) ) = ( 1 / 2 )
117	60, 6, 60, 115, 116	iccshftli 11657	. . . . . . . . . . . 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 21276	. . . . . . . . . . 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 10012	. . . . . . . . . . . 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 10275	. . . . . . . . . . . . 13 |- ( 2 x. ( 1 / 2 ) ) = 1
123	122	oveq2i 6295	. . . . . . . . . . . 12 |- ( ( 2 x. ( 2 x. x ) ) - ( 2 x. ( 1 / 2 ) ) ) = ( ( 2 x. ( 2 x. x ) ) - 1 )
124	121, 123	syl6eq 2524	. . . . . . . . . . 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 5870	. . . . . . . . . 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 2508	. . . . . . . . 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 2512	. . . . . . . 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 3948	. . . . . . . . . 10 |- ( -. x <_ ( 1 / 4 ) -> if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) = ( x + ( 1 / 4 ) ) )
129	128	fveq2d 5870	. . . . . . . . 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 21279	. . . . . . . . 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 2518	. . . . . . 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 3945	. . . . . . . 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 5870	. . . . . . 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 3945	. . . . . . 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 2518	. . . . 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 21199	. . . . . . . 8 |- ( ( x e. ( 0 [,] 1 ) /\ -. x <_ ( 1 / 2 ) ) -> x e. ( ( 1 / 2 ) [,] 1 ) )
142		halfgt0 10756	. . . . . . . . . . . . . . 15 |- 0 < ( 1 / 2 )
143	5, 60, 142	ltleii 9707	. . . . . . . . . . . . . 14 |- 0 <_ ( 1 / 2 )
144		halflt1 10757	. . . . . . . . . . . . . . 15 |- ( 1 / 2 ) < 1
145	60, 6, 144	ltleii 9707	. . . . . . . . . . . . . 14 |- ( 1 / 2 ) <_ 1
146	5, 6	elicc2i 11590	. . . . . . . . . . . . . 14 |- ( ( 1 / 2 ) e. ( 0 [,] 1 ) <-> ( ( 1 / 2 ) e. RR /\ 0 <_ ( 1 / 2 ) /\ ( 1 / 2 ) <_ 1 ) )
147	60, 143, 145, 146	mpbir3an 1178	. . . . . . . . . . . . 13 |- ( 1 / 2 ) e. ( 0 [,] 1 )
148		1elunit 11639	. . . . . . . . . . . . 13 |- 1 e. ( 0 [,] 1 )
149		iccss2 11595	. . . . . . . . . . . . 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 3500	. . . . . . . . . . 11 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> x e. ( 0 [,] 1 ) )
152	4, 25	div0i 10278	. . . . . . . . . . . 12 |- ( 0 / 2 ) = 0
153		eqid 2467	. . . . . . . . . . . 12 |- ( 1 / 2 ) = ( 1 / 2 )
154	5, 6, 21, 152, 153	icccntri 11661	. . . . . . . . . . 11 |- ( x e. ( 0 [,] 1 ) -> ( x / 2 ) e. ( 0 [,] ( 1 / 2 ) ) )
155	32	addid2i 9767	. . . . . . . . . . . 12 |- ( 0 + ( 1 / 2 ) ) = ( 1 / 2 )
156	5, 60, 60, 155, 84	iccshftri 11655	. . . . . . . . . . 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 21279	. . . . . . . . . 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 11590	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( ( 1 / 2 ) [,] 1 ) <-> ( x e. RR /\ ( 1 / 2 ) <_ x /\ x <_ 1 ) )
161	160	simp1bi 1011	. . . . . . . . . . . . . . . . 17 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> x e. RR )
162	161	recnd 9622	. . . . . . . . . . . . . . . 16 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> x e. CC )
163	82	a1i 11	. . . . . . . . . . . . . . . 16 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> 1 e. CC )
164		2cnd 10608	. . . . . . . . . . . . . . . 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 10358	. . . . . . . . . . . . . . 15 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( ( x + 1 ) / 2 ) = ( ( x / 2 ) + ( 1 / 2 ) ) )
167	166	oveq2d 6300	. . . . . . . . . . . . . 14 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( 2 x. ( ( x + 1 ) / 2 ) ) = ( 2 x. ( ( x / 2 ) + ( 1 / 2 ) ) ) )
168		peano2cn 9751	. . . . . . . . . . . . . . . 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 10322	. . . . . . . . . . . . . 14 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( 2 x. ( ( x + 1 ) / 2 ) ) = ( x + 1 ) )
171	167, 170	eqtr3d 2510	. . . . . . . . . . . . 13 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( 2 x. ( ( x / 2 ) + ( 1 / 2 ) ) ) = ( x + 1 ) )
172	171	oveq1d 6299	. . . . . . . . . . . 12 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( ( 2 x. ( ( x / 2 ) + ( 1 / 2 ) ) ) - 1 ) = ( ( x + 1 ) - 1 ) )
173		pncan 9826	. . . . . . . . . . . . 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 2508	. . . . . . . . . . 11 |- ( x e. ( ( 1 / 2 ) [,] 1 ) -> ( ( 2 x. ( ( x / 2 ) + ( 1 / 2 ) ) ) - 1 ) = x )
176	175	fveq2d 5870	. . . . . . . . . 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 21279	. . . . . . . . 9 |- ( ( ph /\ x e. ( ( 1 / 2 ) [,] 1 ) ) -> ( ( G ( *p ` J ) H ) ` x ) = ( H ` ( ( 2 x. x ) - 1 ) ) )
179	159, 177, 178	3eqtrd 2512	. . . . . . . 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 3948	. . . . . . . 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 5870	. . . . . . 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 3948	. . . . . . 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 2518	. . . . 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 4533	. . 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 21146	. . . . . . . . 9 |- II e. (TopOn ` ( 0 [,] 1 ) )
192	191	a1i 11	. . . . . . . 8 |- ( ph -> II e. (TopOn ` ( 0 [,] 1 ) ) )
193	192	cnmptid 19925	. . . . . . . 8 |- ( ph -> ( x e. ( 0 [,] 1 ) |-> x ) e. ( II Cn II ) )
194		0elunit 11638	. . . . . . . . . 10 |- 0 e. ( 0 [,] 1 )
195	194	a1i 11	. . . . . . . . 9 |- ( ph -> 0 e. ( 0 [,] 1 ) )
196	192, 192, 195	cnmptc 19926	. . . . . . . 8 |- ( ph -> ( x e. ( 0 [,] 1 ) |-> 0 ) e. ( II Cn II ) )
197		eqid 2467	. . . . . . . . 9 |- ( topGen ` ran (,) ) = ( topGen ` ran (,) )
198		eqid 2467	. . . . . . . . 9 |- ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) = ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) )
199		eqid 2467	. . . . . . . . 9 |- ( ( topGen ` ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) = ( ( topGen ` ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) )
200		dfii2 21149	. . . . . . . . 9 |- II = ( ( topGen ` ran (,) ) ↾t ( 0 [,] 1 ) )
201		0red 9597	. . . . . . . . 9 |- ( ph -> 0 e. RR )
202		1red 9611	. . . . . . . . 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 6299	. . . . . . . . . . 11 |- ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( y + ( 1 / 4 ) ) = ( ( 1 / 2 ) + ( 1 / 4 ) ) )
206	32, 23	addcomi 9770	. . . . . . . . . . 11 |- ( ( 1 / 2 ) + ( 1 / 4 ) ) = ( ( 1 / 4 ) + ( 1 / 2 ) )
207	205, 206	syl6eq 2524	. . . . . . . . . 10 |- ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( y + ( 1 / 4 ) ) = ( ( 1 / 4 ) + ( 1 / 2 ) ) )
208	18, 60	ltnlei 9705	. . . . . . . . . . . . 13 |- ( ( 1 / 4 ) < ( 1 / 2 ) <-> -. ( 1 / 2 ) <_ ( 1 / 4 ) )
209	78, 208	mpbi 208	. . . . . . . . . . . 12 |- -. ( 1 / 2 ) <_ ( 1 / 4 )
210	204	breq1d 4457	. . . . . . . . . . . 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 3948	. . . . . . . . . . 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 6299	. . . . . . . . . . . 12 |- ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( y / 2 ) = ( ( 1 / 2 ) / 2 ) )
215	214, 30	syl6eq 2524	. . . . . . . . . . 11 |- ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( y / 2 ) = ( 1 / 4 ) )
216	215	oveq1d 6299	. . . . . . . . . 10 |- ( ( ph /\ ( y = ( 1 / 2 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( ( y / 2 ) + ( 1 / 2 ) ) = ( ( 1 / 4 ) + ( 1 / 2 ) ) )
217	207, 213, 216	3eqtr4d 2518	. . . . . . . . 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 2467	. . . . . . . . . 10 |- ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) = ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) )
219		eqid 2467	. . . . . . . . . 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 10451	. . . . . . . . . . . . 13 |- 0 < ( 1 / 4 )
222	5, 18, 221	ltleii 9707	. . . . . . . . . . . 12 |- 0 <_ ( 1 / 4 )
223	5, 60	elicc2i 11590	. . . . . . . . . . . 12 |- ( ( 1 / 4 ) e. ( 0 [,] ( 1 / 2 ) ) <-> ( ( 1 / 4 ) e. RR /\ 0 <_ ( 1 / 4 ) /\ ( 1 / 4 ) <_ ( 1 / 2 ) ) )
224	18, 222, 79, 223	mpbir3an 1178	. . . . . . . . . . 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 6300	. . . . . . . . . . 11 |- ( ( ph /\ ( y = ( 1 / 4 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( 2 x. y ) = ( 2 x. ( 1 / 4 ) ) )
228	226	oveq1d 6299	. . . . . . . . . . 11 |- ( ( ph /\ ( y = ( 1 / 4 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( y + ( 1 / 4 ) ) = ( ( 1 / 4 ) + ( 1 / 4 ) ) )
229	24, 227, 228	3eqtr4a 2534	. . . . . . . . . 10 |- ( ( ph /\ ( y = ( 1 / 4 ) /\ z e. ( 0 [,] 1 ) ) ) -> ( 2 x. y ) = ( y + ( 1 / 4 ) ) )
230		retopon 21033	. . . . . . . . . . . . 13 |- ( topGen ` ran (,) ) e. (TopOn ` RR )
231		0xr 9640	. . . . . . . . . . . . . . . 16 |- 0 e. RR*
232	60	rexri 9646	. . . . . . . . . . . . . . . 16 |- ( 1 / 2 ) e. RR*
233		lbicc2 11636	. . . . . . . . . . . . . . . 16 |- ( ( 0 e. RR* /\ ( 1 / 2 ) e. RR* /\ 0 <_ ( 1 / 2 ) ) -> 0 e. ( 0 [,] ( 1 / 2 ) ) )
234	231, 232, 143, 233	mp3an 1324	. . . . . . . . . . . . . . 15 |- 0 e. ( 0 [,] ( 1 / 2 ) )
235		iccss2 11595	. . . . . . . . . . . . . . 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 11606	. . . . . . . . . . . . . . 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 3513	. . . . . . . . . . . . 13 |- ( 0 [,] ( 1 / 4 ) ) C_ RR
240		resttopon 19456	. . . . . . . . . . . . 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 19932	. . . . . . . . . . 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 21031	. . . . . . . . . . . . . 14 |- ( topGen ` ran (,) ) e. Top
245		ovex 6309	. . . . . . . . . . . . . 14 |- ( 0 [,] ( 1 / 2 ) ) e. _V
246		restabs 19460	. . . . . . . . . . . . . 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 1324	. . . . . . . . . . . . 13 |- ( ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) = ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) )
248	247	eqcomi 2480	. . . . . . . . . . . 12 |- ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) = ( ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 2 ) ) ) ↾t ( 0 [,] ( 1 / 4 ) ) )
249		resttopon 19456	. . . . . . . . . . . . . 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 21195	. . . . . . . . . . . . 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 19940	. . . . . . . . . . 11 |- ( ph -> ( x e. ( 0 [,] ( 1 / 4 ) ) |-> ( 2 x. x ) ) e. ( ( ( topGen ` ran (,) ) ↾t ( 0 [,] ( 1 / 4 ) ) ) Cn II ) )
256		oveq2 6292	. . . . . . . . . . 11 |- ( x = y -> ( 2 x. x ) = ( 2 x. y ) )
257	242, 192, 243, 242, 255, 256	cnmpt21 19935	. . . . . . . . . 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 11606	. . . . . . . . . . . . . 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 19456	. . . . . . . . . . . . 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 19932	. . . . . . . . . . 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 2467	. . . . . . . . . . . 12 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
265	259	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( ( 1 / 4 ) [,] ( 1 / 2 ) ) C_ RR )
266		unitssre 11667	. . . . . . . . . . . . 13 |- ( 0 [,] 1 ) C_ RR
267	266	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( 0 [,] 1 ) C_ RR )
268	150, 87	sseldi 3502	. . . . . . . . . . . . 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 21053	. . . . . . . . . . . . . 14 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
271	270	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> ( TopOpen ` ℂfld ) e. (TopOn ` CC ) )
272	271	cnmptid 19925	. . . . . . . . . . . . 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 9622	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 / 4 ) e. CC )
275	271, 271, 274	cnmptc 19926	. . . . . . . . . . . . 13 |- ( ph -> ( x e. CC |-> ( 1 / 4 ) ) e. ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) ) )
276	264	addcn 21132	. . . . . . . . . . . . . 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 19930	. . . . . . . . . . . 12 |- ( ph -> ( x e. CC |-> ( x + ( 1 / 4 ) ) ) e. ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) ) )
279	264, 219, 200, 265, 267, 269, 278	cnmptre 21190	. . . . . . . . . . 11 |- ( ph -> ( x e. ( ( 1 / 4 ) [,] ( 1 / 2 ) ) |-> ( x + ( 1 / 4 ) ) ) e. ( ( ( topGen ` ran (,) ) ↾t ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ) Cn II ) )
280		oveq1 6291	. . . . . . . . . . 11 |- ( x = y -> ( x + ( 1 / 4 ) ) = ( y + ( 1 / 4 ) ) )
281	262, 192, 263, 262, 279, 280	cnmpt21 19935	. . . . . . . . . 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 21191	. . . . . . . . 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 11606	. . . . . . . . . . . . 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 19456	. . . . . . . . . . . 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 19932	. . . . . . . . . 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 3502	. . . . . . . . . . . 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 21140	. . . . . . . . . . . . . 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 19926	. . . . . . . . . . . 12 |- ( ph -> ( x e. CC |-> ( 1 / 2 ) ) e. ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) ) )
297	271, 294, 296, 277	cnmpt12f 19930	. . . . . . . . . . 11 |- ( ph -> ( x e. CC |-> ( ( x / 2 ) + ( 1 / 2 ) ) ) e. ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) ) )
298	264, 199, 200, 289, 267, 291, 297	cnmptre 21190	. . . . . . . . . 10 |- ( ph -> ( x e. ( ( 1 / 2 ) [,] 1 ) |-> ( ( x / 2 ) + ( 1 / 2 ) ) ) e. ( ( ( topGen ` ran (,) ) ↾t ( ( 1 / 2 ) [,] 1 ) ) Cn II ) )
299		oveq1 6291	. . . . . . . . . . 11 |- ( x = y -> ( x / 2 ) = ( y / 2 ) )
300	299	oveq1d 6299	. . . . . . . . . 10 |- ( x = y -> ( ( x / 2 ) + ( 1 / 2 ) ) = ( ( y / 2 ) + ( 1 / 2 ) ) )
301	287, 192, 288, 287, 298, 300	cnmpt21 19935	. . . . . . . . 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 21191	. . . . . . . 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 4450	. . . . . . . . . . . 12 |- ( x = y -> ( x <_ ( 1 / 2 ) <-> y <_ ( 1 / 2 ) ) )
304		breq1 4450	. . . . . . . . . . . . 13 |- ( x = y -> ( x <_ ( 1 / 4 ) <-> y <_ ( 1 / 4 ) ) )
305	304, 256, 280	ifbieq12d 3966	. . . . . . . . . . . 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 3966	. . . . . . . . . . 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 1744	. . . . . . . . . 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 2475	. . . . . . . 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 19931	. . . . . . 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 2559	. . . . . 6 |- ( ph -> P e. ( II Cn II ) )
312		iiuni 21148	. . . . . . 7 |- ( 0 [,] 1 ) = U. II
313	312, 312	cnf 19541	. . . . . 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 6042	. . . . 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 21280	. . . . . 6 |- ( ph -> ( F ( *p ` J ) ( G ( *p ` J ) H ) ) e. ( II Cn J ) )
319		eqid 2467	. . . . . . 7 |- U. J = U. J
320	312, 319	cnf 19541	. . . . . 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 5920	. . . 4 |- ( ph -> ( F ( *p ` J ) ( G ( *p ` J ) H ) ) = ( y e. ( 0 [,] 1 ) |-> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) ` y ) ) )
323		fveq2 5866	. . . 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 6055	. . 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 21280	. . . 4 |- ( ph -> ( F ( *p ` J ) G ) e. ( II Cn J ) )
326	325, 43	pcoval 21274	. . 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 2519	. 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 4484	. . . . . . 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 4484	. . . . . . 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 6292	. . . . . . 7 |- ( x = 0 -> ( 2 x. x ) = ( 2 x. 0 ) )
334		2t0e0 10691	. . . . . . 7 |- ( 2 x. 0 ) = 0
335	333, 334	syl6eq 2524	. . . . . 6 |- ( x = 0 -> ( 2 x. x ) = 0 )
336	330, 332, 335	3eqtrd 2512	. . . . 5 |- ( x = 0 -> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) = 0 )
337		c0ex 9590	. . . . 5 |- 0 e. _V
338	336, 190, 337	fvmpt 5950	. . . 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 9705	. . . . . . . . 9 |- ( ( 1 / 2 ) < 1 <-> -. 1 <_ ( 1 / 2 ) )
342	144, 341	mpbi 208	. . . . . . . 8 |- -. 1 <_ ( 1 / 2 )
343		breq1 4450	. . . . . . . 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 6291	. . . . . . . 8 |- ( x = 1 -> ( x / 2 ) = ( 1 / 2 ) )
347	346	oveq1d 6299	. . . . . . 7 |- ( x = 1 -> ( ( x / 2 ) + ( 1 / 2 ) ) = ( ( 1 / 2 ) + ( 1 / 2 ) ) )
348	347, 84	syl6eq 2524	. . . . . 6 |- ( x = 1 -> ( ( x / 2 ) + ( 1 / 2 ) ) = 1 )
349	345, 348	eqtrd 2508	. . . . 5 |- ( x = 1 -> if ( x <_ ( 1 / 2 ) , if ( x <_ ( 1 / 4 ) , ( 2 x. x ) , ( x + ( 1 / 4 ) ) ) , ( ( x / 2 ) + ( 1 / 2 ) ) ) = 1 )
350		1ex 9591	. . . . 5 |- 1 e. _V
351	349, 190, 350	fvmpt 5950	. . . 4 |- ( 1 e. ( 0 [,] 1 ) -> ( P ` 1 ) = 1 )
352	340, 351	syl 16	. . 3 |- ( ph -> ( P ` 1 ) = 1 )
353	318, 311, 339, 352	reparpht 21261	. 2 |- ( ph -> ( ( F ( *p ` J ) ( G ( *p ` J ) H ) ) o. P ) ( ~=ph ` J ) ( F ( *p ` J ) ( G ( *p ` J ) H ) ) )
354	327, 353	eqbrtrd 4467	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 1379   e. wcel 1767   =/= wne 2662   A.wral 2814   _Vcvv 3113   C_ wss 3476   ifcif 3939   U.cuni 4245   class class class wbr 4447   |-> cmpt 4505   ran crn 5000   o. ccom 5003   -->wf 5584   ` cfv 5588  (class class class)co 6284   CCcc 9490   RRcr 9491   0cc0 9492   1c1 9493   + caddc 9495   x. cmul 9497   RR*cxr 9627   < clt 9628   <_ cle 9629   - cmin 9805   / cdiv 10206   NNcn 10536   2c2 10585   4c4 10587   (,)cioo 11529   [,]cicc 11532   ↾_t crest 14676   TopOpenctopn 14677   topGenctg 14693  ℂ_fldccnfld 18219   Topctop 19189  TopOnctopon 19190   Cn ccn 19519   tX ctx 19824   IIcii 21142   ~=ph cphtpc 21232   *pcpco 21263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-inf2 8058  ax-cnex 9548  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568  ax-pre-mulgt0 9569  ax-pre-sup 9570  ax-addf 9571  ax-mulf 9572

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-iin 4328  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-isom 5597  df-riota 6245  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-of 6524  df-om 6685  df-1st 6784  df-2nd 6785  df-supp 6902  df-recs 7042  df-rdg 7076  df-1o 7130  df-2o 7131  df-oadd 7134  df-er 7311  df-map 7422  df-ixp 7470  df-en 7517  df-dom 7518  df-sdom 7519  df-fin 7520  df-fsupp 7830  df-fi 7871  df-sup 7901  df-oi 7935  df-card 8320  df-cda 8548  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-sub 9807  df-neg 9808  df-div 10207  df-nn 10537  df-2 10594  df-3 10595  df-4 10596  df-5 10597  df-6 10598  df-7 10599  df-8 10600  df-9 10601  df-10 10602  df-n0 10796  df-z 10865  df-dec 10977  df-uz 11083  df-q 11183  df-rp 11221  df-xneg 11318  df-xadd 11319  df-xmul 11320  df-ioo 11533  df-icc 11536  df-fz 11673  df-fzo 11793  df-seq 12076  df-exp 12135  df-hash 12374  df-cj 12895  df-re 12896  df-im 12897  df-sqrt 13031  df-abs 13032  df-struct 14492  df-ndx 14493  df-slot 14494  df-base 14495  df-sets 14496  df-ress 14497  df-plusg 14568  df-mulr 14569  df-starv 14570  df-sca 14571  df-vsca 14572  df-ip 14573  df-tset 14574  df-ple 14575  df-ds 14577  df-unif 14578  df-hom 14579  df-cco 14580  df-rest 14678  df-topn 14679  df-0g 14697  df-gsum 14698  df-topgen 14699  df-pt 14700  df-prds 14703  df-xrs 14757  df-qtop 14762  df-imas 14763  df-xps 14765  df-mre 14841  df-mrc 14842  df-acs 14844  df-mnd 15732  df-submnd 15787  df-mulg 15870  df-cntz 16160  df-cmn 16606  df-psmet 18210  df-xmet 18211  df-met 18212  df-bl 18213  df-mopn 18214  df-cnfld 18220  df-top 19194  df-bases 19196  df-topon 19197  df-topsp 19198  df-cld 19314  df-cn 19522  df-cnp 19523  df-tx 19826  df-hmeo 20019  df-xms 20586  df-ms 20587  df-tms 20588  df-ii 21144  df-htpy 21233  df-phtpy 21234  df-phtpc 21255  df-pco 21268

This theorem is referenced by:  pcophtb  21292  pi1grplem  21312  pi1xfr  21318  pi1xfrcnvlem  21319