:: by Artur Korni{\l}owicz

::

:: Received May 19, 2013

:: Copyright (c) 2013-2021 Association of Mizar Users

set I = I[01] ;

set II = [:I[01],I[01]:];

set R = R^1 ;

set RR = [:R^1,R^1:];

set A = R^1 [.0,1.];

set cR = the carrier of R^1;

Lm1: the carrier of [:R^1,R^1:] = [: the carrier of R^1, the carrier of R^1:]

by BORSUK_1:def 2;

definition

let A, B be non empty TopSpace;

let C be set ;

let f be Function of [:A,B:],C;

let a be Element of A;

let b be Element of B;

:: original: .

redefine func f . (a,b) -> Element of C;

coherence

f . (a,b) is Element of C

end;
let C be set ;

let f be Function of [:A,B:],C;

let a be Element of A;

let b be Element of B;

:: original: .

redefine func f . (a,b) -> Element of C;

coherence

f . (a,b) is Element of C

proof end;

definition
end;

:: deftheorem Def1 defines unital TOPALG_7:def 1 :

for G being multMagma

for g being Element of G holds

( g is unital iff g = 1_ G );

for G being multMagma

for g being Element of G holds

( g is unital iff g = 1_ G );

registration
end;

registration

let G be unital multMagma ;

let g be Element of G;

let h be unital Element of G;

reducibility

g * h = g

h * g = g

end;
let g be Element of G;

let h be unital Element of G;

reducibility

g * h = g

proof end;

reducibility h * g = g

proof end;

registration
end;

scheme :: TOPALG_7:sch 1

TopFuncEx{ F_{1}() -> non empty TopSpace, F_{2}() -> non empty TopSpace, F_{3}() -> non empty set , F_{4}( Point of F_{1}(), Point of F_{2}()) -> Element of F_{3}() } :

TopFuncEx{ F

ex f being Function of [:F_{1}(),F_{2}():],F_{3}() st

for s being Point of F_{1}()

for t being Point of F_{2}() holds f . (s,t) = F_{4}(s,t)

for s being Point of F

for t being Point of F

proof end;

scheme :: TOPALG_7:sch 2

TopFuncEq{ F_{1}() -> non empty TopSpace, F_{2}() -> non empty TopSpace, F_{3}() -> non empty set , F_{4}( Point of F_{1}(), Point of F_{2}()) -> Element of F_{3}() } :

TopFuncEq{ F

for f, g being Function of [:F_{1}(),F_{2}():],F_{3}() st ( for s being Point of F_{1}()

for t being Point of F_{2}() holds f . (s,t) = F_{4}(s,t) ) & ( for s being Point of F_{1}()

for t being Point of F_{2}() holds g . (s,t) = F_{4}(s,t) ) holds

f = g

for t being Point of F

for t being Point of F

f = g

proof end;

definition

let X be non empty set ;

let T be non empty multMagma ;

let f, g be Function of X,T;

deffunc H_{1}( Element of X) -> Element of the carrier of T = (f . $1) * (g . $1);

ex b_{1} being Function of X,T st

for x being Element of X holds b_{1} . x = (f . x) * (g . x)

for b_{1}, b_{2} being Function of X,T st ( for x being Element of X holds b_{1} . x = (f . x) * (g . x) ) & ( for x being Element of X holds b_{2} . x = (f . x) * (g . x) ) holds

b_{1} = b_{2}

end;
let T be non empty multMagma ;

let f, g be Function of X,T;

deffunc H

func f (#) g -> Function of X,T means :Def2: :: TOPALG_7:def 2

for x being Element of X holds it . x = (f . x) * (g . x);

existence for x being Element of X holds it . x = (f . x) * (g . x);

ex b

for x being Element of X holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines (#) TOPALG_7:def 2 :

for X being non empty set

for T being non empty multMagma

for f, g, b_{5} being Function of X,T holds

( b_{5} = f (#) g iff for x being Element of X holds b_{5} . x = (f . x) * (g . x) );

for X being non empty set

for T being non empty multMagma

for f, g, b

( b

theorem :: TOPALG_7:1

for X being non empty set

for T being non empty associative multMagma

for f, g, h being Function of X,T holds (f (#) g) (#) h = f (#) (g (#) h)

for T being non empty associative multMagma

for f, g, h being Function of X,T holds (f (#) g) (#) h = f (#) (g (#) h)

proof end;

definition

let X be non empty set ;

let T be non empty commutative multMagma ;

let f, g be Function of X,T;

:: original: (#)

redefine func f (#) g -> Function of X,T;

commutativity

for f, g being Function of X,T holds f (#) g = g (#) f

end;
let T be non empty commutative multMagma ;

let f, g be Function of X,T;

:: original: (#)

redefine func f (#) g -> Function of X,T;

commutativity

for f, g being Function of X,T holds f (#) g = g (#) f

proof end;

definition

let T be non empty TopGrStr ;

let t be Point of T;

let f, g be Loop of t;

coherence

f (#) g is Function of I[01],T ;

end;
let t be Point of T;

let f, g be Loop of t;

coherence

f (#) g is Function of I[01],T ;

:: deftheorem defines LoopMlt TOPALG_7:def 3 :

for T being non empty TopGrStr

for t being Point of T

for f, g being Loop of t holds LoopMlt (f,g) = f (#) g;

for T being non empty TopGrStr

for t being Point of T

for f, g being Loop of t holds LoopMlt (f,g) = f (#) g;

definition

let T be non empty TopSpace-like unital BinContinuous TopGrStr ;

let t be unital Point of T;

let f, g be Loop of t;

:: original: LoopMlt

redefine func LoopMlt (f,g) -> Loop of t;

coherence

LoopMlt (f,g) is Loop of t

end;
let t be unital Point of T;

let f, g be Loop of t;

:: original: LoopMlt

redefine func LoopMlt (f,g) -> Loop of t;

coherence

LoopMlt (f,g) is Loop of t

proof end;

definition

let T be TopGroup;

let t be Point of T;

let f be Loop of t;

coherence

(inverse_op T) * f is Function of I[01],T ;

end;
let t be Point of T;

let f be Loop of t;

coherence

(inverse_op T) * f is Function of I[01],T ;

:: deftheorem defines inverse_loop TOPALG_7:def 4 :

for T being TopGroup

for t being Point of T

for f being Loop of t holds inverse_loop f = (inverse_op T) * f;

for T being TopGroup

for t being Point of T

for f being Loop of t holds inverse_loop f = (inverse_op T) * f;

theorem Th2: :: TOPALG_7:2

for x being Point of I[01]

for T being TopGroup

for t being Point of T

for f being Loop of t holds (inverse_loop f) . x = (f . x) "

for T being TopGroup

for t being Point of T

for f being Loop of t holds (inverse_loop f) . x = (f . x) "

proof end;

theorem Th3: :: TOPALG_7:3

for x being Point of I[01]

for T being TopGroup

for t being Point of T

for f being Loop of t holds ((inverse_loop f) . x) * (f . x) = 1_ T

for T being TopGroup

for t being Point of T

for f being Loop of t holds ((inverse_loop f) . x) * (f . x) = 1_ T

proof end;

theorem :: TOPALG_7:4

for x being Point of I[01]

for T being TopGroup

for t being Point of T

for f being Loop of t holds (f . x) * ((inverse_loop f) . x) = 1_ T

for T being TopGroup

for t being Point of T

for f being Loop of t holds (f . x) * ((inverse_loop f) . x) = 1_ T

proof end;

definition

let T be UnContinuous TopGroup;

let t be unital Point of T;

let f be Loop of t;

:: original: inverse_loop

redefine func inverse_loop f -> Loop of t;

coherence

inverse_loop f is Loop of t

end;
let t be unital Point of T;

let f be Loop of t;

:: original: inverse_loop

redefine func inverse_loop f -> Loop of t;

coherence

inverse_loop f is Loop of t

proof end;

definition

let s, t be Point of I[01];

:: original: *

redefine func s * t -> Point of I[01];

coherence

s * t is Point of I[01]

end;
:: original: *

redefine func s * t -> Point of I[01];

coherence

s * t is Point of I[01]

proof end;

definition

ex b_{1} being Function of [:R^1,R^1:],R^1 st

for x, y being Point of R^1 holds b_{1} . (x,y) = x * y

for b_{1}, b_{2} being Function of [:R^1,R^1:],R^1 st ( for x, y being Point of R^1 holds b_{1} . (x,y) = x * y ) & ( for x, y being Point of R^1 holds b_{2} . (x,y) = x * y ) holds

b_{1} = b_{2}
end;

func R^1-TIMES -> Function of [:R^1,R^1:],R^1 means :Def5: :: TOPALG_7:def 5

for x, y being Point of R^1 holds it . (x,y) = x * y;

existence for x, y being Point of R^1 holds it . (x,y) = x * y;

ex b

for x, y being Point of R^1 holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines R^1-TIMES TOPALG_7:def 5 :

for b_{1} being Function of [:R^1,R^1:],R^1 holds

( b_{1} = R^1-TIMES iff for x, y being Point of R^1 holds b_{1} . (x,y) = x * y );

for b

( b

definition

R^1-TIMES || (R^1 [.0,1.]) is Function of [:I[01],I[01]:],I[01]
end;

func I[01]-TIMES -> Function of [:I[01],I[01]:],I[01] equals :: TOPALG_7:def 6

R^1-TIMES || (R^1 [.0,1.]);

coherence R^1-TIMES || (R^1 [.0,1.]);

R^1-TIMES || (R^1 [.0,1.]) is Function of [:I[01],I[01]:],I[01]

proof end;

registration
end;

theorem Th7: :: TOPALG_7:7

for a, b being Point of I[01]

for N being a_neighborhood of a * b ex N1 being a_neighborhood of a ex N2 being a_neighborhood of b st

for x, y being Point of I[01] st x in N1 & y in N2 holds

x * y in N

for N being a_neighborhood of a * b ex N1 being a_neighborhood of a ex N2 being a_neighborhood of b st

for x, y being Point of I[01] st x in N1 & y in N2 holds

x * y in N

proof end;

definition

let T be non empty multMagma ;

let F, G be Function of [:I[01],I[01]:],T;

deffunc H_{1}( Point of I[01], Point of I[01]) -> Element of the carrier of T = (F . ($1,$2)) * (G . ($1,$2));

ex b_{1} being Function of [:I[01],I[01]:],T st

for a, b being Point of I[01] holds b_{1} . (a,b) = (F . (a,b)) * (G . (a,b))

for b_{1}, b_{2} being Function of [:I[01],I[01]:],T st ( for a, b being Point of I[01] holds b_{1} . (a,b) = (F . (a,b)) * (G . (a,b)) ) & ( for a, b being Point of I[01] holds b_{2} . (a,b) = (F . (a,b)) * (G . (a,b)) ) holds

b_{1} = b_{2}

end;
let F, G be Function of [:I[01],I[01]:],T;

deffunc H

func HomotopyMlt (F,G) -> Function of [:I[01],I[01]:],T means :Def7: :: TOPALG_7:def 7

for a, b being Point of I[01] holds it . (a,b) = (F . (a,b)) * (G . (a,b));

existence for a, b being Point of I[01] holds it . (a,b) = (F . (a,b)) * (G . (a,b));

ex b

for a, b being Point of I[01] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines HomotopyMlt TOPALG_7:def 7 :

for T being non empty multMagma

for F, G, b_{4} being Function of [:I[01],I[01]:],T holds

( b_{4} = HomotopyMlt (F,G) iff for a, b being Point of I[01] holds b_{4} . (a,b) = (F . (a,b)) * (G . (a,b)) );

for T being non empty multMagma

for F, G, b

( b

Lm2: now :: thesis: for T being non empty TopSpace-like unital BinContinuous TopGrStr

for t being unital Point of T

for x being Point of I[01]

for f1, f2, g1, g2 being Loop of t

for F being Homotopy of f1,f2

for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds

( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

for t being unital Point of T

for x being Point of I[01]

for f1, f2, g1, g2 being Loop of t

for F being Homotopy of f1,f2

for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds

( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

let T be non empty TopSpace-like unital BinContinuous TopGrStr ; :: thesis: for t being unital Point of T

for x being Point of I[01]

for f1, f2, g1, g2 being Loop of t

for F being Homotopy of f1,f2

for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds

( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

let t be unital Point of T; :: thesis: for x being Point of I[01]

for f1, f2, g1, g2 being Loop of t

for F being Homotopy of f1,f2

for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds

( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

let x be Point of I[01]; :: thesis: for f1, f2, g1, g2 being Loop of t

for F being Homotopy of f1,f2

for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds

( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

let f1, f2, g1, g2 be Loop of t; :: thesis: for F being Homotopy of f1,f2

for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds

( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

let F be Homotopy of f1,f2; :: thesis: for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds

( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

let G be Homotopy of g1,g2; :: thesis: ( f1,f2 are_homotopic & g1,g2 are_homotopic implies ( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t ) )

assume A1: ( f1,f2 are_homotopic & g1,g2 are_homotopic ) ; :: thesis: ( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

then A2: ( F . (x,0[01]) = f1 . x & G . (x,0[01]) = g1 . x ) by BORSUK_6:def 11;

thus (HomotopyMlt (F,G)) . (x,0) = (F . (x,0[01])) * (G . (x,0[01])) by Def7

.= (LoopMlt (f1,g1)) . x by A2, Def2 ; :: thesis: ( (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

A3: ( F . (x,1[01]) = f2 . x & G . (x,1[01]) = g2 . x ) by A1, BORSUK_6:def 11;

thus (HomotopyMlt (F,G)) . (x,1) = (F . (x,1[01])) * (G . (x,1[01])) by Def7

.= (LoopMlt (f2,g2)) . x by A3, Def2 ; :: thesis: ( (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

( F . (0[01],x) = t & G . (0[01],x) = t ) by A1, BORSUK_6:def 11;

hence (HomotopyMlt (F,G)) . (0,x) = t * t by Def7

.= t ;

:: thesis: (HomotopyMlt (F,G)) . (1,x) = t

( F . (1[01],x) = t & G . (1[01],x) = t ) by A1, BORSUK_6:def 11;

hence (HomotopyMlt (F,G)) . (1,x) = t * t by Def7

.= t ;

:: thesis: verum

end;
for x being Point of I[01]

for f1, f2, g1, g2 being Loop of t

for F being Homotopy of f1,f2

for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds

( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

let t be unital Point of T; :: thesis: for x being Point of I[01]

for f1, f2, g1, g2 being Loop of t

for F being Homotopy of f1,f2

for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds

( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

let x be Point of I[01]; :: thesis: for f1, f2, g1, g2 being Loop of t

for F being Homotopy of f1,f2

for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds

( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

let f1, f2, g1, g2 be Loop of t; :: thesis: for F being Homotopy of f1,f2

for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds

( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

let F be Homotopy of f1,f2; :: thesis: for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds

( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

let G be Homotopy of g1,g2; :: thesis: ( f1,f2 are_homotopic & g1,g2 are_homotopic implies ( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t ) )

assume A1: ( f1,f2 are_homotopic & g1,g2 are_homotopic ) ; :: thesis: ( (HomotopyMlt (F,G)) . (x,0) = (LoopMlt (f1,g1)) . x & (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

then A2: ( F . (x,0[01]) = f1 . x & G . (x,0[01]) = g1 . x ) by BORSUK_6:def 11;

thus (HomotopyMlt (F,G)) . (x,0) = (F . (x,0[01])) * (G . (x,0[01])) by Def7

.= (LoopMlt (f1,g1)) . x by A2, Def2 ; :: thesis: ( (HomotopyMlt (F,G)) . (x,1) = (LoopMlt (f2,g2)) . x & (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

A3: ( F . (x,1[01]) = f2 . x & G . (x,1[01]) = g2 . x ) by A1, BORSUK_6:def 11;

thus (HomotopyMlt (F,G)) . (x,1) = (F . (x,1[01])) * (G . (x,1[01])) by Def7

.= (LoopMlt (f2,g2)) . x by A3, Def2 ; :: thesis: ( (HomotopyMlt (F,G)) . (0,x) = t & (HomotopyMlt (F,G)) . (1,x) = t )

( F . (0[01],x) = t & G . (0[01],x) = t ) by A1, BORSUK_6:def 11;

hence (HomotopyMlt (F,G)) . (0,x) = t * t by Def7

.= t ;

:: thesis: (HomotopyMlt (F,G)) . (1,x) = t

( F . (1[01],x) = t & G . (1[01],x) = t ) by A1, BORSUK_6:def 11;

hence (HomotopyMlt (F,G)) . (1,x) = t * t by Def7

.= t ;

:: thesis: verum

theorem Th8: :: TOPALG_7:8

for T being non empty TopSpace-like unital BinContinuous TopGrStr

for F, G being Function of [:I[01],I[01]:],T

for M, N being Subset of [:I[01],I[01]:] holds (HomotopyMlt (F,G)) .: (M /\ N) c= (F .: M) * (G .: N)

for F, G being Function of [:I[01],I[01]:],T

for M, N being Subset of [:I[01],I[01]:] holds (HomotopyMlt (F,G)) .: (M /\ N) c= (F .: M) * (G .: N)

proof end;

registration

let T be non empty TopSpace-like unital BinContinuous TopGrStr ;

let F, G be continuous Function of [:I[01],I[01]:],T;

coherence

HomotopyMlt (F,G) is continuous

end;
let F, G be continuous Function of [:I[01],I[01]:],T;

coherence

HomotopyMlt (F,G) is continuous

proof end;

theorem Th9: :: TOPALG_7:9

for T being non empty TopSpace-like unital BinContinuous TopGrStr

for t being unital Point of T

for f1, f2, g1, g2 being Loop of t st f1,f2 are_homotopic & g1,g2 are_homotopic holds

LoopMlt (f1,g1), LoopMlt (f2,g2) are_homotopic

for t being unital Point of T

for f1, f2, g1, g2 being Loop of t st f1,f2 are_homotopic & g1,g2 are_homotopic holds

LoopMlt (f1,g1), LoopMlt (f2,g2) are_homotopic

proof end;

theorem :: TOPALG_7:10

for T being non empty TopSpace-like unital BinContinuous TopGrStr

for t being unital Point of T

for f1, f2, g1, g2 being Loop of t

for F being Homotopy of f1,f2

for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds

HomotopyMlt (F,G) is Homotopy of LoopMlt (f1,g1), LoopMlt (f2,g2)

for t being unital Point of T

for f1, f2, g1, g2 being Loop of t

for F being Homotopy of f1,f2

for G being Homotopy of g1,g2 st f1,f2 are_homotopic & g1,g2 are_homotopic holds

HomotopyMlt (F,G) is Homotopy of LoopMlt (f1,g1), LoopMlt (f2,g2)

proof end;

theorem Th11: :: TOPALG_7:11

for T being non empty TopSpace-like unital BinContinuous TopGrStr

for t being unital Point of T

for f, g being Loop of t

for c being constant Loop of t holds f + g = LoopMlt ((f + c),(c + g))

for t being unital Point of T

for f, g being Loop of t

for c being constant Loop of t holds f + g = LoopMlt ((f + c),(c + g))

proof end;

theorem Th12: :: TOPALG_7:12

for T being non empty TopSpace-like unital BinContinuous TopGrStr

for t being unital Point of T

for f, g being Loop of t

for c being constant Loop of t holds LoopMlt (f,g), LoopMlt ((f + c),(c + g)) are_homotopic

for t being unital Point of T

for f, g being Loop of t

for c being constant Loop of t holds LoopMlt (f,g), LoopMlt ((f + c),(c + g)) are_homotopic

proof end;

definition

let T be TopGroup;

let t be Point of T;

let f, g be Loop of t;

deffunc H_{1}( Point of I[01], Point of I[01]) -> Element of the carrier of T = ((((inverse_loop f) . ($1 * $2)) * (f . $1)) * (g . $1)) * (f . ($1 * $2));

ex b_{1} being Function of [:I[01],I[01]:],T st

for a, b being Point of I[01] holds b_{1} . (a,b) = ((((inverse_loop f) . (a * b)) * (f . a)) * (g . a)) * (f . (a * b))

for b_{1}, b_{2} being Function of [:I[01],I[01]:],T st ( for a, b being Point of I[01] holds b_{1} . (a,b) = ((((inverse_loop f) . (a * b)) * (f . a)) * (g . a)) * (f . (a * b)) ) & ( for a, b being Point of I[01] holds b_{2} . (a,b) = ((((inverse_loop f) . (a * b)) * (f . a)) * (g . a)) * (f . (a * b)) ) holds

b_{1} = b_{2}

end;
let t be Point of T;

let f, g be Loop of t;

deffunc H

func HopfHomotopy (f,g) -> Function of [:I[01],I[01]:],T means :Def8: :: TOPALG_7:def 8

for a, b being Point of I[01] holds it . (a,b) = ((((inverse_loop f) . (a * b)) * (f . a)) * (g . a)) * (f . (a * b));

existence for a, b being Point of I[01] holds it . (a,b) = ((((inverse_loop f) . (a * b)) * (f . a)) * (g . a)) * (f . (a * b));

ex b

for a, b being Point of I[01] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines HopfHomotopy TOPALG_7:def 8 :

for T being TopGroup

for t being Point of T

for f, g being Loop of t

for b_{5} being Function of [:I[01],I[01]:],T holds

( b_{5} = HopfHomotopy (f,g) iff for a, b being Point of I[01] holds b_{5} . (a,b) = ((((inverse_loop f) . (a * b)) * (f . a)) * (g . a)) * (f . (a * b)) );

for T being TopGroup

for t being Point of T

for f, g being Loop of t

for b

( b

registration

let T be TopologicalGroup;

let t be Point of T;

let f, g be Loop of t;

coherence

HopfHomotopy (f,g) is continuous

end;
let t be Point of T;

let f, g be Loop of t;

coherence

HopfHomotopy (f,g) is continuous

proof end;

Lm3: now :: thesis: for T being TopologicalGroup

for t being unital Point of T

for f, g being Loop of t

for x being Point of I[01] holds

( (HopfHomotopy (f,g)) . (x,0) = (LoopMlt (f,g)) . x & (HopfHomotopy (f,g)) . (x,1) = (LoopMlt (g,f)) . x & (HopfHomotopy (f,g)) . (0,x) = t & (HopfHomotopy (f,g)) . (1,x) = t )

for t being unital Point of T

for f, g being Loop of t

for x being Point of I[01] holds

( (HopfHomotopy (f,g)) . (x,0) = (LoopMlt (f,g)) . x & (HopfHomotopy (f,g)) . (x,1) = (LoopMlt (g,f)) . x & (HopfHomotopy (f,g)) . (0,x) = t & (HopfHomotopy (f,g)) . (1,x) = t )

let T be TopologicalGroup; :: thesis: for t being unital Point of T

for f, g being Loop of t

for x being Point of I[01] holds

( (HopfHomotopy (f,g)) . (x,0) = (LoopMlt (f,g)) . x & (HopfHomotopy (f,g)) . (x,1) = (LoopMlt (g,f)) . x & (HopfHomotopy (f,g)) . (0,x) = t & (HopfHomotopy (f,g)) . (1,x) = t )

let t be unital Point of T; :: thesis: for f, g being Loop of t

for x being Point of I[01] holds

( (HopfHomotopy (f,g)) . (x,0) = (LoopMlt (f,g)) . x & (HopfHomotopy (f,g)) . (x,1) = (LoopMlt (g,f)) . x & (HopfHomotopy (f,g)) . (0,x) = t & (HopfHomotopy (f,g)) . (1,x) = t )

let f, g be Loop of t; :: thesis: for x being Point of I[01] holds

( (HopfHomotopy (f,g)) . (x,0) = (LoopMlt (f,g)) . x & (HopfHomotopy (f,g)) . (x,1) = (LoopMlt (g,f)) . x & (HopfHomotopy (f,g)) . (0,x) = t & (HopfHomotopy (f,g)) . (1,x) = t )

let x be Point of I[01]; :: thesis: ( (HopfHomotopy (f,g)) . (x,0) = (LoopMlt (f,g)) . x & (HopfHomotopy (f,g)) . (x,1) = (LoopMlt (g,f)) . x & (HopfHomotopy (f,g)) . (0,x) = t & (HopfHomotopy (f,g)) . (1,x) = t )

set F = HopfHomotopy (f,g);

set i = inverse_loop f;

A1: t = 1_ T by Def1;

A2: t,t are_connected ;

A3: f . 0[01] = t by A2, BORSUK_2:def 2;

A4: f . 1[01] = t by A2, BORSUK_2:def 2;

A5: g . 0[01] = t by A2, BORSUK_2:def 2;

A6: (inverse_loop f) . 0[01] = t by A2, BORSUK_2:def 2;

thus (HopfHomotopy (f,g)) . (x,0) = ((((inverse_loop f) . (x * 0[01])) * (f . x)) * (g . x)) * (f . (x * 0[01])) by Def8

.= (LoopMlt (f,g)) . x by A3, A6, Def2 ; :: thesis: ( (HopfHomotopy (f,g)) . (x,1) = (LoopMlt (g,f)) . x & (HopfHomotopy (f,g)) . (0,x) = t & (HopfHomotopy (f,g)) . (1,x) = t )

thus (HopfHomotopy (f,g)) . (x,1) = ((((inverse_loop f) . (x * 1[01])) * (f . x)) * (g . x)) * (f . (x * 1[01])) by Def8

.= (t * (g . x)) * (f . x) by A1, Th3

.= (LoopMlt (g,f)) . x by Def2 ; :: thesis: ( (HopfHomotopy (f,g)) . (0,x) = t & (HopfHomotopy (f,g)) . (1,x) = t )

thus (HopfHomotopy (f,g)) . (0,x) = ((((inverse_loop f) . (0[01] * x)) * (f . 0[01])) * (g . 0[01])) * (f . (0[01] * x)) by Def8

.= t by A3, A5, A2, BORSUK_2:def 2 ; :: thesis: (HopfHomotopy (f,g)) . (1,x) = t

thus (HopfHomotopy (f,g)) . (1,x) = ((((inverse_loop f) . (1[01] * x)) * (f . 1[01])) * (g . 1[01])) * (f . (1[01] * x)) by Def8

.= ((((inverse_loop f) . x) * t) * t) * (f . x) by A4, A2, BORSUK_2:def 2

.= t by A1, Th3 ; :: thesis: verum

end;
for f, g being Loop of t

for x being Point of I[01] holds

( (HopfHomotopy (f,g)) . (x,0) = (LoopMlt (f,g)) . x & (HopfHomotopy (f,g)) . (x,1) = (LoopMlt (g,f)) . x & (HopfHomotopy (f,g)) . (0,x) = t & (HopfHomotopy (f,g)) . (1,x) = t )

let t be unital Point of T; :: thesis: for f, g being Loop of t

for x being Point of I[01] holds

( (HopfHomotopy (f,g)) . (x,0) = (LoopMlt (f,g)) . x & (HopfHomotopy (f,g)) . (x,1) = (LoopMlt (g,f)) . x & (HopfHomotopy (f,g)) . (0,x) = t & (HopfHomotopy (f,g)) . (1,x) = t )

let f, g be Loop of t; :: thesis: for x being Point of I[01] holds

( (HopfHomotopy (f,g)) . (x,0) = (LoopMlt (f,g)) . x & (HopfHomotopy (f,g)) . (x,1) = (LoopMlt (g,f)) . x & (HopfHomotopy (f,g)) . (0,x) = t & (HopfHomotopy (f,g)) . (1,x) = t )

let x be Point of I[01]; :: thesis: ( (HopfHomotopy (f,g)) . (x,0) = (LoopMlt (f,g)) . x & (HopfHomotopy (f,g)) . (x,1) = (LoopMlt (g,f)) . x & (HopfHomotopy (f,g)) . (0,x) = t & (HopfHomotopy (f,g)) . (1,x) = t )

set F = HopfHomotopy (f,g);

set i = inverse_loop f;

A1: t = 1_ T by Def1;

A2: t,t are_connected ;

A3: f . 0[01] = t by A2, BORSUK_2:def 2;

A4: f . 1[01] = t by A2, BORSUK_2:def 2;

A5: g . 0[01] = t by A2, BORSUK_2:def 2;

A6: (inverse_loop f) . 0[01] = t by A2, BORSUK_2:def 2;

thus (HopfHomotopy (f,g)) . (x,0) = ((((inverse_loop f) . (x * 0[01])) * (f . x)) * (g . x)) * (f . (x * 0[01])) by Def8

.= (LoopMlt (f,g)) . x by A3, A6, Def2 ; :: thesis: ( (HopfHomotopy (f,g)) . (x,1) = (LoopMlt (g,f)) . x & (HopfHomotopy (f,g)) . (0,x) = t & (HopfHomotopy (f,g)) . (1,x) = t )

thus (HopfHomotopy (f,g)) . (x,1) = ((((inverse_loop f) . (x * 1[01])) * (f . x)) * (g . x)) * (f . (x * 1[01])) by Def8

.= (t * (g . x)) * (f . x) by A1, Th3

.= (LoopMlt (g,f)) . x by Def2 ; :: thesis: ( (HopfHomotopy (f,g)) . (0,x) = t & (HopfHomotopy (f,g)) . (1,x) = t )

thus (HopfHomotopy (f,g)) . (0,x) = ((((inverse_loop f) . (0[01] * x)) * (f . 0[01])) * (g . 0[01])) * (f . (0[01] * x)) by Def8

.= t by A3, A5, A2, BORSUK_2:def 2 ; :: thesis: (HopfHomotopy (f,g)) . (1,x) = t

thus (HopfHomotopy (f,g)) . (1,x) = ((((inverse_loop f) . (1[01] * x)) * (f . 1[01])) * (g . 1[01])) * (f . (1[01] * x)) by Def8

.= ((((inverse_loop f) . x) * t) * t) * (f . x) by A4, A2, BORSUK_2:def 2

.= t by A1, Th3 ; :: thesis: verum

theorem Th13: :: TOPALG_7:13

for T being TopologicalGroup

for t being unital Point of T

for f, g being Loop of t holds LoopMlt (f,g), LoopMlt (g,f) are_homotopic

for t being unital Point of T

for f, g being Loop of t holds LoopMlt (f,g), LoopMlt (g,f) are_homotopic

proof end;

definition

let T be TopologicalGroup;

let t be unital Point of T;

let f, g be Loop of t;

:: original: HopfHomotopy

redefine func HopfHomotopy (f,g) -> Homotopy of LoopMlt (f,g), LoopMlt (g,f);

coherence

HopfHomotopy (f,g) is Homotopy of LoopMlt (f,g), LoopMlt (g,f)

end;
let t be unital Point of T;

let f, g be Loop of t;

:: original: HopfHomotopy

redefine func HopfHomotopy (f,g) -> Homotopy of LoopMlt (f,g), LoopMlt (g,f);

coherence

HopfHomotopy (f,g) is Homotopy of LoopMlt (f,g), LoopMlt (g,f)

proof end;

registration

let T be TopologicalGroup;

let t be unital Point of T;

coherence

pi_1 (T,t) is commutative

end;
let t be unital Point of T;

coherence

pi_1 (T,t) is commutative

proof end;