set G = pi_1 X,a;
set E = EqRel X,a;
thus
pi_1 X,a is associative
:: thesis: pi_1 X,a is Group-likeproof
let x,
y,
z be
Element of
(pi_1 X,a);
:: according to GROUP_1:def 4 :: thesis: (x * y) * z = x * (y * z)
consider A being
Loop of
a such that A1:
x = Class (EqRel X,a),
A
by Th48;
consider B being
Loop of
a such that A2:
y = Class (EqRel X,a),
B
by Th48;
consider C being
Loop of
a such that A3:
z = Class (EqRel X,a),
C
by Th48;
consider AB being
Loop of
a such that A4:
x * y = Class (EqRel X,a),
AB
by Th48;
consider BC being
Loop of
a such that A5:
y * z = Class (EqRel X,a),
BC
by Th48;
A6:
A,
A are_homotopic
by BORSUK_2:15;
A7:
C,
C are_homotopic
by BORSUK_2:15;
x * y = Class (EqRel X,a),
(A + B)
by A1, A2, Lm3;
then
AB,
A + B are_homotopic
by A4, Th47;
then A8:
AB + C,
(A + B) + C are_homotopic
by A7, BORSUK_6:83;
y * z = Class (EqRel X,a),
(B + C)
by A2, A3, Lm3;
then
BC,
B + C are_homotopic
by A5, Th47;
then A9:
A + BC,
A + (B + C) are_homotopic
by A6, BORSUK_6:83;
A10:
(A + B) + C,
A + (B + C) are_homotopic
by BORSUK_6:81;
thus (x * y) * z =
Class (EqRel X,a),
(AB + C)
by A3, A4, Lm3
.=
Class (EqRel X,a),
((A + B) + C)
by A8, Th47
.=
Class (EqRel X,a),
(A + (B + C))
by A10, Th47
.=
Class (EqRel X,a),
(A + BC)
by A9, Th47
.=
x * (y * z)
by A1, A5, Lm3
;
:: thesis: verum
end;
consider C being constant Loop of a;
set e = Class (EqRel X,a),C;
C in Loops a
by Def1;
then
Class (EqRel X,a),C in Class (EqRel X,a)
by EQREL_1:def 5;
then reconsider e = Class (EqRel X,a),C as Element of (pi_1 X,a) by Def3;
take
e
; :: according to GROUP_1:def 3 :: thesis: 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); :: thesis: ( 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
A11:
h = Class (EqRel X,a),A
by Th48;
A12:
A + C,A are_homotopic
by BORSUK_6:88;
A13:
C + A,A are_homotopic
by BORSUK_6:90;
thus h * e =
Class (EqRel X,a),(A + C)
by A11, Lm3
.=
h
by A11, A12, Th47
; :: thesis: ( e * h = h & ex b1 being Element of the carrier of (pi_1 X,a) st
( h * b1 = e & b1 * h = e ) )
thus e * h =
Class (EqRel X,a),(C + A)
by A11, Lm3
.=
h
by A11, A13, Th47
; :: thesis: 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 5;
then reconsider x = Class (EqRel X,a),(- A) as Element of (pi_1 X,a) by Def3;
take
x
; :: thesis: ( h * x = e & x * h = e )
A14:
A + (- A),C are_homotopic
by BORSUK_6:92;
A15:
(- A) + A,C are_homotopic
by BORSUK_6:94;
thus h * x =
Class (EqRel X,a),(A + (- A))
by A11, Lm3
.=
e
by A14, Th47
; :: thesis: x * h = e
thus x * h =
Class (EqRel X,a),((- A) + A)
by A11, Lm3
.=
e
by A15, Th47
; :: thesis: verum