set C = the constant Loop of a;
set E = EqRel (X,a);
set G = pi_1 (X,a);
set e = Class ((EqRel (X,a)), the constant Loop of a);
the constant Loop of a in Loops a
by Def1;
then A1:
Class ((EqRel (X,a)), the constant Loop of a) in Class (EqRel (X,a))
by EQREL_1:def 3;
thus
pi_1 (X,a) is associative
pi_1 (X,a) is Group-like proof
let x,
y,
z be
Element of
(pi_1 (X,a));
GROUP_1:def 3 (x * y) * z = x * (y * z)
consider A being
Loop of
a such that A2:
x = Class (
(EqRel (X,a)),
A)
by Th47;
consider B being
Loop of
a such that A3:
y = Class (
(EqRel (X,a)),
B)
by Th47;
consider BC being
Loop of
a such that A4:
y * z = Class (
(EqRel (X,a)),
BC)
by Th47;
consider C being
Loop of
a such that A5:
z = Class (
(EqRel (X,a)),
C)
by Th47;
y * z = Class (
(EqRel (X,a)),
(B + C))
by A3, A5, Lm4;
then
(
A,
A are_homotopic &
BC,
B + C are_homotopic )
by A4, Th46, BORSUK_2:12;
then A6:
A + BC,
A + (B + C) are_homotopic
by BORSUK_6:75;
consider AB being
Loop of
a such that A7:
x * y = Class (
(EqRel (X,a)),
AB)
by Th47;
x * y = Class (
(EqRel (X,a)),
(A + B))
by A2, A3, Lm4;
then
(
C,
C are_homotopic &
AB,
A + B are_homotopic )
by A7, Th46, BORSUK_2:12;
then A8:
AB + C,
(A + B) + C are_homotopic
by BORSUK_6:75;
A9:
(A + B) + C,
A + (B + C) are_homotopic
by BORSUK_6:73;
thus (x * y) * z =
Class (
(EqRel (X,a)),
(AB + C))
by A5, A7, Lm4
.=
Class (
(EqRel (X,a)),
((A + B) + C))
by A8, Th46
.=
Class (
(EqRel (X,a)),
(A + (B + C)))
by A9, Th46
.=
Class (
(EqRel (X,a)),
(A + BC))
by A6, Th46
.=
x * (y * z)
by A2, A4, Lm4
;
verum
end;
reconsider e = Class ((EqRel (X,a)), the constant Loop of a) as Element of (pi_1 (X,a)) by A1, Def5;
take
e
; GROUP_1:def 2 for b1 being Element of the carrier of (pi_1 (X,a)) holds
( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of (pi_1 (X,a)) st
( b1 * b2 = e & b2 * b1 = e ) )
let h be Element of (pi_1 (X,a)); ( h * e = h & e * h = h & ex b1 being Element of the carrier of (pi_1 (X,a)) st
( h * b1 = e & b1 * h = e ) )
consider A being Loop of a such that
A10:
h = Class ((EqRel (X,a)),A)
by Th47;
A11:
A + the constant Loop of a,A are_homotopic
by BORSUK_6:80;
thus h * e =
Class ((EqRel (X,a)),(A + the constant Loop of a))
by A10, Lm4
.=
h
by A10, A11, Th46
; ( e * h = h & ex b1 being Element of the carrier of (pi_1 (X,a)) st
( h * b1 = e & b1 * h = e ) )
A12:
the constant Loop of a + A,A are_homotopic
by BORSUK_6:82;
thus e * h =
Class ((EqRel (X,a)),( the constant Loop of a + A))
by A10, Lm4
.=
h
by A10, A12, Th46
; ex b1 being Element of the carrier of (pi_1 (X,a)) st
( h * b1 = e & b1 * h = e )
set x = Class ((EqRel (X,a)),(- A));
- A in Loops a
by Def1;
then
Class ((EqRel (X,a)),(- A)) in Class (EqRel (X,a))
by EQREL_1:def 3;
then reconsider x = Class ((EqRel (X,a)),(- A)) as Element of (pi_1 (X,a)) by Def5;
take
x
; ( h * x = e & x * h = e )
A13:
A + (- A), the constant Loop of a are_homotopic
by BORSUK_6:84;
thus h * x =
Class ((EqRel (X,a)),(A + (- A)))
by A10, Lm4
.=
e
by A13, Th46
; x * h = e
A14:
(- A) + A, the constant Loop of a are_homotopic
by BORSUK_6:86;
thus x * h =
Class ((EqRel (X,a)),((- A) + A))
by A10, Lm4
.=
e
by A14, Th46
; verum