let X be non empty TopSpace; for x0, x1 being Point of X
for P being Path of x0,x1 st x0,x1 are_connected holds
(pi_1-iso P) " = pi_1-iso (- P)
let x0, x1 be Point of X; for P being Path of x0,x1 st x0,x1 are_connected holds
(pi_1-iso P) " = pi_1-iso (- P)
let P be Path of x0,x1; ( x0,x1 are_connected implies (pi_1-iso P) " = pi_1-iso (- P) )
set f = pi_1-iso P;
set g = pi_1-iso (- P);
assume A1:
x0,x1 are_connected
; (pi_1-iso P) " = pi_1-iso (- P)
then
( pi_1-iso P is one-to-one & pi_1-iso P is onto )
by Th51, Th52;
then A2:
(pi_1-iso P) " = (pi_1-iso P) "
by TOPS_2:def 4;
A3:
pi_1-iso P is one-to-one
by A1, Th51;
for x being Element of (pi_1 (X,x0)) holds ((pi_1-iso P) ") . x = (pi_1-iso (- P)) . x
proof
let x be
Element of
(pi_1 (X,x0));
((pi_1-iso P) ") . x = (pi_1-iso (- P)) . x
consider Q being
Loop of
x0 such that A4:
x = Class (
(EqRel (X,x0)),
Q)
by Th47;
- (- P) = P
by A1, BORSUK_6:43;
then A5:
(P + (((- P) + Q) + (- (- P)))) + (- P),
Q are_homotopic
by A1, Th41;
dom (pi_1-iso P) = the
carrier of
(pi_1 (X,x1))
by FUNCT_2:def 1;
then A6:
Class (
(EqRel (X,x1)),
(((- P) + Q) + (- (- P))))
in dom (pi_1-iso P)
by Th47;
(pi_1-iso P) . (Class ((EqRel (X,x1)),(((- P) + Q) + (- (- P))))) =
Class (
(EqRel (X,x0)),
((P + (((- P) + Q) + (- (- P)))) + (- P)))
by A1, Def6
.=
x
by A4, A5, Th46
;
hence ((pi_1-iso P) ") . x =
Class (
(EqRel (X,x1)),
(((- P) + Q) + (- (- P))))
by A3, A2, A6, FUNCT_1:32
.=
(pi_1-iso (- P)) . x
by A1, A4, Def6
;
verum
end;
hence
(pi_1-iso P) " = pi_1-iso (- P)
; verum