Theorem phtpyco 16056

Description: Concatenate two path homotopies.

Hypothesis

Ref	Expression
phtpyco.1	|- M = {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(y <_ (1 / 2), (xK(2 x. y)), (xL((2 x. y) - 1))))}

Assertion

Ref	Expression
phtpyco	|- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J)) /\ (((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1)))) -> ((K e. (F(PHtpy` J)G) /\ L e. (G(PHtpy` J)H)) -> M e. (F(PHtpy` J)H)))

Distinct variable groups:   x,J,y,z   x,L,y,z   x,F,y,z   x,G,y,z   x,H,y,z   x,K,y,z

Proof of Theorem phtpyco

Step	Hyp	Ref	Expression
1		simp1 876	. . . . . 6 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J)) /\ (((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1)))) -> J e. Top)
2		opreq1 4889	. . . . . . . . . . . . . 14 |- (r = w -> (rK0) = (wK0))
3		fveq2 4681	. . . . . . . . . . . . . 14 |- (r = w -> (F` r) = (F` w))
4	2, 3	eqeq12d 1899	. . . . . . . . . . . . 13 |- (r = w -> ((rK0) = (F` r) <-> (wK0) = (F` w)))
5		opreq1 4889	. . . . . . . . . . . . . 14 |- (r = w -> (rK1) = (wK1))
6		fveq2 4681	. . . . . . . . . . . . . 14 |- (r = w -> (G` r) = (G` w))
7	5, 6	eqeq12d 1899	. . . . . . . . . . . . 13 |- (r = w -> ((rK1) = (G` r) <-> (wK1) = (G` w)))
8	4, 7	anbi12d 690	. . . . . . . . . . . 12 |- (r = w -> (((rK0) = (F` r) /\ (rK1) = (G` r)) <-> ((wK0) = (F` w) /\ (wK1) = (G` w))))
9		opreq2 4890	. . . . . . . . . . . . . 14 |- (r = w -> (0Kr) = (0Kw))
10	9	eqeq1d 1892	. . . . . . . . . . . . 13 |- (r = w -> ((0Kr) = (F` 0) <-> (0Kw) = (F` 0)))
11		opreq2 4890	. . . . . . . . . . . . . 14 |- (r = w -> (1Kr) = (1Kw))
12	11	eqeq1d 1892	. . . . . . . . . . . . 13 |- (r = w -> ((1Kr) = (F` 1) <-> (1Kw) = (F` 1)))
13	10, 12	anbi12d 690	. . . . . . . . . . . 12 |- (r = w -> (((0Kr) = (F` 0) /\ (1Kr) = (F` 1)) <-> ((0Kw) = (F` 0) /\ (1Kw) = (F` 1))))
14	8, 13	anbi12d 690	. . . . . . . . . . 11 |- (r = w -> ((((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1))) <-> (((wK0) = (F` w) /\ (wK1) = (G` w)) /\ ((0Kw) = (F` 0) /\ (1Kw) = (F` 1)))))
15	14	rcla4v 2376	. . . . . . . . . 10 |- (w e. (0[,]1) -> (A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1))) -> (((wK0) = (F` w) /\ (wK1) = (G` w)) /\ ((0Kw) = (F` 0) /\ (1Kw) = (F` 1)))))
16		opreq1 4889	. . . . . . . . . . . . . 14 |- (s = w -> (sL0) = (wL0))
17		fveq2 4681	. . . . . . . . . . . . . 14 |- (s = w -> (G` s) = (G` w))
18	16, 17	eqeq12d 1899	. . . . . . . . . . . . 13 |- (s = w -> ((sL0) = (G` s) <-> (wL0) = (G` w)))
19		opreq1 4889	. . . . . . . . . . . . . 14 |- (s = w -> (sL1) = (wL1))
20		fveq2 4681	. . . . . . . . . . . . . 14 |- (s = w -> (H` s) = (H` w))
21	19, 20	eqeq12d 1899	. . . . . . . . . . . . 13 |- (s = w -> ((sL1) = (H` s) <-> (wL1) = (H` w)))
22	18, 21	anbi12d 690	. . . . . . . . . . . 12 |- (s = w -> (((sL0) = (G` s) /\ (sL1) = (H` s)) <-> ((wL0) = (G` w) /\ (wL1) = (H` w))))
23		opreq2 4890	. . . . . . . . . . . . . 14 |- (s = w -> (0Ls) = (0Lw))
24	23	eqeq1d 1892	. . . . . . . . . . . . 13 |- (s = w -> ((0Ls) = (G` 0) <-> (0Lw) = (G` 0)))
25		opreq2 4890	. . . . . . . . . . . . . 14 |- (s = w -> (1Ls) = (1Lw))
26	25	eqeq1d 1892	. . . . . . . . . . . . 13 |- (s = w -> ((1Ls) = (G` 1) <-> (1Lw) = (G` 1)))
27	24, 26	anbi12d 690	. . . . . . . . . . . 12 |- (s = w -> (((0Ls) = (G` 0) /\ (1Ls) = (G` 1)) <-> ((0Lw) = (G` 0) /\ (1Lw) = (G` 1))))
28	22, 27	anbi12d 690	. . . . . . . . . . 11 |- (s = w -> ((((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))) <-> (((wL0) = (G` w) /\ (wL1) = (H` w)) /\ ((0Lw) = (G` 0) /\ (1Lw) = (G` 1)))))
29	28	rcla4v 2376	. . . . . . . . . 10 |- (w e. (0[,]1) -> (A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))) -> (((wL0) = (G` w) /\ (wL1) = (H` w)) /\ ((0Lw) = (G` 0) /\ (1Lw) = (G` 1)))))
30	15, 29	anim12d 617	. . . . . . . . 9 |- (w e. (0[,]1) -> ((A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1))) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))) -> ((((wK0) = (F` w) /\ (wK1) = (G` w)) /\ ((0Kw) = (F` 0) /\ (1Kw) = (F` 1))) /\ (((wL0) = (G` w) /\ (wL1) = (H` w)) /\ ((0Lw) = (G` 0) /\ (1Lw) = (G` 1))))))
31		eqtr3 1907	. . . . . . . . . . 11 |- (((wK1) = (G` w) /\ (wL0) = (G` w)) -> (wK1) = (wL0))
32	31	ad2ant2lr 446	. . . . . . . . . 10 |- ((((wK0) = (F` w) /\ (wK1) = (G` w)) /\ ((wL0) = (G` w) /\ (wL1) = (H` w))) -> (wK1) = (wL0))
33	32	ad2ant2r 445	. . . . . . . . 9 |- (((((wK0) = (F` w) /\ (wK1) = (G` w)) /\ ((0Kw) = (F` 0) /\ (1Kw) = (F` 1))) /\ (((wL0) = (G` w) /\ (wL1) = (H` w)) /\ ((0Lw) = (G` 0) /\ (1Lw) = (G` 1)))) -> (wK1) = (wL0))
34	30, 33	syl6com 64	. . . . . . . 8 |- ((A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1))) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))) -> (w e. (0[,]1) -> (wK1) = (wL0)))
35	34	r19.21aiv 2175	. . . . . . 7 |- ((A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1))) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))) -> A.w e. (0[,]1)(wK1) = (wL0))
36	35	ad2ant2l 444	. . . . . 6 |- (((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))))) -> A.w e. (0[,]1)(wK1) = (wL0))
37	1, 36	anim12i 360	. . . . 5 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J)) /\ (((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1)))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) -> (J e. Top /\ A.w e. (0[,]1)(wK1) = (wL0)))
38		simpll 448	. . . . . . 7 |- (((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))))) -> K e. ((II X.t II) Cn J))
39		simprl 450	. . . . . . 7 |- (((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))))) -> L e. ((II X.t II) Cn J))
40	38, 39	jca 310	. . . . . 6 |- (((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))))) -> (K e. ((II X.t II) Cn J) /\ L e. ((II X.t II) Cn J)))
41	40	adantl 424	. . . . 5 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J)) /\ (((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1)))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) -> (K e. ((II X.t II) Cn J) /\ L e. ((II X.t II) Cn J)))
42		phtpyco.1	. . . . . 6 |- M = {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(y <_ (1 / 2), (xK(2 x. y)), (xL((2 x. y) - 1))))}
43	42	phtpycolem5 16055	. . . . 5 |- (((J e. Top /\ A.w e. (0[,]1)(wK1) = (wL0)) /\ (K e. ((II X.t II) Cn J) /\ L e. ((II X.t II) Cn J))) -> M e. ((II X.t II) Cn J))
44	37, 41, 43	syl11anc 524	. . . 4 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J)) /\ (((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1)))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) -> M e. ((II X.t II) Cn J))
45		0re 6603	. . . . . . . . . . . 12 |- 0 e. RR
46		2re 7163	. . . . . . . . . . . . 13 |- 2 e. RR
47		2ne0 7174	. . . . . . . . . . . . 13 |- 2 =/= 0
48	46, 47	rereccli 6979	. . . . . . . . . . . 12 |- (1 / 2) e. RR
49		elicc2 7560	. . . . . . . . . . . 12 |- ((0 e. RR /\ (1 / 2) e. RR) -> (0 e. (0[,](1 / 2)) <-> (0 e. RR /\ 0 <_ 0 /\ 0 <_ (1 / 2))))
50	45, 48, 49	mp2an 761	. . . . . . . . . . 11 |- (0 e. (0[,](1 / 2)) <-> (0 e. RR /\ 0 <_ 0 /\ 0 <_ (1 / 2)))
51	45	leidi 6790	. . . . . . . . . . 11 |- 0 <_ 0
52		halfgt0 7215	. . . . . . . . . . . 12 |- 0 < (1 / 2)
53	45, 48, 52	ltleii 6756	. . . . . . . . . . 11 |- 0 <_ (1 / 2)
54	50, 45, 51, 53	mpbir3an 1052	. . . . . . . . . 10 |- 0 e. (0[,](1 / 2))
55	42	phtpycolem1 16051	. . . . . . . . . 10 |- ((t e. (0[,]1) /\ 0 e. (0[,](1 / 2))) -> (tM0) = (tK(2 x. 0)))
56	54, 55	mpan2 760	. . . . . . . . 9 |- (t e. (0[,]1) -> (tM0) = (tK(2 x. 0)))
57	56	adantl 424	. . . . . . . 8 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. (0[,]1)) -> (tM0) = (tK(2 x. 0)))
58		opreq1 4889	. . . . . . . . . . . . . . . . 17 |- (r = t -> (rK0) = (tK0))
59		fveq2 4681	. . . . . . . . . . . . . . . . 17 |- (r = t -> (F` r) = (F` t))
60	58, 59	eqeq12d 1899	. . . . . . . . . . . . . . . 16 |- (r = t -> ((rK0) = (F` r) <-> (tK0) = (F` t)))
61		opreq1 4889	. . . . . . . . . . . . . . . . 17 |- (r = t -> (rK1) = (tK1))
62		fveq2 4681	. . . . . . . . . . . . . . . . 17 |- (r = t -> (G` r) = (G` t))
63	61, 62	eqeq12d 1899	. . . . . . . . . . . . . . . 16 |- (r = t -> ((rK1) = (G` r) <-> (tK1) = (G` t)))
64	60, 63	anbi12d 690	. . . . . . . . . . . . . . 15 |- (r = t -> (((rK0) = (F` r) /\ (rK1) = (G` r)) <-> ((tK0) = (F` t) /\ (tK1) = (G` t))))
65		opreq2 4890	. . . . . . . . . . . . . . . . 17 |- (r = t -> (0Kr) = (0Kt))
66	65	eqeq1d 1892	. . . . . . . . . . . . . . . 16 |- (r = t -> ((0Kr) = (F` 0) <-> (0Kt) = (F` 0)))
67		opreq2 4890	. . . . . . . . . . . . . . . . 17 |- (r = t -> (1Kr) = (1Kt))
68	67	eqeq1d 1892	. . . . . . . . . . . . . . . 16 |- (r = t -> ((1Kr) = (F` 1) <-> (1Kt) = (F` 1)))
69	66, 68	anbi12d 690	. . . . . . . . . . . . . . 15 |- (r = t -> (((0Kr) = (F` 0) /\ (1Kr) = (F` 1)) <-> ((0Kt) = (F` 0) /\ (1Kt) = (F` 1))))
70	64, 69	anbi12d 690	. . . . . . . . . . . . . 14 |- (r = t -> ((((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1))) <-> (((tK0) = (F` t) /\ (tK1) = (G` t)) /\ ((0Kt) = (F` 0) /\ (1Kt) = (F` 1)))))
71	70	rcla4cva 2379	. . . . . . . . . . . . 13 |- ((A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1))) /\ t e. (0[,]1)) -> (((tK0) = (F` t) /\ (tK1) = (G` t)) /\ ((0Kt) = (F` 0) /\ (1Kt) = (F` 1))))
72		simpll 448	. . . . . . . . . . . . 13 |- ((((tK0) = (F` t) /\ (tK1) = (G` t)) /\ ((0Kt) = (F` 0) /\ (1Kt) = (F` 1))) -> (tK0) = (F` t))
73	71, 72	syl 12	. . . . . . . . . . . 12 |- ((A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1))) /\ t e. (0[,]1)) -> (tK0) = (F` t))
74	73	adantll 428	. . . . . . . . . . 11 |- (((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ t e. (0[,]1)) -> (tK0) = (F` t))
75	74	adantlr 429	. . . . . . . . . 10 |- ((((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))))) /\ t e. (0[,]1)) -> (tK0) = (F` t))
76	75	adantll 428	. . . . . . . . 9 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. (0[,]1)) -> (tK0) = (F` t))
77		2cn 7164	. . . . . . . . . . 11 |- 2 e. CC
78	77	mul01i 6594	. . . . . . . . . 10 |- (2 x. 0) = 0
79	78	opreq2i 4893	. . . . . . . . 9 |- (tK(2 x. 0)) = (tK0)
80	76, 79	syl5eq 1940	. . . . . . . 8 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. (0[,]1)) -> (tK(2 x. 0)) = (F` t))
81	57, 80	eqtrd 1925	. . . . . . 7 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. (0[,]1)) -> (tM0) = (F` t))
82		1re 6598	. . . . . . . . . . . 12 |- 1 e. RR
83		elicc2 7560	. . . . . . . . . . . 12 |- (((1 / 2) e. RR /\ 1 e. RR) -> (1 e. ((1 / 2)[,]1) <-> (1 e. RR /\ (1 / 2) <_ 1 /\ 1 <_ 1)))
84	48, 82, 83	mp2an 761	. . . . . . . . . . 11 |- (1 e. ((1 / 2)[,]1) <-> (1 e. RR /\ (1 / 2) <_ 1 /\ 1 <_ 1))
85		halflt1 7216	. . . . . . . . . . . 12 |- (1 / 2) < 1
86	48, 82, 85	ltleii 6756	. . . . . . . . . . 11 |- (1 / 2) <_ 1
87	82	leidi 6790	. . . . . . . . . . 11 |- 1 <_ 1
88	84, 82, 86, 87	mpbir3an 1052	. . . . . . . . . 10 |- 1 e. ((1 / 2)[,]1)
89	42	phtpycolem2 16052	. . . . . . . . . 10 |- ((A.w e. (0[,]1)(wK1) = (wL0) /\ t e. (0[,]1) /\ 1 e. ((1 / 2)[,]1)) -> (tM1) = (tL((2 x. 1) - 1)))
90	88, 89	mp3an3 1180	. . . . . . . . 9 |- ((A.w e. (0[,]1)(wK1) = (wL0) /\ t e. (0[,]1)) -> (tM1) = (tL((2 x. 1) - 1)))
91	36	adantl 424	. . . . . . . . 9 |- (((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) -> A.w e. (0[,]1)(wK1) = (wL0))
92	90, 91	sylan 497	. . . . . . . 8 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. (0[,]1)) -> (tM1) = (tL((2 x. 1) - 1)))
93		opreq1 4889	. . . . . . . . . . . . . . . . 17 |- (s = t -> (sL0) = (tL0))
94		fveq2 4681	. . . . . . . . . . . . . . . . 17 |- (s = t -> (G` s) = (G` t))
95	93, 94	eqeq12d 1899	. . . . . . . . . . . . . . . 16 |- (s = t -> ((sL0) = (G` s) <-> (tL0) = (G` t)))
96		opreq1 4889	. . . . . . . . . . . . . . . . 17 |- (s = t -> (sL1) = (tL1))
97		fveq2 4681	. . . . . . . . . . . . . . . . 17 |- (s = t -> (H` s) = (H` t))
98	96, 97	eqeq12d 1899	. . . . . . . . . . . . . . . 16 |- (s = t -> ((sL1) = (H` s) <-> (tL1) = (H` t)))
99	95, 98	anbi12d 690	. . . . . . . . . . . . . . 15 |- (s = t -> (((sL0) = (G` s) /\ (sL1) = (H` s)) <-> ((tL0) = (G` t) /\ (tL1) = (H` t))))
100		opreq2 4890	. . . . . . . . . . . . . . . . 17 |- (s = t -> (0Ls) = (0Lt))
101	100	eqeq1d 1892	. . . . . . . . . . . . . . . 16 |- (s = t -> ((0Ls) = (G` 0) <-> (0Lt) = (G` 0)))
102		opreq2 4890	. . . . . . . . . . . . . . . . 17 |- (s = t -> (1Ls) = (1Lt))
103	102	eqeq1d 1892	. . . . . . . . . . . . . . . 16 |- (s = t -> ((1Ls) = (G` 1) <-> (1Lt) = (G` 1)))
104	101, 103	anbi12d 690	. . . . . . . . . . . . . . 15 |- (s = t -> (((0Ls) = (G` 0) /\ (1Ls) = (G` 1)) <-> ((0Lt) = (G` 0) /\ (1Lt) = (G` 1))))
105	99, 104	anbi12d 690	. . . . . . . . . . . . . 14 |- (s = t -> ((((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))) <-> (((tL0) = (G` t) /\ (tL1) = (H` t)) /\ ((0Lt) = (G` 0) /\ (1Lt) = (G` 1)))))
106	105	rcla4cva 2379	. . . . . . . . . . . . 13 |- ((A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))) /\ t e. (0[,]1)) -> (((tL0) = (G` t) /\ (tL1) = (H` t)) /\ ((0Lt) = (G` 0) /\ (1Lt) = (G` 1))))
107		simplr 449	. . . . . . . . . . . . 13 |- ((((tL0) = (G` t) /\ (tL1) = (H` t)) /\ ((0Lt) = (G` 0) /\ (1Lt) = (G` 1))) -> (tL1) = (H` t))
108	106, 107	syl 12	. . . . . . . . . . . 12 |- ((A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))) /\ t e. (0[,]1)) -> (tL1) = (H` t))
109	108	adantll 428	. . . . . . . . . . 11 |- (((L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))) /\ t e. (0[,]1)) -> (tL1) = (H` t))
110	109	adantll 428	. . . . . . . . . 10 |- ((((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))))) /\ t e. (0[,]1)) -> (tL1) = (H` t))
111	110	adantll 428	. . . . . . . . 9 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. (0[,]1)) -> (tL1) = (H` t))
112	77	mulid1i 6485	. . . . . . . . . . . 12 |- (2 x. 1) = 2
113	112	opreq1i 4892	. . . . . . . . . . 11 |- ((2 x. 1) - 1) = (2 - 1)
114		ax1cn 6422	. . . . . . . . . . . 12 |- 1 e. CC
115		df-2 7154	. . . . . . . . . . . . 13 |- 2 = (1 + 1)
116	115	eqcomi 1888	. . . . . . . . . . . 12 |- (1 + 1) = 2
117	77, 114, 114, 116	subaddrii 6529	. . . . . . . . . . 11 |- (2 - 1) = 1
118	113, 117	eqtri 1908	. . . . . . . . . 10 |- ((2 x. 1) - 1) = 1
119	118	opreq2i 4893	. . . . . . . . 9 |- (tL((2 x. 1) - 1)) = (tL1)
120	111, 119	syl5eq 1940	. . . . . . . 8 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. (0[,]1)) -> (tL((2 x. 1) - 1)) = (H` t))
121	92, 120	eqtrd 1925	. . . . . . 7 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. (0[,]1)) -> (tM1) = (H` t))
122		lt01 6871	. . . . . . . . . . . . . . 15 |- 0 < 1
123	45, 82, 122	ltleii 6756	. . . . . . . . . . . . . 14 |- 0 <_ 1
124		lbicc2 7573	. . . . . . . . . . . . . 14 |- ((0 e. RR /\ 1 e. RR /\ 0 <_ 1) -> 0 e. (0[,]1))
125	45, 82, 123, 124	mp3an 1191	. . . . . . . . . . . . 13 |- 0 e. (0[,]1)
126	42	phtpycolem1 16051	. . . . . . . . . . . . 13 |- ((0 e. (0[,]1) /\ t e. (0[,](1 / 2))) -> (0Mt) = (0K(2 x. t)))
127	125, 126	mpan 759	. . . . . . . . . . . 12 |- (t e. (0[,](1 / 2)) -> (0Mt) = (0K(2 x. t)))
128	127	adantl 424	. . . . . . . . . . 11 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. (0[,](1 / 2))) -> (0Mt) = (0K(2 x. t)))
129		opreq1 4889	. . . . . . . . . . . . . . . . . . . 20 |- (r = (2 x. t) -> (rK0) = ((2 x. t)K0))
130		fveq2 4681	. . . . . . . . . . . . . . . . . . . 20 |- (r = (2 x. t) -> (F` r) = (F` (2 x. t)))
131	129, 130	eqeq12d 1899	. . . . . . . . . . . . . . . . . . 19 |- (r = (2 x. t) -> ((rK0) = (F` r) <-> ((2 x. t)K0) = (F` (2 x. t))))
132		opreq1 4889	. . . . . . . . . . . . . . . . . . . 20 |- (r = (2 x. t) -> (rK1) = ((2 x. t)K1))
133		fveq2 4681	. . . . . . . . . . . . . . . . . . . 20 |- (r = (2 x. t) -> (G` r) = (G` (2 x. t)))
134	132, 133	eqeq12d 1899	. . . . . . . . . . . . . . . . . . 19 |- (r = (2 x. t) -> ((rK1) = (G` r) <-> ((2 x. t)K1) = (G` (2 x. t))))
135	131, 134	anbi12d 690	. . . . . . . . . . . . . . . . . 18 |- (r = (2 x. t) -> (((rK0) = (F` r) /\ (rK1) = (G` r)) <-> (((2 x. t)K0) = (F` (2 x. t)) /\ ((2 x. t)K1) = (G` (2 x. t)))))
136		opreq2 4890	. . . . . . . . . . . . . . . . . . . 20 |- (r = (2 x. t) -> (0Kr) = (0K(2 x. t)))
137	136	eqeq1d 1892	. . . . . . . . . . . . . . . . . . 19 |- (r = (2 x. t) -> ((0Kr) = (F` 0) <-> (0K(2 x. t)) = (F` 0)))
138		opreq2 4890	. . . . . . . . . . . . . . . . . . . 20 |- (r = (2 x. t) -> (1Kr) = (1K(2 x. t)))
139	138	eqeq1d 1892	. . . . . . . . . . . . . . . . . . 19 |- (r = (2 x. t) -> ((1Kr) = (F` 1) <-> (1K(2 x. t)) = (F` 1)))
140	137, 139	anbi12d 690	. . . . . . . . . . . . . . . . . 18 |- (r = (2 x. t) -> (((0Kr) = (F` 0) /\ (1Kr) = (F` 1)) <-> ((0K(2 x. t)) = (F` 0) /\ (1K(2 x. t)) = (F` 1))))
141	135, 140	anbi12d 690	. . . . . . . . . . . . . . . . 17 |- (r = (2 x. t) -> ((((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1))) <-> ((((2 x. t)K0) = (F` (2 x. t)) /\ ((2 x. t)K1) = (G` (2 x. t))) /\ ((0K(2 x. t)) = (F` 0) /\ (1K(2 x. t)) = (F` 1)))))
142	141	rcla4cva 2379	. . . . . . . . . . . . . . . 16 |- ((A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1))) /\ (2 x. t) e. (0[,]1)) -> ((((2 x. t)K0) = (F` (2 x. t)) /\ ((2 x. t)K1) = (G` (2 x. t))) /\ ((0K(2 x. t)) = (F` 0) /\ (1K(2 x. t)) = (F` 1))))
143		simprl 450	. . . . . . . . . . . . . . . 16 |- (((((2 x. t)K0) = (F` (2 x. t)) /\ ((2 x. t)K1) = (G` (2 x. t))) /\ ((0K(2 x. t)) = (F` 0) /\ (1K(2 x. t)) = (F` 1))) -> (0K(2 x. t)) = (F` 0))
144	142, 143	syl 12	. . . . . . . . . . . . . . 15 |- ((A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1))) /\ (2 x. t) e. (0[,]1)) -> (0K(2 x. t)) = (F` 0))
145		iihalf1 15872	. . . . . . . . . . . . . . 15 |- (t e. (0[,](1 / 2)) -> (2 x. t) e. (0[,]1))
146	144, 145	sylan2 500	. . . . . . . . . . . . . 14 |- ((A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1))) /\ t e. (0[,](1 / 2))) -> (0K(2 x. t)) = (F` 0))
147	146	adantll 428	. . . . . . . . . . . . 13 |- (((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ t e. (0[,](1 / 2))) -> (0K(2 x. t)) = (F` 0))
148	147	adantlr 429	. . . . . . . . . . . 12 |- ((((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))))) /\ t e. (0[,](1 / 2))) -> (0K(2 x. t)) = (F` 0))
149	148	adantll 428	. . . . . . . . . . 11 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. (0[,](1 / 2))) -> (0K(2 x. t)) = (F` 0))
150	128, 149	eqtrd 1925	. . . . . . . . . 10 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. (0[,](1 / 2))) -> (0Mt) = (F` 0))
151		opreq1 4889	. . . . . . . . . . . . . . . . . . . 20 |- (s = ((2 x. t) - 1) -> (sL0) = (((2 x. t) - 1)L0))
152		fveq2 4681	. . . . . . . . . . . . . . . . . . . 20 |- (s = ((2 x. t) - 1) -> (G` s) = (G` ((2 x. t) - 1)))
153	151, 152	eqeq12d 1899	. . . . . . . . . . . . . . . . . . 19 |- (s = ((2 x. t) - 1) -> ((sL0) = (G` s) <-> (((2 x. t) - 1)L0) = (G` ((2 x. t) - 1))))
154		opreq1 4889	. . . . . . . . . . . . . . . . . . . 20 |- (s = ((2 x. t) - 1) -> (sL1) = (((2 x. t) - 1)L1))
155		fveq2 4681	. . . . . . . . . . . . . . . . . . . 20 |- (s = ((2 x. t) - 1) -> (H` s) = (H` ((2 x. t) - 1)))
156	154, 155	eqeq12d 1899	. . . . . . . . . . . . . . . . . . 19 |- (s = ((2 x. t) - 1) -> ((sL1) = (H` s) <-> (((2 x. t) - 1)L1) = (H` ((2 x. t) - 1))))
157	153, 156	anbi12d 690	. . . . . . . . . . . . . . . . . 18 |- (s = ((2 x. t) - 1) -> (((sL0) = (G` s) /\ (sL1) = (H` s)) <-> ((((2 x. t) - 1)L0) = (G` ((2 x. t) - 1)) /\ (((2 x. t) - 1)L1) = (H` ((2 x. t) - 1)))))
158		opreq2 4890	. . . . . . . . . . . . . . . . . . . 20 |- (s = ((2 x. t) - 1) -> (0Ls) = (0L((2 x. t) - 1)))
159	158	eqeq1d 1892	. . . . . . . . . . . . . . . . . . 19 |- (s = ((2 x. t) - 1) -> ((0Ls) = (G` 0) <-> (0L((2 x. t) - 1)) = (G` 0)))
160		opreq2 4890	. . . . . . . . . . . . . . . . . . . 20 |- (s = ((2 x. t) - 1) -> (1Ls) = (1L((2 x. t) - 1)))
161	160	eqeq1d 1892	. . . . . . . . . . . . . . . . . . 19 |- (s = ((2 x. t) - 1) -> ((1Ls) = (G` 1) <-> (1L((2 x. t) - 1)) = (G` 1)))
162	159, 161	anbi12d 690	. . . . . . . . . . . . . . . . . 18 |- (s = ((2 x. t) - 1) -> (((0Ls) = (G` 0) /\ (1Ls) = (G` 1)) <-> ((0L((2 x. t) - 1)) = (G` 0) /\ (1L((2 x. t) - 1)) = (G` 1))))
163	157, 162	anbi12d 690	. . . . . . . . . . . . . . . . 17 |- (s = ((2 x. t) - 1) -> ((((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))) <-> (((((2 x. t) - 1)L0) = (G` ((2 x. t) - 1)) /\ (((2 x. t) - 1)L1) = (H` ((2 x. t) - 1))) /\ ((0L((2 x. t) - 1)) = (G` 0) /\ (1L((2 x. t) - 1)) = (G` 1)))))
164	163	rcla4cva 2379	. . . . . . . . . . . . . . . 16 |- ((A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))) /\ ((2 x. t) - 1) e. (0[,]1)) -> (((((2 x. t) - 1)L0) = (G` ((2 x. t) - 1)) /\ (((2 x. t) - 1)L1) = (H` ((2 x. t) - 1))) /\ ((0L((2 x. t) - 1)) = (G` 0) /\ (1L((2 x. t) - 1)) = (G` 1))))
165		simprl 450	. . . . . . . . . . . . . . . 16 |- ((((((2 x. t) - 1)L0) = (G` ((2 x. t) - 1)) /\ (((2 x. t) - 1)L1) = (H` ((2 x. t) - 1))) /\ ((0L((2 x. t) - 1)) = (G` 0) /\ (1L((2 x. t) - 1)) = (G` 1))) -> (0L((2 x. t) - 1)) = (G` 0))
166	164, 165	syl 12	. . . . . . . . . . . . . . 15 |- ((A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))) /\ ((2 x. t) - 1) e. (0[,]1)) -> (0L((2 x. t) - 1)) = (G` 0))
167		iihalf2 15873	. . . . . . . . . . . . . . 15 |- (t e. ((1 / 2)[,]1) -> ((2 x. t) - 1) e. (0[,]1))
168	166, 167	sylan2 500	. . . . . . . . . . . . . 14 |- ((A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))) /\ t e. ((1 / 2)[,]1)) -> (0L((2 x. t) - 1)) = (G` 0))
169	168	adantll 428	. . . . . . . . . . . . 13 |- (((L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))) /\ t e. ((1 / 2)[,]1)) -> (0L((2 x. t) - 1)) = (G` 0))
170	169	adantll 428	. . . . . . . . . . . 12 |- ((((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))))) /\ t e. ((1 / 2)[,]1)) -> (0L((2 x. t) - 1)) = (G` 0))
171	170	adantll 428	. . . . . . . . . . 11 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. ((1 / 2)[,]1)) -> (0L((2 x. t) - 1)) = (G` 0))
172	42	phtpycolem2 16052	. . . . . . . . . . . . 13 |- ((A.w e. (0[,]1)(wK1) = (wL0) /\ 0 e. (0[,]1) /\ t e. ((1 / 2)[,]1)) -> (0Mt) = (0L((2 x. t) - 1)))
173	125, 172	mp3an2 1179	. . . . . . . . . . . 12 |- ((A.w e. (0[,]1)(wK1) = (wL0) /\ t e. ((1 / 2)[,]1)) -> (0Mt) = (0L((2 x. t) - 1)))
174	173, 91	sylan 497	. . . . . . . . . . 11 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. ((1 / 2)[,]1)) -> (0Mt) = (0L((2 x. t) - 1)))
175		simpll 448	. . . . . . . . . . . 12 |- ((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) -> (F` 0) = (G` 0))
176	175	ad2antrr 440	. . . . . . . . . . 11 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. ((1 / 2)[,]1)) -> (F` 0) = (G` 0))
177	171, 174, 176	3eqtr4d 1937	. . . . . . . . . 10 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. ((1 / 2)[,]1)) -> (0Mt) = (F` 0))
178	150, 177	jaodan 471	. . . . . . . . 9 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ (t e. (0[,](1 / 2)) \/ t e. ((1 / 2)[,]1))) -> (0Mt) = (F` 0))
179		elicc2 7560	. . . . . . . . . . . . . 14 |- ((0 e. RR /\ 1 e. RR) -> ((1 / 2) e. (0[,]1) <-> ((1 / 2) e. RR /\ 0 <_ (1 / 2) /\ (1 / 2) <_ 1)))
180	45, 82, 179	mp2an 761	. . . . . . . . . . . . 13 |- ((1 / 2) e. (0[,]1) <-> ((1 / 2) e. RR /\ 0 <_ (1 / 2) /\ (1 / 2) <_ 1))
181	180, 48, 53, 86	mpbir3an 1052	. . . . . . . . . . . 12 |- (1 / 2) e. (0[,]1)
182		iccsplit 15854	. . . . . . . . . . . 12 |- ((0 e. RR /\ 1 e. RR /\ (1 / 2) e. (0[,]1)) -> (0[,]1) = ((0[,](1 / 2)) u. ((1 / 2)[,]1)))
183	45, 82, 181, 182	mp3an 1191	. . . . . . . . . . 11 |- (0[,]1) = ((0[,](1 / 2)) u. ((1 / 2)[,]1))
184	183	eleq2i 1961	. . . . . . . . . 10 |- (t e. (0[,]1) <-> t e. ((0[,](1 / 2)) u. ((1 / 2)[,]1)))
185		elun 2741	. . . . . . . . . 10 |- (t e. ((0[,](1 / 2)) u. ((1 / 2)[,]1)) <-> (t e. (0[,](1 / 2)) \/ t e. ((1 / 2)[,]1)))
186	184, 185	bitri 190	. . . . . . . . 9 |- (t e. (0[,]1) <-> (t e. (0[,](1 / 2)) \/ t e. ((1 / 2)[,]1)))
187	178, 186	sylan2b 501	. . . . . . . 8 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. (0[,]1)) -> (0Mt) = (F` 0))
188		ubicc2 7574	. . . . . . . . . . . . . 14 |- ((0 e. RR /\ 1 e. RR /\ 0 <_ 1) -> 1 e. (0[,]1))
189	45, 82, 123, 188	mp3an 1191	. . . . . . . . . . . . 13 |- 1 e. (0[,]1)
190	42	phtpycolem1 16051	. . . . . . . . . . . . 13 |- ((1 e. (0[,]1) /\ t e. (0[,](1 / 2))) -> (1Mt) = (1K(2 x. t)))
191	189, 190	mpan 759	. . . . . . . . . . . 12 |- (t e. (0[,](1 / 2)) -> (1Mt) = (1K(2 x. t)))
192	191	adantl 424	. . . . . . . . . . 11 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. (0[,](1 / 2))) -> (1Mt) = (1K(2 x. t)))
193		simprr 451	. . . . . . . . . . . . . . . 16 |- (((((2 x. t)K0) = (F` (2 x. t)) /\ ((2 x. t)K1) = (G` (2 x. t))) /\ ((0K(2 x. t)) = (F` 0) /\ (1K(2 x. t)) = (F` 1))) -> (1K(2 x. t)) = (F` 1))
194	142, 193	syl 12	. . . . . . . . . . . . . . 15 |- ((A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1))) /\ (2 x. t) e. (0[,]1)) -> (1K(2 x. t)) = (F` 1))
195	194, 145	sylan2 500	. . . . . . . . . . . . . 14 |- ((A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1))) /\ t e. (0[,](1 / 2))) -> (1K(2 x. t)) = (F` 1))
196	195	adantll 428	. . . . . . . . . . . . 13 |- (((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ t e. (0[,](1 / 2))) -> (1K(2 x. t)) = (F` 1))
197	196	adantlr 429	. . . . . . . . . . . 12 |- ((((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))))) /\ t e. (0[,](1 / 2))) -> (1K(2 x. t)) = (F` 1))
198	197	adantll 428	. . . . . . . . . . 11 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. (0[,](1 / 2))) -> (1K(2 x. t)) = (F` 1))
199	192, 198	eqtrd 1925	. . . . . . . . . 10 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. (0[,](1 / 2))) -> (1Mt) = (F` 1))
200		simprr 451	. . . . . . . . . . . . . . . 16 |- ((((((2 x. t) - 1)L0) = (G` ((2 x. t) - 1)) /\ (((2 x. t) - 1)L1) = (H` ((2 x. t) - 1))) /\ ((0L((2 x. t) - 1)) = (G` 0) /\ (1L((2 x. t) - 1)) = (G` 1))) -> (1L((2 x. t) - 1)) = (G` 1))
201	164, 200	syl 12	. . . . . . . . . . . . . . 15 |- ((A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))) /\ ((2 x. t) - 1) e. (0[,]1)) -> (1L((2 x. t) - 1)) = (G` 1))
202	201, 167	sylan2 500	. . . . . . . . . . . . . 14 |- ((A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))) /\ t e. ((1 / 2)[,]1)) -> (1L((2 x. t) - 1)) = (G` 1))
203	202	adantll 428	. . . . . . . . . . . . 13 |- (((L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))) /\ t e. ((1 / 2)[,]1)) -> (1L((2 x. t) - 1)) = (G` 1))
204	203	adantll 428	. . . . . . . . . . . 12 |- ((((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))))) /\ t e. ((1 / 2)[,]1)) -> (1L((2 x. t) - 1)) = (G` 1))
205	204	adantll 428	. . . . . . . . . . 11 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. ((1 / 2)[,]1)) -> (1L((2 x. t) - 1)) = (G` 1))
206	42	phtpycolem2 16052	. . . . . . . . . . . . 13 |- ((A.w e. (0[,]1)(wK1) = (wL0) /\ 1 e. (0[,]1) /\ t e. ((1 / 2)[,]1)) -> (1Mt) = (1L((2 x. t) - 1)))
207	189, 206	mp3an2 1179	. . . . . . . . . . . 12 |- ((A.w e. (0[,]1)(wK1) = (wL0) /\ t e. ((1 / 2)[,]1)) -> (1Mt) = (1L((2 x. t) - 1)))
208	207, 91	sylan 497	. . . . . . . . . . 11 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. ((1 / 2)[,]1)) -> (1Mt) = (1L((2 x. t) - 1)))
209		simplr 449	. . . . . . . . . . . 12 |- ((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) -> (F` 1) = (G` 1))
210	209	ad2antrr 440	. . . . . . . . . . 11 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. ((1 / 2)[,]1)) -> (F` 1) = (G` 1))
211	205, 208, 210	3eqtr4d 1937	. . . . . . . . . 10 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. ((1 / 2)[,]1)) -> (1Mt) = (F` 1))
212	199, 211	jaodan 471	. . . . . . . . 9 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ (t e. (0[,](1 / 2)) \/ t e. ((1 / 2)[,]1))) -> (1Mt) = (F` 1))
213	212, 186	sylan2b 501	. . . . . . . 8 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. (0[,]1)) -> (1Mt) = (F` 1))
214	187, 213	jca 310	. . . . . . 7 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. (0[,]1)) -> ((0Mt) = (F` 0) /\ (1Mt) = (F` 1)))
215	81, 121, 214	jca31 311	. . . . . 6 |- ((((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) /\ t e. (0[,]1)) -> (((tM0) = (F` t) /\ (tM1) = (H` t)) /\ ((0Mt) = (F` 0) /\ (1Mt) = (F` 1))))
216	215	r19.21aiva 2176	. . . . 5 |- (((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) -> A.t e. (0[,]1)(((tM0) = (F` t) /\ (tM1) = (H` t)) /\ ((0Mt) = (F` 0) /\ (1Mt) = (F` 1))))
217	216	3ad2antl3 1040	. . . 4 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J)) /\ (((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1)))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) -> A.t e. (0[,]1)(((tM0) = (F` t) /\ (tM1) = (H` t)) /\ ((0Mt) = (F` 0) /\ (1Mt) = (F` 1))))
218	44, 217	jca 310	. . 3 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J)) /\ (((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1)))) /\ ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))) -> (M e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tM0) = (F` t) /\ (tM1) = (H` t)) /\ ((0Mt) = (F` 0) /\ (1Mt) = (F` 1)))))
219	218	ex 402	. 2 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J)) /\ (((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1)))) -> (((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))))) -> (M e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tM0) = (F` t) /\ (tM1) = (H` t)) /\ ((0Mt) = (F` 0) /\ (1Mt) = (F` 1))))))
220		id 73	. . . . . 6 |- ((J e. Top /\ F e. (II Cn J) /\ G e. (II Cn J)) -> (J e. Top /\ F e. (II Cn J) /\ G e. (II Cn J)))
221	220	3adant3r3 1079	. . . . 5 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J))) -> (J e. Top /\ F e. (II Cn J) /\ G e. (II Cn J)))
222	221	3adant3 896	. . . 4 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J)) /\ (((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1)))) -> (J e. Top /\ F e. (II Cn J) /\ G e. (II Cn J)))
223		simp3l 904	. . . 4 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J)) /\ (((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1)))) -> ((F` 0) = (G` 0) /\ (F` 1) = (G` 1)))
224		isphtpy 16048	. . . 4 |- (((J e. Top /\ F e. (II Cn J) /\ G e. (II Cn J)) /\ ((F` 0) = (G` 0) /\ (F` 1) = (G` 1))) -> (K e. (F(PHtpy` J)G) <-> (K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1))))))
225	222, 223, 224	syl11anc 524	. . 3 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J)) /\ (((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1)))) -> (K e. (F(PHtpy` J)G) <-> (K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1))))))
226		id 73	. . . . . 6 |- ((J e. Top /\ G e. (II Cn J) /\ H e. (II Cn J)) -> (J e. Top /\ G e. (II Cn J) /\ H e. (II Cn J)))
227	226	3adant3r1 1077	. . . . 5 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J))) -> (J e. Top /\ G e. (II Cn J) /\ H e. (II Cn J)))
228	227	3adant3 896	. . . 4 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J)) /\ (((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1)))) -> (J e. Top /\ G e. (II Cn J) /\ H e. (II Cn J)))
229		simp3r 905	. . . 4 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J)) /\ (((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1)))) -> ((G` 0) = (H` 0) /\ (G` 1) = (H` 1)))
230		isphtpy 16048	. . . 4 |- (((J e. Top /\ G e. (II Cn J) /\ H e. (II Cn J)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) -> (L e. (G(PHtpy` J)H) <-> (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))))))
231	228, 229, 230	syl11anc 524	. . 3 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J)) /\ (((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1)))) -> (L e. (G(PHtpy` J)H) <-> (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1))))))
232	225, 231	anbi12d 690	. 2 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J)) /\ (((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1)))) -> ((K e. (F(PHtpy` J)G) /\ L e. (G(PHtpy` J)H)) <-> ((K e. ((II X.t II) Cn J) /\ A.r e. (0[,]1)(((rK0) = (F` r) /\ (rK1) = (G` r)) /\ ((0Kr) = (F` 0) /\ (1Kr) = (F` 1)))) /\ (L e. ((II X.t II) Cn J) /\ A.s e. (0[,]1)(((sL0) = (G` s) /\ (sL1) = (H` s)) /\ ((0Ls) = (G` 0) /\ (1Ls) = (G` 1)))))))
233		id 73	. . . . 5 |- ((J e. Top /\ F e. (II Cn J) /\ H e. (II Cn J)) -> (J e. Top /\ F e. (II Cn J) /\ H e. (II Cn J)))
234	233	3adant3r2 1078	. . . 4 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J))) -> (J e. Top /\ F e. (II Cn J) /\ H e. (II Cn J)))
235	234	3adant3 896	. . 3 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J)) /\ (((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1)))) -> (J e. Top /\ F e. (II Cn J) /\ H e. (II Cn J)))
236		eqtr 1904	. . . . . 6 |- (((F` 0) = (G` 0) /\ (G` 0) = (H` 0)) -> (F` 0) = (H` 0))
237		eqtr 1904	. . . . . 6 |- (((F` 1) = (G` 1) /\ (G` 1) = (H` 1)) -> (F` 1) = (H` 1))
238	236, 237	anim12i 360	. . . . 5 |- ((((F` 0) = (G` 0) /\ (G` 0) = (H` 0)) /\ ((F` 1) = (G` 1) /\ (G` 1) = (H` 1))) -> ((F` 0) = (H` 0) /\ (F` 1) = (H` 1)))
239	238	an4s 566	. . . 4 |- ((((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1))) -> ((F` 0) = (H` 0) /\ (F` 1) = (H` 1)))
240	239	3ad2ant3 899	. . 3 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J)) /\ (((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1)))) -> ((F` 0) = (H` 0) /\ (F` 1) = (H` 1)))
241		isphtpy 16048	. . 3 |- (((J e. Top /\ F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) -> (M e. (F(PHtpy` J)H) <-> (M e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tM0) = (F` t) /\ (tM1) = (H` t)) /\ ((0Mt) = (F` 0) /\ (1Mt) = (F` 1))))))
242	235, 240, 241	syl11anc 524	. 2 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J)) /\ (((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1)))) -> (M e. (F(PHtpy` J)H) <-> (M e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tM0) = (F` t) /\ (tM1) = (H` t)) /\ ((0Mt) = (F` 0) /\ (1Mt) = (F` 1))))))
243	219, 232, 242	3imtr4d 602	1 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ H e. (II Cn J)) /\ (((F` 0) = (G` 0) /\ (F` 1) = (G` 1)) /\ ((G` 0) = (H` 0) /\ (G` 1) = (H` 1)))) -> ((K e. (F(PHtpy` J)G) /\ L e. (G(PHtpy` J)H)) -> M e. (F(PHtpy` J)H)))

Syntax hints:   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105   u. cun 2591  ifcif 2982   class class class wbr 3338  ` cfv 3998  (class class class)co 4884  {copab2 4885  RRcr 6385  0cc0 6386  1c1 6387   + caddc 6389   x. cmul 6391   - cmin 6445   / cdiv 6447   <_ cle 6448  2c2 7145  [,]cicc 7527  Topctop 8857   X.t ctx 8930   Cn ccn 9028  IIcii 15865  PHtpycphtpy 16043

This theorem is referenced by:  phtpcer 16062

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

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-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-ioo 7528  df-icc 7531  df-seq1 7721  df-exp 7812  df-sqr 7920  df-re 8001  df-im 8002  df-cj 8003  df-abs 8004  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-subsp 10243  df-ii 15866  df-phtpy 16045

Copyright terms: Public domain