Table of ContentsTable of Contents Mathbox for Jeff Madsen < Previous   Next >
Related theorems
Unicode version
Theorem pcohtpy 16083
Description: Homotopy invariance of path concatenation.
Assertion
Ref Expression
pcohtpy |- (((J e. Top /\ Y e. X) /\ (H e. A /\ K e. B) /\ (F` 1) = (G` 0)) -> ((F(~=ph` J)H /\ G(~=ph` J)K) -> (F(*p` J)G)(~=ph` J)(H(*p` J)K)))
Proof of Theorem pcohtpy
StepHypRef Expression
1 pcocn 16076 . . . . . . . . . . . . . . . . 17 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> (F(*p` J)G) e. (II Cn J))
21expcom 403 . . . . . . . . . . . . . . . 16 |- ((F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0)) -> (J e. Top -> (F(*p` J)G) e. (II Cn J)))
323expia 1069 . . . . . . . . . . . . . . 15 |- ((F e. (II Cn J) /\ G e. (II Cn J)) -> ((F` 1) = (G` 0) -> (J e. Top -> (F(*p` J)G) e. (II Cn J))))
43com13 37 . . . . . . . . . . . . . 14 |- (J e. Top -> ((F` 1) = (G` 0) -> ((F e. (II Cn J) /\ G e. (II Cn J)) -> (F(*p` J)G) e. (II Cn J))))
54imp31 389 . . . . . . . . . . . . 13 |- (((J e. Top /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ G e. (II Cn J))) -> (F(*p` J)G) e. (II Cn J))
65adantllr 433 . . . . . . . . . . . 12 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ G e. (II Cn J))) -> (F(*p` J)G) e. (II Cn J))
76adantrrr 439 . . . . . . . . . . 11 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ (G e. (II Cn J) /\ K e. (II Cn J)))) -> (F(*p` J)G) e. (II Cn J))
87adantrrr 439 . . . . . . . . . 10 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> (F(*p` J)G) e. (II Cn J))
98adantrrr 439 . . . . . . . . 9 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> (F(*p` J)G) e. (II Cn J))
109adantrlr 437 . . . . . . . 8 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((F e. (II Cn J) /\ H e. (II Cn J)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> (F(*p` J)G) e. (II Cn J))
1110adantrlr 437 . . . . . . 7 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> (F(*p` J)G) e. (II Cn J))
1211adantrlr 437 . . . . . 6 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> (F(*p` J)G) e. (II Cn J))
13 eqeq12 1896 . . . . . . . . . . . . . . . . . 18 |- (((F` 1) = (H` 1) /\ (G` 0) = (K` 0)) -> ((F` 1) = (G` 0) <-> (H` 1) = (K` 0)))
14 pcocn 16076 . . . . . . . . . . . . . . . . . . . . . 22 |- ((J e. Top /\ (H e. (II Cn J) /\ K e. (II Cn J) /\ (H` 1) = (K` 0))) -> (H(*p` J)K) e. (II Cn J))
1514adantlr 429 . . . . . . . . . . . . . . . . . . . . 21 |- (((J e. Top /\ Y e. X) /\ (H e. (II Cn J) /\ K e. (II Cn J) /\ (H` 1) = (K` 0))) -> (H(*p` J)K) e. (II Cn J))
1615expcom 403 . . . . . . . . . . . . . . . . . . . 20 |- ((H e. (II Cn J) /\ K e. (II Cn J) /\ (H` 1) = (K` 0)) -> ((J e. Top /\ Y e. X) -> (H(*p` J)K) e. (II Cn J)))
17163expia 1069 . . . . . . . . . . . . . . . . . . 19 |- ((H e. (II Cn J) /\ K e. (II Cn J)) -> ((H` 1) = (K` 0) -> ((J e. Top /\ Y e. X) -> (H(*p` J)K) e. (II Cn J))))
1817com3l 38 . . . . . . . . . . . . . . . . . 18 |- ((H` 1) = (K` 0) -> ((J e. Top /\ Y e. X) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> (H(*p` J)K) e. (II Cn J))))
1913, 18syl6bi 231 . . . . . . . . . . . . . . . . 17 |- (((F` 1) = (H` 1) /\ (G` 0) = (K` 0)) -> ((F` 1) = (G` 0) -> ((J e. Top /\ Y e. X) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> (H(*p` J)K) e. (II Cn J)))))
2019com23 36 . . . . . . . . . . . . . . . 16 |- (((F` 1) = (H` 1) /\ (G` 0) = (K` 0)) -> ((J e. Top /\ Y e. X) -> ((F` 1) = (G` 0) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> (H(*p` J)K) e. (II Cn J)))))
2120imp3a 388 . . . . . . . . . . . . . . 15 |- (((F` 1) = (H` 1) /\ (G` 0) = (K` 0)) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> (H(*p` J)K) e. (II Cn J))))
2221com23 36 . . . . . . . . . . . . . 14 |- (((F` 1) = (H` 1) /\ (G` 0) = (K` 0)) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> (H(*p` J)K) e. (II Cn J))))
2322ad2ant2lr 446 . . . . . . . . . . . . 13 |- ((((F` 0) = (H` 0) /\ (F` 1) = (H` 1)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> (H(*p` J)K) e. (II Cn J))))
2423com12 14 . . . . . . . . . . . 12 |- ((H e. (II Cn J) /\ K e. (II Cn J)) -> ((((F` 0) = (H` 0) /\ (F` 1) = (H` 1)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> (H(*p` J)K) e. (II Cn J))))
2524ad2ant2l 444 . . . . . . . . . . 11 |- (((F e. (II Cn J) /\ H e. (II Cn J)) /\ (G e. (II Cn J) /\ K e. (II Cn J))) -> ((((F` 0) = (H` 0) /\ (F` 1) = (H` 1)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> (H(*p` J)K) e. (II Cn J))))
2625imp 377 . . . . . . . . . 10 |- ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ (G e. (II Cn J) /\ K e. (II Cn J))) /\ (((F` 0) = (H` 0) /\ (F` 1) = (H` 1)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1)))) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> (H(*p` J)K) e. (II Cn J)))
2726an4s 566 . . . . . . . . 9 |- ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1)))) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> (H(*p` J)K) e. (II Cn J)))
2827impcom 378 . . . . . . . 8 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> (H(*p` J)K) e. (II Cn J))
2928adantrrr 439 . . . . . . 7 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> (H(*p` J)K) e. (II Cn J))
3029adantrlr 437 . . . . . 6 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> (H(*p` J)K) e. (II Cn J))
3112, 30jca 310 . . . . 5 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> ((F(*p` J)G) e. (II Cn J) /\ (H(*p` J)K) e. (II Cn J)))
32 simplrl 454 . . . . . . . 8 |- ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/)) -> (F` 0) = (H` 0))
3332ad2antrl 442 . . . . . . 7 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> (F` 0) = (H` 0))
34 pco0 16077 . . . . . . . . . . . . . . . . . 18 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> ((F(*p` J)G)` 0) = (F` 0))
3534adantlr 429 . . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ Y e. X) /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> ((F(*p` J)G)` 0) = (F` 0))
3635expcom 403 . . . . . . . . . . . . . . . 16 |- ((F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0)) -> ((J e. Top /\ Y e. X) -> ((F(*p` J)G)` 0) = (F` 0)))
37363expia 1069 . . . . . . . . . . . . . . 15 |- ((F e. (II Cn J) /\ G e. (II Cn J)) -> ((F` 1) = (G` 0) -> ((J e. Top /\ Y e. X) -> ((F(*p` J)G)` 0) = (F` 0))))
3837com13 37 . . . . . . . . . . . . . 14 |- ((J e. Top /\ Y e. X) -> ((F` 1) = (G` 0) -> ((F e. (II Cn J) /\ G e. (II Cn J)) -> ((F(*p` J)G)` 0) = (F` 0))))
3938imp31 389 . . . . . . . . . . . . 13 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ G e. (II Cn J))) -> ((F(*p` J)G)` 0) = (F` 0))
4039adantrrr 439 . . . . . . . . . . . 12 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ (G e. (II Cn J) /\ K e. (II Cn J)))) -> ((F(*p` J)G)` 0) = (F` 0))
4140adantrrr 439 . . . . . . . . . . 11 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> ((F(*p` J)G)` 0) = (F` 0))
4241adantrrr 439 . . . . . . . . . 10 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> ((F(*p` J)G)` 0) = (F` 0))
4342adantrlr 437 . . . . . . . . 9 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((F e. (II Cn J) /\ H e. (II Cn J)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> ((F(*p` J)G)` 0) = (F` 0))
4443adantrlr 437 . . . . . . . 8 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> ((F(*p` J)G)` 0) = (F` 0))
4544adantrlr 437 . . . . . . 7 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> ((F(*p` J)G)` 0) = (F` 0))
46 pco0 16077 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((J e. Top /\ (H e. (II Cn J) /\ K e. (II Cn J) /\ (H` 1) = (K` 0))) -> ((H(*p` J)K)` 0) = (H` 0))
4746adantlr 429 . . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Top /\ Y e. X) /\ (H e. (II Cn J) /\ K e. (II Cn J) /\ (H` 1) = (K` 0))) -> ((H(*p` J)K)` 0) = (H` 0))
4847expcom 403 . . . . . . . . . . . . . . . . . . . . 21 |- ((H e. (II Cn J) /\ K e. (II Cn J) /\ (H` 1) = (K` 0)) -> ((J e. Top /\ Y e. X) -> ((H(*p` J)K)` 0) = (H` 0)))
49483expia 1069 . . . . . . . . . . . . . . . . . . . 20 |- ((H e. (II Cn J) /\ K e. (II Cn J)) -> ((H` 1) = (K` 0) -> ((J e. Top /\ Y e. X) -> ((H(*p` J)K)` 0) = (H` 0))))
5049com3l 38 . . . . . . . . . . . . . . . . . . 19 |- ((H` 1) = (K` 0) -> ((J e. Top /\ Y e. X) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> ((H(*p` J)K)` 0) = (H` 0))))
5113, 50syl6bi 231 . . . . . . . . . . . . . . . . . 18 |- (((F` 1) = (H` 1) /\ (G` 0) = (K` 0)) -> ((F` 1) = (G` 0) -> ((J e. Top /\ Y e. X) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> ((H(*p` J)K)` 0) = (H` 0)))))
5251com23 36 . . . . . . . . . . . . . . . . 17 |- (((F` 1) = (H` 1) /\ (G` 0) = (K` 0)) -> ((J e. Top /\ Y e. X) -> ((F` 1) = (G` 0) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> ((H(*p` J)K)` 0) = (H` 0)))))
5352imp3a 388 . . . . . . . . . . . . . . . 16 |- (((F` 1) = (H` 1) /\ (G` 0) = (K` 0)) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> ((H(*p` J)K)` 0) = (H` 0))))
5453com23 36 . . . . . . . . . . . . . . 15 |- (((F` 1) = (H` 1) /\ (G` 0) = (K` 0)) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((H(*p` J)K)` 0) = (H` 0))))
5554ad2ant2lr 446 . . . . . . . . . . . . . 14 |- ((((F` 0) = (H` 0) /\ (F` 1) = (H` 1)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((H(*p` J)K)` 0) = (H` 0))))
5655com12 14 . . . . . . . . . . . . 13 |- ((H e. (II Cn J) /\ K e. (II Cn J)) -> ((((F` 0) = (H` 0) /\ (F` 1) = (H` 1)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((H(*p` J)K)` 0) = (H` 0))))
5756ad2ant2l 444 . . . . . . . . . . . 12 |- (((F e. (II Cn J) /\ H e. (II Cn J)) /\ (G e. (II Cn J) /\ K e. (II Cn J))) -> ((((F` 0) = (H` 0) /\ (F` 1) = (H` 1)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((H(*p` J)K)` 0) = (H` 0))))
5857imp 377 . . . . . . . . . . 11 |- ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ (G e. (II Cn J) /\ K e. (II Cn J))) /\ (((F` 0) = (H` 0) /\ (F` 1) = (H` 1)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1)))) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((H(*p` J)K)` 0) = (H` 0)))
5958an4s 566 . . . . . . . . . 10 |- ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1)))) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((H(*p` J)K)` 0) = (H` 0)))
6059impcom 378 . . . . . . . . 9 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> ((H(*p` J)K)` 0) = (H` 0))
6160adantrrr 439 . . . . . . . 8 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> ((H(*p` J)K)` 0) = (H` 0))
6261adantrlr 437 . . . . . . 7 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> ((H(*p` J)K)` 0) = (H` 0))
6333, 45, 623eqtr4d 1937 . . . . . 6 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> ((F(*p` J)G)` 0) = ((H(*p` J)K)` 0))
64 simplrr 455 . . . . . . . 8 |- ((((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)) -> (G` 1) = (K` 1))
6564ad2antll 443 . . . . . . 7 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> (G` 1) = (K` 1))
66 pco1 16078 . . . . . . . . . . . . . . . . . 18 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> ((F(*p` J)G)` 1) = (G` 1))
6766adantlr 429 . . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ Y e. X) /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> ((F(*p` J)G)` 1) = (G` 1))
6867expcom 403 . . . . . . . . . . . . . . . 16 |- ((F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0)) -> ((J e. Top /\ Y e. X) -> ((F(*p` J)G)` 1) = (G` 1)))
69683expia 1069 . . . . . . . . . . . . . . 15 |- ((F e. (II Cn J) /\ G e. (II Cn J)) -> ((F` 1) = (G` 0) -> ((J e. Top /\ Y e. X) -> ((F(*p` J)G)` 1) = (G` 1))))
7069com13 37 . . . . . . . . . . . . . 14 |- ((J e. Top /\ Y e. X) -> ((F` 1) = (G` 0) -> ((F e. (II Cn J) /\ G e. (II Cn J)) -> ((F(*p` J)G)` 1) = (G` 1))))
7170imp31 389 . . . . . . . . . . . . 13 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ G e. (II Cn J))) -> ((F(*p` J)G)` 1) = (G` 1))
7271adantrrr 439 . . . . . . . . . . . 12 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ (G e. (II Cn J) /\ K e. (II Cn J)))) -> ((F(*p` J)G)` 1) = (G` 1))
7372adantrrr 439 . . . . . . . . . . 11 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> ((F(*p` J)G)` 1) = (G` 1))
7473adantrrr 439 . . . . . . . . . 10 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> ((F(*p` J)G)` 1) = (G` 1))
7574adantrlr 437 . . . . . . . . 9 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((F e. (II Cn J) /\ H e. (II Cn J)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> ((F(*p` J)G)` 1) = (G` 1))
7675adantrlr 437 . . . . . . . 8 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> ((F(*p` J)G)` 1) = (G` 1))
7776adantrlr 437 . . . . . . 7 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> ((F(*p` J)G)` 1) = (G` 1))
78 pco1 16078 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((J e. Top /\ (H e. (II Cn J) /\ K e. (II Cn J) /\ (H` 1) = (K` 0))) -> ((H(*p` J)K)` 1) = (K` 1))
7978adantlr 429 . . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Top /\ Y e. X) /\ (H e. (II Cn J) /\ K e. (II Cn J) /\ (H` 1) = (K` 0))) -> ((H(*p` J)K)` 1) = (K` 1))
8079expcom 403 . . . . . . . . . . . . . . . . . . . . 21 |- ((H e. (II Cn J) /\ K e. (II Cn J) /\ (H` 1) = (K` 0)) -> ((J e. Top /\ Y e. X) -> ((H(*p` J)K)` 1) = (K` 1)))
81803expia 1069 . . . . . . . . . . . . . . . . . . . 20 |- ((H e. (II Cn J) /\ K e. (II Cn J)) -> ((H` 1) = (K` 0) -> ((J e. Top /\ Y e. X) -> ((H(*p` J)K)` 1) = (K` 1))))
8281com3l 38 . . . . . . . . . . . . . . . . . . 19 |- ((H` 1) = (K` 0) -> ((J e. Top /\ Y e. X) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> ((H(*p` J)K)` 1) = (K` 1))))
8313, 82syl6bi 231 . . . . . . . . . . . . . . . . . 18 |- (((F` 1) = (H` 1) /\ (G` 0) = (K` 0)) -> ((F` 1) = (G` 0) -> ((J e. Top /\ Y e. X) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> ((H(*p` J)K)` 1) = (K` 1)))))
8483com23 36 . . . . . . . . . . . . . . . . 17 |- (((F` 1) = (H` 1) /\ (G` 0) = (K` 0)) -> ((J e. Top /\ Y e. X) -> ((F` 1) = (G` 0) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> ((H(*p` J)K)` 1) = (K` 1)))))
8584imp3a 388 . . . . . . . . . . . . . . . 16 |- (((F` 1) = (H` 1) /\ (G` 0) = (K` 0)) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> ((H(*p` J)K)` 1) = (K` 1))))
8685com23 36 . . . . . . . . . . . . . . 15 |- (((F` 1) = (H` 1) /\ (G` 0) = (K` 0)) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((H(*p` J)K)` 1) = (K` 1))))
8786ad2ant2lr 446 . . . . . . . . . . . . . 14 |- ((((F` 0) = (H` 0) /\ (F` 1) = (H` 1)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((H(*p` J)K)` 1) = (K` 1))))
8887com12 14 . . . . . . . . . . . . 13 |- ((H e. (II Cn J) /\ K e. (II Cn J)) -> ((((F` 0) = (H` 0) /\ (F` 1) = (H` 1)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((H(*p` J)K)` 1) = (K` 1))))
8988ad2ant2l 444 . . . . . . . . . . . 12 |- (((F e. (II Cn J) /\ H e. (II Cn J)) /\ (G e. (II Cn J) /\ K e. (II Cn J))) -> ((((F` 0) = (H` 0) /\ (F` 1) = (H` 1)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((H(*p` J)K)` 1) = (K` 1))))
9089imp 377 . . . . . . . . . . 11 |- ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ (G e. (II Cn J) /\ K e. (II Cn J))) /\ (((F` 0) = (H` 0) /\ (F` 1) = (H` 1)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1)))) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((H(*p` J)K)` 1) = (K` 1)))
9190an4s 566 . . . . . . . . . 10 |- ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1)))) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((H(*p` J)K)` 1) = (K` 1)))
9291impcom 378 . . . . . . . . 9 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> ((H(*p` J)K)` 1) = (K` 1))
9392adantrrr 439 . . . . . . . 8 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> ((H(*p` J)K)` 1) = (K` 1))
9493adantrlr 437 . . . . . . 7 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> ((H(*p` J)K)` 1) = (K` 1))
9565, 77, 943eqtr4d 1937 . . . . . 6 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> ((F(*p` J)G)` 1) = ((H(*p` J)K)` 1))
9663, 95jca 310 . . . . 5 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> (((F(*p` J)G)` 0) = ((H(*p` J)K)` 0) /\ ((F(*p` J)G)` 1) = ((H(*p` J)K)` 1)))
97 eeanv 1707 . . . . . . . . . 10 |- (E.mE.n(m e. (F(PHtpy` J)H) /\ n e. (G(PHtpy` J)K)) <-> (E.m m e. (F(PHtpy` J)H) /\ E.n n e. (G(PHtpy` J)K)))
98 eqeq12 1896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((1mt) = (F` 1) /\ (0nt) = (G` 0)) -> ((1mt) = (0nt) <-> (F` 1) = (G` 0)))
9998biimprd 171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((1mt) = (F` 1) /\ (0nt) = (G` 0)) -> ((F` 1) = (G` 0) -> (1mt) = (0nt)))
10099ad2ant2lr 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((0mt) = (F` 0) /\ (1mt) = (F` 1)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))) -> ((F` 1) = (G` 0) -> (1mt) = (0nt)))
101100ad2ant2l 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) /\ (((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))) -> ((F` 1) = (G` 0) -> (1mt) = (0nt)))
102101com12 14 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((F` 1) = (G` 0) -> (((((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) /\ (((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))) -> (1mt) = (0nt)))
103102adantl 424 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((J e. Top /\ (F` 1) = (G` 0)) -> (((((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) /\ (((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))) -> (1mt) = (0nt)))
104103ralimdv 2172 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((J e. Top /\ (F` 1) = (G` 0)) -> (A.t e. (0[,]1)((((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) /\ (((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))) -> A.t e. (0[,]1)(1mt) = (0nt)))
105 eqid 1884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))} = {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}
106105pcohtpylem3 16082 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((J e. Top /\ (m e. ((II X.t II) Cn J) /\ n e. ((II X.t II) Cn J)) /\ A.t e. (0[,]1)(1mt) = (0nt)) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))} e. ((II X.t II) Cn J))
1071063exp 1066 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (J e. Top -> ((m e. ((II X.t II) Cn J) /\ n e. ((II X.t II) Cn J)) -> (A.t e. (0[,]1)(1mt) = (0nt) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))} e. ((II X.t II) Cn J))))
108107adantr 425 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((J e. Top /\ (F` 1) = (G` 0)) -> ((m e. ((II X.t II) Cn J) /\ n e. ((II X.t II) Cn J)) -> (A.t e. (0[,]1)(1mt) = (0nt) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))} e. ((II X.t II) Cn J))))
109108com23 36 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((J e. Top /\ (F` 1) = (G` 0)) -> (A.t e. (0[,]1)(1mt) = (0nt) -> ((m e. ((II X.t II) Cn J) /\ n e. ((II X.t II) Cn J)) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))} e. ((II X.t II) Cn J))))
110104, 109syld 30 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((J e. Top /\ (F` 1) = (G` 0)) -> (A.t e. (0[,]1)((((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) /\ (((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))) -> ((m e. ((II X.t II) Cn J) /\ n e. ((II X.t II) Cn J)) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))} e. ((II X.t II) Cn J))))
111 r19.26 2219 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (A.t e. (0[,]1)((((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) /\ (((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))) <-> (A.t e. (0[,]1)(((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))
112110, 111syl5ibr 224 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((J e. Top /\ (F` 1) = (G` 0)) -> ((A.t e. (0[,]1)(((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))) -> ((m e. ((II X.t II) Cn J) /\ n e. ((II X.t II) Cn J)) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))} e. ((II X.t II) Cn J))))
113112adantlr 429 . . . . . . . . . . . . . . . . . . . . . 22 |- (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((A.t e. (0[,]1)(((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))) -> ((m e. ((II X.t II) Cn J) /\ n e. ((II X.t II) Cn J)) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))} e. ((II X.t II) Cn J))))
114113com13 37 . . . . . . . . . . . . . . . . . . . . 21 |- ((m e. ((II X.t II) Cn J) /\ n e. ((II X.t II) Cn J)) -> ((A.t e. (0[,]1)(((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))} e. ((II X.t II) Cn J))))
115114imp 377 . . . . . . . . . . . . . . . . . . . 20 |- (((m e. ((II X.t II) Cn J) /\ n e. ((II X.t II) Cn J)) /\ (A.t e. (0[,]1)(((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))))) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))} e. ((II X.t II) Cn J)))
116115an4s 566 . . . . . . . . . . . . . . . . . . 19 |- (((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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))))) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))} e. ((II X.t II) Cn J)))
117116impcom 378 . . . . . . . . . . . . . . . . . 18 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))} e. ((II X.t II) Cn J))
118117adantlr 429 . . . . . . . . . . . . . . . . 17 |- (((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))} e. ((II X.t II) Cn J))
119 opreq1 4889 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (t = (2 x. u) -> (tm0) = ((2 x. u)m0))
120 fveq2 4681 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (t = (2 x. u) -> (F` t) = (F` (2 x. u)))
121119, 120eqeq12d 1899 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (t = (2 x. u) -> ((tm0) = (F` t) <-> ((2 x. u)m0) = (F` (2 x. u))))
122121rcla4cva 2379 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A.t e. (0[,]1)(tm0) = (F` t) /\ (2 x. u) e. (0[,]1)) -> ((2 x. u)m0) = (F` (2 x. u)))
123 simpll 448 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) -> (tm0) = (F` t))
124123ralimi 2168 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A.t e. (0[,]1)(((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) -> A.t e. (0[,]1)(tm0) = (F` t))
125 iihalf1 15872 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (u e. (0[,](1 / 2)) -> (2 x. u) e. (0[,]1))
126122, 124, 125syl2an 503 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A.t e. (0[,]1)(((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) /\ u e. (0[,](1 / 2))) -> ((2 x. u)m0) = (F` (2 x. u)))
127126adantll 428 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (((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)))) /\ u e. (0[,](1 / 2))) -> ((2 x. u)m0) = (F` (2 x. u)))
128127adantlr 429 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((((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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))))) /\ u e. (0[,](1 / 2))) -> ((2 x. u)m0) = (F` (2 x. u)))
129128adantll 428 . . . . . . . . . . . . . . . . . . . . . 22 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. (0[,](1 / 2))) -> ((2 x. u)m0) = (F` (2 x. u)))
130 0re 6603 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- 0 e. RR
131 1re 6598 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- 1 e. RR
132 elicc2 7560 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((0 e. RR /\ 1 e. RR) -> (0 e. (0[,]1) <-> (0 e. RR /\ 0 <_ 0 /\ 0 <_ 1)))
133130, 131, 132mp2an 761 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (0 e. (0[,]1) <-> (0 e. RR /\ 0 <_ 0 /\ 0 <_ 1))
134130leidi 6790 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- 0 <_ 0
135 lt01 6871 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- 0 < 1
136130, 131, 135ltleii 6756 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- 0 <_ 1
137133, 130, 134, 136mpbir3an 1052 . . . . . . . . . . . . . . . . . . . . . . . 24 |- 0 e. (0[,]1)
138105pcohtpylem1 16080 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((u e. (0[,](1 / 2)) /\ 0 e. (0[,]1)) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = ((2 x. u)m0))
139137, 138mpan2 760 . . . . . . . . . . . . . . . . . . . . . . 23 |- (u e. (0[,](1 / 2)) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = ((2 x. u)m0))
140139adantl 424 . . . . . . . . . . . . . . . . . . . . . 22 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. (0[,](1 / 2))) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = ((2 x. u)m0))
141 pcoval1 16074 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ u e. (0[,](1 / 2))) -> ((F(*p` J)G)` u) = (F` (2 x. u)))
142141ex 402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> (u e. (0[,](1 / 2)) -> ((F(*p` J)G)` u) = (F` (2 x. u))))
143142expcom 403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0)) -> (J e. Top -> (u e. (0[,](1 / 2)) -> ((F(*p` J)G)` u) = (F` (2 x. u)))))
1441433expia 1069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((F e. (II Cn J) /\ G e. (II Cn J)) -> ((F` 1) = (G` 0) -> (J e. Top -> (u e. (0[,](1 / 2)) -> ((F(*p` J)G)` u) = (F` (2 x. u))))))
145144com13 37 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (J e. Top -> ((F` 1) = (G` 0) -> ((F e. (II Cn J) /\ G e. (II Cn J)) -> (u e. (0[,](1 / 2)) -> ((F(*p` J)G)` u) = (F` (2 x. u))))))
146145imp31 389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((J e. Top /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ G e. (II Cn J))) -> (u e. (0[,](1 / 2)) -> ((F(*p` J)G)` u) = (F` (2 x. u))))
147146adantllr 433 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ G e. (II Cn J))) -> (u e. (0[,](1 / 2)) -> ((F(*p` J)G)` u) = (F` (2 x. u))))
148147adantrrr 439 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ (G e. (II Cn J) /\ K e. (II Cn J)))) -> (u e. (0[,](1 / 2)) -> ((F(*p` J)G)` u) = (F` (2 x. u))))
149148adantrrr 439 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> (u e. (0[,](1 / 2)) -> ((F(*p` J)G)` u) = (F` (2 x. u))))
150149adantrlr 437 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> (u e. (0[,](1 / 2)) -> ((F(*p` J)G)` u) = (F` (2 x. u))))
151150adantrlr 437 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> (u e. (0[,](1 / 2)) -> ((F(*p` J)G)` u) = (F` (2 x. u))))
152151adantr 425 . . . . . . . . . . . . . . . . . . . . . . 23 |- (((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) -> (u e. (0[,](1 / 2)) -> ((F(*p` J)G)` u) = (F` (2 x. u))))
153152imp 377 . . . . . . . . . . . . . . . . . . . . . 22 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. (0[,](1 / 2))) -> ((F(*p` J)G)` u) = (F` (2 x. u)))
154129, 140, 1533eqtr4d 1937 . . . . . . . . . . . . . . . . . . . . 21 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. (0[,](1 / 2))) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = ((F(*p` J)G)` u))
155 opreq1 4889 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (t = ((2 x. u) - 1) -> (tn0) = (((2 x. u) - 1)n0))
156 fveq2 4681 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (t = ((2 x. u) - 1) -> (G` t) = (G` ((2 x. u) - 1)))
157155, 156eqeq12d 1899 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (t = ((2 x. u) - 1) -> ((tn0) = (G` t) <-> (((2 x. u) - 1)n0) = (G` ((2 x. u) - 1))))
158157rcla4cva 2379 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A.t e. (0[,]1)(tn0) = (G` t) /\ ((2 x. u) - 1) e. (0[,]1)) -> (((2 x. u) - 1)n0) = (G` ((2 x. u) - 1)))
159 simpll 448 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))) -> (tn0) = (G` t))
160159ralimi 2168 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))) -> A.t e. (0[,]1)(tn0) = (G` t))
161 iihalf2 15873 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (u e. ((1 / 2)[,]1) -> ((2 x. u) - 1) e. (0[,]1))
162158, 160, 161syl2an 503 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))) /\ u e. ((1 / 2)[,]1)) -> (((2 x. u) - 1)n0) = (G` ((2 x. u) - 1)))
163162adantll 428 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (((n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))) /\ u e. ((1 / 2)[,]1)) -> (((2 x. u) - 1)n0) = (G` ((2 x. u) - 1)))
164163adantll 428 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((((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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))))) /\ u e. ((1 / 2)[,]1)) -> (((2 x. u) - 1)n0) = (G` ((2 x. u) - 1)))
165164adantll 428 . . . . . . . . . . . . . . . . . . . . . 22 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. ((1 / 2)[,]1)) -> (((2 x. u) - 1)n0) = (G` ((2 x. u) - 1)))
166 r19.28av 2226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((F` 1) = (G` 0) /\ A.t e. (0[,]1)((1mt) = (F` 1) /\ (0nt) = (G` 0))) -> A.t e. (0[,]1)((F` 1) = (G` 0) /\ ((1mt) = (F` 1) /\ (0nt) = (G` 0))))
167 simpl 346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((F` 1) = (G` 0) /\ ((1mt) = (F` 1) /\ (0nt) = (G` 0))) -> (F` 1) = (G` 0))
168 simprl 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((F` 1) = (G` 0) /\ ((1mt) = (F` 1) /\ (0nt) = (G` 0))) -> (1mt) = (F` 1))
169 simprr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((F` 1) = (G` 0) /\ ((1mt) = (F` 1) /\ (0nt) = (G` 0))) -> (0nt) = (G` 0))
170167, 168, 1693eqtr4d 1937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((F` 1) = (G` 0) /\ ((1mt) = (F` 1) /\ (0nt) = (G` 0))) -> (1mt) = (0nt))
171170ralimi 2168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (A.t e. (0[,]1)((F` 1) = (G` 0) /\ ((1mt) = (F` 1) /\ (0nt) = (G` 0))) -> A.t e. (0[,]1)(1mt) = (0nt))
172105pcohtpylem2 16081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((u e. ((1 / 2)[,]1) /\ 0 e. (0[,]1)) /\ A.t e. (0[,]1)(1mt) = (0nt)) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = (((2 x. u) - 1)n0))
173137, 172mpanl2 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((u e. ((1 / 2)[,]1) /\ A.t e. (0[,]1)(1mt) = (0nt)) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = (((2 x. u) - 1)n0))
174173expcom 403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (A.t e. (0[,]1)(1mt) = (0nt) -> (u e. ((1 / 2)[,]1) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = (((2 x. u) - 1)n0)))
175166, 171, 1743syl 24 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((F` 1) = (G` 0) /\ A.t e. (0[,]1)((1mt) = (F` 1) /\ (0nt) = (G` 0))) -> (u e. ((1 / 2)[,]1) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = (((2 x. u) - 1)n0)))
176 r19.26 2219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (A.t e. (0[,]1)((1mt) = (F` 1) /\ (0nt) = (G` 0)) <-> (A.t e. (0[,]1)(1mt) = (F` 1) /\ A.t e. (0[,]1)(0nt) = (G` 0)))
177176biimpri 169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((A.t e. (0[,]1)(1mt) = (F` 1) /\ A.t e. (0[,]1)(0nt) = (G` 0)) -> A.t e. (0[,]1)((1mt) = (F` 1) /\ (0nt) = (G` 0)))
178 simprr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) -> (1mt) = (F` 1))
179178ralimi 2168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (A.t e. (0[,]1)(((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) -> A.t e. (0[,]1)(1mt) = (F` 1))
180 simprl 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))) -> (0nt) = (G` 0))
181180ralimi 2168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))) -> A.t e. (0[,]1)(0nt) = (G` 0))
182177, 179, 181syl2an 503 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((A.t e. (0[,]1)(((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))) -> A.t e. (0[,]1)((1mt) = (F` 1) /\ (0nt) = (G` 0)))
183175, 182sylan2 500 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((F` 1) = (G` 0) /\ (A.t e. (0[,]1)(((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))))) -> (u e. ((1 / 2)[,]1) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = (((2 x. u) - 1)n0)))
184183adantrrl 438 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((F` 1) = (G` 0) /\ (A.t e. (0[,]1)(((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) -> (u e. ((1 / 2)[,]1) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = (((2 x. u) - 1)n0)))
185184adantrll 436 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F` 1) = (G` 0) /\ ((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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) -> (u e. ((1 / 2)[,]1) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = (((2 x. u) - 1)n0)))
186185adantlr 429 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((F` 1) = (G` 0) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) -> (u e. ((1 / 2)[,]1) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = (((2 x. u) - 1)n0)))
187186adantlll 432 . . . . . . . . . . . . . . . . . . . . . . 23 |- (((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) -> (u e. ((1 / 2)[,]1) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = (((2 x. u) - 1)n0)))
188187imp 377 . . . . . . . . . . . . . . . . . . . . . 22 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. ((1 / 2)[,]1)) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = (((2 x. u) - 1)n0))
189 pcoval2 16075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((J e. Top /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ u e. ((1 / 2)[,]1)) -> ((F(*p` J)G)` u) = (G` ((2 x. u) - 1)))
190189adantllr 433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((J e. Top /\ Y e. X) /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) /\ u e. ((1 / 2)[,]1)) -> ((F(*p` J)G)` u) = (G` ((2 x. u) - 1)))
191190ex 402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((J e. Top /\ Y e. X) /\ (F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0))) -> (u e. ((1 / 2)[,]1) -> ((F(*p` J)G)` u) = (G` ((2 x. u) - 1))))
192191expcom 403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0)) -> ((J e. Top /\ Y e. X) -> (u e. ((1 / 2)[,]1) -> ((F(*p` J)G)` u) = (G` ((2 x. u) - 1)))))
1931923expia 1069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((F e. (II Cn J) /\ G e. (II Cn J)) -> ((F` 1) = (G` 0) -> ((J e. Top /\ Y e. X) -> (u e. ((1 / 2)[,]1) -> ((F(*p` J)G)` u) = (G` ((2 x. u) - 1))))))
194193com13 37 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((J e. Top /\ Y e. X) -> ((F` 1) = (G` 0) -> ((F e. (II Cn J) /\ G e. (II Cn J)) -> (u e. ((1 / 2)[,]1) -> ((F(*p` J)G)` u) = (G` ((2 x. u) - 1))))))
195194imp31 389 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ G e. (II Cn J))) -> (u e. ((1 / 2)[,]1) -> ((F(*p` J)G)` u) = (G` ((2 x. u) - 1))))
196195adantrrr 439 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ (G e. (II Cn J) /\ K e. (II Cn J)))) -> (u e. ((1 / 2)[,]1) -> ((F(*p` J)G)` u) = (G` ((2 x. u) - 1))))
197196adantrrr 439 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> (u e. ((1 / 2)[,]1) -> ((F(*p` J)G)` u) = (G` ((2 x. u) - 1))))
198197adantrlr 437 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> (u e. ((1 / 2)[,]1) -> ((F(*p` J)G)` u) = (G` ((2 x. u) - 1))))
199198adantrlr 437 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> (u e. ((1 / 2)[,]1) -> ((F(*p` J)G)` u) = (G` ((2 x. u) - 1))))
200199adantr 425 . . . . . . . . . . . . . . . . . . . . . . 23 |- (((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) -> (u e. ((1 / 2)[,]1) -> ((F(*p` J)G)` u) = (G` ((2 x. u) - 1))))
201200imp 377 . . . . . . . . . . . . . . . . . . . . . 22 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. ((1 / 2)[,]1)) -> ((F(*p` J)G)` u) = (G` ((2 x. u) - 1)))
202165, 188, 2013eqtr4d 1937 . . . . . . . . . . . . . . . . . . . . 21 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. ((1 / 2)[,]1)) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = ((F(*p` J)G)` u))
203154, 202jaodan 471 . . . . . . . . . . . . . . . . . . . 20 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ (u e. (0[,](1 / 2)) \/ u e. ((1 / 2)[,]1))) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = ((F(*p` J)G)` u))
204 elicc2 7560 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((0 e. RR /\ 1 e. RR) -> ((1 / 2) e. (0[,]1) <-> ((1 / 2) e. RR /\ 0 <_ (1 / 2) /\ (1 / 2) <_ 1)))
205130, 131, 204mp2an 761 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((1 / 2) e. (0[,]1) <-> ((1 / 2) e. RR /\ 0 <_ (1 / 2) /\ (1 / 2) <_ 1))
206 2re 7163 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- 2 e. RR
207 2ne0 7174 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- 2 =/= 0
208206, 207rereccli 6979 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (1 / 2) e. RR
209 halfgt0 7215 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- 0 < (1 / 2)
210130, 208, 209ltleii 6756 . . . . . . . . . . . . . . . . . . . . . . . 24 |- 0 <_ (1 / 2)
211 halflt1 7216 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (1 / 2) < 1
212208, 131, 211ltleii 6756 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (1 / 2) <_ 1
213205, 208, 210, 212mpbir3an 1052 . . . . . . . . . . . . . . . . . . . . . . 23 |- (1 / 2) e. (0[,]1)
214 iccsplit 15854 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((0 e. RR /\ 1 e. RR /\ (1 / 2) e. (0[,]1)) -> (0[,]1) = ((0[,](1 / 2)) u. ((1 / 2)[,]1)))
215130, 131, 213, 214mp3an 1191 . . . . . . . . . . . . . . . . . . . . . 22 |- (0[,]1) = ((0[,](1 / 2)) u. ((1 / 2)[,]1))
216215eleq2i 1961 . . . . . . . . . . . . . . . . . . . . 21 |- (u e. (0[,]1) <-> u e. ((0[,](1 / 2)) u. ((1 / 2)[,]1)))
217 elun 2741 . . . . . . . . . . . . . . . . . . . . 21 |- (u e. ((0[,](1 / 2)) u. ((1 / 2)[,]1)) <-> (u e. (0[,](1 / 2)) \/ u e. ((1 / 2)[,]1)))
218216, 217bitri 190 . . . . . . . . . . . . . . . . . . . 20 |- (u e. (0[,]1) <-> (u e. (0[,](1 / 2)) \/ u e. ((1 / 2)[,]1)))
219203, 218sylan2b 501 . . . . . . . . . . . . . . . . . . 19 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. (0[,]1)) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = ((F(*p` J)G)` u))
220 opreq1 4889 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (t = (2 x. u) -> (tm1) = ((2 x. u)m1))
221 fveq2 4681 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (t = (2 x. u) -> (H` t) = (H` (2 x. u)))
222220, 221eqeq12d 1899 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (t = (2 x. u) -> ((tm1) = (H` t) <-> ((2 x. u)m1) = (H` (2 x. u))))
223222rcla4cva 2379 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A.t e. (0[,]1)(tm1) = (H` t) /\ (2 x. u) e. (0[,]1)) -> ((2 x. u)m1) = (H` (2 x. u)))
224 simplr 449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) -> (tm1) = (H` t))
225224ralimi 2168 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A.t e. (0[,]1)(((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) -> A.t e. (0[,]1)(tm1) = (H` t))
226223, 225, 125syl2an 503 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A.t e. (0[,]1)(((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) /\ u e. (0[,](1 / 2))) -> ((2 x. u)m1) = (H` (2 x. u)))
227226adantll 428 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (((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)))) /\ u e. (0[,](1 / 2))) -> ((2 x. u)m1) = (H` (2 x. u)))
228227adantlr 429 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((((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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))))) /\ u e. (0[,](1 / 2))) -> ((2 x. u)m1) = (H` (2 x. u)))
229228adantll 428 . . . . . . . . . . . . . . . . . . . . . 22 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. (0[,](1 / 2))) -> ((2 x. u)m1) = (H` (2 x. u)))
230 elicc2 7560 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((0 e. RR /\ 1 e. RR) -> (1 e. (0[,]1) <-> (1 e. RR /\ 0 <_ 1 /\ 1 <_ 1)))
231130, 131, 230mp2an 761 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (1 e. (0[,]1) <-> (1 e. RR /\ 0 <_ 1 /\ 1 <_ 1))
232131leidi 6790 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- 1 <_ 1
233231, 131, 136, 232mpbir3an 1052 . . . . . . . . . . . . . . . . . . . . . . . 24 |- 1 e. (0[,]1)
234105pcohtpylem1 16080 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((u e. (0[,](1 / 2)) /\ 1 e. (0[,]1)) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = ((2 x. u)m1))
235233, 234mpan2 760 . . . . . . . . . . . . . . . . . . . . . . 23 |- (u e. (0[,](1 / 2)) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = ((2 x. u)m1))
236235adantl 424 . . . . . . . . . . . . . . . . . . . . . 22 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. (0[,](1 / 2))) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = ((2 x. u)m1))
237 pcoval1 16074 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((J e. Top /\ (H e. (II Cn J) /\ K e. (II Cn J) /\ (H` 1) = (K` 0))) /\ u e. (0[,](1 / 2))) -> ((H(*p` J)K)` u) = (H` (2 x. u)))
238237ex 402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((J e. Top /\ (H e. (II Cn J) /\ K e. (II Cn J) /\ (H` 1) = (K` 0))) -> (u e. (0[,](1 / 2)) -> ((H(*p` J)K)` u) = (H` (2 x. u))))
239238expcom 403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((H e. (II Cn J) /\ K e. (II Cn J) /\ (H` 1) = (K` 0)) -> (J e. Top -> (u e. (0[,](1 / 2)) -> ((H(*p` J)K)` u) = (H` (2 x. u)))))
2402393expia 1069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((H e. (II Cn J) /\ K e. (II Cn J)) -> ((H` 1) = (K` 0) -> (J e. Top -> (u e. (0[,](1 / 2)) -> ((H(*p` J)K)` u) = (H` (2 x. u))))))
241240com3l 38 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((H` 1) = (K` 0) -> (J e. Top -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> (u e. (0[,](1 / 2)) -> ((H(*p` J)K)` u) = (H` (2 x. u))))))
24213, 241syl6bi 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((F` 1) = (H` 1) /\ (G` 0) = (K` 0)) -> ((F` 1) = (G` 0) -> (J e. Top -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> (u e. (0[,](1 / 2)) -> ((H(*p` J)K)` u) = (H` (2 x. u)))))))
243242com23 36 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((F` 1) = (H` 1) /\ (G` 0) = (K` 0)) -> (J e. Top -> ((F` 1) = (G` 0) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> (u e. (0[,](1 / 2)) -> ((H(*p` J)K)` u) = (H` (2 x. u)))))))
244243imp3a 388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((F` 1) = (H` 1) /\ (G` 0) = (K` 0)) -> ((J e. Top /\ (F` 1) = (G` 0)) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> (u e. (0[,](1 / 2)) -> ((H(*p` J)K)` u) = (H` (2 x. u))))))
245244com23 36 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((F` 1) = (H` 1) /\ (G` 0) = (K` 0)) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> ((J e. Top /\ (F` 1) = (G` 0)) -> (u e. (0[,](1 / 2)) -> ((H(*p` J)K)` u) = (H` (2 x. u))))))
246245ad2ant2lr 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((F` 0) = (H` 0) /\ (F` 1) = (H` 1)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> ((J e. Top /\ (F` 1) = (G` 0)) -> (u e. (0[,](1 / 2)) -> ((H(*p` J)K)` u) = (H` (2 x. u))))))
247246com12 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((H e. (II Cn J) /\ K e. (II Cn J)) -> ((((F` 0) = (H` 0) /\ (F` 1) = (H` 1)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) -> ((J e. Top /\ (F` 1) = (G` 0)) -> (u e. (0[,](1 / 2)) -> ((H(*p` J)K)` u) = (H` (2 x. u))))))
248247ad2ant2l 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((F e. (II Cn J) /\ H e. (II Cn J)) /\ (G e. (II Cn J) /\ K e. (II Cn J))) -> ((((F` 0) = (H` 0) /\ (F` 1) = (H` 1)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) -> ((J e. Top /\ (F` 1) = (G` 0)) -> (u e. (0[,](1 / 2)) -> ((H(*p` J)K)` u) = (H` (2 x. u))))))
249248imp 377 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ (G e. (II Cn J) /\ K e. (II Cn J))) /\ (((F` 0) = (H` 0) /\ (F` 1) = (H` 1)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1)))) -> ((J e. Top /\ (F` 1) = (G` 0)) -> (u e. (0[,](1 / 2)) -> ((H(*p` J)K)` u) = (H` (2 x. u)))))
250249an4s 566 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1)))) -> ((J e. Top /\ (F` 1) = (G` 0)) -> (u e. (0[,](1 / 2)) -> ((H(*p` J)K)` u) = (H` (2 x. u)))))
251250impcom 378 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((J e. Top /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> (u e. (0[,](1 / 2)) -> ((H(*p` J)K)` u) = (H` (2 x. u))))
252251adantllr 433 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> (u e. (0[,](1 / 2)) -> ((H(*p` J)K)` u) = (H` (2 x. u))))
253252adantr 425 . . . . . . . . . . . . . . . . . . . . . . 23 |- (((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) -> (u e. (0[,](1 / 2)) -> ((H(*p` J)K)` u) = (H` (2 x. u))))
254253imp 377 . . . . . . . . . . . . . . . . . . . . . 22 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. (0[,](1 / 2))) -> ((H(*p` J)K)` u) = (H` (2 x. u)))
255229, 236, 2543eqtr4d 1937 . . . . . . . . . . . . . . . . . . . . 21 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. (0[,](1 / 2))) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = ((H(*p` J)K)` u))
256 opreq1 4889 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (t = ((2 x. u) - 1) -> (tn1) = (((2 x. u) - 1)n1))
257 fveq2 4681 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (t = ((2 x. u) - 1) -> (K` t) = (K` ((2 x. u) - 1)))
258256, 257eqeq12d 1899 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (t = ((2 x. u) - 1) -> ((tn1) = (K` t) <-> (((2 x. u) - 1)n1) = (K` ((2 x. u) - 1))))
259258rcla4cva 2379 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A.t e. (0[,]1)(tn1) = (K` t) /\ ((2 x. u) - 1) e. (0[,]1)) -> (((2 x. u) - 1)n1) = (K` ((2 x. u) - 1)))
260 simplr 449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))) -> (tn1) = (K` t))
261260ralimi 2168 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))) -> A.t e. (0[,]1)(tn1) = (K` t))
262259, 261, 161syl2an 503 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))) /\ u e. ((1 / 2)[,]1)) -> (((2 x. u) - 1)n1) = (K` ((2 x. u) - 1)))
263262adantll 428 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (((n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))) /\ u e. ((1 / 2)[,]1)) -> (((2 x. u) - 1)n1) = (K` ((2 x. u) - 1)))
264263adantll 428 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((((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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))))) /\ u e. ((1 / 2)[,]1)) -> (((2 x. u) - 1)n1) = (K` ((2 x. u) - 1)))
265264adantll 428 . . . . . . . . . . . . . . . . . . . . . 22 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. ((1 / 2)[,]1)) -> (((2 x. u) - 1)n1) = (K` ((2 x. u) - 1)))
266105pcohtpylem2 16081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((u e. ((1 / 2)[,]1) /\ 1 e. (0[,]1)) /\ A.t e. (0[,]1)(1mt) = (0nt)) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = (((2 x. u) - 1)n1))
267233, 266mpanl2 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((u e. ((1 / 2)[,]1) /\ A.t e. (0[,]1)(1mt) = (0nt)) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = (((2 x. u) - 1)n1))
268267expcom 403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (A.t e. (0[,]1)(1mt) = (0nt) -> (u e. ((1 / 2)[,]1) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = (((2 x. u) - 1)n1)))
269166, 171, 2683syl 24 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((F` 1) = (G` 0) /\ A.t e. (0[,]1)((1mt) = (F` 1) /\ (0nt) = (G` 0))) -> (u e. ((1 / 2)[,]1) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = (((2 x. u) - 1)n1)))
270269, 182sylan2 500 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((F` 1) = (G` 0) /\ (A.t e. (0[,]1)(((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))))) -> (u e. ((1 / 2)[,]1) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = (((2 x. u) - 1)n1)))
271270adantrrl 438 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((F` 1) = (G` 0) /\ (A.t e. (0[,]1)(((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) -> (u e. ((1 / 2)[,]1) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = (((2 x. u) - 1)n1)))
272271adantrll 436 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F` 1) = (G` 0) /\ ((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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) -> (u e. ((1 / 2)[,]1) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = (((2 x. u) - 1)n1)))
273272adantlr 429 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((F` 1) = (G` 0) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) -> (u e. ((1 / 2)[,]1) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = (((2 x. u) - 1)n1)))
274273adantlll 432 . . . . . . . . . . . . . . . . . . . . . . 23 |- (((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) -> (u e. ((1 / 2)[,]1) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = (((2 x. u) - 1)n1)))
275274imp 377 . . . . . . . . . . . . . . . . . . . . . 22 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. ((1 / 2)[,]1)) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = (((2 x. u) - 1)n1))
276 pcoval2 16075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((J e. Top /\ (H e. (II Cn J) /\ K e. (II Cn J) /\ (H` 1) = (K` 0))) /\ u e. ((1 / 2)[,]1)) -> ((H(*p` J)K)` u) = (K` ((2 x. u) - 1)))
277276ex 402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((J e. Top /\ (H e. (II Cn J) /\ K e. (II Cn J) /\ (H` 1) = (K` 0))) -> (u e. ((1 / 2)[,]1) -> ((H(*p` J)K)` u) = (K` ((2 x. u) - 1))))
278277expcom 403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((H e. (II Cn J) /\ K e. (II Cn J) /\ (H` 1) = (K` 0)) -> (J e. Top -> (u e. ((1 / 2)[,]1) -> ((H(*p` J)K)` u) = (K` ((2 x. u) - 1)))))
2792783expia 1069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((H e. (II Cn J) /\ K e. (II Cn J)) -> ((H` 1) = (K` 0) -> (J e. Top -> (u e. ((1 / 2)[,]1) -> ((H(*p` J)K)` u) = (K` ((2 x. u) - 1))))))
280279com3l 38 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((H` 1) = (K` 0) -> (J e. Top -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> (u e. ((1 / 2)[,]1) -> ((H(*p` J)K)` u) = (K` ((2 x. u) - 1))))))
28113, 280syl6bi 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((F` 1) = (H` 1) /\ (G` 0) = (K` 0)) -> ((F` 1) = (G` 0) -> (J e. Top -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> (u e. ((1 / 2)[,]1) -> ((H(*p` J)K)` u) = (K` ((2 x. u) - 1)))))))
282281com23 36 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((F` 1) = (H` 1) /\ (G` 0) = (K` 0)) -> (J e. Top -> ((F` 1) = (G` 0) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> (u e. ((1 / 2)[,]1) -> ((H(*p` J)K)` u) = (K` ((2 x. u) - 1)))))))
283282imp3a 388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((F` 1) = (H` 1) /\ (G` 0) = (K` 0)) -> ((J e. Top /\ (F` 1) = (G` 0)) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> (u e. ((1 / 2)[,]1) -> ((H(*p` J)K)` u) = (K` ((2 x. u) - 1))))))
284283com23 36 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((F` 1) = (H` 1) /\ (G` 0) = (K` 0)) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> ((J e. Top /\ (F` 1) = (G` 0)) -> (u e. ((1 / 2)[,]1) -> ((H(*p` J)K)` u) = (K` ((2 x. u) - 1))))))
285284ad2ant2lr 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((F` 0) = (H` 0) /\ (F` 1) = (H` 1)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) -> ((H e. (II Cn J) /\ K e. (II Cn J)) -> ((J e. Top /\ (F` 1) = (G` 0)) -> (u e. ((1 / 2)[,]1) -> ((H(*p` J)K)` u) = (K` ((2 x. u) - 1))))))
286285com12 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((H e. (II Cn J) /\ K e. (II Cn J)) -> ((((F` 0) = (H` 0) /\ (F` 1) = (H` 1)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) -> ((J e. Top /\ (F` 1) = (G` 0)) -> (u e. ((1 / 2)[,]1) -> ((H(*p` J)K)` u) = (K` ((2 x. u) - 1))))))
287286ad2ant2l 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((F e. (II Cn J) /\ H e. (II Cn J)) /\ (G e. (II Cn J) /\ K e. (II Cn J))) -> ((((F` 0) = (H` 0) /\ (F` 1) = (H` 1)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) -> ((J e. Top /\ (F` 1) = (G` 0)) -> (u e. ((1 / 2)[,]1) -> ((H(*p` J)K)` u) = (K` ((2 x. u) - 1))))))
288287imp 377 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ (G e. (II Cn J) /\ K e. (II Cn J))) /\ (((F` 0) = (H` 0) /\ (F` 1) = (H` 1)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1)))) -> ((J e. Top /\ (F` 1) = (G` 0)) -> (u e. ((1 / 2)[,]1) -> ((H(*p` J)K)` u) = (K` ((2 x. u) - 1)))))
289288an4s 566 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1)))) -> ((J e. Top /\ (F` 1) = (G` 0)) -> (u e. ((1 / 2)[,]1) -> ((H(*p` J)K)` u) = (K` ((2 x. u) - 1)))))
290289impcom 378 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((J e. Top /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> (u e. ((1 / 2)[,]1) -> ((H(*p` J)K)` u) = (K` ((2 x. u) - 1))))
291290adantllr 433 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> (u e. ((1 / 2)[,]1) -> ((H(*p` J)K)` u) = (K` ((2 x. u) - 1))))
292291adantr 425 . . . . . . . . . . . . . . . . . . . . . . 23 |- (((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) -> (u e. ((1 / 2)[,]1) -> ((H(*p` J)K)` u) = (K` ((2 x. u) - 1))))
293292imp 377 . . . . . . . . . . . . . . . . . . . . . 22 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. ((1 / 2)[,]1)) -> ((H(*p` J)K)` u) = (K` ((2 x. u) - 1)))
294265, 275, 2933eqtr4d 1937 . . . . . . . . . . . . . . . . . . . . 21 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. ((1 / 2)[,]1)) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = ((H(*p` J)K)` u))
295255, 294jaodan 471 . . . . . . . . . . . . . . . . . . . 20 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ (u e. (0[,](1 / 2)) \/ u e. ((1 / 2)[,]1))) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = ((H(*p` J)K)` u))
296295, 218sylan2b 501 . . . . . . . . . . . . . . . . . . 19 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. (0[,]1)) -> (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = ((H(*p` J)K)` u))
297 opreq2 4890 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (t = u -> (0mt) = (0mu))
298297eqeq1d 1892 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (t = u -> ((0mt) = (F` 0) <-> (0mu) = (F` 0)))
299298rcla4cva 2379 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A.t e. (0[,]1)(0mt) = (F` 0) /\ u e. (0[,]1)) -> (0mu) = (F` 0))
300 simprl 450 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) -> (0mt) = (F` 0))
301300ralimi 2168 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A.t e. (0[,]1)(((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) -> A.t e. (0[,]1)(0mt) = (F` 0))
302299, 301sylan 497 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A.t e. (0[,]1)(((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) /\ u e. (0[,]1)) -> (0mu) = (F` 0))
303302adantll 428 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (((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)))) /\ u e. (0[,]1)) -> (0mu) = (F` 0))
304303adantlr 429 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((((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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))))) /\ u e. (0[,]1)) -> (0mu) = (F` 0))
305304adantll 428 . . . . . . . . . . . . . . . . . . . . . 22 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. (0[,]1)) -> (0mu) = (F` 0))
306 2cn 7164 . . . . . . . . . . . . . . . . . . . . . . . 24 |- 2 e. CC
307306mul01i 6594 . . . . . . . . . . . . . . . . . . . . . . 23 |- (2 x. 0) = 0
308307opreq1i 4892 . . . . . . . . . . . . . . . . . . . . . 22 |- ((2 x. 0)mu) = (0mu)
309305, 308syl5eq 1940 . . . . . . . . . . . . . . . . . . . . 21 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. (0[,]1)) -> ((2 x. 0)mu) = (F` 0))
310 elicc2 7560 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((0 e. RR /\ (1 / 2) e. RR) -> (0 e. (0[,](1 / 2)) <-> (0 e. RR /\ 0 <_ 0 /\ 0 <_ (1 / 2))))
311130, 208, 310mp2an 761 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (0 e. (0[,](1 / 2)) <-> (0 e. RR /\ 0 <_ 0 /\ 0 <_ (1 / 2)))
312311, 130, 134, 210mpbir3an 1052 . . . . . . . . . . . . . . . . . . . . . . 23 |- 0 e. (0[,](1 / 2))
313105pcohtpylem1 16080 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((0 e. (0[,](1 / 2)) /\ u e. (0[,]1)) -> (0{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = ((2 x. 0)mu))
314312, 313mpan 759 . . . . . . . . . . . . . . . . . . . . . 22 |- (u e. (0[,]1) -> (0{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = ((2 x. 0)mu))
315314adantl 424 . . . . . . . . . . . . . . . . . . . . 21 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. (0[,]1)) -> (0{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = ((2 x. 0)mu))
31634expcom 403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0)) -> (J e. Top -> ((F(*p` J)G)` 0) = (F` 0)))
3173163expia 1069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((F e. (II Cn J) /\ G e. (II Cn J)) -> ((F` 1) = (G` 0) -> (J e. Top -> ((F(*p` J)G)` 0) = (F` 0))))
318317com13 37 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (J e. Top -> ((F` 1) = (G` 0) -> ((F e. (II Cn J) /\ G e. (II Cn J)) -> ((F(*p` J)G)` 0) = (F` 0))))
319318imp31 389 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((J e. Top /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ G e. (II Cn J))) -> ((F(*p` J)G)` 0) = (F` 0))
320319adantllr 433 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ G e. (II Cn J))) -> ((F(*p` J)G)` 0) = (F` 0))
321320adantrrr 439 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ (G e. (II Cn J) /\ K e. (II Cn J)))) -> ((F(*p` J)G)` 0) = (F` 0))
322321adantrrr 439 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> ((F(*p` J)G)` 0) = (F` 0))
323322adantrlr 437 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> ((F(*p` J)G)` 0) = (F` 0))
324323adantrlr 437 . . . . . . . . . . . . . . . . . . . . . 22 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> ((F(*p` J)G)` 0) = (F` 0))
325324ad2antrr 440 . . . . . . . . . . . . . . . . . . . . 21 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. (0[,]1)) -> ((F(*p` J)G)` 0) = (F` 0))
326309, 315, 3253eqtr4d 1937 . . . . . . . . . . . . . . . . . . . 20 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. (0[,]1)) -> (0{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = ((F(*p` J)G)` 0))
327 opreq2 4890 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (t = u -> (1nt) = (1nu))
328327eqeq1d 1892 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (t = u -> ((1nt) = (G` 1) <-> (1nu) = (G` 1)))
329328rcla4cva 2379 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A.t e. (0[,]1)(1nt) = (G` 1) /\ u e. (0[,]1)) -> (1nu) = (G` 1))
330 simprr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))) -> (1nt) = (G` 1))
331330ralimi 2168 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))) -> A.t e. (0[,]1)(1nt) = (G` 1))
332329, 331sylan 497 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))) /\ u e. (0[,]1)) -> (1nu) = (G` 1))
333332adantll 428 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (((n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))) /\ u e. (0[,]1)) -> (1nu) = (G` 1))
334333adantll 428 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((((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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))))) /\ u e. (0[,]1)) -> (1nu) = (G` 1))
335334adantll 428 . . . . . . . . . . . . . . . . . . . . . 22 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. (0[,]1)) -> (1nu) = (G` 1))
336306mulid1i 6485 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (2 x. 1) = 2
337336opreq1i 4892 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((2 x. 1) - 1) = (2 - 1)
338 ax1cn 6422 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- 1 e. CC
339 1p1e2 10145 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (1 + 1) = 2
340306, 338, 338, 339subaddrii 6529 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (2 - 1) = 1
341337, 340eqtri 1908 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((2 x. 1) - 1) = 1
342341opreq1i 4892 . . . . . . . . . . . . . . . . . . . . . 22 |- (((2 x. 1) - 1)nu) = (1nu)
343335, 342syl5eq 1940 . . . . . . . . . . . . . . . . . . . . 21 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. (0[,]1)) -> (((2 x. 1) - 1)nu) = (G` 1))
344 elicc2 7560 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((1 / 2) e. RR /\ 1 e. RR) -> (1 e. ((1 / 2)[,]1) <-> (1 e. RR /\ (1 / 2) <_ 1 /\ 1 <_ 1)))
345208, 131, 344mp2an 761 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (1 e. ((1 / 2)[,]1) <-> (1 e. RR /\ (1 / 2) <_ 1 /\ 1 <_ 1))
346345, 131, 212, 232mpbir3an 1052 . . . . . . . . . . . . . . . . . . . . . . . 24 |- 1 e. ((1 / 2)[,]1)
347105pcohtpylem2 16081 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (((1 e. ((1 / 2)[,]1) /\ u e. (0[,]1)) /\ A.t e. (0[,]1)(1mt) = (0nt)) -> (1{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = (((2 x. 1) - 1)nu))
348346, 347mpanl1 770 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((u e. (0[,]1) /\ A.t e. (0[,]1)(1mt) = (0nt)) -> (1{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = (((2 x. 1) - 1)nu))
349348ancoms 484 . . . . . . . . . . . . . . . . . . . . . 22 |- ((A.t e. (0[,]1)(1mt) = (0nt) /\ u e. (0[,]1)) -> (1{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = (((2 x. 1) - 1)nu))
350166, 171syl 12 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((F` 1) = (G` 0) /\ A.t e. (0[,]1)((1mt) = (F` 1) /\ (0nt) = (G` 0))) -> A.t e. (0[,]1)(1mt) = (0nt))
351350, 182sylan2 500 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((F` 1) = (G` 0) /\ (A.t e. (0[,]1)(((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))))) -> A.t e. (0[,]1)(1mt) = (0nt))
352351adantrrl 438 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F` 1) = (G` 0) /\ (A.t e. (0[,]1)(((tm0) = (F` t) /\ (tm1) = (H` t)) /\ ((0mt) = (F` 0) /\ (1mt) = (F` 1))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) -> A.t e. (0[,]1)(1mt) = (0nt))
353352adantrll 436 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (((F` 1) = (G` 0) /\ ((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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) -> A.t e. (0[,]1)(1mt) = (0nt))
354353adantll 428 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) -> A.t e. (0[,]1)(1mt) = (0nt))
355354adantlr 429 . . . . . . . . . . . . . . . . . . . . . 22 |- (((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) -> A.t e. (0[,]1)(1mt) = (0nt))
356349, 355sylan 497 . . . . . . . . . . . . . . . . . . . . 21 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. (0[,]1)) -> (1{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = (((2 x. 1) - 1)nu))
35766expcom 403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((F e. (II Cn J) /\ G e. (II Cn J) /\ (F` 1) = (G` 0)) -> (J e. Top -> ((F(*p` J)G)` 1) = (G` 1)))
3583573expia 1069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((F e. (II Cn J) /\ G e. (II Cn J)) -> ((F` 1) = (G` 0) -> (J e. Top -> ((F(*p` J)G)` 1) = (G` 1))))
359358com13 37 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (J e. Top -> ((F` 1) = (G` 0) -> ((F e. (II Cn J) /\ G e. (II Cn J)) -> ((F(*p` J)G)` 1) = (G` 1))))
360359imp31 389 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((J e. Top /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ G e. (II Cn J))) -> ((F(*p` J)G)` 1) = (G` 1))
361360adantllr 433 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ G e. (II Cn J))) -> ((F(*p` J)G)` 1) = (G` 1))
362361adantrrr 439 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ (G e. (II Cn J) /\ K e. (II Cn J)))) -> ((F(*p` J)G)` 1) = (G` 1))
363362adantrrr 439 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (F e. (II Cn J) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> ((F(*p` J)G)` 1) = (G` 1))
364363adantrlr 437 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> ((F(*p` J)G)` 1) = (G` 1))
365364adantrlr 437 . . . . . . . . . . . . . . . . . . . . . 22 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> ((F(*p` J)G)` 1) = (G` 1))
366365ad2antrr 440 . . . . . . . . . . . . . . . . . . . . 21 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. (0[,]1)) -> ((F(*p` J)G)` 1) = (G` 1))
367343, 356, 3663eqtr4d 1937 . . . . . . . . . . . . . . . . . . . 20 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. (0[,]1)) -> (1{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = ((F(*p` J)G)` 1))
368326, 367jca 310 . . . . . . . . . . . . . . . . . . 19 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. (0[,]1)) -> ((0{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = ((F(*p` J)G)` 0) /\ (1{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = ((F(*p` J)G)` 1)))
369219, 296, 368jca31 311 . . . . . . . . . . . . . . . . . 18 |- ((((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) /\ u e. (0[,]1)) -> (((u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = ((F(*p` J)G)` u) /\ (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = ((H(*p` J)K)` u)) /\ ((0{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = ((F(*p` J)G)` 0) /\ (1{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = ((F(*p` J)G)` 1))))
370369r19.21aiva 2176 . . . . . . . . . . . . . . . . 17 |- (((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) -> A.u e. (0[,]1)(((u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = ((F(*p` J)G)` u) /\ (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = ((H(*p` J)K)` u)) /\ ((0{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = ((F(*p` J)G)` 0) /\ (1{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = ((F(*p` J)G)` 1))))
371118, 370jca 310 . . . . . . . . . . . . . . . 16 |- (((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))) -> ({<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))} e. ((II X.t II) Cn J) /\ A.u e. (0[,]1)(((u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = ((F(*p` J)G)` u) /\ (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = ((H(*p` J)K)` u)) /\ ((0{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = ((F(*p` J)G)` 0) /\ (1{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = ((F(*p` J)G)` 1)))))
372371ex 402 . . . . . . . . . . . . . . 15 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))))) -> ({<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))} e. ((II X.t II) Cn J) /\ A.u e. (0[,]1)(((u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = ((F(*p` J)G)` u) /\ (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = ((H(*p` J)K)` u)) /\ ((0{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = ((F(*p` J)G)` 0) /\ (1{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = ((F(*p` J)G)` 1))))))
373 isphtpy 16048 . . . . . . . . . . . . . . . . . . . . 21 |- (((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))))))
374373ex 402 . . . . . . . . . . . . . . . . . . . 20 |- ((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)))))))
3753743expb 1068 . . . . . . . . . . . . . . . . . . 19 |- ((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)))))))
376375impr 422 . . . . . . . . . . . . . . . . . 18 |- ((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))))))
377376adantlr 429 . . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ Y e. X) /\ ((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))))))
378377ad2ant2r 445 . . . . . . . . . . . . . . . 16 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 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))))))
379 isphtpy 16048 . . . . . . . . . . . . . . . . . . . . 21 |- (((J e. Top /\ G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) -> (n e. (G(PHtpy` J)K) <-> (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))))))
380379ex 402 . . . . . . . . . . . . . . . . . . . 20 |- ((J e. Top /\ G e. (II Cn J) /\ K e. (II Cn J)) -> (((G` 0) = (K` 0) /\ (G` 1) = (K` 1)) -> (n e. (G(PHtpy` J)K) <-> (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))))
3813803expb 1068 . . . . . . . . . . . . . . . . . . 19 |- ((J e. Top /\ (G e. (II Cn J) /\ K e. (II Cn J))) -> (((G` 0) = (K` 0) /\ (G` 1) = (K` 1)) -> (n e. (G(PHtpy` J)K) <-> (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))))
382381impr 422 . . . . . . . . . . . . . . . . . 18 |- ((J e. Top /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1)))) -> (n e. (G(PHtpy` J)K) <-> (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))))))
383382adantlr 429 . . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ Y e. X) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1)))) -> (n e. (G(PHtpy` J)K) <-> (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))))))
384383ad2ant2rl 447 . . . . . . . . . . . . . . . 16 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> (n e. (G(PHtpy` J)K) <-> (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1))))))
385378, 384anbi12d 690 . . . . . . . . . . . . . . 15 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> ((m e. (F(PHtpy` J)H) /\ n e. (G(PHtpy` J)K)) <-> ((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)))) /\ (n e. ((II X.t II) Cn J) /\ A.t e. (0[,]1)(((tn0) = (G` t) /\ (tn1) = (K` t)) /\ ((0nt) = (G` 0) /\ (1nt) = (G` 1)))))))
386 simplll 452 . . . . . . . . . . . . . . . 16 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> J e. Top)
3878adantrlr 437 . . . . . . . . . . . . . . . . 17 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> (F(*p` J)G) e. (II Cn J))
388387adantrlr 437 . . . . . . . . . . . . . . . 16 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> (F(*p` J)G) e. (II Cn J))
389 simprl 450 . . . . . . . . . . . . . . . . . 18 |- (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) -> (F` 0) = (H` 0))
390389ad2antrl 442 . . . . . . . . . . . . . . . . 17 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> (F` 0) = (H` 0))
39141adantrlr 437 . . . . . . . . . . . . . . . . . 18 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> ((F(*p` J)G)` 0) = (F` 0))
392391adantrlr 437 . . . . . . . . . . . . . . . . 17 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> ((F(*p` J)G)` 0) = (F` 0))
393390, 392, 603eqtr4d 1937 . . . . . . . . . . . . . . . 16 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> ((F(*p` J)G)` 0) = ((H(*p` J)K)` 0))
394 simprr 451 . . . . . . . . . . . . . . . . . 18 |- (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) -> (G` 1) = (K` 1))
395394ad2antll 443 . . . . . . . . . . . . . . . . 17 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> (G` 1) = (K` 1))
39673adantrlr 437 . . . . . . . . . . . . . . . . . 18 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> ((F(*p` J)G)` 1) = (G` 1))
397396adantrlr 437 . . . . . . . . . . . . . . . . 17 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> ((F(*p` J)G)` 1) = (G` 1))
398395, 397, 923eqtr4d 1937 . . . . . . . . . . . . . . . 16 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> ((F(*p` J)G)` 1) = ((H(*p` J)K)` 1))
399 isphtpy 16048 . . . . . . . . . . . . . . . 16 |- (((J e. Top /\ (F(*p` J)G) e. (II Cn J) /\ (H(*p` J)K) e. (II Cn J)) /\ (((F(*p` J)G)` 0) = ((H(*p` J)K)` 0) /\ ((F(*p` J)G)` 1) = ((H(*p` J)K)` 1))) -> ({<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))} e. ((F(*p` J)G)(PHtpy` J)(H(*p` J)K)) <-> ({<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))} e. ((II X.t II) Cn J) /\ A.u e. (0[,]1)(((u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = ((F(*p` J)G)` u) /\ (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = ((H(*p` J)K)` u)) /\ ((0{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = ((F(*p` J)G)` 0) /\ (1{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = ((F(*p` J)G)` 1))))))
400386, 388, 28, 393, 398, 399syl32anc 1108 . . . . . . . . . . . . . . 15 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> ({<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))} e. ((F(*p` J)G)(PHtpy` J)(H(*p` J)K)) <-> ({<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))} e. ((II X.t II) Cn J) /\ A.u e. (0[,]1)(((u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}0) = ((F(*p` J)G)` u) /\ (u{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}1) = ((H(*p` J)K)` u)) /\ ((0{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = ((F(*p` J)G)` 0) /\ (1{<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))}u) = ((F(*p` J)G)` 1))))))
401372, 385, 4003imtr4d 602 . . . . . . . . . . . . . 14 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> ((m e. (F(PHtpy` J)H) /\ n e. (G(PHtpy` J)K)) -> {<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))} e. ((F(*p` J)G)(PHtpy` J)(H(*p` J)K))))
402 ne0i 2881 . . . . . . . . . . . . . 14 |- ({<.<.x, y>., z>. | ((x e. (0[,]1) /\ y e. (0[,]1)) /\ z = if(x <_ (1 / 2), ((2 x. x)my), (((2 x. x) - 1)ny)))} e. ((F(*p` J)G)(PHtpy` J)(H(*p` J)K)) -> ((F(*p` J)G)(PHtpy` J)(H(*p` J)K)) =/= (/))
403401, 402syl6 25 . . . . . . . . . . . . 13 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))))) -> ((m e. (F(PHtpy` J)H) /\ n e. (G(PHtpy` J)K)) -> ((F(*p` J)G)(PHtpy` J)(H(*p` J)K)) =/= (/)))
404403ex 402 . . . . . . . . . . . 12 |- (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1)))) -> ((m e. (F(PHtpy` J)H) /\ n e. (G(PHtpy` J)K)) -> ((F(*p` J)G)(PHtpy` J)(H(*p` J)K)) =/= (/))))
405404com13 37 . . . . . . . . . . 11 |- ((m e. (F(PHtpy` J)H) /\ n e. (G(PHtpy` J)K)) -> ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1)))) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((F(*p` J)G)(PHtpy` J)(H(*p` J)K)) =/= (/))))
40640519.23aivv 1675 . . . . . . . . . 10 |- (E.mE.n(m e. (F(PHtpy` J)H) /\ n e. (G(PHtpy` J)K)) -> ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1)))) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((F(*p` J)G)(PHtpy` J)(H(*p` J)K)) =/= (/))))
40797, 406sylbir 218 . . . . . . . . 9 |- ((E.m m e. (F(PHtpy` J)H) /\ E.n n e. (G(PHtpy` J)K)) -> ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1)))) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((F(*p` J)G)(PHtpy` J)(H(*p` J)K)) =/= (/))))
408 n0 2884 . . . . . . . . 9 |- ((F(PHtpy` J)H) =/= (/) <-> E.m m e. (F(PHtpy` J)H))
409 n0 2884 . . . . . . . . 9 |- ((G(PHtpy` J)K) =/= (/) <-> E.n n e. (G(PHtpy` J)K))
410407, 408, 409syl2anb 504 . . . . . . . 8 |- (((F(PHtpy` J)H) =/= (/) /\ (G(PHtpy` J)K) =/= (/)) -> ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1)))) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((F(*p` J)G)(PHtpy` J)(H(*p` J)K)) =/= (/))))
411410impcom 378 . . . . . . 7 |- (((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ ((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1)))) /\ ((F(PHtpy` J)H) =/= (/) /\ (G(PHtpy` J)K) =/= (/))) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((F(*p` J)G)(PHtpy` J)(H(*p` J)K)) =/= (/)))
412411an4s 566 . . . . . 6 |- (((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/))) -> (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> ((F(*p` J)G)(PHtpy` J)(H(*p` J)K)) =/= (/)))
413412impcom 378 . . . . 5 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> ((F(*p` J)G)(PHtpy` J)(H(*p` J)K)) =/= (/))
41431, 96, 413jca31 311 . . . 4 |- ((((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) /\ ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))) -> ((((F(*p` J)G) e. (II Cn J) /\ (H(*p` J)K) e. (II Cn J)) /\ (((F(*p` J)G)` 0) = ((H(*p` J)K)` 0) /\ ((F(*p` J)G)` 1) = ((H(*p` J)K)` 1))) /\ ((F(*p` J)G)(PHtpy` J)(H(*p` J)K)) =/= (/)))
415414ex 402 . . 3 |- (((J e. Top /\ Y e. X) /\ (F` 1) = (G` 0)) -> (((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/))) -> ((((F(*p` J)G) e. (II Cn J) /\ (H(*p` J)K) e. (II Cn J)) /\ (((F(*p` J)G)` 0) = ((H(*p` J)K)` 0) /\ ((F(*p` J)G)` 1) = ((H(*p` J)K)` 1))) /\ ((F(*p` J)G)(PHtpy` J)(H(*p` J)K)) =/= (/))))
4164153adant2 895 . 2 |- (((J e. Top /\ Y e. X) /\ (H e. A /\ K e. B) /\ (F` 1) = (G` 0)) -> (((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/))) -> ((((F(*p` J)G) e. (II Cn J) /\ (H(*p` J)K) e. (II Cn J)) /\ (((F(*p` J)G)` 0) = ((H(*p` J)K)` 0) /\ ((F(*p` J)G)` 1) = ((H(*p` J)K)` 1))) /\ ((F(*p` J)G)(PHtpy` J)(H(*p` J)K)) =/= (/))))
417 isphtpc2 16060 . . . . . 6 |- ((J e. Top /\ H e. A) -> (F(~=ph` J)H <-> (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/))))
418417adantrr 431 . . . . 5 |- ((J e. Top /\ (H e. A /\ K e. B)) -> (F(~=ph` J)H <-> (((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/))))
419 isphtpc2 16060 . . . . . 6 |- ((J e. Top /\ K e. B) -> (G(~=ph` J)K <-> (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/))))
420419adantrl 430 . . . . 5 |- ((J e. Top /\ (H e. A /\ K e. B)) -> (G(~=ph` J)K <-> (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/))))
421418, 420anbi12d 690 . . . 4 |- ((J e. Top /\ (H e. A /\ K e. B)) -> ((F(~=ph` J)H /\ G(~=ph` J)K) <-> ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))))
422421adantlr 429 . . 3 |- (((J e. Top /\ Y e. X) /\ (H e. A /\ K e. B)) -> ((F(~=ph` J)H /\ G(~=ph` J)K) <-> ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))))
4234223adant3 896 . 2 |- (((J e. Top /\ Y e. X) /\ (H e. A /\ K e. B) /\ (F` 1) = (G` 0)) -> ((F(~=ph` J)H /\ G(~=ph` J)K) <-> ((((F e. (II Cn J) /\ H e. (II Cn J)) /\ ((F` 0) = (H` 0) /\ (F` 1) = (H` 1))) /\ (F(PHtpy` J)H) =/= (/)) /\ (((G e. (II Cn J) /\ K e. (II Cn J)) /\ ((G` 0) = (K` 0) /\ (G` 1) = (K` 1))) /\ (G(PHtpy` J)K) =/= (/)))))
424 oprex 4907 . . . . 5 |- (H(*p` J)K) e. _V
425 isphtpc2 16060 . . . . 5 |- ((J e. Top /\ (H(*p` J)K) e. _V) -> ((F(*p` J)G)(~=ph` J)(H(*p` J)K) <-> ((((F(*p` J)G) e. (II Cn J) /\ (H(*p` J)K) e. (II Cn J)) /\ (((F(*p` J)G)` 0) = ((H(*p` J)K)` 0) /\ ((F(*p` J)G)` 1) = ((H(*p` J)K)` 1))) /\ ((F(*p` J)G)(PHtpy` J)(H(*p` J)K)) =/= (/))))
426424, 425mpan2 760 . . . 4 |- (J e. Top -> ((F(*p` J)G)(~=ph` J)(H(*p` J)K) <-> ((((F(*p` J)G) e. (II Cn J) /\ (H(*p` J)K) e. (II Cn J)) /\ (((F(*p` J)G)` 0) = ((H(*p` J)K)` 0) /\ ((F(*p` J)G)` 1) = ((H(*p` J)K)` 1))) /\ ((F(*p` J)G)(PHtpy` J)(H(*p` J)K)) =/= (/))))
427426adantr 425 . . 3 |- ((J e. Top /\ Y e. X) -> ((F(*p` J)G)(~=ph` J)(H(*p` J)K) <-> ((((F(*p` J)G) e. (II Cn J) /\ (H(*p` J)K) e. (II Cn J)) /\ (((F(*p` J)G)` 0) = ((H(*p` J)K)` 0) /\ ((F(*p` J)G)` 1) = ((H(*p` J)K)` 1))) /\ ((F(*p` J)G)(PHtpy` J)(H(*p` J)K)) =/= (/))))
4284273ad2ant1 897 . 2 |- (((J e. Top /\ Y e. X) /\ (H e. A /\ K e. B) /\ (F` 1) = (G` 0)) -> ((F(*p` J)G)(~=ph` J)(H(*p` J)K) <-> ((((F(*p` J)G) e. (II Cn J) /\ (H(*p` J)K) e. (II Cn J)) /\ (((F(*p` J)G)` 0) = ((H(*p` J)K)` 0) /\ ((F(*p` J)G)` 1) = ((H(*p` J)K)` 1))) /\ ((F(*p` J)G)(PHtpy` J)(H(*p` J)K)) =/= (/))))
429416, 423, 4283imtr4d 602 1 |- (((J e. Top /\ Y e. X) /\ (H e. A /\ K e. B) /\ (F` 1) = (G` 0)) -> ((F(~=ph` J)H /\ G(~=ph` J)K) -> (F(*p` J)G)(~=ph` J)(H(*p` J)K)))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326   =/= wne 2017  A.wral 2105  _Vcvv 2292   u. cun 2591  (/)c0 2875  ifcif 2982   class class class wbr 3338  ` cfv 3998  (class class class)co 4884  {copab2 4885  RRcr 6385  0cc0 6386  1c1 6387   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  ~=phcphtpc 16044  *pcpco 16067
This theorem is referenced by:  pi1f 16093  pi1val 16094
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