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 is Homomorphism of (pi_1 X,x1),(pi_1 X,x0)
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 is Homomorphism of (pi_1 X,x1),(pi_1 X,x0)
let P be Path of x0,x1; :: thesis: ( x0,x1 are_connected implies pi_1-iso P is Homomorphism of (pi_1 X,x1),(pi_1 X,x0) )
assume A1:
x0,x1 are_connected
; :: thesis: pi_1-iso P is Homomorphism of (pi_1 X,x1),(pi_1 X,x0)
set f = pi_1-iso P;
now let x,
y be
Element of
(pi_1 X,x1);
:: thesis: (pi_1-iso P) . (x * y) = ((pi_1-iso P) . x) * ((pi_1-iso P) . y)consider A being
Loop of
x1 such that A2:
x = Class (EqRel X,x1),
A
by Th48;
consider B being
Loop of
x1 such that A3:
y = Class (EqRel X,x1),
B
by Th48;
consider C being
Loop of
x0 such that A4:
(pi_1-iso P) . x = Class (EqRel X,x0),
C
by Th48;
consider D being
Loop of
x0 such that A5:
(pi_1-iso P) . y = Class (EqRel X,x0),
D
by Th48;
(pi_1-iso P) . x = Class (EqRel X,x0),
((P + A) + (- P))
by A1, A2, Def4;
then A6:
C,
(P + A) + (- P) are_homotopic
by A4, Th47;
(pi_1-iso P) . y = Class (EqRel X,x0),
((P + B) + (- P))
by A1, A3, Def4;
then
D,
(P + B) + (- P) are_homotopic
by A5, Th47;
then A7:
C + D,
((P + A) + (- P)) + ((P + B) + (- P)) are_homotopic
by A6, BORSUK_6:83;
(P + (A + B)) + (- P),
((P + A) + (- P)) + ((P + B) + (- P)) are_homotopic
by A1, Th44;
then A8:
(P + (A + B)) + (- P),
C + D are_homotopic
by A7, BORSUK_6:87;
thus (pi_1-iso P) . (x * y) =
(pi_1-iso P) . (Class (EqRel X,x1),(A + B))
by A2, A3, Lm3
.=
Class (EqRel X,x0),
((P + (A + B)) + (- P))
by A1, Def4
.=
Class (EqRel X,x0),
(C + D)
by A8, Th47
.=
((pi_1-iso P) . x) * ((pi_1-iso P) . y)
by A4, A5, Lm3
;
:: thesis: verum end;
hence
pi_1-iso P is Homomorphism of (pi_1 X,x1),(pi_1 X,x0)
by GROUP_6:def 7; :: thesis: verum