let T be non empty TopSpace; for a, b, c, d being Point of T
for P being Path of a,b
for Q being Path of b,c
for R being Path of c,d st a,b are_connected & b,c are_connected & c,d are_connected holds
RePar (((P + Q) + R),3RP) = P + (Q + R)
let a, b, c, d be Point of T; for P being Path of a,b
for Q being Path of b,c
for R being Path of c,d st a,b are_connected & b,c are_connected & c,d are_connected holds
RePar (((P + Q) + R),3RP) = P + (Q + R)
let P be Path of a,b; for Q being Path of b,c
for R being Path of c,d st a,b are_connected & b,c are_connected & c,d are_connected holds
RePar (((P + Q) + R),3RP) = P + (Q + R)
let Q be Path of b,c; for R being Path of c,d st a,b are_connected & b,c are_connected & c,d are_connected holds
RePar (((P + Q) + R),3RP) = P + (Q + R)
let R be Path of c,d; ( a,b are_connected & b,c are_connected & c,d are_connected implies RePar (((P + Q) + R),3RP) = P + (Q + R) )
assume that
A1:
a,b are_connected
and
A2:
b,c are_connected
and
A3:
c,d are_connected
; RePar (((P + Q) + R),3RP) = P + (Q + R)
set F = (P + Q) + R;
set f = RePar (((P + Q) + R),3RP);
set g = P + (Q + R);
A4:
a,c are_connected
by A1, A2, Th42;
A5:
b,d are_connected
by A2, A3, Th42;
for x being Point of I[01] holds (RePar (((P + Q) + R),3RP)) . x = (P + (Q + R)) . x
proof
let x be
Point of
I[01];
(RePar (((P + Q) + R),3RP)) . x = (P + (Q + R)) . x
x in the
carrier of
I[01]
;
then A6:
x in dom 3RP
by FUNCT_2:def 1;
A7:
(RePar (((P + Q) + R),3RP)) . x =
(((P + Q) + R) * 3RP) . x
by A3, A4, Def4, Th42, Th49
.=
((P + Q) + R) . (3RP . x)
by A6, FUNCT_1:13
;
per cases
( x <= 1 / 2 or ( x > 1 / 2 & x <= 3 / 4 ) or x > 3 / 4 )
;
suppose A8:
x <= 1
/ 2
;
(RePar (((P + Q) + R),3RP)) . x = (P + (Q + R)) . xreconsider y =
(1 / 2) * x as
Point of
I[01] by Th6;
(1 / 2) * x <= (1 / 2) * (1 / 2)
by A8, XREAL_1:64;
then A9:
y <= 1
/ 2
by XXREAL_0:2;
reconsider z = 2
* y as
Point of
I[01] ;
(RePar (((P + Q) + R),3RP)) . x =
((P + Q) + R) . y
by A7, A8, Def7
.=
(P + Q) . z
by A3, A4, A9, BORSUK_2:def 5
.=
P . (2 * x)
by A1, A2, A8, BORSUK_2:def 5
.=
(P + (Q + R)) . x
by A1, A5, A8, BORSUK_2:def 5
;
hence
(RePar (((P + Q) + R),3RP)) . x = (P + (Q + R)) . x
;
verum end; suppose A10:
(
x > 1
/ 2 &
x <= 3
/ 4 )
;
(RePar (((P + Q) + R),3RP)) . x = (P + (Q + R)) . xthen A11:
(1 / 2) - (1 / 4) <= x - (1 / 4)
by XREAL_1:9;
A12:
x - (1 / 4) <= (3 / 4) - (1 / 4)
by A10, XREAL_1:9;
then
x - (1 / 4) <= 1
by XXREAL_0:2;
then reconsider y =
x - (1 / 4) as
Point of
I[01] by A11, BORSUK_1:43;
reconsider z = 2
* y as
Point of
I[01] by A12, Th3;
A13:
2
* y >= 2
* (1 / 4)
by A11, XREAL_1:64;
reconsider w =
(2 * x) - 1 as
Point of
I[01] by A10, Th4;
2
* x <= 2
* (3 / 4)
by A10, XREAL_1:64;
then A14:
(2 * x) - 1
<= (3 / 2) - 1
by XREAL_1:9;
(RePar (((P + Q) + R),3RP)) . x =
((P + Q) + R) . y
by A7, A10, Def7
.=
(P + Q) . z
by A3, A4, A12, BORSUK_2:def 5
.=
Q . ((2 * z) - 1)
by A1, A2, A13, BORSUK_2:def 5
.=
Q . (2 * w)
.=
(Q + R) . w
by A2, A3, A14, BORSUK_2:def 5
.=
(P + (Q + R)) . x
by A1, A5, A10, BORSUK_2:def 5
;
hence
(RePar (((P + Q) + R),3RP)) . x = (P + (Q + R)) . x
;
verum end; suppose A15:
x > 3
/ 4
;
(RePar (((P + Q) + R),3RP)) . x = (P + (Q + R)) . xthen reconsider w =
(2 * x) - 1 as
Point of
I[01] by Th4, XXREAL_0:2;
2
* x > 2
* (3 / 4)
by A15, XREAL_1:68;
then A16:
(2 * x) - 1
> (2 * (3 / 4)) - 1
by XREAL_1:14;
reconsider y =
(2 * x) - 1 as
Point of
I[01] by A15, Th4, XXREAL_0:2;
A17:
x > 1
/ 2
by A15, XXREAL_0:2;
(RePar (((P + Q) + R),3RP)) . x =
((P + Q) + R) . y
by A7, A15, Def7
.=
R . ((2 * y) - 1)
by A3, A4, A16, BORSUK_2:def 5
.=
(Q + R) . w
by A2, A3, A16, BORSUK_2:def 5
.=
(P + (Q + R)) . x
by A1, A5, A17, BORSUK_2:def 5
;
hence
(RePar (((P + Q) + R),3RP)) . x = (P + (Q + R)) . x
;
verum end;
end;
hence
RePar (((P + Q) + R),3RP) = P + (Q + R)
by FUNCT_2:63; verum