:: On the Fundamental Groups of Products of Topological Spaces
:: by Artur Korni{\l}owicz
::
:: Received August 20, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

Lm1:  1 in {1,2}
by TARSKI:def_2;

Lm2:  2 in {1,2}
by TARSKI:def_2;

theorem Th1: :: TOPALG_4:1
for G, H being non empty multMagma
for x being Element of (product <*G,H*>) ex g being Element of G ex h being Element of H st x = <*g,h*>
proofend;

definition
let G1, G2, H1, H2 be non empty multMagma ;
let f be Function of G1,H1;
let g be Function of G2,H2;
func Gr2Iso (f,g) ->  Function of (product <*G1,G2*>),(product <*H1,H2*>) means :Def1: :: TOPALG_4:def 1
 for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st
( x = <*x1,x2*> &amp; it . x = <*(f . x1),(g . x2)*> );
existence
 ex b1 being Function of (product <*G1,G2*>),(product <*H1,H2*>) st
for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st
( x = <*x1,x2*> &amp; b1 . x = <*(f . x1),(g . x2)*> )
proofend;
uniqueness
 for b1, b2 being Function of (product <*G1,G2*>),(product <*H1,H2*>) st ( for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st
( x = <*x1,x2*> &amp; b1 . x = <*(f . x1),(g . x2)*> ) ) &amp; ( for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st
( x = <*x1,x2*> &amp; b2 . x = <*(f . x1),(g . x2)*> ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines Gr2Iso TOPALG_4:def_1_:_
 for G1, G2, H1, H2 being non empty multMagma
for f being Function of G1,H1
for g being Function of G2,H2
for b7 being Function of (product <*G1,G2*>),(product <*H1,H2*>) holds
( b7 = Gr2Iso (f,g) iff for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st
( x = <*x1,x2*> &amp; b7 . x = <*(f . x1),(g . x2)*> ) );

theorem :: TOPALG_4:2
for G1, G2, H1, H2 being non empty multMagma
for f being Function of G1,H1
for g being Function of G2,H2
for x1 being Element of G1
for x2 being Element of G2 holds (Gr2Iso (f,g)) . <*x1,x2*> = <*(f . x1),(g . x2)*>
proofend;

registration
let G1, G2, H1, H2 be Group;
let f be Homomorphism of G1,H1;
let g be Homomorphism of G2,H2;
cluster Gr2Iso (f,g) ->  multiplicative ;
coherence
 Gr2Iso (f,g) is multiplicative
proofend;
end;

theorem Th3: :: TOPALG_4:3
for G1, G2, H1, H2 being non empty multMagma
for f being Function of G1,H1
for g being Function of G2,H2 st f is one-to-one &amp; g is one-to-one holds
Gr2Iso (f,g) is one-to-one
proofend;

theorem Th4: :: TOPALG_4:4
for G1, G2, H1, H2 being non empty multMagma
for f being Function of G1,H1
for g being Function of G2,H2 st f is onto &amp; g is onto holds
Gr2Iso (f,g) is onto
proofend;

theorem Th5: :: TOPALG_4:5
for G1, G2, H1, H2 being Group
for f being Homomorphism of G1,H1
for g being Homomorphism of G2,H2 st f is bijective &amp; g is bijective holds
Gr2Iso (f,g) is bijective
proofend;

theorem Th6: :: TOPALG_4:6
for G1, G2, H1, H2 being Group st G1,H1 are_isomorphic &amp; G2,H2 are_isomorphic holds
product <*G1,G2*>, product <*H1,H2*> are_isomorphic
proofend;

begin

set I = the carrier of I[01];

reconsider j0 = 0 , j1 = 1 as Point of I[01] by BORSUK_1:def_14, BORSUK_1:def_15;

theorem Th7: :: TOPALG_4:7
for f, g being Function st dom f = dom g holds
pr1 <:f,g:> = f
proofend;

theorem Th8: :: TOPALG_4:8
for f, g being Function st dom f = dom g holds
pr2 <:f,g:> = g
proofend;

definition
let S, T, Y be non empty TopSpace;
let f be Function of Y,S;
let g be Function of Y,T;
:: original:<:
redefine func<:f,g:> ->  Function of Y,[:S,T:];
coherence
 <:f,g:> is Function of Y,[:S,T:]
proofend;
end;

definition
let S, T, Y be non empty TopSpace;
let f be Function of Y,[:S,T:];
:: original:pr1
redefine func pr1 f ->  Function of Y,S;
coherence
 pr1 f is Function of Y,S
proofend;
:: original:pr2
redefine func pr2 f ->  Function of Y,T;
coherence
 pr2 f is Function of Y,T
proofend;
end;

theorem Th9: :: TOPALG_4:9
for Y, S, T being non empty TopSpace
for f being continuous Function of Y,[:S,T:] holds pr1 f is continuous
proofend;

theorem Th10: :: TOPALG_4:10
for Y, S, T being non empty TopSpace
for f being continuous Function of Y,[:S,T:] holds pr2 f is continuous
proofend;

theorem Th11: :: TOPALG_4:11
for S, T being non empty TopSpace
for s1, s2 being Point of S
for t1, t2 being Point of T st [s1,t1],[s2,t2] are_connected holds
s1,s2 are_connected
proofend;

theorem Th12: :: TOPALG_4:12
for S, T being non empty TopSpace
for s1, s2 being Point of S
for t1, t2 being Point of T st [s1,t1],[s2,t2] are_connected holds
t1,t2 are_connected
proofend;

theorem Th13: :: TOPALG_4:13
for S, T being non empty TopSpace
for s1, s2 being Point of S
for t1, t2 being Point of T st [s1,t1],[s2,t2] are_connected holds
for L being Path of [s1,t1],[s2,t2] holds pr1 L is Path of s1,s2
proofend;

theorem Th14: :: TOPALG_4:14
for S, T being non empty TopSpace
for s1, s2 being Point of S
for t1, t2 being Point of T st [s1,t1],[s2,t2] are_connected holds
for L being Path of [s1,t1],[s2,t2] holds pr2 L is Path of t1,t2
proofend;

theorem Th15: :: TOPALG_4:15
for S, T being non empty TopSpace
for s1, s2 being Point of S
for t1, t2 being Point of T st s1,s2 are_connected &amp; t1,t2 are_connected holds
[s1,t1],[s2,t2] are_connected
proofend;

theorem Th16: :: TOPALG_4:16
for S, T being non empty TopSpace
for s1, s2 being Point of S
for t1, t2 being Point of T st s1,s2 are_connected &amp; t1,t2 are_connected holds
for L1 being Path of s1,s2
for L2 being Path of t1,t2 holds <:L1,L2:> is Path of [s1,t1],[s2,t2]
proofend;

definition
let S, T be non empty pathwise_connected TopSpace;
let s1, s2 be Point of S;
let t1, t2 be Point of T;
let L1 be Path of s1,s2;
let L2 be Path of t1,t2;
:: original:<:
redefine func<:L1,L2:> ->  Path of [s1,t1],[s2,t2];
coherence
 <:L1,L2:> is Path of [s1,t1],[s2,t2]
proofend;
end;

definition
let S, T be non empty TopSpace;
let s be Point of S;
let t be Point of T;
let L1 be Loop of s;
let L2 be Loop of t;
:: original:<:
redefine func<:L1,L2:> ->  Loop of [s,t];
coherence
 <:L1,L2:> is Loop of [s,t] by Th16;
end;

registration
let S, T be non empty pathwise_connected TopSpace;
cluster[:S,T:] ->  pathwise_connected ;
coherence
 [:S,T:] is pathwise_connected
proofend;
end;

definition
let S, T be non empty pathwise_connected TopSpace;
let s1, s2 be Point of S;
let t1, t2 be Point of T;
let L be Path of [s1,t1],[s2,t2];
:: original:pr1
redefine func pr1 L ->  Path of s1,s2;
coherence
 pr1 L is Path of s1,s2
proofend;
:: original:pr2
redefine func pr2 L ->  Path of t1,t2;
coherence
 pr2 L is Path of t1,t2
proofend;
end;

definition
let S, T be non empty TopSpace;
let s be Point of S;
let t be Point of T;
let L be Loop of [s,t];
:: original:pr1
redefine func pr1 L ->  Loop of s;
coherence
 pr1 L is Loop of s by Th13;
:: original:pr2
redefine func pr2 L ->  Loop of t;
coherence
 pr2 L is Loop of t by Th14;
end;

Lm3:  for S, T being non empty TopSpace
for s1, s2 being Point of S
for t1, t2 being Point of T
for l1, l2 being Path of [s1,t1],[s2,t2]
for H being Homotopy of l1,l2 st l1,l2 are_homotopic holds
( pr1 H is continuous &amp; ( for a being Point of I[01] holds
( (pr1 H) . (a,0) = (pr1 l1) . a &amp; (pr1 H) . (a,1) = (pr1 l2) . a &amp; ( for b being Point of I[01] holds
( (pr1 H) . (0,b) = s1 &amp; (pr1 H) . (1,b) = s2 ) ) ) ) )
proofend;

Lm4:  for S, T being non empty TopSpace
for s1, s2 being Point of S
for t1, t2 being Point of T
for l1, l2 being Path of [s1,t1],[s2,t2]
for H being Homotopy of l1,l2 st l1,l2 are_homotopic holds
( pr2 H is continuous &amp; ( for a being Point of I[01] holds
( (pr2 H) . (a,0) = (pr2 l1) . a &amp; (pr2 H) . (a,1) = (pr2 l2) . a &amp; ( for b being Point of I[01] holds
( (pr2 H) . (0,b) = t1 &amp; (pr2 H) . (1,b) = t2 ) ) ) ) )
proofend;

theorem :: TOPALG_4:17
for S, T being non empty TopSpace
for s1, s2 being Point of S
for t1, t2 being Point of T
for l1, l2 being Path of [s1,t1],[s2,t2]
for H being Homotopy of l1,l2
for p, q being Path of s1,s2 st p = pr1 l1 &amp; q = pr1 l2 &amp; l1,l2 are_homotopic holds
pr1 H is Homotopy of p,q
proofend;

theorem :: TOPALG_4:18
for S, T being non empty TopSpace
for s1, s2 being Point of S
for t1, t2 being Point of T
for l1, l2 being Path of [s1,t1],[s2,t2]
for H being Homotopy of l1,l2
for p, q being Path of t1,t2 st p = pr2 l1 &amp; q = pr2 l2 &amp; l1,l2 are_homotopic holds
pr2 H is Homotopy of p,q
proofend;

theorem Th19: :: TOPALG_4:19
for S, T being non empty TopSpace
for s1, s2 being Point of S
for t1, t2 being Point of T
for l1, l2 being Path of [s1,t1],[s2,t2]
for p, q being Path of s1,s2 st p = pr1 l1 &amp; q = pr1 l2 &amp; l1,l2 are_homotopic holds
p,q are_homotopic
proofend;

theorem Th20: :: TOPALG_4:20
for S, T being non empty TopSpace
for s1, s2 being Point of S
for t1, t2 being Point of T
for l1, l2 being Path of [s1,t1],[s2,t2]
for p, q being Path of t1,t2 st p = pr2 l1 &amp; q = pr2 l2 &amp; l1,l2 are_homotopic holds
p,q are_homotopic
proofend;

Lm5:  for S, T being non empty TopSpace
for s1, s2 being Point of S
for t1, t2 being Point of T
for l1, l2 being Path of [s1,t1],[s2,t2]
for p, q being Path of s1,s2
for x, y being Path of t1,t2
for f being Homotopy of p,q
for g being Homotopy of x,y st p = pr1 l1 &amp; q = pr1 l2 &amp; x = pr2 l1 &amp; y = pr2 l2 &amp; p,q are_homotopic &amp; x,y are_homotopic holds
( <:f,g:> is continuous &amp; ( for a being Point of I[01] holds
( <:f,g:> . (a,0) = l1 . a &amp; <:f,g:> . (a,1) = l2 . a &amp; ( for b being Point of I[01] holds
( <:f,g:> . (0,b) = [s1,t1] &amp; <:f,g:> . (1,b) = [s2,t2] ) ) ) ) )
proofend;

theorem :: TOPALG_4:21
for S, T being non empty TopSpace
for s1, s2 being Point of S
for t1, t2 being Point of T
for l1, l2 being Path of [s1,t1],[s2,t2]
for p, q being Path of s1,s2
for x, y being Path of t1,t2
for f being Homotopy of p,q
for g being Homotopy of x,y st p = pr1 l1 &amp; q = pr1 l2 &amp; x = pr2 l1 &amp; y = pr2 l2 &amp; p,q are_homotopic &amp; x,y are_homotopic holds
<:f,g:> is Homotopy of l1,l2
proofend;

theorem Th22: :: TOPALG_4:22
for S, T being non empty TopSpace
for s1, s2 being Point of S
for t1, t2 being Point of T
for l1, l2 being Path of [s1,t1],[s2,t2]
for p, q being Path of s1,s2
for x, y being Path of t1,t2 st p = pr1 l1 &amp; q = pr1 l2 &amp; x = pr2 l1 &amp; y = pr2 l2 &amp; p,q are_homotopic &amp; x,y are_homotopic holds
l1,l2 are_homotopic
proofend;

theorem Th23: :: TOPALG_4:23
for S, T being non empty TopSpace
for s1, s2, s3 being Point of S
for t1, t2, t3 being Point of T
for l1 being Path of [s1,t1],[s2,t2]
for l2 being Path of [s2,t2],[s3,t3]
for p1 being Path of s1,s2
for p2 being Path of s2,s3 st [s1,t1],[s2,t2] are_connected &amp; [s2,t2],[s3,t3] are_connected &amp; p1 = pr1 l1 &amp; p2 = pr1 l2 holds
pr1 (l1 + l2) = p1 + p2
proofend;

theorem :: TOPALG_4:24
for S, T being non empty pathwise_connected TopSpace
for s1, s2, s3 being Point of S
for t1, t2, t3 being Point of T
for l1 being Path of [s1,t1],[s2,t2]
for l2 being Path of [s2,t2],[s3,t3] holds pr1 (l1 + l2) = (pr1 l1) + (pr1 l2)
proofend;

theorem Th25: :: TOPALG_4:25
for S, T being non empty TopSpace
for s1, s2, s3 being Point of S
for t1, t2, t3 being Point of T
for l1 being Path of [s1,t1],[s2,t2]
for l2 being Path of [s2,t2],[s3,t3]
for p1 being Path of t1,t2
for p2 being Path of t2,t3 st [s1,t1],[s2,t2] are_connected &amp; [s2,t2],[s3,t3] are_connected &amp; p1 = pr2 l1 &amp; p2 = pr2 l2 holds
pr2 (l1 + l2) = p1 + p2
proofend;

theorem :: TOPALG_4:26
for S, T being non empty pathwise_connected TopSpace
for s1, s2, s3 being Point of S
for t1, t2, t3 being Point of T
for l1 being Path of [s1,t1],[s2,t2]
for l2 being Path of [s2,t2],[s3,t3] holds pr2 (l1 + l2) = (pr2 l1) + (pr2 l2)
proofend;

definition
let S, T be non empty TopSpace;
let s be Point of S;
let t be Point of T;
set pS = pi_1 ([:S,T:],[s,t]);
set G = <*(pi_1 (S,s)),(pi_1 (T,t))*>;
set pT = product <*(pi_1 (S,s)),(pi_1 (T,t))*>;
func FGPrIso (s,t) ->  Function of (pi_1 ([:S,T:],[s,t])),(product <*(pi_1 (S,s)),(pi_1 (T,t))*>) means :Def2: :: TOPALG_4:def 2
 for x being Point of (pi_1 ([:S,T:],[s,t])) ex l being Loop of [s,t] st
( x = Class ((EqRel ([:S,T:],[s,t])),l) &amp; it . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> );
existence
 ex b1 being Function of (pi_1 ([:S,T:],[s,t])),(product <*(pi_1 (S,s)),(pi_1 (T,t))*>) st
for x being Point of (pi_1 ([:S,T:],[s,t])) ex l being Loop of [s,t] st
( x = Class ((EqRel ([:S,T:],[s,t])),l) &amp; b1 . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> )
proofend;
uniqueness
 for b1, b2 being Function of (pi_1 ([:S,T:],[s,t])),(product <*(pi_1 (S,s)),(pi_1 (T,t))*>) st ( for x being Point of (pi_1 ([:S,T:],[s,t])) ex l being Loop of [s,t] st
( x = Class ((EqRel ([:S,T:],[s,t])),l) &amp; b1 . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> ) ) &amp; ( for x being Point of (pi_1 ([:S,T:],[s,t])) ex l being Loop of [s,t] st
( x = Class ((EqRel ([:S,T:],[s,t])),l) &amp; b2 . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines FGPrIso TOPALG_4:def_2_:_
 for S, T being non empty TopSpace
for s being Point of S
for t being Point of T
for b5 being Function of (pi_1 ([:S,T:],[s,t])),(product <*(pi_1 (S,s)),(pi_1 (T,t))*>) holds
( b5 = FGPrIso (s,t) iff for x being Point of (pi_1 ([:S,T:],[s,t])) ex l being Loop of [s,t] st
( x = Class ((EqRel ([:S,T:],[s,t])),l) &amp; b5 . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> ) );

theorem Th27: :: TOPALG_4:27
for S, T being non empty TopSpace
for s being Point of S
for t being Point of T
for x being Point of (pi_1 ([:S,T:],[s,t]))
for l being Loop of [s,t] st x = Class ((EqRel ([:S,T:],[s,t])),l) holds
(FGPrIso (s,t)) . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*>
proofend;

theorem Th28: :: TOPALG_4:28
for S, T being non empty TopSpace
for s being Point of S
for t being Point of T
for l being Loop of [s,t] holds (FGPrIso (s,t)) . (Class ((EqRel ([:S,T:],[s,t])),l)) = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*>
proofend;

registration
let S, T be non empty TopSpace;
let s be Point of S;
let t be Point of T;
cluster FGPrIso (s,t) ->  one-to-one onto ;
coherence
 ( FGPrIso (s,t) is one-to-one &amp; FGPrIso (s,t) is onto )
proofend;
end;

registration
let S, T be non empty TopSpace;
let s be Point of S;
let t be Point of T;
cluster FGPrIso (s,t) ->  multiplicative ;
coherence
 FGPrIso (s,t) is multiplicative
proofend;
end;

theorem Th29: :: TOPALG_4:29
for S, T being non empty TopSpace
for s being Point of S
for t being Point of T holds FGPrIso (s,t) is bijective
proofend;

theorem Th30: :: TOPALG_4:30
for S, T being non empty TopSpace
for s being Point of S
for t being Point of T holds pi_1 ([:S,T:],[s,t]), product <*(pi_1 (S,s)),(pi_1 (T,t))*> are_isomorphic
proofend;

theorem :: TOPALG_4:31
for S, T being non empty TopSpace
for s1, s2 being Point of S
for t1, t2 being Point of T
for f being Homomorphism of (pi_1 (S,s1)),(pi_1 (S,s2))
for g being Homomorphism of (pi_1 (T,t1)),(pi_1 (T,t2)) st f is bijective &amp; g is bijective holds
(Gr2Iso (f,g)) * (FGPrIso (s1,t1)) is bijective
proofend;

theorem :: TOPALG_4:32
for S, T being non empty pathwise_connected TopSpace
for s1, s2 being Point of S
for t1, t2 being Point of T holds pi_1 ([:S,T:],[s1,t1]), product <*(pi_1 (S,s2)),(pi_1 (T,t2))*> are_isomorphic
proofend;