let T be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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
; :: thesis: RePar ((P + Q) + R),3RP = P + (Q + R)
A4:
a,c are_connected
by A1, A2, Th46;
A5:
b,d are_connected
by A2, A3, Th46;
set F = (P + Q) + R;
set f = RePar ((P + Q) + R),3RP ;
set g = P + (Q + R);
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] ;
:: thesis: (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, Def6, Th46, Th57
.=
((P + Q) + R) . (3RP . x)
by A6, FUNCT_1:23
;
per cases
( x <= 1 / 2 or ( x > 1 / 2 & x <= 3 / 4 ) or x > 3 / 4 )
;
suppose A8:
x <= 1
/ 2
;
:: thesis: (RePar ((P + Q) + R),3RP ) . x = (P + (Q + R)) . xreconsider y =
(1 / 2) * x as
Point of
I[01] by Th9;
(1 / 2) * x <= (1 / 2) * (1 / 2)
by A8, XREAL_1:66;
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, Def9
.=
(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
;
:: thesis: verum end; suppose A10:
(
x > 1
/ 2 &
x <= 3
/ 4 )
;
:: thesis: (RePar ((P + Q) + R),3RP ) . x = (P + (Q + R)) . xthen A11:
x - (1 / 4) <= (3 / 4) - (1 / 4)
by XREAL_1:11;
then A12:
x - (1 / 4) <= 1
by XXREAL_0:2;
A13:
(1 / 2) - (1 / 4) <= x - (1 / 4)
by A10, XREAL_1:11;
then reconsider y =
x - (1 / 4) as
Point of
I[01] by A12, BORSUK_1:86;
reconsider z = 2
* y as
Point of
I[01] by A11, Th6;
A14:
2
* y >= 2
* (1 / 4)
by A13, XREAL_1:66;
reconsider w =
(2 * x) - 1 as
Point of
I[01] by A10, Th7;
2
* x <= 2
* (3 / 4)
by A10, XREAL_1:66;
then A15:
(2 * x) - 1
<= (3 / 2) - 1
by XREAL_1:11;
(RePar ((P + Q) + R),3RP ) . x =
((P + Q) + R) . y
by A7, A10, Def9
.=
(P + Q) . z
by A3, A4, A11, BORSUK_2:def 5
.=
Q . ((2 * z) - 1)
by A1, A2, A14, BORSUK_2:def 5
.=
Q . (2 * w)
.=
(Q + R) . w
by A2, A3, A15, 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
;
:: thesis: verum end; suppose A16:
x > 3
/ 4
;
:: thesis: (RePar ((P + Q) + R),3RP ) . x = (P + (Q + R)) . xthen A17:
x > 1
/ 2
by XXREAL_0:2;
reconsider y =
(2 * x) - 1 as
Point of
I[01] by A16, Th7, XXREAL_0:2;
2
* x > 2
* (3 / 4)
by A16, XREAL_1:70;
then A18:
(2 * x) - 1
> (2 * (3 / 4)) - 1
by XREAL_1:16;
reconsider w =
(2 * x) - 1 as
Point of
I[01] by A16, Th7, XXREAL_0:2;
(RePar ((P + Q) + R),3RP ) . x =
((P + Q) + R) . y
by A7, A16, Def9
.=
R . ((2 * y) - 1)
by A3, A4, A18, BORSUK_2:def 5
.=
(Q + R) . w
by A2, A3, A18, 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
;
:: thesis: verum end;
end;
hence
RePar ((P + Q) + R),3RP = P + (Q + R)
by FUNCT_2:113; :: thesis: verum