Theorem pcorev 16087

Description: Concatenation with the reverse path.

Hypotheses

Ref	Expression
pcorev.1	|- G = {<.x, y>. | (x e. (0[,]1) /\ y = (F` (1 - x)))}
pcorev.2	|- P = ((0[,]1) X. {Y})

Assertion

Ref	Expression
pcorev	|- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> (G(*p` J)F)(~=ph` J)P)

Distinct variable groups:   x,P,y   x,J,y   x,F,y   x,Y,y

Proof of Theorem pcorev

Step	Hyp	Ref	Expression
1		simp1 876	. . . . 5 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> J e. Top)
2		iitop 15867	. . . . . . . . . 10 |- II e. Top
3		iiuni 15868	. . . . . . . . . . 11 |- (0[,]1) = U.II
4		eqid 1884	. . . . . . . . . . 11 |- U.J = U.J
5	3, 4	cnf 9038	. . . . . . . . . 10 |- ((II e. Top /\ J e. Top /\ F e. (II Cn J)) -> F:(0[,]1)-->U.J)
6	2, 5	mp3an1 1178	. . . . . . . . 9 |- ((J e. Top /\ F e. (II Cn J)) -> F:(0[,]1)-->U.J)
7		ffn 4562	. . . . . . . . 9 |- (F:(0[,]1)-->U.J -> F Fn (0[,]1))
8		iirev 15871	. . . . . . . . . 10 |- (x e. (0[,]1) -> (1 - x) e. (0[,]1))
9		eqid 1884	. . . . . . . . . 10 |- {<.x, y>. | (x e. (0[,]1) /\ y = (1 - x))} = {<.x, y>. | (x e. (0[,]1) /\ y = (1 - x))}
10		eqid 1884	. . . . . . . . . 10 |- {<.x, y>. | (x e. (0[,]1) /\ y = (F` (1 - x)))} = {<.x, y>. | (x e. (0[,]1) /\ y = (F` (1 - x)))}
11	8, 9, 10	fnopabco 15711	. . . . . . . . 9 |- (F Fn (0[,]1) -> {<.x, y>. | (x e. (0[,]1) /\ y = (F` (1 - x)))} = (F o. {<.x, y>. | (x e. (0[,]1) /\ y = (1 - x))}))
12	6, 7, 11	3syl 24	. . . . . . . 8 |- ((J e. Top /\ F e. (II Cn J)) -> {<.x, y>. | (x e. (0[,]1) /\ y = (F` (1 - x)))} = (F o. {<.x, y>. | (x e. (0[,]1) /\ y = (1 - x))}))
13	2	a1i 8	. . . . . . . . 9 |- ((J e. Top /\ F e. (II Cn J)) -> II e. Top)
14		simpl 346	. . . . . . . . 9 |- ((J e. Top /\ F e. (II Cn J)) -> J e. Top)
15		simpr 350	. . . . . . . . . 10 |- ((J e. Top /\ F e. (II Cn J)) -> F e. (II Cn J))
16		0re 6603	. . . . . . . . . . . . 13 |- 0 e. RR
17		1re 6598	. . . . . . . . . . . . 13 |- 1 e. RR
18		iccssre 7565	. . . . . . . . . . . . 13 |- ((0 e. RR /\ 1 e. RR) -> (0[,]1) C_ RR)
19	16, 17, 18	mp2an 761	. . . . . . . . . . . 12 |- (0[,]1) C_ RR
20		axresscn 6420	. . . . . . . . . . . 12 |- RR C_ CC
21	19, 20	sstri 2626	. . . . . . . . . . 11 |- (0[,]1) C_ CC
22		eqid 1884	. . . . . . . . . . 11 |- {<.x, y>. | (x e. CC /\ y = (1 - x))} = {<.x, y>. | (x e. CC /\ y = (1 - x))}
23		ax1cn 6422	. . . . . . . . . . . 12 |- 1 e. CC
24	22	sub2cncf 15886	. . . . . . . . . . . 12 |- (1 e. CC -> {<.x, y>. | (x e. CC /\ y = (1 - x))} e. (CC-cn->CC))
25	23, 24	ax-mp 7	. . . . . . . . . . 11 |- {<.x, y>. | (x e. CC /\ y = (1 - x))} e. (CC-cn->CC)
26		df-ii 15866	. . . . . . . . . . 11 |- II = (Open` ((abs o. - ) |` ((0[,]1) X. (0[,]1))))
27	21, 21, 22, 9, 8, 25, 26, 26	cncfres 15895	. . . . . . . . . 10 |- {<.x, y>. | (x e. (0[,]1) /\ y = (1 - x))} e. (II Cn II)
28	15, 27	jctil 316	. . . . . . . . 9 |- ((J e. Top /\ F e. (II Cn J)) -> ({<.x, y>. | (x e. (0[,]1) /\ y = (1 - x))} e. (II Cn II) /\ F e. (II Cn J)))
29		cnco 9045	. . . . . . . . 9 |- (((II e. Top /\ II e. Top /\ J e. Top) /\ ({<.x, y>. | (x e. (0[,]1) /\ y = (1 - x))} e. (II Cn II) /\ F e. (II Cn J))) -> (F o. {<.x, y>. | (x e. (0[,]1) /\ y = (1 - x))}) e. (II Cn J))
30	13, 13, 14, 28, 29	syl31anc 1103	. . . . . . . 8 |- ((J e. Top /\ F e. (II Cn J)) -> (F o. {<.x, y>. | (x e. (0[,]1) /\ y = (1 - x))}) e. (II Cn J))
31	12, 30	eqeltrd 1971	. . . . . . 7 |- ((J e. Top /\ F e. (II Cn J)) -> {<.x, y>. | (x e. (0[,]1) /\ y = (F` (1 - x)))} e. (II Cn J))
32	31	3adant3 896	. . . . . 6 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> {<.x, y>. | (x e. (0[,]1) /\ y = (F` (1 - x)))} e. (II Cn J))
33		pcorev.1	. . . . . 6 |- G = {<.x, y>. | (x e. (0[,]1) /\ y = (F` (1 - x)))}
34	32, 33	syl5eqel 1975	. . . . 5 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> G e. (II Cn J))
35		simp2 877	. . . . 5 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> F e. (II Cn J))
36		lt01 6871	. . . . . . . . 9 |- 0 < 1
37	16, 17, 36	ltleii 6756	. . . . . . . 8 |- 0 <_ 1
38		ubicc2 7574	. . . . . . . 8 |- ((0 e. RR /\ 1 e. RR /\ 0 <_ 1) -> 1 e. (0[,]1))
39	16, 17, 37, 38	mp3an 1191	. . . . . . 7 |- 1 e. (0[,]1)
40		opreq2 4890	. . . . . . . . . 10 |- (x = 1 -> (1 - x) = (1 - 1))
41	40	fveq2d 4685	. . . . . . . . 9 |- (x = 1 -> (F` (1 - x)) = (F` (1 - 1)))
42	23	subidi 6551	. . . . . . . . . 10 |- (1 - 1) = 0
43	42	fveq2i 4684	. . . . . . . . 9 |- (F` (1 - 1)) = (F` 0)
44	41, 43	syl6eq 1944	. . . . . . . 8 |- (x = 1 -> (F` (1 - x)) = (F` 0))
45		fvex 4689	. . . . . . . 8 |- (F` 0) e. _V
46	44, 33, 45	fvopab4 4743	. . . . . . 7 |- (1 e. (0[,]1) -> (G` 1) = (F` 0))
47	39, 46	ax-mp 7	. . . . . 6 |- (G` 1) = (F` 0)
48	47	a1i 8	. . . . 5 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> (G` 1) = (F` 0))
49		pcocn 16076	. . . . 5 |- ((J e. Top /\ (G e. (II Cn J) /\ F e. (II Cn J) /\ (G` 1) = (F` 0))) -> (G(*p` J)F) e. (II Cn J))
50	1, 34, 35, 48, 49	syl13anc 1102	. . . 4 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> (G(*p` J)F) e. (II Cn J))
51		eleq1 1957	. . . . . . . . . 10 |- ((F` 1) = Y -> ((F` 1) e. U.J <-> Y e. U.J))
52		ffvelrn 4787	. . . . . . . . . . 11 |- ((F:(0[,]1)-->U.J /\ 1 e. (0[,]1)) -> (F` 1) e. U.J)
53	39, 52	mpan2 760	. . . . . . . . . 10 |- (F:(0[,]1)-->U.J -> (F` 1) e. U.J)
54	51, 53	syl5bi 225	. . . . . . . . 9 |- ((F` 1) = Y -> (F:(0[,]1)-->U.J -> Y e. U.J))
55	6, 54	mpan9 521	. . . . . . . 8 |- (((J e. Top /\ F e. (II Cn J)) /\ (F` 1) = Y) -> Y e. U.J)
56	55	anasss 488	. . . . . . 7 |- ((J e. Top /\ (F e. (II Cn J) /\ (F` 1) = Y)) -> Y e. U.J)
57	3, 4	cnconst 9057	. . . . . . . . 9 |- (((II e. Top /\ J e. Top) /\ (Y e. U.J /\ ((0[,]1) X. {Y}):(0[,]1)-->{Y})) -> ((0[,]1) X. {Y}) e. (II Cn J))
58	2, 57	mpanl1 770	. . . . . . . 8 |- ((J e. Top /\ (Y e. U.J /\ ((0[,]1) X. {Y}):(0[,]1)-->{Y})) -> ((0[,]1) X. {Y}) e. (II Cn J))
59		fconstg 4604	. . . . . . . . 9 |- (Y e. U.J -> ((0[,]1) X. {Y}):(0[,]1)-->{Y})
60	59	ancli 320	. . . . . . . 8 |- (Y e. U.J -> (Y e. U.J /\ ((0[,]1) X. {Y}):(0[,]1)-->{Y}))
61	58, 60	sylan2 500	. . . . . . 7 |- ((J e. Top /\ Y e. U.J) -> ((0[,]1) X. {Y}) e. (II Cn J))
62	56, 61	syldan 516	. . . . . 6 |- ((J e. Top /\ (F e. (II Cn J) /\ (F` 1) = Y)) -> ((0[,]1) X. {Y}) e. (II Cn J))
63	62	3impb 1063	. . . . 5 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> ((0[,]1) X. {Y}) e. (II Cn J))
64		pcorev.2	. . . . 5 |- P = ((0[,]1) X. {Y})
65	63, 64	syl5eqel 1975	. . . 4 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> P e. (II Cn J))
66	50, 65	jca 310	. . 3 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> ((G(*p` J)F) e. (II Cn J) /\ P e. (II Cn J)))
67		lbicc2 7573	. . . . . . . . 9 |- ((0 e. RR /\ 1 e. RR /\ 0 <_ 1) -> 0 e. (0[,]1))
68	16, 17, 37, 67	mp3an 1191	. . . . . . . 8 |- 0 e. (0[,]1)
69		opreq2 4890	. . . . . . . . . . 11 |- (x = 0 -> (1 - x) = (1 - 0))
70	69	fveq2d 4685	. . . . . . . . . 10 |- (x = 0 -> (F` (1 - x)) = (F` (1 - 0)))
71	23	subid1i 6552	. . . . . . . . . . 11 |- (1 - 0) = 1
72	71	fveq2i 4684	. . . . . . . . . 10 |- (F` (1 - 0)) = (F` 1)
73	70, 72	syl6eq 1944	. . . . . . . . 9 |- (x = 0 -> (F` (1 - x)) = (F` 1))
74		fvex 4689	. . . . . . . . 9 |- (F` 1) e. _V
75	73, 33, 74	fvopab4 4743	. . . . . . . 8 |- (0 e. (0[,]1) -> (G` 0) = (F` 1))
76	68, 75	ax-mp 7	. . . . . . 7 |- (G` 0) = (F` 1)
77		eqeq2 1893	. . . . . . 7 |- ((F` 1) = Y -> ((G` 0) = (F` 1) <-> (G` 0) = Y))
78	76, 77	mpbii 210	. . . . . 6 |- ((F` 1) = Y -> (G` 0) = Y)
79	78	3ad2ant3 899	. . . . 5 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> (G` 0) = Y)
80		pco0 16077	. . . . . 6 |- ((J e. Top /\ (G e. (II Cn J) /\ F e. (II Cn J) /\ (G` 1) = (F` 0))) -> ((G(*p` J)F)` 0) = (G` 0))
81	1, 34, 35, 48, 80	syl13anc 1102	. . . . 5 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> ((G(*p` J)F)` 0) = (G` 0))
82	55	3impa 1062	. . . . . 6 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> Y e. U.J)
83		fvconst2g 4820	. . . . . . . 8 |- ((Y e. U.J /\ 0 e. (0[,]1)) -> (((0[,]1) X. {Y})` 0) = Y)
84	68, 83	mpan2 760	. . . . . . 7 |- (Y e. U.J -> (((0[,]1) X. {Y})` 0) = Y)
85	64	fveq1i 4682	. . . . . . 7 |- (P` 0) = (((0[,]1) X. {Y})` 0)
86	84, 85	syl5eq 1940	. . . . . 6 |- (Y e. U.J -> (P` 0) = Y)
87	82, 86	syl 12	. . . . 5 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> (P` 0) = Y)
88	79, 81, 87	3eqtr4d 1937	. . . 4 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> ((G(*p` J)F)` 0) = (P` 0))
89		simp3 878	. . . . 5 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> (F` 1) = Y)
90		pco1 16078	. . . . . 6 |- ((J e. Top /\ (G e. (II Cn J) /\ F e. (II Cn J) /\ (G` 1) = (F` 0))) -> ((G(*p` J)F)` 1) = (F` 1))
91	1, 34, 35, 48, 90	syl13anc 1102	. . . . 5 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> ((G(*p` J)F)` 1) = (F` 1))
92		fvconst2g 4820	. . . . . . . 8 |- ((Y e. U.J /\ 1 e. (0[,]1)) -> (((0[,]1) X. {Y})` 1) = Y)
93	39, 92	mpan2 760	. . . . . . 7 |- (Y e. U.J -> (((0[,]1) X. {Y})` 1) = Y)
94	64	fveq1i 4682	. . . . . . 7 |- (P` 1) = (((0[,]1) X. {Y})` 1)
95	93, 94	syl5eq 1940	. . . . . 6 |- (Y e. U.J -> (P` 1) = Y)
96	82, 95	syl 12	. . . . 5 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> (P` 1) = Y)
97	89, 91, 96	3eqtr4d 1937	. . . 4 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> ((G(*p` J)F)` 1) = (P` 1))
98	88, 97	jca 310	. . 3 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> (((G(*p` J)F)` 0) = (P` 0) /\ ((G(*p` J)F)` 1) = (P` 1)))
99		isphtpy 16048	. . . . . 6 |- (((J e. Top /\ (G(*p` J)F) e. (II Cn J) /\ P e. (II Cn J)) /\ (((G(*p` J)F)` 0) = (P` 0) /\ ((G(*p` J)F)` 1) = (P` 1))) -> ({<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))} e. ((G(*p` J)F)(PHtpy` J)P) <-> ({<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))} e. ((II X.t II) Cn J) /\ A.v e. (0[,]1)(((v{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}0) = ((G(*p` J)F)` v) /\ (v{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}1) = (P` v)) /\ ((0{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}v) = ((G(*p` J)F)` 0) /\ (1{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}v) = ((G(*p` J)F)` 1))))))
100	1, 50, 65, 88, 97, 99	syl32anc 1108	. . . . 5 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> ({<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))} e. ((G(*p` J)F)(PHtpy` J)P) <-> ({<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))} e. ((II X.t II) Cn J) /\ A.v e. (0[,]1)(((v{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}0) = ((G(*p` J)F)` v) /\ (v{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}1) = (P` v)) /\ ((0{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}v) = ((G(*p` J)F)` 0) /\ (1{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}v) = ((G(*p` J)F)` 1))))))
101		eqid 1884	. . . . . . 7 |- {<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))} = {<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}
102	101	pcorevlem 16086	. . . . . 6 |- ((J e. Top /\ F e. (II Cn J)) -> {<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))} e. ((II X.t II) Cn J))
103	102	3adant3 896	. . . . 5 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> {<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))} e. ((II X.t II) Cn J))
104	21	sseli 2617	. . . . . . . . . . . . . 14 |- (v e. (0[,]1) -> v e. CC)
105		2cn 7164	. . . . . . . . . . . . . . 15 |- 2 e. CC
106		mulcl 6456	. . . . . . . . . . . . . . 15 |- ((2 e. CC /\ v e. CC) -> (2 x. v) e. CC)
107	105, 106	mpan 759	. . . . . . . . . . . . . 14 |- (v e. CC -> (2 x. v) e. CC)
108		mulid2 6578	. . . . . . . . . . . . . . . . 17 |- ((2 x. v) e. CC -> (1 x. (2 x. v)) = (2 x. v))
109	71	opreq1i 4892	. . . . . . . . . . . . . . . . 17 |- ((1 - 0) x. (2 x. v)) = (1 x. (2 x. v))
110	108, 109	syl5eq 1940	. . . . . . . . . . . . . . . 16 |- ((2 x. v) e. CC -> ((1 - 0) x. (2 x. v)) = (2 x. v))
111	110	opreq2d 4898	. . . . . . . . . . . . . . 15 |- ((2 x. v) e. CC -> (1 - ((1 - 0) x. (2 x. v))) = (1 - (2 x. v)))
112	111	fveq2d 4685	. . . . . . . . . . . . . 14 |- ((2 x. v) e. CC -> (F` (1 - ((1 - 0) x. (2 x. v)))) = (F` (1 - (2 x. v))))
113	104, 107, 112	3syl 24	. . . . . . . . . . . . 13 |- (v e. (0[,]1) -> (F` (1 - ((1 - 0) x. (2 x. v)))) = (F` (1 - (2 x. v))))
114	113	adantr 425	. . . . . . . . . . . 12 |- ((v e. (0[,]1) /\ v <_ (1 / 2)) -> (F` (1 - ((1 - 0) x. (2 x. v)))) = (F` (1 - (2 x. v))))
115	19	sseli 2617	. . . . . . . . . . . . . . . 16 |- (v e. (0[,]1) -> v e. RR)
116	115	adantr 425	. . . . . . . . . . . . . . 15 |- ((v e. (0[,]1) /\ v <_ (1 / 2)) -> v e. RR)
117		elicc2 7560	. . . . . . . . . . . . . . . . . 18 |- ((0 e. RR /\ 1 e. RR) -> (v e. (0[,]1) <-> (v e. RR /\ 0 <_ v /\ v <_ 1)))
118	16, 17, 117	mp2an 761	. . . . . . . . . . . . . . . . 17 |- (v e. (0[,]1) <-> (v e. RR /\ 0 <_ v /\ v <_ 1))
119	118	simp2bi 892	. . . . . . . . . . . . . . . 16 |- (v e. (0[,]1) -> 0 <_ v)
120	119	adantr 425	. . . . . . . . . . . . . . 15 |- ((v e. (0[,]1) /\ v <_ (1 / 2)) -> 0 <_ v)
121		simpr 350	. . . . . . . . . . . . . . 15 |- ((v e. (0[,]1) /\ v <_ (1 / 2)) -> v <_ (1 / 2))
122	116, 120, 121	3jca 1050	. . . . . . . . . . . . . 14 |- ((v e. (0[,]1) /\ v <_ (1 / 2)) -> (v e. RR /\ 0 <_ v /\ v <_ (1 / 2)))
123		2re 7163	. . . . . . . . . . . . . . . 16 |- 2 e. RR
124		2ne0 7174	. . . . . . . . . . . . . . . 16 |- 2 =/= 0
125	123, 124	rereccli 6979	. . . . . . . . . . . . . . 15 |- (1 / 2) e. RR
126		elicc2 7560	. . . . . . . . . . . . . . 15 |- ((0 e. RR /\ (1 / 2) e. RR) -> (v e. (0[,](1 / 2)) <-> (v e. RR /\ 0 <_ v /\ v <_ (1 / 2))))
127	16, 125, 126	mp2an 761	. . . . . . . . . . . . . 14 |- (v e. (0[,](1 / 2)) <-> (v e. RR /\ 0 <_ v /\ v <_ (1 / 2)))
128	122, 127	sylibr 217	. . . . . . . . . . . . 13 |- ((v e. (0[,]1) /\ v <_ (1 / 2)) -> v e. (0[,](1 / 2)))
129		iihalf1 15872	. . . . . . . . . . . . 13 |- (v e. (0[,](1 / 2)) -> (2 x. v) e. (0[,]1))
130		opreq2 4890	. . . . . . . . . . . . . . 15 |- (x = (2 x. v) -> (1 - x) = (1 - (2 x. v)))
131	130	fveq2d 4685	. . . . . . . . . . . . . 14 |- (x = (2 x. v) -> (F` (1 - x)) = (F` (1 - (2 x. v))))
132		fvex 4689	. . . . . . . . . . . . . 14 |- (F` (1 - (2 x. v))) e. _V
133	131, 33, 132	fvopab4 4743	. . . . . . . . . . . . 13 |- ((2 x. v) e. (0[,]1) -> (G` (2 x. v)) = (F` (1 - (2 x. v))))
134	128, 129, 133	3syl 24	. . . . . . . . . . . 12 |- ((v e. (0[,]1) /\ v <_ (1 / 2)) -> (G` (2 x. v)) = (F` (1 - (2 x. v))))
135	114, 134	eqtr4d 1928	. . . . . . . . . . 11 |- ((v e. (0[,]1) /\ v <_ (1 / 2)) -> (F` (1 - ((1 - 0) x. (2 x. v)))) = (G` (2 x. v)))
136	135	ifeq1da 15693	. . . . . . . . . 10 |- (v e. (0[,]1) -> if(v <_ (1 / 2), (F` (1 - ((1 - 0) x. (2 x. v)))), (F` (0 + ((1 - 0) x. ((2 x. v) - 1))))) = if(v <_ (1 / 2), (G` (2 x. v)), (F` (0 + ((1 - 0) x. ((2 x. v) - 1))))))
137	106, 105, 104	sylancr 526	. . . . . . . . . . . . 13 |- (v e. (0[,]1) -> (2 x. v) e. CC)
138		subcl 6524	. . . . . . . . . . . . . 14 |- (((2 x. v) e. CC /\ 1 e. CC) -> ((2 x. v) - 1) e. CC)
139	23, 138	mpan2 760	. . . . . . . . . . . . 13 |- ((2 x. v) e. CC -> ((2 x. v) - 1) e. CC)
140		mulid2 6578	. . . . . . . . . . . . . . . 16 |- (((2 x. v) - 1) e. CC -> (1 x. ((2 x. v) - 1)) = ((2 x. v) - 1))
141	71	opreq1i 4892	. . . . . . . . . . . . . . . 16 |- ((1 - 0) x. ((2 x. v) - 1)) = (1 x. ((2 x. v) - 1))
142	140, 141	syl5eq 1940	. . . . . . . . . . . . . . 15 |- (((2 x. v) - 1) e. CC -> ((1 - 0) x. ((2 x. v) - 1)) = ((2 x. v) - 1))
143	142	opreq2d 4898	. . . . . . . . . . . . . 14 |- (((2 x. v) - 1) e. CC -> (0 + ((1 - 0) x. ((2 x. v) - 1))) = (0 + ((2 x. v) - 1)))
144		addid2 6482	. . . . . . . . . . . . . 14 |- (((2 x. v) - 1) e. CC -> (0 + ((2 x. v) - 1)) = ((2 x. v) - 1))
145	143, 144	eqtrd 1925	. . . . . . . . . . . . 13 |- (((2 x. v) - 1) e. CC -> (0 + ((1 - 0) x. ((2 x. v) - 1))) = ((2 x. v) - 1))
146	137, 139, 145	3syl 24	. . . . . . . . . . . 12 |- (v e. (0[,]1) -> (0 + ((1 - 0) x. ((2 x. v) - 1))) = ((2 x. v) - 1))
147	146	fveq2d 4685	. . . . . . . . . . 11 |- (v e. (0[,]1) -> (F` (0 + ((1 - 0) x. ((2 x. v) - 1)))) = (F` ((2 x. v) - 1)))
148	147	ifeq2d 2994	. . . . . . . . . 10 |- (v e. (0[,]1) -> if(v <_ (1 / 2), (G` (2 x. v)), (F` (0 + ((1 - 0) x. ((2 x. v) - 1))))) = if(v <_ (1 / 2), (G` (2 x. v)), (F` ((2 x. v) - 1))))
149	136, 148	eqtrd 1925	. . . . . . . . 9 |- (v e. (0[,]1) -> if(v <_ (1 / 2), (F` (1 - ((1 - 0) x. (2 x. v)))), (F` (0 + ((1 - 0) x. ((2 x. v) - 1))))) = if(v <_ (1 / 2), (G` (2 x. v)), (F` ((2 x. v) - 1))))
150	149	adantl 424	. . . . . . . 8 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> if(v <_ (1 / 2), (F` (1 - ((1 - 0) x. (2 x. v)))), (F` (0 + ((1 - 0) x. ((2 x. v) - 1))))) = if(v <_ (1 / 2), (G` (2 x. v)), (F` ((2 x. v) - 1))))
151		fvex 4689	. . . . . . . . . . . 12 |- (F` (1 - ((1 - 0) x. (2 x. v)))) e. _V
152		fvex 4689	. . . . . . . . . . . 12 |- (F` (0 + ((1 - 0) x. ((2 x. v) - 1)))) e. _V
153	151, 152	ifex 3031	. . . . . . . . . . 11 |- if(v <_ (1 / 2), (F` (1 - ((1 - 0) x. (2 x. v)))), (F` (0 + ((1 - 0) x. ((2 x. v) - 1))))) e. _V
154		breq1 3341	. . . . . . . . . . . 12 |- (s = v -> (s <_ (1 / 2) <-> v <_ (1 / 2)))
155		opreq2 4890	. . . . . . . . . . . . . . 15 |- (s = v -> (2 x. s) = (2 x. v))
156	155	opreq2d 4898	. . . . . . . . . . . . . 14 |- (s = v -> ((1 - t) x. (2 x. s)) = ((1 - t) x. (2 x. v)))
157	156	opreq2d 4898	. . . . . . . . . . . . 13 |- (s = v -> (1 - ((1 - t) x. (2 x. s))) = (1 - ((1 - t) x. (2 x. v))))
158	157	fveq2d 4685	. . . . . . . . . . . 12 |- (s = v -> (F` (1 - ((1 - t) x. (2 x. s)))) = (F` (1 - ((1 - t) x. (2 x. v)))))
159	155	opreq1d 4897	. . . . . . . . . . . . . . 15 |- (s = v -> ((2 x. s) - 1) = ((2 x. v) - 1))
160	159	opreq2d 4898	. . . . . . . . . . . . . 14 |- (s = v -> ((1 - t) x. ((2 x. s) - 1)) = ((1 - t) x. ((2 x. v) - 1)))
161	160	opreq2d 4898	. . . . . . . . . . . . 13 |- (s = v -> (t + ((1 - t) x. ((2 x. s) - 1))) = (t + ((1 - t) x. ((2 x. v) - 1))))
162	161	fveq2d 4685	. . . . . . . . . . . 12 |- (s = v -> (F` (t + ((1 - t) x. ((2 x. s) - 1)))) = (F` (t + ((1 - t) x. ((2 x. v) - 1)))))
163	154, 158, 162	ifbieq12d 2998	. . . . . . . . . . 11 |- (s = v -> if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))) = if(v <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. v)))), (F` (t + ((1 - t) x. ((2 x. v) - 1))))))
164		biidd 188	. . . . . . . . . . . 12 |- (t = 0 -> (v <_ (1 / 2) <-> v <_ (1 / 2)))
165		opreq2 4890	. . . . . . . . . . . . . . 15 |- (t = 0 -> (1 - t) = (1 - 0))
166	165	opreq1d 4897	. . . . . . . . . . . . . 14 |- (t = 0 -> ((1 - t) x. (2 x. v)) = ((1 - 0) x. (2 x. v)))
167	166	opreq2d 4898	. . . . . . . . . . . . 13 |- (t = 0 -> (1 - ((1 - t) x. (2 x. v))) = (1 - ((1 - 0) x. (2 x. v))))
168	167	fveq2d 4685	. . . . . . . . . . . 12 |- (t = 0 -> (F` (1 - ((1 - t) x. (2 x. v)))) = (F` (1 - ((1 - 0) x. (2 x. v)))))
169		id 73	. . . . . . . . . . . . . 14 |- (t = 0 -> t = 0)
170	165	opreq1d 4897	. . . . . . . . . . . . . 14 |- (t = 0 -> ((1 - t) x. ((2 x. v) - 1)) = ((1 - 0) x. ((2 x. v) - 1)))
171	169, 170	opreq12d 4900	. . . . . . . . . . . . 13 |- (t = 0 -> (t + ((1 - t) x. ((2 x. v) - 1))) = (0 + ((1 - 0) x. ((2 x. v) - 1))))
172	171	fveq2d 4685	. . . . . . . . . . . 12 |- (t = 0 -> (F` (t + ((1 - t) x. ((2 x. v) - 1)))) = (F` (0 + ((1 - 0) x. ((2 x. v) - 1)))))
173	164, 168, 172	ifbieq12d 2998	. . . . . . . . . . 11 |- (t = 0 -> if(v <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. v)))), (F` (t + ((1 - t) x. ((2 x. v) - 1))))) = if(v <_ (1 / 2), (F` (1 - ((1 - 0) x. (2 x. v)))), (F` (0 + ((1 - 0) x. ((2 x. v) - 1))))))
174	153, 163, 173, 101	oprabval2 4957	. . . . . . . . . 10 |- ((v e. (0[,]1) /\ 0 e. (0[,]1)) -> (v{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}0) = if(v <_ (1 / 2), (F` (1 - ((1 - 0) x. (2 x. v)))), (F` (0 + ((1 - 0) x. ((2 x. v) - 1))))))
175	68, 174	mpan2 760	. . . . . . . . 9 |- (v e. (0[,]1) -> (v{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}0) = if(v <_ (1 / 2), (F` (1 - ((1 - 0) x. (2 x. v)))), (F` (0 + ((1 - 0) x. ((2 x. v) - 1))))))
176	175	adantl 424	. . . . . . . 8 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> (v{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}0) = if(v <_ (1 / 2), (F` (1 - ((1 - 0) x. (2 x. v)))), (F` (0 + ((1 - 0) x. ((2 x. v) - 1))))))
177		pcoval 16073	. . . . . . . . . . 11 |- ((J e. Top /\ (G e. (II Cn J) /\ F e. (II Cn J) /\ (G` 1) = (F` 0))) -> (G(*p` J)F) = {<.p, q>. | (p e. (0[,]1) /\ q = if(p <_ (1 / 2), (G` (2 x. p)), (F` ((2 x. p) - 1))))})
178	1, 34, 35, 48, 177	syl13anc 1102	. . . . . . . . . 10 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> (G(*p` J)F) = {<.p, q>. | (p e. (0[,]1) /\ q = if(p <_ (1 / 2), (G` (2 x. p)), (F` ((2 x. p) - 1))))})
179	178	fveq1d 4683	. . . . . . . . 9 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> ((G(*p` J)F)` v) = ({<.p, q>. | (p e. (0[,]1) /\ q = if(p <_ (1 / 2), (G` (2 x. p)), (F` ((2 x. p) - 1))))}` v))
180		breq1 3341	. . . . . . . . . . 11 |- (p = v -> (p <_ (1 / 2) <-> v <_ (1 / 2)))
181		opreq2 4890	. . . . . . . . . . . 12 |- (p = v -> (2 x. p) = (2 x. v))
182	181	fveq2d 4685	. . . . . . . . . . 11 |- (p = v -> (G` (2 x. p)) = (G` (2 x. v)))
183	181	opreq1d 4897	. . . . . . . . . . . 12 |- (p = v -> ((2 x. p) - 1) = ((2 x. v) - 1))
184	183	fveq2d 4685	. . . . . . . . . . 11 |- (p = v -> (F` ((2 x. p) - 1)) = (F` ((2 x. v) - 1)))
185	180, 182, 184	ifbieq12d 2998	. . . . . . . . . 10 |- (p = v -> if(p <_ (1 / 2), (G` (2 x. p)), (F` ((2 x. p) - 1))) = if(v <_ (1 / 2), (G` (2 x. v)), (F` ((2 x. v) - 1))))
186		eqid 1884	. . . . . . . . . 10 |- {<.p, q>. | (p e. (0[,]1) /\ q = if(p <_ (1 / 2), (G` (2 x. p)), (F` ((2 x. p) - 1))))} = {<.p, q>. | (p e. (0[,]1) /\ q = if(p <_ (1 / 2), (G` (2 x. p)), (F` ((2 x. p) - 1))))}
187		fvex 4689	. . . . . . . . . . 11 |- (G` (2 x. v)) e. _V
188		fvex 4689	. . . . . . . . . . 11 |- (F` ((2 x. v) - 1)) e. _V
189	187, 188	ifex 3031	. . . . . . . . . 10 |- if(v <_ (1 / 2), (G` (2 x. v)), (F` ((2 x. v) - 1))) e. _V
190	185, 186, 189	fvopab4 4743	. . . . . . . . 9 |- (v e. (0[,]1) -> ({<.p, q>. | (p e. (0[,]1) /\ q = if(p <_ (1 / 2), (G` (2 x. p)), (F` ((2 x. p) - 1))))}` v) = if(v <_ (1 / 2), (G` (2 x. v)), (F` ((2 x. v) - 1))))
191	179, 190	sylan9eq 1948	. . . . . . . 8 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> ((G(*p` J)F)` v) = if(v <_ (1 / 2), (G` (2 x. v)), (F` ((2 x. v) - 1))))
192	150, 176, 191	3eqtr4d 1937	. . . . . . 7 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> (v{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}0) = ((G(*p` J)F)` v))
193		biidd 188	. . . . . . . . . . . . . . 15 |- ((2 x. v) e. CC -> (v <_ (1 / 2) <-> v <_ (1 / 2)))
194		mul02 6607	. . . . . . . . . . . . . . . . . 18 |- ((2 x. v) e. CC -> (0 x. (2 x. v)) = 0)
195	42	opreq1i 4892	. . . . . . . . . . . . . . . . . 18 |- ((1 - 1) x. (2 x. v)) = (0 x. (2 x. v))
196	194, 195	syl5eq 1940	. . . . . . . . . . . . . . . . 17 |- ((2 x. v) e. CC -> ((1 - 1) x. (2 x. v)) = 0)
197	196	opreq2d 4898	. . . . . . . . . . . . . . . 16 |- ((2 x. v) e. CC -> (1 - ((1 - 1) x. (2 x. v))) = (1 - 0))
198	197, 71	syl6eq 1944	. . . . . . . . . . . . . . 15 |- ((2 x. v) e. CC -> (1 - ((1 - 1) x. (2 x. v))) = 1)
199		mul02 6607	. . . . . . . . . . . . . . . . . . 19 |- (((2 x. v) - 1) e. CC -> (0 x. ((2 x. v) - 1)) = 0)
200	42	opreq1i 4892	. . . . . . . . . . . . . . . . . . 19 |- ((1 - 1) x. ((2 x. v) - 1)) = (0 x. ((2 x. v) - 1))
201	199, 200	syl5eq 1940	. . . . . . . . . . . . . . . . . 18 |- (((2 x. v) - 1) e. CC -> ((1 - 1) x. ((2 x. v) - 1)) = 0)
202	201	opreq2d 4898	. . . . . . . . . . . . . . . . 17 |- (((2 x. v) - 1) e. CC -> (1 + ((1 - 1) x. ((2 x. v) - 1))) = (1 + 0))
203	23	addid1i 6483	. . . . . . . . . . . . . . . . 17 |- (1 + 0) = 1
204	202, 203	syl6eq 1944	. . . . . . . . . . . . . . . 16 |- (((2 x. v) - 1) e. CC -> (1 + ((1 - 1) x. ((2 x. v) - 1))) = 1)
205	139, 204	syl 12	. . . . . . . . . . . . . . 15 |- ((2 x. v) e. CC -> (1 + ((1 - 1) x. ((2 x. v) - 1))) = 1)
206	193, 198, 205	ifbieq12d 2998	. . . . . . . . . . . . . 14 |- ((2 x. v) e. CC -> if(v <_ (1 / 2), (1 - ((1 - 1) x. (2 x. v))), (1 + ((1 - 1) x. ((2 x. v) - 1)))) = if(v <_ (1 / 2), 1, 1))
207	104, 107, 206	3syl 24	. . . . . . . . . . . . 13 |- (v e. (0[,]1) -> if(v <_ (1 / 2), (1 - ((1 - 1) x. (2 x. v))), (1 + ((1 - 1) x. ((2 x. v) - 1)))) = if(v <_ (1 / 2), 1, 1))
208		ifid 3003	. . . . . . . . . . . . 13 |- if(v <_ (1 / 2), 1, 1) = 1
209	207, 208	syl6eq 1944	. . . . . . . . . . . 12 |- (v e. (0[,]1) -> if(v <_ (1 / 2), (1 - ((1 - 1) x. (2 x. v))), (1 + ((1 - 1) x. ((2 x. v) - 1)))) = 1)
210	209	adantl 424	. . . . . . . . . . 11 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> if(v <_ (1 / 2), (1 - ((1 - 1) x. (2 x. v))), (1 + ((1 - 1) x. ((2 x. v) - 1)))) = 1)
211	210	fveq2d 4685	. . . . . . . . . 10 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> (F` if(v <_ (1 / 2), (1 - ((1 - 1) x. (2 x. v))), (1 + ((1 - 1) x. ((2 x. v) - 1))))) = (F` 1))
212		simpl3 881	. . . . . . . . . 10 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> (F` 1) = Y)
213	211, 212	eqtrd 1925	. . . . . . . . 9 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> (F` if(v <_ (1 / 2), (1 - ((1 - 1) x. (2 x. v))), (1 + ((1 - 1) x. ((2 x. v) - 1))))) = Y)
214		fvif 15692	. . . . . . . . 9 |- (F` if(v <_ (1 / 2), (1 - ((1 - 1) x. (2 x. v))), (1 + ((1 - 1) x. ((2 x. v) - 1))))) = if(v <_ (1 / 2), (F` (1 - ((1 - 1) x. (2 x. v)))), (F` (1 + ((1 - 1) x. ((2 x. v) - 1)))))
215	213, 214	syl5eqr 1942	. . . . . . . 8 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> if(v <_ (1 / 2), (F` (1 - ((1 - 1) x. (2 x. v)))), (F` (1 + ((1 - 1) x. ((2 x. v) - 1))))) = Y)
216		fvex 4689	. . . . . . . . . . . 12 |- (F` (1 - ((1 - 1) x. (2 x. v)))) e. _V
217		fvex 4689	. . . . . . . . . . . 12 |- (F` (1 + ((1 - 1) x. ((2 x. v) - 1)))) e. _V
218	216, 217	ifex 3031	. . . . . . . . . . 11 |- if(v <_ (1 / 2), (F` (1 - ((1 - 1) x. (2 x. v)))), (F` (1 + ((1 - 1) x. ((2 x. v) - 1))))) e. _V
219		biidd 188	. . . . . . . . . . . 12 |- (t = 1 -> (v <_ (1 / 2) <-> v <_ (1 / 2)))
220		opreq2 4890	. . . . . . . . . . . . . . 15 |- (t = 1 -> (1 - t) = (1 - 1))
221	220	opreq1d 4897	. . . . . . . . . . . . . 14 |- (t = 1 -> ((1 - t) x. (2 x. v)) = ((1 - 1) x. (2 x. v)))
222	221	opreq2d 4898	. . . . . . . . . . . . 13 |- (t = 1 -> (1 - ((1 - t) x. (2 x. v))) = (1 - ((1 - 1) x. (2 x. v))))
223	222	fveq2d 4685	. . . . . . . . . . . 12 |- (t = 1 -> (F` (1 - ((1 - t) x. (2 x. v)))) = (F` (1 - ((1 - 1) x. (2 x. v)))))
224		id 73	. . . . . . . . . . . . . 14 |- (t = 1 -> t = 1)
225	220	opreq1d 4897	. . . . . . . . . . . . . 14 |- (t = 1 -> ((1 - t) x. ((2 x. v) - 1)) = ((1 - 1) x. ((2 x. v) - 1)))
226	224, 225	opreq12d 4900	. . . . . . . . . . . . 13 |- (t = 1 -> (t + ((1 - t) x. ((2 x. v) - 1))) = (1 + ((1 - 1) x. ((2 x. v) - 1))))
227	226	fveq2d 4685	. . . . . . . . . . . 12 |- (t = 1 -> (F` (t + ((1 - t) x. ((2 x. v) - 1)))) = (F` (1 + ((1 - 1) x. ((2 x. v) - 1)))))
228	219, 223, 227	ifbieq12d 2998	. . . . . . . . . . 11 |- (t = 1 -> if(v <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. v)))), (F` (t + ((1 - t) x. ((2 x. v) - 1))))) = if(v <_ (1 / 2), (F` (1 - ((1 - 1) x. (2 x. v)))), (F` (1 + ((1 - 1) x. ((2 x. v) - 1))))))
229	218, 163, 228, 101	oprabval2 4957	. . . . . . . . . 10 |- ((v e. (0[,]1) /\ 1 e. (0[,]1)) -> (v{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}1) = if(v <_ (1 / 2), (F` (1 - ((1 - 1) x. (2 x. v)))), (F` (1 + ((1 - 1) x. ((2 x. v) - 1))))))
230	39, 229	mpan2 760	. . . . . . . . 9 |- (v e. (0[,]1) -> (v{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}1) = if(v <_ (1 / 2), (F` (1 - ((1 - 1) x. (2 x. v)))), (F` (1 + ((1 - 1) x. ((2 x. v) - 1))))))
231	230	adantl 424	. . . . . . . 8 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> (v{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}1) = if(v <_ (1 / 2), (F` (1 - ((1 - 1) x. (2 x. v)))), (F` (1 + ((1 - 1) x. ((2 x. v) - 1))))))
232		fvconst2g 4820	. . . . . . . . . 10 |- ((Y e. U.J /\ v e. (0[,]1)) -> (((0[,]1) X. {Y})` v) = Y)
233	232, 82	sylan 497	. . . . . . . . 9 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> (((0[,]1) X. {Y})` v) = Y)
234	64	fveq1i 4682	. . . . . . . . 9 |- (P` v) = (((0[,]1) X. {Y})` v)
235	233, 234	syl5eq 1940	. . . . . . . 8 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> (P` v) = Y)
236	215, 231, 235	3eqtr4d 1937	. . . . . . 7 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> (v{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}1) = (P` v))
237	105	mul01i 6594	. . . . . . . . . . . . . . . . . . 19 |- (2 x. 0) = 0
238	237	a1i 8	. . . . . . . . . . . . . . . . . 18 |- (v e. CC -> (2 x. 0) = 0)
239	238	opreq2d 4898	. . . . . . . . . . . . . . . . 17 |- (v e. CC -> ((1 - v) x. (2 x. 0)) = ((1 - v) x. 0))
240		subcl 6524	. . . . . . . . . . . . . . . . . . 19 |- ((1 e. CC /\ v e. CC) -> (1 - v) e. CC)
241	23, 240	mpan 759	. . . . . . . . . . . . . . . . . 18 |- (v e. CC -> (1 - v) e. CC)
242		mul01 6606	. . . . . . . . . . . . . . . . . 18 |- ((1 - v) e. CC -> ((1 - v) x. 0) = 0)
243	241, 242	syl 12	. . . . . . . . . . . . . . . . 17 |- (v e. CC -> ((1 - v) x. 0) = 0)
244	239, 243	eqtrd 1925	. . . . . . . . . . . . . . . 16 |- (v e. CC -> ((1 - v) x. (2 x. 0)) = 0)
245	244	opreq2d 4898	. . . . . . . . . . . . . . 15 |- (v e. CC -> (1 - ((1 - v) x. (2 x. 0))) = (1 - 0))
246	245, 71	syl6eq 1944	. . . . . . . . . . . . . 14 |- (v e. CC -> (1 - ((1 - v) x. (2 x. 0))) = 1)
247	104, 246	syl 12	. . . . . . . . . . . . 13 |- (v e. (0[,]1) -> (1 - ((1 - v) x. (2 x. 0))) = 1)
248	247	adantl 424	. . . . . . . . . . . 12 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> (1 - ((1 - v) x. (2 x. 0))) = 1)
249	248	fveq2d 4685	. . . . . . . . . . 11 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> (F` (1 - ((1 - v) x. (2 x. 0)))) = (F` 1))
250	249, 212	eqtrd 1925	. . . . . . . . . 10 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> (F` (1 - ((1 - v) x. (2 x. 0)))) = Y)
251		halfgt0 7215	. . . . . . . . . . . 12 |- 0 < (1 / 2)
252	16, 125, 251	ltleii 6756	. . . . . . . . . . 11 |- 0 <_ (1 / 2)
253		iftrue 2989	. . . . . . . . . . 11 |- (0 <_ (1 / 2) -> if(0 <_ (1 / 2), (F` (1 - ((1 - v) x. (2 x. 0)))), (F` (v + ((1 - v) x. ((2 x. 0) - 1))))) = (F` (1 - ((1 - v) x. (2 x. 0)))))
254	252, 253	ax-mp 7	. . . . . . . . . 10 |- if(0 <_ (1 / 2), (F` (1 - ((1 - v) x. (2 x. 0)))), (F` (v + ((1 - v) x. ((2 x. 0) - 1))))) = (F` (1 - ((1 - v) x. (2 x. 0))))
255	250, 254	syl5eq 1940	. . . . . . . . 9 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> if(0 <_ (1 / 2), (F` (1 - ((1 - v) x. (2 x. 0)))), (F` (v + ((1 - v) x. ((2 x. 0) - 1))))) = Y)
256		fvex 4689	. . . . . . . . . . . . 13 |- (F` (1 - ((1 - v) x. (2 x. 0)))) e. _V
257		fvex 4689	. . . . . . . . . . . . 13 |- (F` (v + ((1 - v) x. ((2 x. 0) - 1)))) e. _V
258	256, 257	ifex 3031	. . . . . . . . . . . 12 |- if(0 <_ (1 / 2), (F` (1 - ((1 - v) x. (2 x. 0)))), (F` (v + ((1 - v) x. ((2 x. 0) - 1))))) e. _V
259		breq1 3341	. . . . . . . . . . . . 13 |- (s = 0 -> (s <_ (1 / 2) <-> 0 <_ (1 / 2)))
260		opreq2 4890	. . . . . . . . . . . . . . . 16 |- (s = 0 -> (2 x. s) = (2 x. 0))
261	260	opreq2d 4898	. . . . . . . . . . . . . . 15 |- (s = 0 -> ((1 - t) x. (2 x. s)) = ((1 - t) x. (2 x. 0)))
262	261	opreq2d 4898	. . . . . . . . . . . . . 14 |- (s = 0 -> (1 - ((1 - t) x. (2 x. s))) = (1 - ((1 - t) x. (2 x. 0))))
263	262	fveq2d 4685	. . . . . . . . . . . . 13 |- (s = 0 -> (F` (1 - ((1 - t) x. (2 x. s)))) = (F` (1 - ((1 - t) x. (2 x. 0)))))
264	260	opreq1d 4897	. . . . . . . . . . . . . . . 16 |- (s = 0 -> ((2 x. s) - 1) = ((2 x. 0) - 1))
265	264	opreq2d 4898	. . . . . . . . . . . . . . 15 |- (s = 0 -> ((1 - t) x. ((2 x. s) - 1)) = ((1 - t) x. ((2 x. 0) - 1)))
266	265	opreq2d 4898	. . . . . . . . . . . . . 14 |- (s = 0 -> (t + ((1 - t) x. ((2 x. s) - 1))) = (t + ((1 - t) x. ((2 x. 0) - 1))))
267	266	fveq2d 4685	. . . . . . . . . . . . 13 |- (s = 0 -> (F` (t + ((1 - t) x. ((2 x. s) - 1)))) = (F` (t + ((1 - t) x. ((2 x. 0) - 1)))))
268	259, 263, 267	ifbieq12d 2998	. . . . . . . . . . . 12 |- (s = 0 -> if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))) = if(0 <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. 0)))), (F` (t + ((1 - t) x. ((2 x. 0) - 1))))))
269		biidd 188	. . . . . . . . . . . . 13 |- (t = v -> (0 <_ (1 / 2) <-> 0 <_ (1 / 2)))
270		opreq2 4890	. . . . . . . . . . . . . . . 16 |- (t = v -> (1 - t) = (1 - v))
271	270	opreq1d 4897	. . . . . . . . . . . . . . 15 |- (t = v -> ((1 - t) x. (2 x. 0)) = ((1 - v) x. (2 x. 0)))
272	271	opreq2d 4898	. . . . . . . . . . . . . 14 |- (t = v -> (1 - ((1 - t) x. (2 x. 0))) = (1 - ((1 - v) x. (2 x. 0))))
273	272	fveq2d 4685	. . . . . . . . . . . . 13 |- (t = v -> (F` (1 - ((1 - t) x. (2 x. 0)))) = (F` (1 - ((1 - v) x. (2 x. 0)))))
274		id 73	. . . . . . . . . . . . . . 15 |- (t = v -> t = v)
275	270	opreq1d 4897	. . . . . . . . . . . . . . 15 |- (t = v -> ((1 - t) x. ((2 x. 0) - 1)) = ((1 - v) x. ((2 x. 0) - 1)))
276	274, 275	opreq12d 4900	. . . . . . . . . . . . . 14 |- (t = v -> (t + ((1 - t) x. ((2 x. 0) - 1))) = (v + ((1 - v) x. ((2 x. 0) - 1))))
277	276	fveq2d 4685	. . . . . . . . . . . . 13 |- (t = v -> (F` (t + ((1 - t) x. ((2 x. 0) - 1)))) = (F` (v + ((1 - v) x. ((2 x. 0) - 1)))))
278	269, 273, 277	ifbieq12d 2998	. . . . . . . . . . . 12 |- (t = v -> if(0 <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. 0)))), (F` (t + ((1 - t) x. ((2 x. 0) - 1))))) = if(0 <_ (1 / 2), (F` (1 - ((1 - v) x. (2 x. 0)))), (F` (v + ((1 - v) x. ((2 x. 0) - 1))))))
279	258, 268, 278, 101	oprabval2 4957	. . . . . . . . . . 11 |- ((0 e. (0[,]1) /\ v e. (0[,]1)) -> (0{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}v) = if(0 <_ (1 / 2), (F` (1 - ((1 - v) x. (2 x. 0)))), (F` (v + ((1 - v) x. ((2 x. 0) - 1))))))
280	68, 279	mpan 759	. . . . . . . . . 10 |- (v e. (0[,]1) -> (0{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}v) = if(0 <_ (1 / 2), (F` (1 - ((1 - v) x. (2 x. 0)))), (F` (v + ((1 - v) x. ((2 x. 0) - 1))))))
281	280	adantl 424	. . . . . . . . 9 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> (0{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}v) = if(0 <_ (1 / 2), (F` (1 - ((1 - v) x. (2 x. 0)))), (F` (v + ((1 - v) x. ((2 x. 0) - 1))))))
282	81, 79	eqtrd 1925	. . . . . . . . . 10 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> ((G(*p` J)F)` 0) = Y)
283	282	adantr 425	. . . . . . . . 9 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> ((G(*p` J)F)` 0) = Y)
284	255, 281, 283	3eqtr4d 1937	. . . . . . . 8 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> (0{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}v) = ((G(*p` J)F)` 0))
285	105	mulid1i 6485	. . . . . . . . . . . . . . . . . . . . 21 |- (2 x. 1) = 2
286	285	opreq1i 4892	. . . . . . . . . . . . . . . . . . . 20 |- ((2 x. 1) - 1) = (2 - 1)
287		1p1e2 10145	. . . . . . . . . . . . . . . . . . . . 21 |- (1 + 1) = 2
288	105, 23, 23, 287	subaddrii 6529	. . . . . . . . . . . . . . . . . . . 20 |- (2 - 1) = 1
289	286, 288	eqtri 1908	. . . . . . . . . . . . . . . . . . 19 |- ((2 x. 1) - 1) = 1
290	289	a1i 8	. . . . . . . . . . . . . . . . . 18 |- (v e. CC -> ((2 x. 1) - 1) = 1)
291	290	opreq2d 4898	. . . . . . . . . . . . . . . . 17 |- (v e. CC -> ((1 - v) x. ((2 x. 1) - 1)) = ((1 - v) x. 1))
292		ax1id 6435	. . . . . . . . . . . . . . . . . 18 |- ((1 - v) e. CC -> ((1 - v) x. 1) = (1 - v))
293	241, 292	syl 12	. . . . . . . . . . . . . . . . 17 |- (v e. CC -> ((1 - v) x. 1) = (1 - v))
294	291, 293	eqtrd 1925	. . . . . . . . . . . . . . . 16 |- (v e. CC -> ((1 - v) x. ((2 x. 1) - 1)) = (1 - v))
295	294	opreq2d 4898	. . . . . . . . . . . . . . 15 |- (v e. CC -> (v + ((1 - v) x. ((2 x. 1) - 1))) = (v + (1 - v)))
296		pncan3 6534	. . . . . . . . . . . . . . . 16 |- ((v e. CC /\ 1 e. CC) -> (v + (1 - v)) = 1)
297	23, 296	mpan2 760	. . . . . . . . . . . . . . 15 |- (v e. CC -> (v + (1 - v)) = 1)
298	295, 297	eqtrd 1925	. . . . . . . . . . . . . 14 |- (v e. CC -> (v + ((1 - v) x. ((2 x. 1) - 1))) = 1)
299	104, 298	syl 12	. . . . . . . . . . . . 13 |- (v e. (0[,]1) -> (v + ((1 - v) x. ((2 x. 1) - 1))) = 1)
300	299	adantl 424	. . . . . . . . . . . 12 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> (v + ((1 - v) x. ((2 x. 1) - 1))) = 1)
301	300	fveq2d 4685	. . . . . . . . . . 11 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> (F` (v + ((1 - v) x. ((2 x. 1) - 1)))) = (F` 1))
302	301, 212	eqtrd 1925	. . . . . . . . . 10 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> (F` (v + ((1 - v) x. ((2 x. 1) - 1)))) = Y)
303		halflt1 7216	. . . . . . . . . . . 12 |- (1 / 2) < 1
304	125, 17	ltnlei 6754	. . . . . . . . . . . 12 |- ((1 / 2) < 1 <-> -. 1 <_ (1 / 2))
305	303, 304	mpbi 206	. . . . . . . . . . 11 |- -. 1 <_ (1 / 2)
306		iffalse 2991	. . . . . . . . . . 11 |- (-. 1 <_ (1 / 2) -> if(1 <_ (1 / 2), (F` (1 - ((1 - v) x. (2 x. 1)))), (F` (v + ((1 - v) x. ((2 x. 1) - 1))))) = (F` (v + ((1 - v) x. ((2 x. 1) - 1)))))
307	305, 306	ax-mp 7	. . . . . . . . . 10 |- if(1 <_ (1 / 2), (F` (1 - ((1 - v) x. (2 x. 1)))), (F` (v + ((1 - v) x. ((2 x. 1) - 1))))) = (F` (v + ((1 - v) x. ((2 x. 1) - 1))))
308	302, 307	syl5eq 1940	. . . . . . . . 9 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> if(1 <_ (1 / 2), (F` (1 - ((1 - v) x. (2 x. 1)))), (F` (v + ((1 - v) x. ((2 x. 1) - 1))))) = Y)
309		fvex 4689	. . . . . . . . . . . . 13 |- (F` (1 - ((1 - v) x. (2 x. 1)))) e. _V
310		fvex 4689	. . . . . . . . . . . . 13 |- (F` (v + ((1 - v) x. ((2 x. 1) - 1)))) e. _V
311	309, 310	ifex 3031	. . . . . . . . . . . 12 |- if(1 <_ (1 / 2), (F` (1 - ((1 - v) x. (2 x. 1)))), (F` (v + ((1 - v) x. ((2 x. 1) - 1))))) e. _V
312		breq1 3341	. . . . . . . . . . . . 13 |- (s = 1 -> (s <_ (1 / 2) <-> 1 <_ (1 / 2)))
313		opreq2 4890	. . . . . . . . . . . . . . . 16 |- (s = 1 -> (2 x. s) = (2 x. 1))
314	313	opreq2d 4898	. . . . . . . . . . . . . . 15 |- (s = 1 -> ((1 - t) x. (2 x. s)) = ((1 - t) x. (2 x. 1)))
315	314	opreq2d 4898	. . . . . . . . . . . . . 14 |- (s = 1 -> (1 - ((1 - t) x. (2 x. s))) = (1 - ((1 - t) x. (2 x. 1))))
316	315	fveq2d 4685	. . . . . . . . . . . . 13 |- (s = 1 -> (F` (1 - ((1 - t) x. (2 x. s)))) = (F` (1 - ((1 - t) x. (2 x. 1)))))
317	313	opreq1d 4897	. . . . . . . . . . . . . . . 16 |- (s = 1 -> ((2 x. s) - 1) = ((2 x. 1) - 1))
318	317	opreq2d 4898	. . . . . . . . . . . . . . 15 |- (s = 1 -> ((1 - t) x. ((2 x. s) - 1)) = ((1 - t) x. ((2 x. 1) - 1)))
319	318	opreq2d 4898	. . . . . . . . . . . . . 14 |- (s = 1 -> (t + ((1 - t) x. ((2 x. s) - 1))) = (t + ((1 - t) x. ((2 x. 1) - 1))))
320	319	fveq2d 4685	. . . . . . . . . . . . 13 |- (s = 1 -> (F` (t + ((1 - t) x. ((2 x. s) - 1)))) = (F` (t + ((1 - t) x. ((2 x. 1) - 1)))))
321	312, 316, 320	ifbieq12d 2998	. . . . . . . . . . . 12 |- (s = 1 -> if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))) = if(1 <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. 1)))), (F` (t + ((1 - t) x. ((2 x. 1) - 1))))))
322		biidd 188	. . . . . . . . . . . . 13 |- (t = v -> (1 <_ (1 / 2) <-> 1 <_ (1 / 2)))
323	270	opreq1d 4897	. . . . . . . . . . . . . . 15 |- (t = v -> ((1 - t) x. (2 x. 1)) = ((1 - v) x. (2 x. 1)))
324	323	opreq2d 4898	. . . . . . . . . . . . . 14 |- (t = v -> (1 - ((1 - t) x. (2 x. 1))) = (1 - ((1 - v) x. (2 x. 1))))
325	324	fveq2d 4685	. . . . . . . . . . . . 13 |- (t = v -> (F` (1 - ((1 - t) x. (2 x. 1)))) = (F` (1 - ((1 - v) x. (2 x. 1)))))
326	270	opreq1d 4897	. . . . . . . . . . . . . . 15 |- (t = v -> ((1 - t) x. ((2 x. 1) - 1)) = ((1 - v) x. ((2 x. 1) - 1)))
327	274, 326	opreq12d 4900	. . . . . . . . . . . . . 14 |- (t = v -> (t + ((1 - t) x. ((2 x. 1) - 1))) = (v + ((1 - v) x. ((2 x. 1) - 1))))
328	327	fveq2d 4685	. . . . . . . . . . . . 13 |- (t = v -> (F` (t + ((1 - t) x. ((2 x. 1) - 1)))) = (F` (v + ((1 - v) x. ((2 x. 1) - 1)))))
329	322, 325, 328	ifbieq12d 2998	. . . . . . . . . . . 12 |- (t = v -> if(1 <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. 1)))), (F` (t + ((1 - t) x. ((2 x. 1) - 1))))) = if(1 <_ (1 / 2), (F` (1 - ((1 - v) x. (2 x. 1)))), (F` (v + ((1 - v) x. ((2 x. 1) - 1))))))
330	311, 321, 329, 101	oprabval2 4957	. . . . . . . . . . 11 |- ((1 e. (0[,]1) /\ v e. (0[,]1)) -> (1{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}v) = if(1 <_ (1 / 2), (F` (1 - ((1 - v) x. (2 x. 1)))), (F` (v + ((1 - v) x. ((2 x. 1) - 1))))))
331	39, 330	mpan 759	. . . . . . . . . 10 |- (v e. (0[,]1) -> (1{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}v) = if(1 <_ (1 / 2), (F` (1 - ((1 - v) x. (2 x. 1)))), (F` (v + ((1 - v) x. ((2 x. 1) - 1))))))
332	331	adantl 424	. . . . . . . . 9 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> (1{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}v) = if(1 <_ (1 / 2), (F` (1 - ((1 - v) x. (2 x. 1)))), (F` (v + ((1 - v) x. ((2 x. 1) - 1))))))
333	91, 89	eqtrd 1925	. . . . . . . . . 10 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> ((G(*p` J)F)` 1) = Y)
334	333	adantr 425	. . . . . . . . 9 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> ((G(*p` J)F)` 1) = Y)
335	308, 332, 334	3eqtr4d 1937	. . . . . . . 8 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> (1{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}v) = ((G(*p` J)F)` 1))
336	284, 335	jca 310	. . . . . . 7 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> ((0{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}v) = ((G(*p` J)F)` 0) /\ (1{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}v) = ((G(*p` J)F)` 1)))
337	192, 236, 336	jca31 311	. . . . . 6 |- (((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) /\ v e. (0[,]1)) -> (((v{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}0) = ((G(*p` J)F)` v) /\ (v{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}1) = (P` v)) /\ ((0{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}v) = ((G(*p` J)F)` 0) /\ (1{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}v) = ((G(*p` J)F)` 1))))
338	337	r19.21aiva 2176	. . . . 5 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> A.v e. (0[,]1)(((v{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}0) = ((G(*p` J)F)` v) /\ (v{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}1) = (P` v)) /\ ((0{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}v) = ((G(*p` J)F)` 0) /\ (1{<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))}v) = ((G(*p` J)F)` 1))))
339	100, 103, 338	mpbir2and 802	. . . 4 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> {<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))} e. ((G(*p` J)F)(PHtpy` J)P))
340		ne0i 2881	. . . 4 |- ({<.<.s, t>., u>. | ((s e. (0[,]1) /\ t e. (0[,]1)) /\ u = if(s <_ (1 / 2), (F` (1 - ((1 - t) x. (2 x. s)))), (F` (t + ((1 - t) x. ((2 x. s) - 1))))))} e. ((G(*p` J)F)(PHtpy` J)P) -> ((G(*p` J)F)(PHtpy` J)P) =/= (/))
341	339, 340	syl 12	. . 3 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> ((G(*p` J)F)(PHtpy` J)P) =/= (/))
342	66, 98, 341	jca31 311	. 2 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> ((((G(*p` J)F) e. (II Cn J) /\ P e. (II Cn J)) /\ (((G(*p` J)F)` 0) = (P` 0) /\ ((G(*p` J)F)` 1) = (P` 1))) /\ ((G(*p` J)F)(PHtpy` J)P) =/= (/)))
343		oprex 4907	. . . . . 6 |- (0[,]1) e. _V
344		snex 3492	. . . . . 6 |- {Y} e. _V
345	343, 344	xpex 4096	. . . . 5 |- ((0[,]1) X. {Y}) e. _V
346	64, 345	eqeltri 1967	. . . 4 |- P e. _V
347		isphtpc2 16060	. . . 4 |- ((J e. Top /\ P e. _V) -> ((G(*p` J)F)(~=ph` J)P <-> ((((G(*p` J)F) e. (II Cn J) /\ P e. (II Cn J)) /\ (((G(*p` J)F)` 0) = (P` 0) /\ ((G(*p` J)F)` 1) = (P` 1))) /\ ((G(*p` J)F)(PHtpy` J)P) =/= (/))))
348	346, 347	mpan2 760	. . 3 |- (J e. Top -> ((G(*p` J)F)(~=ph` J)P <-> ((((G(*p` J)F) e. (II Cn J) /\ P e. (II Cn J)) /\ (((G(*p` J)F)` 0) = (P` 0) /\ ((G(*p` J)F)` 1) = (P` 1))) /\ ((G(*p` J)F)(PHtpy` J)P) =/= (/))))
349	348	3ad2ant1 897	. 2 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> ((G(*p` J)F)(~=ph` J)P <-> ((((G(*p` J)F) e. (II Cn J) /\ P e. (II Cn J)) /\ (((G(*p` J)F)` 0) = (P` 0) /\ ((G(*p` J)F)` 1) = (P` 1))) /\ ((G(*p` J)F)(PHtpy` J)P) =/= (/))))
350	342, 349	mpbird 213	1 |- ((J e. Top /\ F e. (II Cn J) /\ (F` 1) = Y) -> (G(*p` J)F)(~=ph` J)P)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  _Vcvv 2292   C_ wss 2593  (/)c0 2875  ifcif 2982  {csn 3044  U.cuni 3177   class class class wbr 3338  {copab 3395   X. cxp 3984   o. ccom 3990   Fn wfn 3993  -->wf 3994  ` cfv 3998  (class class class)co 4884  {copab2 4885  CCcc 6384  RRcr 6385  0cc0 6386  1c1 6387   + caddc 6389   x. cmul 6391   - cmin 6445   / cdiv 6447   <_ cle 6448   < clt 6653  2c2 7145  [,]cicc 7527  -cn->ccncf 8524  Topctop 8857   X.t ctx 8930   Cn ccn 9028  IIcii 15865  PHtpycphtpy 16043  ~=phcphtpc 16044  *pcpco 16067

This theorem is referenced by:  pi1gp 16095

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1302  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-reg 5695  ax-inf2 5731  ax-ac 5906

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-iin 3258  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-map 5383  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-sup 5664  df-r1 5750  df-rank 5751  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-div 6892  df-n 7108  df-2 7154  df-rp 7232  df-n0 7309  df-z 7345  df-q 7436  df-fl 7463  df-ioo 7528  df-icc 7531  df-uz 7587  df-seq1 7721  df-exp 7812  df-sqr 7920  df-re 8001  df-im 8002  df-cj 8003  df-abs 8004  df-clim 8235  df-cncf 8525  df-top 8861  df-topsp 8862  df-bases 8863  df-topgen 8864  df-tx 8931  df-cld 8939  df-cn 9030  df-cnp 9031  df-met 9070  df-bl 9072  df-opn 9073  df-lm 9200  df-subsp 10243  df-ii 15866  df-phtpy 16045  df-phtpc 16057  df-pco 16069

Copyright terms: Public domain