let X be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( x0,x1 are_connected implies (pi_1-iso P) " = pi_1-iso (- P) )
assume A1:
x0,x1 are_connected
; :: thesis: (pi_1-iso P) " = pi_1-iso (- P)
set f = pi_1-iso P;
set g = pi_1-iso (- P);
A2:
pi_1-iso P is one-to-one
by A1, Th52;
pi_1-iso P is onto
by A1, Th53;
then
rng (pi_1-iso P) = the carrier of (pi_1 X,x0)
by FUNCT_2:def 3;
then A3:
(pi_1-iso P) " = (pi_1-iso P) "
by A1, Th52, TOPS_2:def 4;
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);
:: thesis: ((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 Th48;
dom (pi_1-iso P) = the
carrier of
(pi_1 X,x1)
by FUNCT_2:def 1;
then A5:
Class (EqRel X,x1),
(((- P) + Q) + (- (- P))) in dom (pi_1-iso P)
by Th48;
- (- P) = P
by A1, BORSUK_6:50;
then A6:
(P + (((- P) + Q) + (- (- P)))) + (- P),
Q are_homotopic
by A1, Th42;
(pi_1-iso P) . (Class (EqRel X,x1),(((- P) + Q) + (- (- P)))) =
Class (EqRel X,x0),
((P + (((- P) + Q) + (- (- P)))) + (- P))
by A1, Def4
.=
x
by A4, A6, Th47
;
hence ((pi_1-iso P) " ) . x =
Class (EqRel X,x1),
(((- P) + Q) + (- (- P)))
by A2, A3, A5, FUNCT_1:54
.=
(pi_1-iso (- P)) . x
by A1, A4, Def4
;
:: thesis: verum
end;
hence
(pi_1-iso P) " = pi_1-iso (- P)
by FUNCT_2:113; :: thesis: verum