topalg_7.miz

    begin

    set I = I[01] ;

    set II = [:I, I:];

    set R = R^1 ;

    set RR = [:R, R:];

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

    set cR = the carrier of R;



     Lm1: the carrier of RR = [:cR, cR:] by BORSUK_1:def 2;

    definition

      let A,B be non empty TopSpace, C be set, 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

      proof

        (f . [a, b]) is Element of C;

        hence thesis;

      end;

    end

    definition

      let G be multMagma, g be Element of G;

      :: TOPALG_7:def1

      attr g is unital means

      : Def1: g = ( 1_ G);

    end

    registration

      let G be multMagma;

      cluster ( 1_ G) -> unital;

      coherence ;

    end

    registration

      let G be unital multMagma;

      cluster unital for Element of G;

      existence

      proof

        take ( 1_ G);

        thus ( 1_ G) = ( 1_ G);

      end;

    end

    registration

      let G be unital multMagma, g be Element of G, h be unital Element of G;

      reduce (g * h) to g;

      reducibility

      proof

        h = ( 1_ G) by Def1;

        hence thesis by GROUP_1:def 4;

      end;

      reduce (h * g) to g;

      reducibility

      proof

        h = ( 1_ G) by Def1;

        hence thesis by GROUP_1:def 4;

      end;

    end

    registration

      let G be Group;

      reduce (( 1_ G) " ) to ( 1_ G);

      reducibility by GROUP_1: 8;

    end

    scheme :: TOPALG_7:sch1

    TopFuncEx { S,T() -> non empty TopSpace , X() -> non empty set , F( Point of S(), Point of T()) -> Element of X() } :

ex f be Function of [:S(), T():], X() st for s be Point of S(), t be Point of T() holds (f . (s,t)) = F(s,t);

      consider f be Function of [:the carrier of S(), the carrier of T():], X() such that

       A1: for x be Point of S(), y be Point of T() holds (f . (x,y)) = F(x,y) from BINOP_1:sch 4;

       [:the carrier of S(), the carrier of T():] = the carrier of [:S(), T():] by BORSUK_1:def 2;

      then

      reconsider f as Function of [:S(), T():], X();

      take f;

      thus thesis by A1;

    end;

    scheme :: TOPALG_7:sch2

    TopFuncEq { S,T() -> non empty TopSpace , X() -> non empty set , F( Point of S(), Point of T()) -> Element of X() } :

for f,g be Function of [:S(), T():], X() st (for s be Point of S(), t be Point of T() holds (f . (s,t)) = F(s,t)) & (for s be Point of S(), t be Point of T() holds (g . (s,t)) = F(s,t)) holds f = g;

      let f,g be Function of [:S(), T():], X() such that

       A1: for a be Point of S(), b be Point of T() holds (f . (a,b)) = F(a,b) and

       A2: for a be Point of S(), b be Point of T() holds (g . (a,b)) = F(a,b);

      let x be Point of [:S(), T():];

      consider a be Point of S(), b be Point of T() such that

       A3: x = [a, b] by BORSUK_1: 10;



      thus (f . x) = (f . (a,b)) by A3

      .= F(a,b) by A1

      .= (g . (a,b)) by A2

      .= (g . x) by A3;

    end;

    definition

      let X be non empty set;

      let T be non empty multMagma;

      let f,g be Function of X, T;

      deffunc F( Element of X) = ((f . $1) * (g . $1));

      :: TOPALG_7:def2

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

      : Def2: for x be Element of X holds (it . x) = ((f . x) * (g . x));

      existence

      proof

        thus ex f be Function of X, T st for x be Element of X holds (f . x) = F(x) from FUNCT_2:sch 4;

      end;

      uniqueness

      proof

        let F,G be Function of X, T such that

         A1: for x be Element of X holds (F . x) = F(x) and

         A2: for x be Element of X holds (G . x) = F(x);

        let x be Element of X;



        thus (F . x) = F(x) by A1

        .= (G . x) by A2;

      end;

    end

    theorem :: TOPALG_7:1

    for X be non empty set, T be associative non empty multMagma holds for f,g,h be Function of X, T holds ((f (#) g) (#) h) = (f (#) (g (#) h))

    proof

      let X be non empty set;

      let T be associative non empty multMagma;

      let f,g,h be Function of X, T;

      let x be Element of X;



      thus (((f (#) g) (#) h) . x) = (((f (#) g) . x) * (h . x)) by Def2

      .= (((f . x) * (g . x)) * (h . x)) by Def2

      .= ((f . x) * ((g . x) * (h . x))) by GROUP_1:def 3

      .= ((f . x) * ((g (#) h) . x)) by Def2

      .= ((f (#) (g (#) h)) . x) by Def2;

    end;

    definition

      let X be non empty set, T be commutative non empty multMagma;

      let f,g be Function of X, T;

      :: original: (#)

      redefine

      func f (#) g;

      commutativity

      proof

        let f,g be Function of X, T;

        let x be Element of X;



        thus ((f (#) g) . x) = ((f . x) * (g . x)) by Def2

        .= ((g (#) f) . x) by Def2;

      end;

    end

    definition

      let T be non empty TopGrStr;

      let t be Point of T;

      let f,g be Loop of t;

      :: TOPALG_7:def3

      func LoopMlt (f,g) -> Function of I[01] , T equals (f (#) g);

      coherence ;

    end

    reserve T for BinContinuous unital TopSpace-like non empty TopGrStr,

x,y for Point of I[01] ,

s,t for unital Point of T,

f,g for Loop of t,

c for constant Loop of t;

    definition

      let T, t, f, g;

      :: original: LoopMlt

      redefine

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

      coherence

      proof

        set F = ( LoopMlt (f,g));

        thus

         A1: (t,t) are_connected ;

        thus F is continuous

        proof

          let a be Point of I, G be a_neighborhood of (F . a);

          (F . a) = ((f . a) * (g . a)) by Def2;

          then

          consider A be open a_neighborhood of (f . a), B be open a_neighborhood of (g . a) such that

           A2: (A * B) c= G by TOPGRP_1: 37;

          consider Ha be a_neighborhood of a such that

           A3: (f .: Ha) c= A by BORSUK_1:def 1;

          consider Hb be a_neighborhood of a such that

           A4: (g .: Hb) c= B by BORSUK_1:def 1;

          reconsider H = (Ha /\ Hb) as a_neighborhood of a by CONNSP_2: 2;

          take H;

          (F .: H) c= (A * B)

          proof

            let y be object;

            assume y in (F .: H);

            then

            consider c be Element of I such that

             A5: c in H and

             A6: (F . c) = y by FUNCT_2: 65;



             A7: (F . c) = ((f . c) * (g . c)) by Def2;

            c in Ha & c in Hb by A5, XBOOLE_0:def 4;

            then (f . c) in (f .: Ha) & (g . c) in (g .: Hb) by FUNCT_2: 35;

            hence thesis by A3, A4, A6, A7;

          end;

          hence (F .: H) c= G by A2;

        end;



         A8: t = ( 1_ T) by Def1;



         A9: (( 1_ T) * ( 1_ T)) = ( 1_ T);

        (f . 0[01] ) = t & (g . 0[01] ) = t & (f . 1[01] ) = t & (g . 1[01] ) = t by A1, BORSUK_2:def 2;

        hence thesis by A8, A9, Def2;

      end;

    end

    registration

      let T be UnContinuous TopGroup;

      cluster ( inverse_op T) -> continuous;

      coherence ;

    end

    definition

      let T be TopGroup, t be Point of T, f be Loop of t;

      :: TOPALG_7:def4

      func inverse_loop (f) -> Function of I[01] , T equals (( inverse_op T) * f);

      coherence ;

    end

    theorem :: TOPALG_7:2



     Th2: for T be TopGroup, t be Point of T, f be Loop of t holds (( inverse_loop f) . x) = ((f . x) " )

    proof

      let T be TopGroup;

      let t be Point of T;

      let f be Loop of t;



      thus (( inverse_loop f) . x) = (( inverse_op T) . (f . x)) by FUNCT_2: 15

      .= ((f . x) " ) by GROUP_1:def 6;

    end;

    theorem :: TOPALG_7:3



     Th3: for T be TopGroup, t be Point of T, f be Loop of t holds ((( inverse_loop f) . x) * (f . x)) = ( 1_ T)

    proof

      let T be TopGroup, t be Point of T, f be Loop of t;

      (( inverse_loop f) . x) = ((f . x) " ) by Th2;

      hence thesis by GROUP_1:def 5;

    end;

    theorem :: TOPALG_7:4

    for T be TopGroup, t be Point of T, f be Loop of t holds ((f . x) * (( inverse_loop f) . x)) = ( 1_ T)

    proof

      let T be TopGroup, t be Point of T, f be Loop of t;

      (( inverse_loop f) . x) = ((f . x) " ) by Th2;

      hence thesis by GROUP_1:def 5;

    end;

    definition

      let T be UnContinuous TopGroup, t be unital Point of T, f be Loop of t;

      :: original: inverse_loop

      redefine

      func inverse_loop (f) -> Loop of t ;

      coherence

      proof

        thus

         A1: (t,t) are_connected ;

        thus ( inverse_loop f) is continuous;



         A2: t = ( 1_ T) by Def1;



         A3: (( 1_ T) " ) = ( 1_ T);

        (f . 0[01] ) = t & (f . 1[01] ) = t by A1, BORSUK_2:def 2;

        hence thesis by A2, A3, Th2;

      end;

    end

    definition

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

      :: original: *

      redefine

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

      coherence

      proof

         0 <= s & 0 <= t & s <= 1 & t <= 1 by BORSUK_1: 43;

        hence thesis by BORSUK_1: 43, XREAL_1: 160;

      end;

    end

    definition

      :: TOPALG_7:def5

      func R^1-TIMES -> Function of [: R^1 , R^1 :], R^1 means

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

      existence

      proof

        deffunc F( Point of R, Point of R) = ( R^1 ($1 * $2));

        consider f be Function of RR, R such that

         A1: for s,t be Point of R holds (f . (s,t)) = F(s,t) from TopFuncEx;

        take f;

        let x,y be Point of R;

        (f . (x,y)) = F(x,y) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be Function of RR, R such that

         A2: for x,y be Point of R holds (f . (x,y)) = (x * y) and

         A3: for x,y be Point of R holds (g . (x,y)) = (x * y);

        now

          let x,y be Point of R;



          thus (f . (x,y)) = (x * y) by A2

          .= (g . (x,y)) by A3;

        end;

        hence thesis by Lm1, BINOP_1: 2;

      end;

    end

    registration

      cluster R^1-TIMES -> continuous;

      coherence

      proof

        reconsider f1 = ( pr1 (cR,cR)) as continuous Function of RR, R by YELLOW12: 39;

        reconsider f2 = ( pr2 (cR,cR)) as continuous Function of RR, R by YELLOW12: 40;

        consider g be Function of RR, R such that

         A1: for p be Point of RR, r1,r2 be Real st (f1 . p) = r1 & (f2 . p) = r2 holds (g . p) = (r1 * r2) and

         A2: g is continuous by JGRAPH_2: 25;

        now

          let a,b be Point of R;



           A3: (f1 . (a,b)) = a & (f2 . (a,b)) = b by FUNCT_3:def 4, FUNCT_3:def 5;



          thus ( R^1-TIMES . (a,b)) = (a * b) by Def5

          .= (g . [a, b]) by A1, A3

          .= (g . (a,b));

        end;

        hence thesis by A2, Lm1, BINOP_1: 2;

      end;

    end

    theorem :: TOPALG_7:5



     Th5: ( [: R^1 , R^1 :] | [:( R^1 [. 0 , 1.]), ( R^1 [. 0 , 1.]):]) = [: I[01] , I[01] :]

    proof



       A1: II is SubSpace of RR by BORSUK_3: 21;

      the carrier of II = [:A, A:] by BORSUK_1:def 2, BORSUK_1: 40;

      hence thesis by A1, TSEP_1: 5, PRE_TOPC: 8;

    end;

    definition

      :: TOPALG_7:def6

      func I[01]-TIMES -> Function of [: I[01] , I[01] :], I[01] equals ( R^1-TIMES || ( R^1 [. 0 , 1.]));

      coherence

      proof

        reconsider f = R^1-TIMES as BinOp of cR by Lm1;

        for x be set holds x in [:A, A:] implies (f . x) in A

        proof

          let x be set;

          assume x in [:A, A:];

          then

          consider a,b be object such that

           A1: a in A & b in A and

           A2: x = [a, b] by ZFMISC_1:def 2;

          reconsider a, b as Point of I by A1, BORSUK_1: 40;

          reconsider a1 = a, b1 = b as Point of R by A1;

          (f . (a1,b1)) = (a * b) by Def5;

          hence (f . x) in A by A2, BORSUK_1: 40;

        end;

        then

        reconsider A as Preserv of f by REALSET1:def 1;



         A3: the carrier of II = [:the carrier of I, the carrier of I:] by BORSUK_1:def 2;

        (f || A) is BinOp of A;

        hence thesis by A3, BORSUK_1: 40;

      end;

    end

    theorem :: TOPALG_7:6



     Th6: ( I[01]-TIMES . (x,y)) = (x * y)

    proof

      x is Point of R & y is Point of R by PRE_TOPC: 25;



      hence (x * y) = ( R^1-TIMES . (x,y)) by Def5

      .= ( I[01]-TIMES . (x,y)) by FUNCT_1: 49, ZFMISC_1: 87, BORSUK_1: 40;

    end;

    registration

      cluster I[01]-TIMES -> continuous;

      coherence

      proof

        reconsider f = I[01]-TIMES as Function of II, R by TOPREALA: 7;

        f is continuous by Th5, TOPMETR: 7;

        hence thesis by PRE_TOPC: 27;

      end;

    end

    theorem :: TOPALG_7:7



     Th7: for a,b be Point of I[01] holds for N be a_neighborhood of (a * b) holds ex N1 be a_neighborhood of a, N2 be a_neighborhood of b st for x,y be Point of I[01] st x in N1 & y in N2 holds (x * y) in N

    proof

      let a,b be Point of I;

      let N be a_neighborhood of (a * b);

      set g = I[01]-TIMES ;

      (g . (a,b)) = (a * b) by Th6;

      then

      consider H be a_neighborhood of [a, b] such that

       A1: (g .: H) c= N by BORSUK_1:def 1;

      consider F be Subset-Family of [:I, I:] such that

       A2: ( Int H) = ( union F) and

       A3: for e be set st e in F holds ex X1,Y1 be Subset of I st e = [:X1, Y1:] & X1 is open & Y1 is open by BORSUK_1: 5;

       [a, b] in ( Int H) by CONNSP_2:def 1;

      then

      consider M be set such that

       A4: [a, b] in M and

       A5: M in F by A2, TARSKI:def 4;

      consider A,B be Subset of I such that

       A6: M = [:A, B:] and

       A7: A is open and

       A8: B is open by A3, A5;

      a in A by A4, A6, ZFMISC_1: 87;

      then

       A9: a in ( Int A) by A7, TOPS_1: 23;

      b in B by A4, A6, ZFMISC_1: 87;

      then b in ( Int B) by A8, TOPS_1: 23;

      then

      reconsider B as open a_neighborhood of b by A8, CONNSP_2:def 1;

      reconsider A as open a_neighborhood of a by A7, A9, CONNSP_2:def 1;

      take A, B;

      let x,y be Point of I such that

       A10: x in A & y in B;



       A11: ( Int H) c= H by TOPS_1: 16;



       A12: (g . (x,y)) = (x * y) by Th6;

       [x, y] in M by A6, A10, ZFMISC_1: 87;

      then [x, y] in ( Int H) by A2, A5, TARSKI:def 4;

      then (g . (x,y)) in (g .: H) by A11, FUNCT_2: 35;

      hence thesis by A1, A12;

    end;

    definition

      let T be non empty multMagma;

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

      deffunc F( Point of I, Point of I) = ((F . ($1,$2)) * (G . ($1,$2)));

      :: TOPALG_7:def7

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

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

      existence

      proof

        thus ex f be Function of II, T st for a,b be Point of I holds (f . (a,b)) = F(a,b) from TopFuncEx;

      end;

      uniqueness

      proof

        thus for f,g be Function of II, T st (for a,b be Point of I holds (f . (a,b)) = F(a,b)) & (for a,b be Point of I holds (g . (a,b)) = F(a,b)) holds f = g from TopFuncEq;

      end;

    end

     Lm2:

    now

      let T, t, x;

      let f1,f2,g1,g2 be Loop of t, F be Homotopy of f1, f2, G be Homotopy of g1, g2;

      assume

       A1: (f1,f2) are_homotopic & (g1,g2) are_homotopic ;

      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;



       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;

      (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;

      (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;

    end;

    theorem :: TOPALG_7:8



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

    proof

      let F,G be Function of II, T;

      let M,N be Subset of II;

      let y be object;

      assume y in (( HomotopyMlt (F,G)) .: (M /\ N));

      then

      consider x be Point of II such that

       A1: x in (M /\ N) and

       A2: (( HomotopyMlt (F,G)) . x) = y by FUNCT_2: 65;

      consider a,b be Point of I such that

       A3: x = [a, b] by BORSUK_1: 10;



       A4: (( HomotopyMlt (F,G)) . (a,b)) = ((F . (a,b)) * (G . (a,b))) by Def7;

       [a, b] in M & [a, b] in N by A1, A3, XBOOLE_0:def 4;

      then (F . (a,b)) in (F .: M) & (G . (a,b)) in (G .: N) by FUNCT_2: 35;

      hence thesis by A2, A3, A4;

    end;

    registration

      let T;

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

      cluster ( HomotopyMlt (F,G)) -> continuous;

      coherence

      proof

        let W be Point of II, N be a_neighborhood of (( HomotopyMlt (F,G)) . W);

        consider a,b be Point of I such that

         A1: W = [a, b] by BORSUK_1: 10;

        (( HomotopyMlt (F,G)) . (a,b)) = ((F . (a,b)) * (G . (a,b))) by Def7;

        then

        consider A be open a_neighborhood of (F . (a,b)), B be open a_neighborhood of (G . (a,b)) such that

         A2: (A * B) c= N by A1, TOPGRP_1: 37;

        consider NF be a_neighborhood of [a, b] such that

         A3: (F .: NF) c= A by BORSUK_1:def 1;

        consider NG be a_neighborhood of [a, b] such that

         A4: (G .: NG) c= B by BORSUK_1:def 1;

        reconsider H = (NF /\ NG) as a_neighborhood of W by A1, CONNSP_2: 2;

        take H;



         A5: (( HomotopyMlt (F,G)) .: (NF /\ NG)) c= ((F .: NF) * (G .: NG)) by Th8;

        ((F .: NF) * (G .: NG)) c= (A * B) by A3, A4, TOPGRP_1: 4;

        hence thesis by A5, A2;

      end;

    end

    theorem :: TOPALG_7:9



     Th9: for f1,f2,g1,g2 be Loop of t st (f1,f2) are_homotopic & (g1,g2) are_homotopic holds (( LoopMlt (f1,g1)),( LoopMlt (f2,g2))) are_homotopic

    proof

      let f1,f2,g1,g2 be Loop of t;

      assume

       A1: (f1,f2) are_homotopic ;

      then

      consider F be Function of II, T such that

       A2: F is continuous & for x be Point of I holds (F . (x, 0 )) = (f1 . x) & (F . (x,1)) = (f2 . x) & (F . ( 0 ,x)) = t & (F . (1,x)) = t;

      assume

       A3: (g1,g2) are_homotopic ;

      then

      consider G be Function of II, T such that

       A4: G is continuous & for x be Point of I holds (G . (x, 0 )) = (g1 . x) & (G . (x,1)) = (g2 . x) & (G . ( 0 ,x)) = t & (G . (1,x)) = t;

      take ( HomotopyMlt (F,G));

      F is Homotopy of f1, f2 & G is Homotopy of g1, g2 by A2, A4, A1, A3, BORSUK_6:def 11;

      hence thesis by A1, A2, A3, A4, Lm2;

    end;

    theorem :: TOPALG_7:10

    for f1,f2,g1,g2 be Loop of t, F be Homotopy of f1, f2, G be 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

      let f1,f2,g1,g2 be Loop of t, F be Homotopy of f1, f2, G be Homotopy of g1, g2 such that

       A1: (f1,f2) are_homotopic & (g1,g2) are_homotopic ;

      thus (( LoopMlt (f1,g1)),( LoopMlt (f2,g2))) are_homotopic by A1, Th9;

      F is continuous & G is continuous by A1, BORSUK_6:def 11;

      hence ( HomotopyMlt (F,G)) is continuous;

      thus thesis by A1, Lm2;

    end;

    theorem :: TOPALG_7:11



     Th11: (f + g) = ( LoopMlt ((f + c),(c + g)))

    proof

      let x;



       A1: c = (I --> t) by BORSUK_2: 5;

      now

        per cases ;

          suppose

           A2: x <= (1 / 2);

          then

          reconsider z = (2 * x) as Point of I by BORSUK_6: 3;



           A3: ((f + c) . x) = (f . z) by A2, BORSUK_2:def 5;

          ((c + g) . x) = (c . z) by A2, BORSUK_2:def 5

          .= t by A1;

          hence ((f + g) . x) = (((f + c) . x) * ((c + g) . x)) by A2, A3, BORSUK_2:def 5;

        end;

          suppose

           A4: x >= (1 / 2);

          then

          reconsider z = ((2 * x) - 1) as Point of I by BORSUK_6: 4;



           A5: ((f + c) . x) = (c . z) by A4, BORSUK_2:def 5

          .= t by A1;

          ((c + g) . x) = (g . z) by A4, BORSUK_2:def 5;

          hence ((f + g) . x) = (((f + c) . x) * ((c + g) . x)) by A5, A4, BORSUK_2:def 5;

        end;

      end;

      hence thesis by Def2;

    end;

    theorem :: TOPALG_7:12



     Th12: (( LoopMlt (f,g)),( LoopMlt ((f + c),(c + g)))) are_homotopic

    proof

      (f,(f + c)) are_homotopic & ((c + g),g) are_homotopic by BORSUK_6: 80, BORSUK_6: 82;

      hence thesis by Th9;

    end;

    definition

      let T be TopGroup, t be Point of T, f,g be Loop of t;

      deffunc F( Point of I, Point of I) = ((((( inverse_loop f) . ($1 * $2)) * (f . $1)) * (g . $1)) * (f . ($1 * $2)));

      :: TOPALG_7:def8

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

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

      existence

      proof

        thus ex F be Function of II, T st for x,y be Point of I holds (F . (x,y)) = F(x,y) from TopFuncEx;

      end;

      uniqueness

      proof

        thus for f,g be Function of II, T st (for a,b be Point of I holds (f . (a,b)) = F(a,b)) & (for a,b be Point of I holds (g . (a,b)) = F(a,b)) holds f = g from TopFuncEq;

      end;

    end

    registration

      let T be TopologicalGroup, t be Point of T, f,g be Loop of t;

      cluster ( HopfHomotopy (f,g)) -> continuous;

      coherence

      proof

        set F = ( HopfHomotopy (f,g));

        set i = ( inverse_loop f);

        let W be Point of II, G be a_neighborhood of (F . W);

        consider a,b be Point of I such that

         A1: W = [a, b] by BORSUK_1: 10;

        (F . (a,b)) = ((((i . (a * b)) * (f . a)) * (g . a)) * (f . (a * b))) by Def8;

        then

        consider A1 be open a_neighborhood of (((i . (a * b)) * (f . a)) * (g . a)), B1 be open a_neighborhood of (f . (a * b)) such that

         A2: (A1 * B1) c= G by A1, TOPGRP_1: 37;

        consider A2 be open a_neighborhood of ((i . (a * b)) * (f . a)), B2 be open a_neighborhood of (g . a) such that

         A3: (A2 * B2) c= A1 by TOPGRP_1: 37;

        consider A3 be open a_neighborhood of (i . (a * b)), B3 be open a_neighborhood of (f . a) such that

         A4: (A3 * B3) c= A2 by TOPGRP_1: 37;

        (i . (a * b)) = (( inverse_op T) . (f . (a * b))) by FUNCT_2: 15

        .= ((f . (a * b)) " ) by GROUP_1:def 6;

        then

        consider A4 be open a_neighborhood of (f . (a * b)) such that

         A5: (A4 " ) c= A3 by TOPGRP_1: 39;

        consider A5 be a_neighborhood of (a * b) such that

         A6: (f .: A5) c= A4 by BORSUK_1:def 1;

        consider NB1 be a_neighborhood of (a * b) such that

         A7: (f .: NB1) c= B1 by BORSUK_1:def 1;

        consider NB2 be a_neighborhood of a such that

         A8: (g .: NB2) c= B2 by BORSUK_1:def 1;

        consider NB3 be a_neighborhood of a such that

         A9: (f .: NB3) c= B3 by BORSUK_1:def 1;

        (A5 /\ NB1) is a_neighborhood of (a * b) by CONNSP_2: 2;

        then

        consider N1 be a_neighborhood of a, N2 be a_neighborhood of b such that

         A10: for x,y be Point of I st x in N1 & y in N2 holds (x * y) in (A5 /\ NB1) by Th7;

        (N1 /\ NB2) is a_neighborhood of a by CONNSP_2: 2;

        then

        reconsider Na = ((N1 /\ NB2) /\ NB3) as a_neighborhood of a by CONNSP_2: 2;

        reconsider H = [:Na, N2:] as a_neighborhood of W by A1;

        take H;

        let y be object;

        assume y in (F .: H);

        then

        consider x be Element of II such that

         A11: x in H and

         A12: (F . x) = y by FUNCT_2: 65;

        consider c,d be Point of I such that

         A13: x = [c, d] by BORSUK_1: 10;



         A14: (i . (c * d)) = (( inverse_op T) . (f . (c * d))) by FUNCT_2: 15

        .= ((f . (c * d)) " ) by GROUP_1:def 6;



         A15: (F . (c,d)) = ((((i . (c * d)) * (f . c)) * (g . c)) * (f . (c * d))) by Def8;



         A16: c in ((N1 /\ NB2) /\ NB3) by A11, A13, ZFMISC_1: 87;



         A17: c in (N1 /\ NB2) by A16, XBOOLE_0:def 4;

        then

         A18: c in N1 by XBOOLE_0:def 4;

        d in N2 by A11, A13, ZFMISC_1: 87;

        then

         A19: (c * d) in (A5 /\ NB1) by A18, A10;

        then (c * d) in A5 by XBOOLE_0:def 4;

        then (f . (c * d)) in (f .: A5) by FUNCT_2: 35;

        then

         A20: ((f . (c * d)) " ) in (A4 " ) by A6;

        c in NB3 by A16, XBOOLE_0:def 4;

        then (f . c) in (f .: NB3) by FUNCT_2: 35;

        then

         A21: ((i . (c * d)) * (f . c)) in (A3 * B3) by A5, A9, A14, A20;

        c in NB2 by A17, XBOOLE_0:def 4;

        then (g . c) in (g .: NB2) by FUNCT_2: 35;

        then

         A22: (((i . (c * d)) * (f . c)) * (g . c)) in (A2 * B2) by A4, A8, A21;

        (c * d) in NB1 by A19, XBOOLE_0:def 4;

        then (f . (c * d)) in (f .: NB1) by FUNCT_2: 35;

        then ((((i . (c * d)) * (f . c)) * (g . c)) * (f . (c * d))) in (A1 * B1) by A3, A7, A22;

        hence thesis by A2, A12, A13, A15;

      end;

    end

    reserve T for TopologicalGroup,

t for unital Point of T,

f,g for Loop of t;

     Lm3:

    now

      let T, t, f, g, x;

      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: (i . 0[01] ) = t by A2, BORSUK_2:def 2;



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

      .= (( LoopMlt (f,g)) . x) by A3, A6, Def2;



      thus (F . (x,1)) = ((((i . (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;



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

      .= t by A3, A5, A2, BORSUK_2:def 2;



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

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

      .= t by A1, Th3;

    end;

    theorem :: TOPALG_7:13



     Th13: (( LoopMlt (f,g)),( LoopMlt (g,f))) are_homotopic

    proof

      take ( HopfHomotopy (f,g));

      thus thesis by Lm3;

    end;

    definition

      let T, t, f, g;

      :: original: HopfHomotopy

      redefine

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

      coherence

      proof

        thus (( LoopMlt (f,g)),( LoopMlt (g,f))) are_homotopic by Th13;

        thus thesis by Lm3;

      end;

    end

    registration

      let T, t;

      cluster ( pi_1 (T,t)) -> commutative;

      coherence

      proof

        set c = the constant Loop of t;

        set E = ( EqRel (T,t));

        let x,y be Element of ( pi_1 (T,t));

        consider f be Loop of t such that

         A1: x = ( Class (E,f)) by TOPALG_1: 47;

        consider g be Loop of t such that

         A2: y = ( Class (E,g)) by TOPALG_1: 47;



         A3: (x * y) = ( Class (E,(f + g))) & (y * x) = ( Class (E,(g + f))) by A1, A2, TOPALG_1: 61;



         A4: (f + g) = ( LoopMlt ((f + c),(c + g))) & (g + f) = ( LoopMlt ((g + c),(c + f))) by Th11;



         A5: (( LoopMlt (f,g)),( LoopMlt ((f + c),(c + g)))) are_homotopic by Th12;



         A6: (( LoopMlt (g,f)),( LoopMlt ((g + c),(c + f)))) are_homotopic by Th12;

        (( LoopMlt (f,g)),( LoopMlt (g,f))) are_homotopic by Th13;

        then (( LoopMlt (f,g)),( LoopMlt ((g + c),(c + f)))) are_homotopic by A6, BORSUK_6: 79;

        then (( LoopMlt ((f + c),(c + g))),( LoopMlt ((g + c),(c + f)))) are_homotopic by A5, BORSUK_6: 79;

        hence thesis by A3, A4, TOPALG_1: 46;

      end;

    end