:: TOPALG_4 semantic presentation

Lemma1: 1 in {1,2}
by TARSKI:def 2;

Lemma2: 2 in {1,2}
by TARSKI:def 2;

theorem Th1: :: TOPALG_4:1

for b₁, b₂ being non empty HGrStr
for b₃ being Element of (product <*b₁,b₂*>) ex b₄ being Element of b₁ex b₅ being Element of b₂ st b₃ = <*b₄,b₅*>

proof end;

definition

let c₁, c₂, c₃, c₄ be non empty HGrStr ;
let c₅ be Function of c₁,c₃;
let c₆ be Function of c₂,c₄;
func Gr2Iso c₅,c₆ -> Function of (product <*a₁,a₂*>),(product <*a₃,a₄*>) means :Def1: :: TOPALG_4:def 1
for b₁ being Element of (product <*a₁,a₂*>) ex b₂ being Element of a₁ex b₃ being Element of a₂ st
( b₁ = <*b₂,b₃*> & a₇ . b₁ = <*(a₅ . b₂),(a₆ . b₃)*> );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Gr2Iso TOPALG_4:def 1 :

theorem Th2: :: TOPALG_4:2

for b₁, b₂, b₃, b₄ being non empty HGrStr
for b₅ being Function of b₁,b₃
for b₆ being Function of b₂,b₄
for b₇ being Element of b₁
for b₈ being Element of b₂ holds (Gr2Iso b₅,b₆) . <*b₇,b₈*> = <*(b₅ . b₇),(b₆ . b₈)*>

proof end;

definition

let c₁, c₂, c₃, c₄ be Group;
let c₅ be Homomorphism of c₁,c₃;
let c₆ be Homomorphism of c₂,c₄;
redefine func Gr2Iso as Gr2Iso c₅,c₆ -> Homomorphism of (product <*a₁,a₂*>),(product <*a₃,a₄*>);
coherence

proof end;

end;

theorem Th3: :: TOPALG_4:3

for b₁, b₂, b₃, b₄ being non empty HGrStr
for b₅ being Function of b₁,b₃
for b₆ being Function of b₂,b₄ st b₅ is one-to-one & b₆ is one-to-one holds
Gr2Iso b₅,b₆ is one-to-one

proof end;

theorem Th4: :: TOPALG_4:4

for b₁, b₂, b₃, b₄ being non empty HGrStr
for b₅ being Function of b₁,b₃
for b₆ being Function of b₂,b₄ st b₅ is onto & b₆ is onto holds
Gr2Iso b₅,b₆ is onto

proof end;

theorem Th5: :: TOPALG_4:5

for b₁, b₂, b₃, b₄ being Group
for b₅ being Homomorphism of b₁,b₃
for b₆ being Homomorphism of b₂,b₄ st b₅ is being_isomorphism & b₆ is being_isomorphism holds
Gr2Iso b₅,b₆ is being_isomorphism

proof end;

theorem Th6: :: TOPALG_4:6

for b₁, b₂, b₃, b₄ being Group st b₁,b₃ are_isomorphic & b₂,b₄ are_isomorphic holds
product <*b₁,b₂*>, product <*b₃,b₄*> are_isomorphic

proof end;

set c₁ = the carrier of I[01] ;

reconsider c₂ = 0, c₃ = 1 as Point of I[01] by BORSUK_1:def 17, BORSUK_1:def 18;

theorem Th7: :: TOPALG_4:7

for b₁, b₂ being Function st dom b₁ = dom b₂ holds
pr1 <:b₁,b₂:> = b₁

proof end;

theorem Th8: :: TOPALG_4:8

for b₁, b₂ being Function st dom b₁ = dom b₂ holds
pr2 <:b₁,b₂:> = b₂

proof end;

definition

let c₄, c₅, c₆ be non empty TopSpace;
let c₇ be Function of c₆,c₄;
let c₈ be Function of c₆,c₅;
redefine func <: as <:c₄,c₅:> -> Function of a₃,[:a₁,a₂:];
coherence

proof end;

end;

definition

let c₄, c₅, c₆ be non empty TopSpace;
let c₇ be Function of c₆,[:c₄,c₅:];
redefine func pr1 as pr1 c₄ -> Function of a₃,a₁;
coherence

proof end;

redefine func pr2 as pr2 c₄ -> Function of a₃,a₂;
coherence

proof end;

end;

theorem Th9: :: TOPALG_4:9

for b₁, b₂, b₃ being non empty TopSpace
for b₄ being continuous Function of b₁,[:b₂,b₃:] holds pr1 b₄ is continuous

proof end;

theorem Th10: :: TOPALG_4:10

for b₁, b₂, b₃ being non empty TopSpace
for b₄ being continuous Function of b₁,[:b₂,b₃:] holds pr2 b₄ is continuous

proof end;

theorem Th11: :: TOPALG_4:11

for b₁, b₂ being non empty TopSpace
for b₃, b₄ being Point of b₁
for b₅, b₆ being Point of b₂ st [b₃,b₅],[b₄,b₆] are_connected holds
b₃,b₄ are_connected

proof end;

theorem Th12: :: TOPALG_4:12

for b₁, b₂ being non empty TopSpace
for b₃, b₄ being Point of b₁
for b₅, b₆ being Point of b₂ st [b₃,b₅],[b₄,b₆] are_connected holds
b₅,b₆ are_connected

proof end;

theorem Th13: :: TOPALG_4:13

for b₁, b₂ being non empty TopSpace
for b₃, b₄ being Point of b₁
for b₅, b₆ being Point of b₂ st [b₃,b₅],[b₄,b₆] are_connected holds
for b₇ being Path of [b₃,b₅],[b₄,b₆] holds pr1 b₇ is Path of b₃,b₄

proof end;

theorem Th14: :: TOPALG_4:14

for b₁, b₂ being non empty TopSpace
for b₃, b₄ being Point of b₁
for b₅, b₆ being Point of b₂ st [b₃,b₅],[b₄,b₆] are_connected holds
for b₇ being Path of [b₃,b₅],[b₄,b₆] holds pr2 b₇ is Path of b₅,b₆

proof end;

theorem Th15: :: TOPALG_4:15

for b₁, b₂ being non empty TopSpace
for b₃, b₄ being Point of b₁
for b₅, b₆ being Point of b₂ st b₃,b₄ are_connected & b₅,b₆ are_connected holds
[b₃,b₅],[b₄,b₆] are_connected

proof end;

theorem Th16: :: TOPALG_4:16

for b₁, b₂ being non empty TopSpace
for b₃, b₄ being Point of b₁
for b₅, b₆ being Point of b₂ st b₃,b₄ are_connected & b₅,b₆ are_connected holds
for b₇ being Path of b₃,b₄
for b₈ being Path of b₅,b₆ holds <:b₇,b₈:> is Path of [b₃,b₅],[b₄,b₆]

proof end;

definition

let c₄, c₅ be non empty arcwise_connected TopSpace;
let c₆, c₇ be Point of c₄;
let c₈, c₉ be Point of c₅;
let c₁₀ be Path of c₆,c₇;
let c₁₁ be Path of c₈,c₉;
redefine func <: as <:c₇,c₈:> -> Path of [a₃,a₅],[a₄,a₆];
coherence

proof end;

end;

definition

let c₄, c₅ be non empty TopSpace;
let c₆ be Point of c₄;
let c₇ be Point of c₅;
let c₈ be Loop of c₆;
let c₉ be Loop of c₇;
redefine func <: as <:c₅,c₆:> -> Loop of [a₃,a₄];
coherence by Th16;

end;

registration

let c₄, c₅ be non empty arcwise_connected TopSpace;
cluster [:a₁,a₂:] -> arcwise_connected ;
coherence

proof end;

end;

definition

let c₄, c₅ be non empty arcwise_connected TopSpace;
let c₆, c₇ be Point of c₄;
let c₈, c₉ be Point of c₅;
let c₁₀ be Path of [c₆,c₈],[c₇,c₉];
redefine func pr1 as pr1 c₇ -> Path of a₃,a₄;
coherence

proof end;

redefine func pr2 as pr2 c₇ -> Path of a₅,a₆;
coherence

proof end;

end;

definition

let c₄, c₅ be non empty TopSpace;
let c₆ be Point of c₄;
let c₇ be Point of c₅;
let c₈ be Loop of [c₆,c₇];
redefine func pr1 as pr1 c₅ -> Loop of a₃;
coherence by Th13;
redefine func pr2 as pr2 c₅ -> Loop of a₄;
coherence by Th14;

end;

Lemma19: for b₁, b₂ being non empty TopSpace
for b₃, b₄ being Point of b₁
for b₅, b₆ being Point of b₂
for b₇, b₈ being Path of [b₃,b₅],[b₄,b₆]
for b₉ being Homotopy of b₇,b₈ st b₇,b₈ are_homotopic holds
( pr1 b₉ is continuous & ( for b₁₀ being Point of I[01] holds
( (pr1 b₉) . b₁₀,0 = (pr1 b₇) . b₁₀ & (pr1 b₉) . b₁₀,1 = (pr1 b₈) . b₁₀ & ( for b₁₁ being Point of I[01] holds
( (pr1 b₉) . 0,b₁₁ = b₃ & (pr1 b₉) . 1,b₁₁ = b₄ ) ) ) ) )

proof end;

Lemma20: for b₁, b₂ being non empty TopSpace
for b₃, b₄ being Point of b₁
for b₅, b₆ being Point of b₂
for b₇, b₈ being Path of [b₃,b₅],[b₄,b₆]
for b₉ being Homotopy of b₇,b₈ st b₇,b₈ are_homotopic holds
( pr2 b₉ is continuous & ( for b₁₀ being Point of I[01] holds
( (pr2 b₉) . b₁₀,0 = (pr2 b₇) . b₁₀ & (pr2 b₉) . b₁₀,1 = (pr2 b₈) . b₁₀ & ( for b₁₁ being Point of I[01] holds
( (pr2 b₉) . 0,b₁₁ = b₅ & (pr2 b₉) . 1,b₁₁ = b₆ ) ) ) ) )

proof end;

theorem Th17: :: TOPALG_4:17

for b₁, b₂ being non empty TopSpace
for b₃, b₄ being Point of b₁
for b₅, b₆ being Point of b₂
for b₇, b₈ being Path of [b₃,b₅],[b₄,b₆]
for b₉ being Homotopy of b₇,b₈
for b₁₀, b₁₁ being Path of b₃,b₄ st b₁₀ = pr1 b₇ & b₁₁ = pr1 b₈ & b₇,b₈ are_homotopic holds
pr1 b₉ is Homotopy of b₁₀,b₁₁

proof end;

theorem Th18: :: TOPALG_4:18

for b₁, b₂ being non empty TopSpace
for b₃, b₄ being Point of b₁
for b₅, b₆ being Point of b₂
for b₇, b₈ being Path of [b₃,b₅],[b₄,b₆]
for b₉ being Homotopy of b₇,b₈
for b₁₀, b₁₁ being Path of b₅,b₆ st b₁₀ = pr2 b₇ & b₁₁ = pr2 b₈ & b₇,b₈ are_homotopic holds
pr2 b₉ is Homotopy of b₁₀,b₁₁

proof end;

theorem Th19: :: TOPALG_4:19

for b₁, b₂ being non empty TopSpace
for b₃, b₄ being Point of b₁
for b₅, b₆ being Point of b₂
for b₇, b₈ being Path of [b₃,b₅],[b₄,b₆]
for b₉, b₁₀ being Path of b₃,b₄ st b₉ = pr1 b₇ & b₁₀ = pr1 b₈ & b₇,b₈ are_homotopic holds
b₉,b₁₀ are_homotopic

proof end;

theorem Th20: :: TOPALG_4:20

for b₁, b₂ being non empty TopSpace
for b₃, b₄ being Point of b₁
for b₅, b₆ being Point of b₂
for b₇, b₈ being Path of [b₃,b₅],[b₄,b₆]
for b₉, b₁₀ being Path of b₅,b₆ st b₉ = pr2 b₇ & b₁₀ = pr2 b₈ & b₇,b₈ are_homotopic holds
b₉,b₁₀ are_homotopic

proof end;

Lemma23: for b₁, b₂ being non empty TopSpace
for b₃, b₄ being Point of b₁
for b₅, b₆ being Point of b₂
for b₇, b₈ being Path of [b₃,b₅],[b₄,b₆]
for b₉, b₁₀ being Path of b₃,b₄
for b₁₁, b₁₂ being Path of b₅,b₆
for b₁₃ being Homotopy of b₉,b₁₀
for b₁₄ being Homotopy of b₁₁,b₁₂ st b₉ = pr1 b₇ & b₁₀ = pr1 b₈ & b₁₁ = pr2 b₇ & b₁₂ = pr2 b₈ & b₉,b₁₀ are_homotopic & b₁₁,b₁₂ are_homotopic holds
( <:b₁₃,b₁₄:> is continuous & ( for b₁₅ being Point of I[01] holds
( <:b₁₃,b₁₄:> . b₁₅,0 = b₇ . b₁₅ & <:b₁₃,b₁₄:> . b₁₅,1 = b₈ . b₁₅ & ( for b₁₆ being Point of I[01] holds
( <:b₁₃,b₁₄:> . 0,b₁₆ = [b₃,b₅] & <:b₁₃,b₁₄:> . 1,b₁₆ = [b₄,b₆] ) ) ) ) )

proof end;

theorem Th21: :: TOPALG_4:21

for b₁, b₂ being non empty TopSpace
for b₃, b₄ being Point of b₁
for b₅, b₆ being Point of b₂
for b₇, b₈ being Path of [b₃,b₅],[b₄,b₆]
for b₉, b₁₀ being Path of b₃,b₄
for b₁₁, b₁₂ being Path of b₅,b₆
for b₁₃ being Homotopy of b₉,b₁₀
for b₁₄ being Homotopy of b₁₁,b₁₂ st b₉ = pr1 b₇ & b₁₀ = pr1 b₈ & b₁₁ = pr2 b₇ & b₁₂ = pr2 b₈ & b₉,b₁₀ are_homotopic & b₁₁,b₁₂ are_homotopic holds
<:b₁₃,b₁₄:> is Homotopy of b₇,b₈

proof end;

theorem Th22: :: TOPALG_4:22

for b₁, b₂ being non empty TopSpace
for b₃, b₄ being Point of b₁
for b₅, b₆ being Point of b₂
for b₇, b₈ being Path of [b₃,b₅],[b₄,b₆]
for b₉, b₁₀ being Path of b₃,b₄
for b₁₁, b₁₂ being Path of b₅,b₆ st b₉ = pr1 b₇ & b₁₀ = pr1 b₈ & b₁₁ = pr2 b₇ & b₁₂ = pr2 b₈ & b₉,b₁₀ are_homotopic & b₁₁,b₁₂ are_homotopic holds
b₇,b₈ are_homotopic

proof end;

theorem Th23: :: TOPALG_4:23

for b₁, b₂ being non empty TopSpace
for b₃, b₄, b₅ being Point of b₁
for b₆, b₇, b₈ being Point of b₂
for b₉ being Path of [b₃,b₆],[b₄,b₇]
for b₁₀ being Path of [b₄,b₇],[b₅,b₈]
for b₁₁ being Path of b₃,b₄
for b₁₂ being Path of b₄,b₅ st [b₃,b₆],[b₄,b₇] are_connected & [b₄,b₇],[b₅,b₈] are_connected & b₁₁ = pr1 b₉ & b₁₂ = pr1 b₁₀ holds
pr1 (b₉ + b₁₀) = b₁₁ + b₁₂

proof end;

theorem Th24: :: TOPALG_4:24

for b₁, b₂ being non empty arcwise_connected TopSpace
for b₃, b₄, b₅ being Point of b₁
for b₆, b₇, b₈ being Point of b₂
for b₉ being Path of [b₃,b₆],[b₄,b₇]
for b₁₀ being Path of [b₄,b₇],[b₅,b₈] holds pr1 (b₉ + b₁₀) = (pr1 b₉) + (pr1 b₁₀)

proof end;

theorem Th25: :: TOPALG_4:25

for b₁, b₂ being non empty TopSpace
for b₃, b₄, b₅ being Point of b₁
for b₆, b₇, b₈ being Point of b₂
for b₉ being Path of [b₃,b₆],[b₄,b₇]
for b₁₀ being Path of [b₄,b₇],[b₅,b₈]
for b₁₁ being Path of b₆,b₇
for b₁₂ being Path of b₇,b₈ st [b₃,b₆],[b₄,b₇] are_connected & [b₄,b₇],[b₅,b₈] are_connected & b₁₁ = pr2 b₉ & b₁₂ = pr2 b₁₀ holds
pr2 (b₉ + b₁₀) = b₁₁ + b₁₂

proof end;

theorem Th26: :: TOPALG_4:26

proof end;

definition

let c₄, c₅ be non empty TopSpace;
let c₆ be Point of c₄;
let c₇ be Point of c₅;
set c₈ = pi_1 [:c₄,c₅:],[c₆,c₇];
set c₉ = <*(pi_1 c₄,c₆),(pi_1 c₅,c₇)*>;
set c₁₀ = product <*(pi_1 c₄,c₆),(pi_1 c₅,c₇)*>;
func FGPrIso c₃,c₄ -> Function of (pi_1 [:a₁,a₂:],[a₃,a₄]),(product <*(pi_1 a₁,a₃),(pi_1 a₂,a₄)*>) means :Def2: :: TOPALG_4:def 2
for b₁ being Point of (pi_1 [:a₁,a₂:],[a₃,a₄]) ex b₂ being Loop of [a₃,a₄] st
( b₁ = Class (EqRel [:a₁,a₂:],[a₃,a₄]),b₂ & a₅ . b₁ = <*(Class (EqRel a₁,a₃),(pr1 b₂)),(Class (EqRel a₂,a₄),(pr2 b₂))*> );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines FGPrIso TOPALG_4:def 2 :

theorem Th27: :: TOPALG_4:27

for b₁, b₂ being non empty TopSpace
for b₃ being Point of b₁
for b₄ being Point of b₂
for b₅ being Point of (pi_1 [:b₁,b₂:],[b₃,b₄])
for b₆ being Loop of [b₃,b₄] st b₅ = Class (EqRel [:b₁,b₂:],[b₃,b₄]),b₆ holds
(FGPrIso b₃,b₄) . b₅ = <*(Class (EqRel b₁,b₃),(pr1 b₆)),(Class (EqRel b₂,b₄),(pr2 b₆))*>

proof end;

theorem Th28: :: TOPALG_4:28

for b₁, b₂ being non empty TopSpace
for b₃ being Point of b₁
for b₄ being Point of b₂
for b₅ being Loop of [b₃,b₄] holds (FGPrIso b₃,b₄) . (Class (EqRel [:b₁,b₂:],[b₃,b₄]),b₅) = <*(Class (EqRel b₁,b₃),(pr1 b₅)),(Class (EqRel b₂,b₄),(pr2 b₅))*>

proof end;

registration

let c₄, c₅ be non empty TopSpace;
let c₆ be Point of c₄;
let c₇ be Point of c₅;
cluster FGPrIso a₃,a₄ -> one-to-one onto ;
coherence

proof end;

end;

definition

let c₄, c₅ be non empty TopSpace;
let c₆ be Point of c₄;
let c₇ be Point of c₅;
redefine func FGPrIso as FGPrIso c₃,c₄ -> Homomorphism of (pi_1 [:a₁,a₂:],[a₃,a₄]),(product <*(pi_1 a₁,a₃),(pi_1 a₂,a₄)*>);
coherence

proof end;

end;

theorem Th29: :: TOPALG_4:29

for b₁, b₂ being non empty TopSpace
for b₃ being Point of b₁
for b₄ being Point of b₂ holds FGPrIso b₃,b₄ is being_isomorphism

proof end;

theorem Th30: :: TOPALG_4:30

for b₁, b₂ being non empty TopSpace
for b₃ being Point of b₁
for b₄ being Point of b₂ holds pi_1 [:b₁,b₂:],[b₃,b₄], product <*(pi_1 b₁,b₃),(pi_1 b₂,b₄)*> are_isomorphic

proof end;

theorem Th31: :: TOPALG_4:31

for b₁, b₂ being non empty TopSpace
for b₃, b₄ being Point of b₁
for b₅, b₆ being Point of b₂
for b₇ being Homomorphism of (pi_1 b₁,b₃),(pi_1 b₁,b₄)
for b₈ being Homomorphism of (pi_1 b₂,b₅),(pi_1 b₂,b₆) st b₇ is being_isomorphism & b₈ is being_isomorphism holds
(Gr2Iso b₇,b₈) * (FGPrIso b₃,b₅) is being_isomorphism

proof end;

theorem Th32: :: TOPALG_4:32

for b₁, b₂ being non empty arcwise_connected TopSpace
for b₃, b₄ being Point of b₁
for b₅, b₆ being Point of b₂ holds pi_1 [:b₁,b₂:],[b₃,b₅], product <*(pi_1 b₁,b₄),(pi_1 b₂,b₆)*> are_isomorphic

proof end;