Theorem reparpht 16065

Description: Reparametrization lemma. The reparametrization of a path by any continuous map G:II-->II with G(0) = 0 and G(1) = 1 is path-homotopic to the original path.

Assertion

Ref	Expression
reparpht	|- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> (F o. G)(~=ph` J)F)

Proof of Theorem reparpht

Step	Hyp	Ref	Expression
1		iitop 15867	. . . . . . . . 9 |- II e. Top
2		cnco 9045	. . . . . . . . . 10 |- (((II e. Top /\ II e. Top /\ J e. Top) /\ (G e. (II Cn II) /\ F e. (II Cn J))) -> (F o. G) e. (II Cn J))
3	2	ex 402	. . . . . . . . 9 |- ((II e. Top /\ II e. Top /\ J e. Top) -> ((G e. (II Cn II) /\ F e. (II Cn J)) -> (F o. G) e. (II Cn J)))
4	1, 1, 3	mp3an12 1181	. . . . . . . 8 |- (J e. Top -> ((G e. (II Cn II) /\ F e. (II Cn J)) -> (F o. G) e. (II Cn J)))
5	4	imp 377	. . . . . . 7 |- ((J e. Top /\ (G e. (II Cn II) /\ F e. (II Cn J))) -> (F o. G) e. (II Cn J))
6	5	anassrs 489	. . . . . 6 |- (((J e. Top /\ G e. (II Cn II)) /\ F e. (II Cn J)) -> (F o. G) e. (II Cn J))
7	6	an1rs 547	. . . . 5 |- (((J e. Top /\ F e. (II Cn J)) /\ G e. (II Cn II)) -> (F o. G) e. (II Cn J))
8	7	3ad2antr1 1041	. . . 4 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> (F o. G) e. (II Cn J))
9		simplr 449	. . . 4 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> F e. (II Cn J))
10	8, 9	jca 310	. . 3 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> ((F o. G) e. (II Cn J) /\ F e. (II Cn J)))
11		fvco 4736	. . . . . . . . 9 |- ((Fun F /\ Fun G /\ 0 e. dom G) -> ((F o. G)` 0) = (F` (G` 0)))
12	11	3expb 1068	. . . . . . . 8 |- ((Fun F /\ (Fun G /\ 0 e. dom G)) -> ((F o. G)` 0) = (F` (G` 0)))
13		ffun 4565	. . . . . . . 8 |- (F:(0[,]1)-->U.J -> Fun F)
14		ffun 4565	. . . . . . . . 9 |- (G:(0[,]1)-->(0[,]1) -> Fun G)
15		fdm 4567	. . . . . . . . . 10 |- (G:(0[,]1)-->(0[,]1) -> dom G = (0[,]1))
16		0re 6603	. . . . . . . . . . 11 |- 0 e. RR
17		1re 6598	. . . . . . . . . . 11 |- 1 e. RR
18		lt01 6871	. . . . . . . . . . . 12 |- 0 < 1
19	16, 17, 18	ltleii 6756	. . . . . . . . . . 11 |- 0 <_ 1
20		lbicc2 7573	. . . . . . . . . . 11 |- ((0 e. RR /\ 1 e. RR /\ 0 <_ 1) -> 0 e. (0[,]1))
21	16, 17, 19, 20	mp3an 1191	. . . . . . . . . 10 |- 0 e. (0[,]1)
22	15, 21	syl5eleqr 1978	. . . . . . . . 9 |- (G:(0[,]1)-->(0[,]1) -> 0 e. dom G)
23	14, 22	jca 310	. . . . . . . 8 |- (G:(0[,]1)-->(0[,]1) -> (Fun G /\ 0 e. dom G))
24	12, 13, 23	syl2an 503	. . . . . . 7 |- ((F:(0[,]1)-->U.J /\ G:(0[,]1)-->(0[,]1)) -> ((F o. G)` 0) = (F` (G` 0)))
25		iiuni 15868	. . . . . . . . 9 |- (0[,]1) = U.II
26		eqid 1884	. . . . . . . . 9 |- U.J = U.J
27	25, 26	cnf 9038	. . . . . . . 8 |- ((II e. Top /\ J e. Top /\ F e. (II Cn J)) -> F:(0[,]1)-->U.J)
28	1, 27	mp3an1 1178	. . . . . . 7 |- ((J e. Top /\ F e. (II Cn J)) -> F:(0[,]1)-->U.J)
29	25, 25	cnf 9038	. . . . . . . 8 |- ((II e. Top /\ II e. Top /\ G e. (II Cn II)) -> G:(0[,]1)-->(0[,]1))
30	1, 1, 29	mp3an12 1181	. . . . . . 7 |- (G e. (II Cn II) -> G:(0[,]1)-->(0[,]1))
31	24, 28, 30	syl2an 503	. . . . . 6 |- (((J e. Top /\ F e. (II Cn J)) /\ G e. (II Cn II)) -> ((F o. G)` 0) = (F` (G` 0)))
32	31	3ad2antr1 1041	. . . . 5 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> ((F o. G)` 0) = (F` (G` 0)))
33		simpr2 883	. . . . . 6 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> (G` 0) = 0)
34	33	fveq2d 4685	. . . . 5 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> (F` (G` 0)) = (F` 0))
35	32, 34	eqtrd 1925	. . . 4 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> ((F o. G)` 0) = (F` 0))
36		fvco 4736	. . . . . . . . 9 |- ((Fun F /\ Fun G /\ 1 e. dom G) -> ((F o. G)` 1) = (F` (G` 1)))
37	36	3expb 1068	. . . . . . . 8 |- ((Fun F /\ (Fun G /\ 1 e. dom G)) -> ((F o. G)` 1) = (F` (G` 1)))
38		ubicc2 7574	. . . . . . . . . . 11 |- ((0 e. RR /\ 1 e. RR /\ 0 <_ 1) -> 1 e. (0[,]1))
39	16, 17, 19, 38	mp3an 1191	. . . . . . . . . 10 |- 1 e. (0[,]1)
40	15, 39	syl5eleqr 1978	. . . . . . . . 9 |- (G:(0[,]1)-->(0[,]1) -> 1 e. dom G)
41	14, 40	jca 310	. . . . . . . 8 |- (G:(0[,]1)-->(0[,]1) -> (Fun G /\ 1 e. dom G))
42	37, 13, 41	syl2an 503	. . . . . . 7 |- ((F:(0[,]1)-->U.J /\ G:(0[,]1)-->(0[,]1)) -> ((F o. G)` 1) = (F` (G` 1)))
43	42, 28, 30	syl2an 503	. . . . . 6 |- (((J e. Top /\ F e. (II Cn J)) /\ G e. (II Cn II)) -> ((F o. G)` 1) = (F` (G` 1)))
44	43	3ad2antr1 1041	. . . . 5 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> ((F o. G)` 1) = (F` (G` 1)))
45		simpr3 884	. . . . . 6 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> (G` 1) = 1)
46	45	fveq2d 4685	. . . . 5 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> (F` (G` 1)) = (F` 1))
47	44, 46	eqtrd 1925	. . . 4 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> ((F o. G)` 1) = (F` 1))
48	35, 47	jca 310	. . 3 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> (((F o. G)` 0) = (F` 0) /\ ((F o. G)` 1) = (F` 1)))
49		simpll 448	. . . . . 6 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> J e. Top)
50		isphtpy 16048	. . . . . 6 |- (((J e. Top /\ (F o. G) e. (II Cn J) /\ F e. (II Cn J)) /\ (((F o. G)` 0) = (F` 0) /\ ((F o. G)` 1) = (F` 1))) -> ({<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))} e. ((F o. G)(PHtpy` J)F) <-> ({<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))} e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((s{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}0) = ((F o. G)` s) /\ (s{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}1) = (F` s)) /\ ((0{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}s) = ((F o. G)` 0) /\ (1{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}s) = ((F o. G)` 1))))))
51	49, 8, 9, 35, 47, 50	syl32anc 1108	. . . . 5 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> ({<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))} e. ((F o. G)(PHtpy` J)F) <-> ({<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))} e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((s{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}0) = ((F o. G)` s) /\ (s{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}1) = (F` s)) /\ ((0{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}s) = ((F o. G)` 0) /\ (1{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}s) = ((F o. G)` 1))))))
52		ffn 4562	. . . . . . . . 9 |- (F:(0[,]1)-->U.J -> F Fn (0[,]1))
53		fveq1 4680	. . . . . . . . . . . . . . . . . 18 |- (G = if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1))) -> (G` x) = (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x))
54	53	opreq2d 4898	. . . . . . . . . . . . . . . . 17 |- (G = if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1))) -> ((1 - y) x. (G` x)) = ((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)))
55	54	opreq1d 4897	. . . . . . . . . . . . . . . 16 |- (G = if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1))) -> (((1 - y) x. (G` x)) + (y x. x)) = (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x)))
56	55	fveq2d 4685	. . . . . . . . . . . . . . 15 |- (G = if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1))) -> (F` (((1 - y) x. (G` x)) + (y x. x))) = (F` (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x))))
57	56	eqeq2d 1895	. . . . . . . . . . . . . 14 |- (G = if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1))) -> (z = (F` (((1 - y) x. (G` x)) + (y x. x))) <-> z = (F` (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x)))))
58	57	anbi2d 678	. . . . . . . . . . . . 13 |- (G = if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1))) -> (((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x)))) <-> ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x))))))
59	58	oprabbidv 4922	. . . . . . . . . . . 12 |- (G = if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1))) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))} = {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x))))})
60	55	eqeq2d 1895	. . . . . . . . . . . . . . 15 |- (G = if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1))) -> (w = (((1 - y) x. (G` x)) + (y x. x)) <-> w = (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x))))
61	60	anbi2d 678	. . . . . . . . . . . . . 14 |- (G = if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1))) -> (((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (G` x)) + (y x. x))) <-> ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x)))))
62	61	oprabbidv 4922	. . . . . . . . . . . . 13 |- (G = if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1))) -> {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (G` x)) + (y x. x)))} = {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x)))})
63	62	coeq2d 4128	. . . . . . . . . . . 12 |- (G = if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1))) -> (F o. {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (G` x)) + (y x. x)))}) = (F o. {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x)))}))
64	59, 63	eqeq12d 1899	. . . . . . . . . . 11 |- (G = if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1))) -> ({<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))} = (F o. {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (G` x)) + (y x. x)))}) <-> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x))))} = (F o. {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x)))})))
65	64	imbi2d 674	. . . . . . . . . 10 |- (G = if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1))) -> ((F Fn (0[,]1) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))} = (F o. {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (G` x)) + (y x. x)))})) <-> (F Fn (0[,]1) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x))))} = (F o. {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x)))}))))
66		lincmb01icc 15879	. . . . . . . . . . . . . 14 |- ((0 e. RR /\ 1 e. RR) -> (((if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x) e. (0[,]1) /\ x e. (0[,]1) /\ y e. (0[,]1)) -> (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x)) e. (0[,]1)))
67	16, 17, 66	mp2an 761	. . . . . . . . . . . . 13 |- (((if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x) e. (0[,]1) /\ x e. (0[,]1) /\ y e. (0[,]1)) -> (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x)) e. (0[,]1))
68	67	3expa 1067	. . . . . . . . . . . 12 |- ((((if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x) e. (0[,]1) /\ x e. (0[,]1)) /\ y e. (0[,]1)) -> (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x)) e. (0[,]1))
69		f1oi 4671	. . . . . . . . . . . . . . . 16 |- ( _I |` (0[,]1)):(0[,]1)-1-1-onto->(0[,]1)
70		f1of 4635	. . . . . . . . . . . . . . . 16 |- (( _I |` (0[,]1)):(0[,]1)-1-1-onto->(0[,]1) -> ( _I |` (0[,]1)):(0[,]1)-->(0[,]1))
71	69, 70	ax-mp 7	. . . . . . . . . . . . . . 15 |- ( _I |` (0[,]1)):(0[,]1)-->(0[,]1)
72	71	elimf 4561	. . . . . . . . . . . . . 14 |- if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1))):(0[,]1)-->(0[,]1)
73	72	ffvelrni 4788	. . . . . . . . . . . . 13 |- (x e. (0[,]1) -> (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x) e. (0[,]1))
74	73	ancri 321	. . . . . . . . . . . 12 |- (x e. (0[,]1) -> ((if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x) e. (0[,]1) /\ x e. (0[,]1)))
75	68, 74	sylan 497	. . . . . . . . . . 11 |- ((x e. (0[,]1) /\ y e. (0[,]1)) -> (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x)) e. (0[,]1))
76		eqid 1884	. . . . . . . . . . 11 |- {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x)))} = {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x)))}
77		eqid 1884	. . . . . . . . . . 11 |- {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x))))} = {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x))))}
78	75, 76, 77	oprabco 10159	. . . . . . . . . 10 |- (F Fn (0[,]1) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x))))} = (F o. {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (if(G:(0[,]1)-->(0[,]1), G, ( _I |` (0[,]1)))` x)) + (y x. x)))}))
79	65, 78	dedth 3011	. . . . . . . . 9 |- (G:(0[,]1)-->(0[,]1) -> (F Fn (0[,]1) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))} = (F o. {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (G` x)) + (y x. x)))})))
80	52, 79	mpan9 521	. . . . . . . 8 |- ((F:(0[,]1)-->U.J /\ G:(0[,]1)-->(0[,]1)) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))} = (F o. {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (G` x)) + (y x. x)))}))
81	80, 28, 30	syl2an 503	. . . . . . 7 |- (((J e. Top /\ F e. (II Cn J)) /\ G e. (II Cn II)) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))} = (F o. {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (G` x)) + (y x. x)))}))
82	1, 1	txtopi 15909	. . . . . . . . . . 11 |- (II X.t II) e. Top
83	82	a1i 8	. . . . . . . . . 10 |- (J e. Top -> (II X.t II) e. Top)
84	1	a1i 8	. . . . . . . . . 10 |- (J e. Top -> II e. Top)
85		id 73	. . . . . . . . . 10 |- (J e. Top -> J e. Top)
86	83, 84, 85	3jca 1050	. . . . . . . . 9 |- (J e. Top -> ((II X.t II) e. Top /\ II e. Top /\ J e. Top))
87	86	ad2antrr 440	. . . . . . . 8 |- (((J e. Top /\ F e. (II Cn J)) /\ G e. (II Cn II)) -> ((II X.t II) e. Top /\ II e. Top /\ J e. Top))
88		fveq1 4680	. . . . . . . . . . . . . . . 16 |- (G = if(G e. (II Cn II), G, ( _I |` (0[,]1))) -> (G` x) = (if(G e. (II Cn II), G, ( _I |` (0[,]1)))` x))
89	88	opreq2d 4898	. . . . . . . . . . . . . . 15 |- (G = if(G e. (II Cn II), G, ( _I |` (0[,]1))) -> ((1 - y) x. (G` x)) = ((1 - y) x. (if(G e. (II Cn II), G, ( _I |` (0[,]1)))` x)))
90	89	opreq1d 4897	. . . . . . . . . . . . . 14 |- (G = if(G e. (II Cn II), G, ( _I |` (0[,]1))) -> (((1 - y) x. (G` x)) + (y x. x)) = (((1 - y) x. (if(G e. (II Cn II), G, ( _I |` (0[,]1)))` x)) + (y x. x)))
91	90	eqeq2d 1895	. . . . . . . . . . . . 13 |- (G = if(G e. (II Cn II), G, ( _I |` (0[,]1))) -> (w = (((1 - y) x. (G` x)) + (y x. x)) <-> w = (((1 - y) x. (if(G e. (II Cn II), G, ( _I |` (0[,]1)))` x)) + (y x. x))))
92	91	anbi2d 678	. . . . . . . . . . . 12 |- (G = if(G e. (II Cn II), G, ( _I |` (0[,]1))) -> (((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (G` x)) + (y x. x))) <-> ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (if(G e. (II Cn II), G, ( _I |` (0[,]1)))` x)) + (y x. x)))))
93	92	oprabbidv 4922	. . . . . . . . . . 11 |- (G = if(G e. (II Cn II), G, ( _I |` (0[,]1))) -> {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (G` x)) + (y x. x)))} = {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (if(G e. (II Cn II), G, ( _I |` (0[,]1)))` x)) + (y x. x)))})
94	93	eleq1d 1963	. . . . . . . . . 10 |- (G = if(G e. (II Cn II), G, ( _I |` (0[,]1))) -> ({<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (G` x)) + (y x. x)))} e. ((II X.t II) Cn II) <-> {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (if(G e. (II Cn II), G, ( _I |` (0[,]1)))` x)) + (y x. x)))} e. ((II X.t II) Cn II)))
95	25	idcn 9042	. . . . . . . . . . . . 13 |- (II e. Top -> ( _I |` (0[,]1)) e. (II Cn II))
96	1, 95	ax-mp 7	. . . . . . . . . . . 12 |- ( _I |` (0[,]1)) e. (II Cn II)
97	96	elimel 3025	. . . . . . . . . . 11 |- if(G e. (II Cn II), G, ( _I |` (0[,]1))) e. (II Cn II)
98		eqid 1884	. . . . . . . . . . 11 |- {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (if(G e. (II Cn II), G, ( _I |` (0[,]1)))` x)) + (y x. x)))} = {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (if(G e. (II Cn II), G, ( _I |` (0[,]1)))` x)) + (y x. x)))}
99	97, 98	reparphtlem2 16064	. . . . . . . . . 10 |- {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (if(G e. (II Cn II), G, ( _I |` (0[,]1)))` x)) + (y x. x)))} e. ((II X.t II) Cn II)
100	94, 99	dedth 3011	. . . . . . . . 9 |- (G e. (II Cn II) -> {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (G` x)) + (y x. x)))} e. ((II X.t II) Cn II))
101	100	adantl 424	. . . . . . . 8 |- (((J e. Top /\ F e. (II Cn J)) /\ G e. (II Cn II)) -> {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (G` x)) + (y x. x)))} e. ((II X.t II) Cn II))
102		simplr 449	. . . . . . . 8 |- (((J e. Top /\ F e. (II Cn J)) /\ G e. (II Cn II)) -> F e. (II Cn J))
103		cnco 9045	. . . . . . . 8 |- ((((II X.t II) e. Top /\ II e. Top /\ J e. Top) /\ ({<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (G` x)) + (y x. x)))} e. ((II X.t II) Cn II) /\ F e. (II Cn J))) -> (F o. {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (G` x)) + (y x. x)))}) e. ((II X.t II) Cn J))
104	87, 101, 102, 103	syl12anc 1098	. . . . . . 7 |- (((J e. Top /\ F e. (II Cn J)) /\ G e. (II Cn II)) -> (F o. {<.<.x, y>., w>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ w = (((1 - y) x. (G` x)) + (y x. x)))}) e. ((II X.t II) Cn J))
105	81, 104	eqeltrd 1971	. . . . . 6 |- (((J e. Top /\ F e. (II Cn J)) /\ G e. (II Cn II)) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))} e. ((II X.t II) Cn J))
106	105	3ad2antr1 1041	. . . . 5 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))} e. ((II X.t II) Cn J))
107		ffvelrn 4787	. . . . . . . . . . 11 |- ((G:(0[,]1)-->(0[,]1) /\ s e. (0[,]1)) -> (G` s) e. (0[,]1))
108		mulid2 6578	. . . . . . . . . . . . . . . 16 |- ((G` s) e. CC -> (1 x. (G` s)) = (G` s))
109		ax1cn 6422	. . . . . . . . . . . . . . . . . 18 |- 1 e. CC
110	109	subid1i 6552	. . . . . . . . . . . . . . . . 17 |- (1 - 0) = 1
111	110	opreq1i 4892	. . . . . . . . . . . . . . . 16 |- ((1 - 0) x. (G` s)) = (1 x. (G` s))
112	108, 111	syl5eq 1940	. . . . . . . . . . . . . . 15 |- ((G` s) e. CC -> ((1 - 0) x. (G` s)) = (G` s))
113		mul02 6607	. . . . . . . . . . . . . . 15 |- (s e. CC -> (0 x. s) = 0)
114	112, 113	opreqan12rd 4903	. . . . . . . . . . . . . 14 |- ((s e. CC /\ (G` s) e. CC) -> (((1 - 0) x. (G` s)) + (0 x. s)) = ((G` s) + 0))
115		ax0id 6434	. . . . . . . . . . . . . . 15 |- ((G` s) e. CC -> ((G` s) + 0) = (G` s))
116	115	adantl 424	. . . . . . . . . . . . . 14 |- ((s e. CC /\ (G` s) e. CC) -> ((G` s) + 0) = (G` s))
117	114, 116	eqtrd 1925	. . . . . . . . . . . . 13 |- ((s e. CC /\ (G` s) e. CC) -> (((1 - 0) x. (G` s)) + (0 x. s)) = (G` s))
118		iccssre 7565	. . . . . . . . . . . . . . . 16 |- ((0 e. RR /\ 1 e. RR) -> (0[,]1) C_ RR)
119	16, 17, 118	mp2an 761	. . . . . . . . . . . . . . 15 |- (0[,]1) C_ RR
120	119	sseli 2617	. . . . . . . . . . . . . 14 |- (s e. (0[,]1) -> s e. RR)
121	120	recnd 6468	. . . . . . . . . . . . 13 |- (s e. (0[,]1) -> s e. CC)
122	119	sseli 2617	. . . . . . . . . . . . . 14 |- ((G` s) e. (0[,]1) -> (G` s) e. RR)
123	122	recnd 6468	. . . . . . . . . . . . 13 |- ((G` s) e. (0[,]1) -> (G` s) e. CC)
124	117, 121, 123	syl2an 503	. . . . . . . . . . . 12 |- ((s e. (0[,]1) /\ (G` s) e. (0[,]1)) -> (((1 - 0) x. (G` s)) + (0 x. s)) = (G` s))
125	124	adantll 428	. . . . . . . . . . 11 |- (((G:(0[,]1)-->(0[,]1) /\ s e. (0[,]1)) /\ (G` s) e. (0[,]1)) -> (((1 - 0) x. (G` s)) + (0 x. s)) = (G` s))
126	107, 125	mpdan 768	. . . . . . . . . 10 |- ((G:(0[,]1)-->(0[,]1) /\ s e. (0[,]1)) -> (((1 - 0) x. (G` s)) + (0 x. s)) = (G` s))
127	30	adantl 424	. . . . . . . . . . . 12 |- ((J e. Top /\ G e. (II Cn II)) -> G:(0[,]1)-->(0[,]1))
128	127	3ad2antr1 1041	. . . . . . . . . . 11 |- ((J e. Top /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> G:(0[,]1)-->(0[,]1))
129	128	adantlr 429	. . . . . . . . . 10 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> G:(0[,]1)-->(0[,]1))
130	126, 129	sylan 497	. . . . . . . . 9 |- ((((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) /\ s e. (0[,]1)) -> (((1 - 0) x. (G` s)) + (0 x. s)) = (G` s))
131	130	fveq2d 4685	. . . . . . . 8 |- ((((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) /\ s e. (0[,]1)) -> (F` (((1 - 0) x. (G` s)) + (0 x. s))) = (F` (G` s)))
132		eqid 1884	. . . . . . . . . . 11 |- {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))} = {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}
133	132	reparphtlem1 16063	. . . . . . . . . 10 |- ((s e. (0[,]1) /\ 0 e. (0[,]1)) -> (s{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}0) = (F` (((1 - 0) x. (G` s)) + (0 x. s))))
134	21, 133	mpan2 760	. . . . . . . . 9 |- (s e. (0[,]1) -> (s{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}0) = (F` (((1 - 0) x. (G` s)) + (0 x. s))))
135	134	adantl 424	. . . . . . . 8 |- ((((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) /\ s e. (0[,]1)) -> (s{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}0) = (F` (((1 - 0) x. (G` s)) + (0 x. s))))
136		fvco 4736	. . . . . . . . . . . . . 14 |- ((Fun F /\ Fun G /\ s e. dom G) -> ((F o. G)` s) = (F` (G` s)))
137	136	3expb 1068	. . . . . . . . . . . . 13 |- ((Fun F /\ (Fun G /\ s e. dom G)) -> ((F o. G)` s) = (F` (G` s)))
138	14	adantr 425	. . . . . . . . . . . . . 14 |- ((G:(0[,]1)-->(0[,]1) /\ s e. (0[,]1)) -> Fun G)
139	15	eleq2d 1964	. . . . . . . . . . . . . . 15 |- (G:(0[,]1)-->(0[,]1) -> (s e. dom G <-> s e. (0[,]1)))
140	139	biimpar 461	. . . . . . . . . . . . . 14 |- ((G:(0[,]1)-->(0[,]1) /\ s e. (0[,]1)) -> s e. dom G)
141	138, 140	jca 310	. . . . . . . . . . . . 13 |- ((G:(0[,]1)-->(0[,]1) /\ s e. (0[,]1)) -> (Fun G /\ s e. dom G))
142	137, 13, 141	syl2an 503	. . . . . . . . . . . 12 |- ((F:(0[,]1)-->U.J /\ (G:(0[,]1)-->(0[,]1) /\ s e. (0[,]1))) -> ((F o. G)` s) = (F` (G` s)))
143	142	expr 418	. . . . . . . . . . 11 |- ((F:(0[,]1)-->U.J /\ G:(0[,]1)-->(0[,]1)) -> (s e. (0[,]1) -> ((F o. G)` s) = (F` (G` s))))
144	143, 28, 30	syl2an 503	. . . . . . . . . 10 |- (((J e. Top /\ F e. (II Cn J)) /\ G e. (II Cn II)) -> (s e. (0[,]1) -> ((F o. G)` s) = (F` (G` s))))
145	144	3ad2antr1 1041	. . . . . . . . 9 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> (s e. (0[,]1) -> ((F o. G)` s) = (F` (G` s))))
146	145	imp 377	. . . . . . . 8 |- ((((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) /\ s e. (0[,]1)) -> ((F o. G)` s) = (F` (G` s)))
147	131, 135, 146	3eqtr4d 1937	. . . . . . 7 |- ((((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) /\ s e. (0[,]1)) -> (s{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}0) = ((F o. G)` s))
148	132	reparphtlem1 16063	. . . . . . . . . 10 |- ((s e. (0[,]1) /\ 1 e. (0[,]1)) -> (s{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}1) = (F` (((1 - 1) x. (G` s)) + (1 x. s))))
149	39, 148	mpan2 760	. . . . . . . . 9 |- (s e. (0[,]1) -> (s{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}1) = (F` (((1 - 1) x. (G` s)) + (1 x. s))))
150	149	adantl 424	. . . . . . . 8 |- ((((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) /\ s e. (0[,]1)) -> (s{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}1) = (F` (((1 - 1) x. (G` s)) + (1 x. s))))
151		mul02 6607	. . . . . . . . . . . . . . . 16 |- ((G` s) e. CC -> (0 x. (G` s)) = 0)
152	109	subidi 6551	. . . . . . . . . . . . . . . . 17 |- (1 - 1) = 0
153	152	opreq1i 4892	. . . . . . . . . . . . . . . 16 |- ((1 - 1) x. (G` s)) = (0 x. (G` s))
154	151, 153	syl5eq 1940	. . . . . . . . . . . . . . 15 |- ((G` s) e. CC -> ((1 - 1) x. (G` s)) = 0)
155		mulid2 6578	. . . . . . . . . . . . . . 15 |- (s e. CC -> (1 x. s) = s)
156	154, 155	opreqan12rd 4903	. . . . . . . . . . . . . 14 |- ((s e. CC /\ (G` s) e. CC) -> (((1 - 1) x. (G` s)) + (1 x. s)) = (0 + s))
157		addid2 6482	. . . . . . . . . . . . . . 15 |- (s e. CC -> (0 + s) = s)
158	157	adantr 425	. . . . . . . . . . . . . 14 |- ((s e. CC /\ (G` s) e. CC) -> (0 + s) = s)
159	156, 158	eqtrd 1925	. . . . . . . . . . . . 13 |- ((s e. CC /\ (G` s) e. CC) -> (((1 - 1) x. (G` s)) + (1 x. s)) = s)
160	159, 121, 123	syl2an 503	. . . . . . . . . . . 12 |- ((s e. (0[,]1) /\ (G` s) e. (0[,]1)) -> (((1 - 1) x. (G` s)) + (1 x. s)) = s)
161	160	adantll 428	. . . . . . . . . . 11 |- (((G:(0[,]1)-->(0[,]1) /\ s e. (0[,]1)) /\ (G` s) e. (0[,]1)) -> (((1 - 1) x. (G` s)) + (1 x. s)) = s)
162	107, 161	mpdan 768	. . . . . . . . . 10 |- ((G:(0[,]1)-->(0[,]1) /\ s e. (0[,]1)) -> (((1 - 1) x. (G` s)) + (1 x. s)) = s)
163	162, 129	sylan 497	. . . . . . . . 9 |- ((((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) /\ s e. (0[,]1)) -> (((1 - 1) x. (G` s)) + (1 x. s)) = s)
164	163	fveq2d 4685	. . . . . . . 8 |- ((((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) /\ s e. (0[,]1)) -> (F` (((1 - 1) x. (G` s)) + (1 x. s))) = (F` s))
165	150, 164	eqtrd 1925	. . . . . . 7 |- ((((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) /\ s e. (0[,]1)) -> (s{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}1) = (F` s))
166		opreq2 4890	. . . . . . . . . . . . . . . . 17 |- ((G` 0) = 0 -> ((1 - s) x. (G` 0)) = ((1 - s) x. 0))
167		subcl 6524	. . . . . . . . . . . . . . . . . . 19 |- ((1 e. CC /\ s e. CC) -> (1 - s) e. CC)
168	109, 167	mpan 759	. . . . . . . . . . . . . . . . . 18 |- (s e. CC -> (1 - s) e. CC)
169		mul01 6606	. . . . . . . . . . . . . . . . . 18 |- ((1 - s) e. CC -> ((1 - s) x. 0) = 0)
170	168, 169	syl 12	. . . . . . . . . . . . . . . . 17 |- (s e. CC -> ((1 - s) x. 0) = 0)
171	166, 170	sylan9eq 1948	. . . . . . . . . . . . . . . 16 |- (((G` 0) = 0 /\ s e. CC) -> ((1 - s) x. (G` 0)) = 0)
172		mul01 6606	. . . . . . . . . . . . . . . . 17 |- (s e. CC -> (s x. 0) = 0)
173	172	adantl 424	. . . . . . . . . . . . . . . 16 |- (((G` 0) = 0 /\ s e. CC) -> (s x. 0) = 0)
174	171, 173	opreq12d 4900	. . . . . . . . . . . . . . 15 |- (((G` 0) = 0 /\ s e. CC) -> (((1 - s) x. (G` 0)) + (s x. 0)) = (0 + 0))
175		0cn 6481	. . . . . . . . . . . . . . . 16 |- 0 e. CC
176	175	addid1i 6483	. . . . . . . . . . . . . . 15 |- (0 + 0) = 0
177	174, 176	syl6eq 1944	. . . . . . . . . . . . . 14 |- (((G` 0) = 0 /\ s e. CC) -> (((1 - s) x. (G` 0)) + (s x. 0)) = 0)
178	177, 121	sylan2 500	. . . . . . . . . . . . 13 |- (((G` 0) = 0 /\ s e. (0[,]1)) -> (((1 - s) x. (G` 0)) + (s x. 0)) = 0)
179		simpl 346	. . . . . . . . . . . . 13 |- (((G` 0) = 0 /\ s e. (0[,]1)) -> (G` 0) = 0)
180	178, 179	eqtr4d 1928	. . . . . . . . . . . 12 |- (((G` 0) = 0 /\ s e. (0[,]1)) -> (((1 - s) x. (G` 0)) + (s x. 0)) = (G` 0))
181	180	3ad2antl2 1039	. . . . . . . . . . 11 |- (((G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1) /\ s e. (0[,]1)) -> (((1 - s) x. (G` 0)) + (s x. 0)) = (G` 0))
182	181	adantll 428	. . . . . . . . . 10 |- ((((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) /\ s e. (0[,]1)) -> (((1 - s) x. (G` 0)) + (s x. 0)) = (G` 0))
183	182	fveq2d 4685	. . . . . . . . 9 |- ((((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) /\ s e. (0[,]1)) -> (F` (((1 - s) x. (G` 0)) + (s x. 0))) = (F` (G` 0)))
184	132	reparphtlem1 16063	. . . . . . . . . . 11 |- ((0 e. (0[,]1) /\ s e. (0[,]1)) -> (0{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}s) = (F` (((1 - s) x. (G` 0)) + (s x. 0))))
185	21, 184	mpan 759	. . . . . . . . . 10 |- (s e. (0[,]1) -> (0{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}s) = (F` (((1 - s) x. (G` 0)) + (s x. 0))))
186	185	adantl 424	. . . . . . . . 9 |- ((((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) /\ s e. (0[,]1)) -> (0{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}s) = (F` (((1 - s) x. (G` 0)) + (s x. 0))))
187	32	adantr 425	. . . . . . . . 9 |- ((((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) /\ s e. (0[,]1)) -> ((F o. G)` 0) = (F` (G` 0)))
188	183, 186, 187	3eqtr4d 1937	. . . . . . . 8 |- ((((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) /\ s e. (0[,]1)) -> (0{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}s) = ((F o. G)` 0))
189		opreq2 4890	. . . . . . . . . . . . . . . . 17 |- ((G` 1) = 1 -> ((1 - s) x. (G` 1)) = ((1 - s) x. 1))
190		ax1id 6435	. . . . . . . . . . . . . . . . . 18 |- ((1 - s) e. CC -> ((1 - s) x. 1) = (1 - s))
191	168, 190	syl 12	. . . . . . . . . . . . . . . . 17 |- (s e. CC -> ((1 - s) x. 1) = (1 - s))
192	189, 191	sylan9eq 1948	. . . . . . . . . . . . . . . 16 |- (((G` 1) = 1 /\ s e. CC) -> ((1 - s) x. (G` 1)) = (1 - s))
193		ax1id 6435	. . . . . . . . . . . . . . . . 17 |- (s e. CC -> (s x. 1) = s)
194	193	adantl 424	. . . . . . . . . . . . . . . 16 |- (((G` 1) = 1 /\ s e. CC) -> (s x. 1) = s)
195	192, 194	opreq12d 4900	. . . . . . . . . . . . . . 15 |- (((G` 1) = 1 /\ s e. CC) -> (((1 - s) x. (G` 1)) + (s x. 1)) = ((1 - s) + s))
196		npcan 6559	. . . . . . . . . . . . . . . . 17 |- ((1 e. CC /\ s e. CC) -> ((1 - s) + s) = 1)
197	109, 196	mpan 759	. . . . . . . . . . . . . . . 16 |- (s e. CC -> ((1 - s) + s) = 1)
198	197	adantl 424	. . . . . . . . . . . . . . 15 |- (((G` 1) = 1 /\ s e. CC) -> ((1 - s) + s) = 1)
199	195, 198	eqtrd 1925	. . . . . . . . . . . . . 14 |- (((G` 1) = 1 /\ s e. CC) -> (((1 - s) x. (G` 1)) + (s x. 1)) = 1)
200	199, 121	sylan2 500	. . . . . . . . . . . . 13 |- (((G` 1) = 1 /\ s e. (0[,]1)) -> (((1 - s) x. (G` 1)) + (s x. 1)) = 1)
201		simpl 346	. . . . . . . . . . . . 13 |- (((G` 1) = 1 /\ s e. (0[,]1)) -> (G` 1) = 1)
202	200, 201	eqtr4d 1928	. . . . . . . . . . . 12 |- (((G` 1) = 1 /\ s e. (0[,]1)) -> (((1 - s) x. (G` 1)) + (s x. 1)) = (G` 1))
203	202	3ad2antl3 1040	. . . . . . . . . . 11 |- (((G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1) /\ s e. (0[,]1)) -> (((1 - s) x. (G` 1)) + (s x. 1)) = (G` 1))
204	203	adantll 428	. . . . . . . . . 10 |- ((((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) /\ s e. (0[,]1)) -> (((1 - s) x. (G` 1)) + (s x. 1)) = (G` 1))
205	204	fveq2d 4685	. . . . . . . . 9 |- ((((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) /\ s e. (0[,]1)) -> (F` (((1 - s) x. (G` 1)) + (s x. 1))) = (F` (G` 1)))
206	132	reparphtlem1 16063	. . . . . . . . . . 11 |- ((1 e. (0[,]1) /\ s e. (0[,]1)) -> (1{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}s) = (F` (((1 - s) x. (G` 1)) + (s x. 1))))
207	39, 206	mpan 759	. . . . . . . . . 10 |- (s e. (0[,]1) -> (1{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}s) = (F` (((1 - s) x. (G` 1)) + (s x. 1))))
208	207	adantl 424	. . . . . . . . 9 |- ((((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) /\ s e. (0[,]1)) -> (1{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}s) = (F` (((1 - s) x. (G` 1)) + (s x. 1))))
209	44	adantr 425	. . . . . . . . 9 |- ((((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) /\ s e. (0[,]1)) -> ((F o. G)` 1) = (F` (G` 1)))
210	205, 208, 209	3eqtr4d 1937	. . . . . . . 8 |- ((((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) /\ s e. (0[,]1)) -> (1{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}s) = ((F o. G)` 1))
211	188, 210	jca 310	. . . . . . 7 |- ((((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) /\ s e. (0[,]1)) -> ((0{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}s) = ((F o. G)` 0) /\ (1{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}s) = ((F o. G)` 1)))
212	147, 165, 211	jca31 311	. . . . . 6 |- ((((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) /\ s e. (0[,]1)) -> (((s{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}0) = ((F o. G)` s) /\ (s{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}1) = (F` s)) /\ ((0{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}s) = ((F o. G)` 0) /\ (1{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}s) = ((F o. G)` 1))))
213	212	r19.21aiva 2176	. . . . 5 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> A.s e. (0[,]1)(((s{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}0) = ((F o. G)` s) /\ (s{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}1) = (F` s)) /\ ((0{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}s) = ((F o. G)` 0) /\ (1{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))}s) = ((F o. G)` 1))))
214	51, 106, 213	mpbir2and 802	. . . 4 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))} e. ((F o. G)(PHtpy` J)F))
215		ne0i 2881	. . . 4 |- ({<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = (F` (((1 - y) x. (G` x)) + (y x. x))))} e. ((F o. G)(PHtpy` J)F) -> ((F o. G)(PHtpy` J)F) =/= (/))
216	214, 215	syl 12	. . 3 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> ((F o. G)(PHtpy` J)F) =/= (/))
217	10, 48, 216	jca31 311	. 2 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> ((((F o. G) e. (II Cn J) /\ F e. (II Cn J)) /\ (((F o. G)` 0) = (F` 0) /\ ((F o. G)` 1) = (F` 1))) /\ ((F o. G)(PHtpy` J)F) =/= (/)))
218		isphtpc2 16060	. . 3 |- ((J e. Top /\ F e. (II Cn J)) -> ((F o. G)(~=ph` J)F <-> ((((F o. G) e. (II Cn J) /\ F e. (II Cn J)) /\ (((F o. G)` 0) = (F` 0) /\ ((F o. G)` 1) = (F` 1))) /\ ((F o. G)(PHtpy` J)F) =/= (/))))
219	218	adantr 425	. 2 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> ((F o. G)(~=ph` J)F <-> ((((F o. G) e. (II Cn J) /\ F e. (II Cn J)) /\ (((F o. G)` 0) = (F` 0) /\ ((F o. G)` 1) = (F` 1))) /\ ((F o. G)(PHtpy` J)F) =/= (/))))
220	217, 219	mpbird 213	1 |- (((J e. Top /\ F e. (II Cn J)) /\ (G e. (II Cn II) /\ (G` 0) = 0 /\ (G` 1) = 1)) -> (F o. G)(~=ph` J)F)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105   C_ wss 2593  (/)c0 2875  ifcif 2982  U.cuni 3177   class class class wbr 3338   _I cid 3582  dom cdm 3986   |` cres 3988   o. ccom 3990  Fun wfun 3992   Fn wfn 3993  -->wf 3994  -1-1-onto->wf1o 3997  ` cfv 3998  (class class class)co 4884  {copab2 4885  CCcc 6384  RRcr 6385  0cc0 6386  1c1 6387   + caddc 6389   x. cmul 6391   - cmin 6445   <_ cle 6448  [,]cicc 7527  Topctop 8857   X.t ctx 8930   Cn ccn 9028  IIcii 15865  PHtpycphtpy 16043  ~=phcphtpc 16044

This theorem is referenced by:  pcopt 16084  pcoass 16085

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-fl 7463  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-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

Copyright terms: Public domain