(*

This file is a part of IsarMathLib -

a library of formalized mathematics written for Isabelle/Isar.

Copyright (C) 2009-2013 Slawomir Kolodynski

This program is free software; Redistribution and use in source and binary forms,

with or without modification, are permitted provided that the following conditions are met:

1. Redistributions of source code must retain the above copyright notice,

this list of conditions and the following disclaimer.

2. Redistributions in binary form must reproduce the above copyright notice,

this list of conditions and the following disclaimer in the documentation and/or

other materials provided with the distribution.

3. The name of the author may not be used to endorse or promote products

derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES,

INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A

PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT,

INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT

LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES LOSS OF USE, DATA, OR PROFITS OR

BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,

STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE

USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

*)

header{*\isaheader{TopologicalGroup\_ZF.thy}*}

theory TopologicalGroup_ZF imports Topology_ZF_3 Group_ZF_1 Semigroup_ZF

begin

text{*This theory is about the first subject of algebraic topology:

topological groups.*}

section{*Topological group: definition and notation*}

text{*Topological group is a group that is a topological space

at the same time. This means that a topological group is a triple of sets,

say $(G,f,T)$ such that $T$ is a topology on $G$, $f$ is a group

operation on $G$ and both $f$ and the operation of taking inverse in $G$

are continuous. Since IsarMathLib defines topology without using the carrier,

(see @{text "Topology_ZF"}), in our setup we just use $\bigcup T$ instead

of $G$ and say that the pair of sets $(\bigcup T , f)$ is a group.

This way our definition of being a topological group is a statement about two

sets: the topology $T$ and the group operation $f$ on $G=\bigcup T$.

Since the domain of the group operation is $G\times G$, the pair of

topologies in which $f$ is supposed to be continuous is $T$ and

the product topology on $G\times G$ (which we will call $\tau$ below).*}

text{*This way we arrive at the following definition of a predicate that

states that pair of sets is a topological group.*}

definition

"IsAtopologicalGroup(T,f) ≡ (T {is a topology}) ∧ IsAgroup(\<Union>T,f) ∧

IsContinuous(ProductTopology(T,T),T,f) ∧

IsContinuous(T,T,GroupInv(\<Union>T,f))"

text{*We will inherit notation from the @{text "topology0"} locale. That locale assumes that

$T$ is a topology. For convenience we will denote $G=\bigcup T$ and $\tau$ to be

the product topology on $G\times G$. To that we add some

notation specific to groups. We will use additive notation

for the group operation, even though we don't assume that the group is abelian.

The notation $g+A$ will mean the left translation of the set $A$ by element $g$, i.e.

$g+A=\{g+a|a\in A\}$.

The group operation $G$ induces a natural operation on the subsets of $G$

defined as $\langle A,B\rangle \mapsto \{x+y | x\in A, y\in B \}$.

Such operation has been considered in @{text "func_ZF"} and called

$f$ ''lifted to subsets of'' $G$. We will denote the value of such operation

on sets $A,B$ as $A+B$.

The set of neigboorhoods of zero (denoted @{text "\<N>⇩_{0}"}) is the

collection of (not necessarily open) sets whose interior contains the neutral

element of the group.*}

locale topgroup = topology0 +

fixes G

defines G_def [simp]: "G ≡ \<Union>T"

fixes prodtop ("τ")

defines prodtop_def [simp]: "τ ≡ ProductTopology(T,T)"

fixes f

assumes Ggroup: "IsAgroup(G,f)"

assumes fcon: "IsContinuous(τ,T,f)"

assumes inv_cont: "IsContinuous(T,T,GroupInv(G,f))"

fixes grop (infixl "\<ra>" 90)

defines grop_def [simp]: "x\<ra>y ≡ f`⟨x,y⟩"

fixes grinv ("\<rm> _" 89)

defines grinv_def [simp]: "(\<rm>x) ≡ GroupInv(G,f)`(x)"

fixes grsub (infixl "\<rs>" 90)

defines grsub_def [simp]: "x\<rs>y ≡ x\<ra>(\<rm>y)"

fixes setinv ("\<sm> _" 72)

defines setninv_def [simp]: "\<sm>A ≡ GroupInv(G,f)``(A)"

fixes ltrans (infix "\<ltr>" 73)

defines ltrans_def [simp]: "x \<ltr> A ≡ LeftTranslation(G,f,x)``(A)"

fixes rtrans (infix "\<rtr>" 73)

defines rtrans_def [simp]: "A \<rtr> x ≡ RightTranslation(G,f,x)``(A)"

fixes setadd (infixl "\<sad>" 71)

defines setadd_def [simp]: "A\<sad>B ≡ (f {lifted to subsets of} G)`⟨A,B⟩"

fixes gzero ("\<zero>")

defines gzero_def [simp]: "\<zero> ≡ TheNeutralElement(G,f)"

fixes zerohoods ("\<N>⇩_{0}")

defines zerohoods_def [simp]: "\<N>⇩_{0}≡ {A ∈ Pow(G). \<zero> ∈ int(A)}"

fixes listsum ("∑ _" 70)

defines listsum_def[simp]: "∑k ≡ Fold1(f,k)"

text{*The first lemma states that we indeeed talk about topological group

in the context of @{text "topgroup"} locale.*}

lemma (in topgroup) topGroup: shows "IsAtopologicalGroup(T,f)"

using topSpaceAssum Ggroup fcon inv_cont IsAtopologicalGroup_def

by simp;

text{* If a pair of sets $(T,f)$ forms a topological group, then

all theorems proven in the @{text "topgroup"} context are valid as applied to

$(T,f)$.*}

lemma topGroupLocale: assumes "IsAtopologicalGroup(T,f)"

shows "topgroup(T,f)"

using assms IsAtopologicalGroup_def topgroup_def

topgroup_axioms.intro topology0_def by simp;

text{*We can use the @{text "group0"} locale in the context of @{text "topgroup"}.*}

lemma (in topgroup) group0_valid_in_tgroup: shows "group0(G,f)"

using Ggroup group0_def by simp

text{*We can use @{text "semigr0"} locale in the context of @{text "topgroup"}. *}

lemma (in topgroup) semigr0_valid_in_tgroup: shows "semigr0(G,f)"

using Ggroup IsAgroup_def IsAmonoid_def semigr0_def by simp

text{*We can use the @{text "prod_top_spaces0"} locale in the context of @{text "topgroup"}.*}

lemma (in topgroup) prod_top_spaces0_valid: shows "prod_top_spaces0(T,T,T)"

using topSpaceAssum prod_top_spaces0_def by simp

text{*Negative of a group element is in group.*}

lemma (in topgroup) neg_in_tgroup: assumes "g∈G" shows "(\<rm>g) ∈ G"

proof -

from assms have "GroupInv(G,f)`(g) ∈ G"

using group0_valid_in_tgroup group0.inverse_in_group by blast

thus ?thesis by simp

qed

text{*Zero is in the group.*}

lemma (in topgroup) zero_in_tgroup: shows "\<zero>∈G"

proof -

have "TheNeutralElement(G,f) ∈ G"

using group0_valid_in_tgroup group0.group0_2_L2 by blast

then show "\<zero>∈G" by simp

qed

text{*Of course the product topology is a topology (on $G\times G$).*}

lemma (in topgroup) prod_top_on_G:

shows "τ {is a topology}" and "\<Union>τ = G×G"

using topSpaceAssum Top_1_4_T1 by auto;

text{*Let's recall that $f$ is a binary operation on $G$ in this context.*}

lemma (in topgroup) topgroup_f_binop: shows "f : G×G -> G"

using Ggroup group0_def group0.group_oper_assocA by simp;

text{*A subgroup of a topological group is a topological group

with relative topology

and restricted operation. Relative topology is the same

as @{text "T {restricted to} H"}

which is defined to be $\{V \cap H: V\in T\}$ in @{text "ZF1"} theory.*}

lemma (in topgroup) top_subgroup: assumes A1: "IsAsubgroup(H,f)"

shows "IsAtopologicalGroup(T {restricted to} H,restrict(f,H×H))"

proof -

let ?τ⇩_{0}= "T {restricted to} H"

let ?f⇩_{H}= "restrict(f,H×H)"

have "\<Union>?τ⇩_{0}= G ∩ H" using union_restrict by simp;

also from A1 have "… = H"

using group0_valid_in_tgroup group0.group0_3_L2 by blast;

finally have "\<Union>?τ⇩_{0}= H" by simp;

have "?τ⇩_{0}{is a topology}" using Top_1_L4 by simp;

moreover from A1 `\<Union>?τ⇩_{0}= H` have "IsAgroup(\<Union>?τ⇩_{0},?f⇩_{H})"

using IsAsubgroup_def by simp;

moreover have "IsContinuous(ProductTopology(?τ⇩_{0},?τ⇩_{0}),?τ⇩_{0},?f⇩_{H})"

proof -

have "two_top_spaces0(τ, T,f)"

using topSpaceAssum prod_top_on_G topgroup_f_binop prod_top_on_G

two_top_spaces0_def by simp;

moreover

from A1 have "H ⊆ G" using group0_valid_in_tgroup group0.group0_3_L2

by simp;

then have "H×H ⊆ \<Union>τ" using prod_top_on_G by auto;

moreover have "IsContinuous(τ,T,f)" using fcon by simp;

ultimately have

"IsContinuous(τ {restricted to} H×H, T {restricted to} ?f⇩_{H}``(H×H),?f⇩_{H})"

using two_top_spaces0.restr_restr_image_cont by simp;

moreover have

"ProductTopology(?τ⇩_{0},?τ⇩_{0}) = τ {restricted to} H×H"

using topSpaceAssum prod_top_restr_comm by simp;

moreover from A1 have "?f⇩_{H}``(H×H) = H" using image_subgr_op

by simp;

ultimately show ?thesis by simp;

qed

moreover have "IsContinuous(?τ⇩_{0},?τ⇩_{0},GroupInv(\<Union>?τ⇩_{0},?f⇩_{H}))"

proof -

let ?g = "restrict(GroupInv(G,f),H)"

have "GroupInv(G,f) : G -> G"

using Ggroup group0_2_T2 by simp;

then have "two_top_spaces0(T,T,GroupInv(G,f))"

using topSpaceAssum two_top_spaces0_def by simp;

moreover from A1 have "H ⊆ \<Union>T"

using group0_valid_in_tgroup group0.group0_3_L2

by simp;

ultimately have

"IsContinuous(?τ⇩_{0},T {restricted to} ?g``(H),?g)"

using inv_cont two_top_spaces0.restr_restr_image_cont

by simp;

moreover from A1 have "?g``(H) = H"

using group0_valid_in_tgroup group0.restr_inv_onto

by simp;

moreover

from A1 have "GroupInv(H,?f⇩_{H}) = ?g"

using group0_valid_in_tgroup group0.group0_3_T1

by simp;

with `\<Union>?τ⇩_{0}= H` have "?g = GroupInv(\<Union>?τ⇩_{0},?f⇩_{H})" by simp;

ultimately show ?thesis by simp;

qed

ultimately show ?thesis unfolding IsAtopologicalGroup_def by simp;

qed

section{*Interval arithmetic, translations and inverse of set*}

text{*In this section we list some properties of operations of translating a

set and reflecting it around the neutral element of the group. Many of the results

are proven in other theories, here we just collect them and rewrite in notation

specific to the @{text "topgroup"} context.*}

text{*Different ways of looking at adding sets.*}

lemma (in topgroup) interval_add: assumes "A⊆G" "B⊆G" shows

"A\<sad>B ⊆ G" and "A\<sad>B = f``(A×B)" "A\<sad>B = (\<Union>x∈A. x\<ltr>B)"

proof -

from assms show "A\<sad>B ⊆ G" and "A\<sad>B = f``(A×B)"

using topgroup_f_binop lift_subsets_explained by auto

from assms show "A\<sad>B = (\<Union>x∈A. x\<ltr>B)"

using group0_valid_in_tgroup group0.image_ltrans_union by simp

qed

text{*Right and left translations are continuous.*}

lemma (in topgroup) trans_cont: assumes "g∈G" shows

"IsContinuous(T,T,RightTranslation(G,f,g))" and

"IsContinuous(T,T,LeftTranslation(G,f,g))"

using assms group0_valid_in_tgroup group0.trans_eq_section

topgroup_f_binop fcon prod_top_spaces0_valid

prod_top_spaces0.fix_1st_var_cont prod_top_spaces0.fix_2nd_var_cont

by auto

text{*Left and right translations of an open set are open.*}

lemma (in topgroup) open_tr_open: assumes "g∈G" and "V∈T"

shows "g\<ltr>V ∈ T" and "V\<rtr>g ∈ T"

using assms neg_in_tgroup trans_cont IsContinuous_def

group0_valid_in_tgroup group0.trans_image_vimage by auto

text{*Right and left translations are homeomorphisms.*}

lemma (in topgroup) tr_homeo: assumes "g∈G" shows

"IsAhomeomorphism(T,T,RightTranslation(G,f,g))" and

"IsAhomeomorphism(T,T,LeftTranslation(G,f,g))"

using assms group0_valid_in_tgroup group0.trans_bij trans_cont open_tr_open

bij_cont_open_homeo by auto

text{*Translations preserve interior.*}

lemma (in topgroup) trans_interior: assumes A1: "g∈G" and A2: "A⊆G"

shows "g \<ltr> int(A) = int(g\<ltr>A)"

proof -

from assms have "A ⊆ \<Union>T" and "IsAhomeomorphism(T,T,LeftTranslation(G,f,g))"

using tr_homeo by auto

then show ?thesis using int_top_invariant by simp

qed

(*

text{*Translating by an inverse and then by an element cancels out.*}

lemma (in topgroup) trans_inverse_elem: assumes "g∈G" and "A⊆G"

shows "g\<ltr>((\<rm>g)\<ltr>A) = A"

using assms neg_in_tgroup group0_valid_in_tgroup group0.trans_comp_image

group0.group0_2_L6 group0.trans_neutral image_id_same by simp*)

text{*Inverse of an open set is open.*}

lemma (in topgroup) open_inv_open: assumes "V∈T" shows "(\<sm>V) ∈ T"

using assms group0_valid_in_tgroup group0.inv_image_vimage

inv_cont IsContinuous_def by simp

text{*Inverse is a homeomorphism.*}

lemma (in topgroup) inv_homeo: shows "IsAhomeomorphism(T,T,GroupInv(G,f))"

using group0_valid_in_tgroup group0.group_inv_bij inv_cont open_inv_open

bij_cont_open_homeo by simp

text{*Taking negative preserves interior.*}

lemma (in topgroup) int_inv_inv_int: assumes "A ⊆ G"

shows "int(\<sm>A) = \<sm>(int(A))"

using assms inv_homeo int_top_invariant by simp

section{*Neighborhoods of zero*}

text{*Zero neighborhoods are (not necessarily open) sets whose interior

contains the neutral element of the group. In the @{text "topgroup"} locale

the collection of neighboorhoods of zero is denoted @{text "\<N>⇩_{0}"}. *}

text{*The whole space is a neighborhood of zero.*}

lemma (in topgroup) zneigh_not_empty: shows "G ∈ \<N>⇩_{0}"

using topSpaceAssum IsATopology_def Top_2_L3 zero_in_tgroup

by simp

text{*Any element belongs to the interior of any neighboorhood of zero

translated by that element.*}

lemma (in topgroup) elem_in_int_trans:

assumes A1: "g∈G" and A2: "H ∈ \<N>⇩_{0}"

shows "g ∈ int(g\<ltr>H)"

proof -

from A2 have "\<zero> ∈ int(H)" and "int(H) ⊆ G" using Top_2_L2 by auto

with A1 have "g ∈ g \<ltr> int(H)"

using group0_valid_in_tgroup group0.neut_trans_elem by simp

with assms show ?thesis using trans_interior by simp

qed

text{*Negative of a neighborhood of zero is a neighborhood of zero.*}

lemma (in topgroup) neg_neigh_neigh: assumes "H ∈ \<N>⇩_{0}"

shows "(\<sm>H) ∈ \<N>⇩_{0}"

proof -

from assms have "int(H) ⊆ G" and "\<zero> ∈ int(H)" using Top_2_L1 by auto

with assms have "\<zero> ∈ int(\<sm>H)" using group0_valid_in_tgroup group0.neut_inv_neut

int_inv_inv_int by simp

moreover

have "GroupInv(G,f):G->G" using Ggroup group0_2_T2 by simp

then have "(\<sm>H) ⊆ G" using func1_1_L6 by simp

ultimately show ?thesis by simp

qed

text{*Translating an open set by a negative of a point that belongs to it

makes it a neighboorhood of zero.*}

lemma (in topgroup) open_trans_neigh: assumes A1: "U∈T" and "g∈U"

shows "(\<rm>g)\<ltr>U ∈ \<N>⇩_{0}"

proof -

let ?H = "(\<rm>g)\<ltr>U"

from assms have "g∈G" by auto

then have "(\<rm>g) ∈ G" using neg_in_tgroup by simp

with A1 have "?H∈T" using open_tr_open by simp

hence "?H ⊆ G" by auto

moreover have "\<zero> ∈ int(?H)"

proof -

from assms have "U⊆G" and "g∈U" by auto

with `?H∈T` show "\<zero> ∈ int(?H)"

using group0_valid_in_tgroup group0.elem_trans_neut Top_2_L3

by auto

qed

ultimately show ?thesis by simp

qed

section{*Closure in topological groups*}

text{*This section is devoted to a characterization of closure

in topological groups.*}

text{*Closure of a set is contained in the sum of the set and any

neighboorhood of zero.*}

lemma (in topgroup) cl_contains_zneigh:

assumes A1: "A⊆G" and A2: "H ∈ \<N>⇩_{0}"

shows "cl(A) ⊆ A\<sad>H"

proof

fix x assume "x ∈ cl(A)"

from A1 have "cl(A) ⊆ G" using Top_3_L11 by simp

with `x ∈ cl(A)` have "x∈G" by auto

have "int(H) ⊆ G" using Top_2_L2 by auto

let ?V = "int(x \<ltr> (\<sm>H))"

have "?V = x \<ltr> (\<sm>int(H))"

proof -

from A2 `x∈G` have "?V = x \<ltr> int(\<sm>H)"

using neg_neigh_neigh trans_interior by simp

with A2 show ?thesis using int_inv_inv_int by simp

qed

have "A∩?V ≠ 0"

proof -

from A2 `x∈G` `x ∈ cl(A)` have "?V∈T" and "x ∈ cl(A) ∩ ?V"

using neg_neigh_neigh elem_in_int_trans Top_2_L2 by auto

with A1 show "A∩?V ≠ 0" using cl_inter_neigh by simp

qed

then obtain y where "y∈A" and "y∈?V" by auto

with `?V = x \<ltr> (\<sm>int(H))` `int(H) ⊆ G` `x∈G` have "x ∈ y\<ltr>int(H)"

using group0_valid_in_tgroup group0.ltrans_inv_in by simp

with `y∈A` have "x ∈ (\<Union>y∈A. y\<ltr>H)" using Top_2_L1 func1_1_L8 by auto

with assms show "x ∈ A\<sad>H" using interval_add by simp

qed

text{*The next theorem provides a characterization of closure in topological

groups in terms of neighborhoods of zero.*}

theorem (in topgroup) cl_topgroup:

assumes "A⊆G" shows "cl(A) = (\<Inter>H∈\<N>⇩_{0}. A\<sad>H)"

proof

from assms show "cl(A) ⊆ (\<Inter>H∈\<N>⇩_{0}. A\<sad>H)"

using zneigh_not_empty cl_contains_zneigh by auto

next

{ fix x assume "x ∈ (\<Inter>H∈\<N>⇩_{0}. A\<sad>H)"

then have "x ∈ A\<sad>G" using zneigh_not_empty by auto

with assms have "x∈G" using interval_add by blast

have "∀U∈T. x∈U --> U∩A ≠ 0"

proof -

{ fix U assume "U∈T" and "x∈U"

let ?H = "\<sm>((\<rm>x)\<ltr>U)"

from `U∈T` and `x∈U` have "(\<rm>x)\<ltr>U ⊆ G" and "?H ∈ \<N>⇩_{0}"

using open_trans_neigh neg_neigh_neigh by auto

with `x ∈ (\<Inter>H∈\<N>⇩_{0}. A\<sad>H)` have "x ∈ A\<sad>?H" by auto

with assms `?H ∈ \<N>⇩_{0}` obtain y where "y∈A" and "x ∈ y\<ltr>?H"

using interval_add by auto

have "y∈U"

proof -

from assms `y∈A` have "y∈G" by auto

with `(\<rm>x)\<ltr>U ⊆ G` and `x ∈ y\<ltr>?H` have "y ∈ x\<ltr>((\<rm>x)\<ltr>U)"

using group0_valid_in_tgroup group0.ltrans_inv_in by simp

with `U∈T` `x∈G` show "y∈U"

using neg_in_tgroup group0_valid_in_tgroup group0.trans_comp_image

group0.group0_2_L6 group0.trans_neutral image_id_same

by auto

qed

with `y∈A` have "U∩A ≠ 0" by auto

} thus ?thesis by simp

qed

with assms `x∈G` have "x ∈ cl(A)" using inter_neigh_cl by simp

} thus "(\<Inter>H∈\<N>⇩_{0}. A\<sad>H) ⊆ cl(A)" by auto

qed

section{*Sums of sequences of elements and subsets*}

text{* In this section we consider properties of the function $G^n\rightarrow G$,

$x=(x_0,x_1,...,x_{n-1})\mapsto \sum_{i=0}^{n-1}x_i$. We will model the cartesian product

$G^n$ by the space of sequences $n\rightarrow G$, where $n=\{0,1,...,n-1]\}$ is a natural number.

This space is equipped with a natural product topology defined in @{text "Topology_ZF_3"}. *}

text{*Let's recall first that the sum of elements of a group is an element of the group.*}

lemma (in topgroup) sum_list_in_group:

assumes "n ∈ nat" and "x: succ(n)->G"

shows "(∑x) ∈ G"

proof -

from assms have "semigr0(G,f)" and "n ∈ nat" "x: succ(n)->G"

using semigr0_valid_in_tgroup by auto

then have "Fold1(f,x) ∈ G" by (rule semigr0.prod_type)

thus "(∑x) ∈ G" by simp

qed

text{*In this context @{text"x\<ra>y"} is the same as the value of the group operation

on the elements $x$ and $y$. Normally we shouldn't need to state this a s separate lemma.

*}

lemma (in topgroup) grop_def1: shows "f`⟨x,y⟩ = x\<ra>y" by simp

text{*Another theorem from @{text "Semigroup_ZF"} theory that is useful to have in the

additive notation. *}

lemma (in topgroup) shorter_set_add:

assumes "n ∈ nat" and "x: succ(succ(n))->G"

shows "(∑x) = (∑Init(x)) \<ra> (x`(succ(n)))"

proof -

from assms have "semigr0(G,f)" and "n ∈ nat" "x: succ(succ(n))->G"

using semigr0_valid_in_tgroup by auto

then have "Fold1(f,x) = f`⟨Fold1(f,Init(x)),x`(succ(n))⟩"

by (rule semigr0.shorter_seq)

thus ?thesis by simp

qed

text{*Sum is a continuous function in the product topology.*}

theorem (in topgroup) sum_continuous: assumes "n ∈ nat"

shows "IsContinuous(SeqProductTopology(succ(n),T),T,{⟨x,∑x⟩.x∈succ(n)->G})"

proof -

note `n ∈ nat`

moreover have "IsContinuous(SeqProductTopology(succ(0),T),T,{⟨x,∑x⟩.x∈succ(0)->G})"

proof -

have "{⟨x,∑x⟩.x∈succ(0)->G} = {⟨x,x`(0)⟩. x∈1->G}"

using semigr0_valid_in_tgroup semigr0.prod_of_1elem by simp

moreover have

"IsAhomeomorphism(SeqProductTopology(1,T),T,{⟨x,x`(0)⟩. x∈1->\<Union>T})"

using topSpaceAssum singleton_prod_top1 by simp

ultimately show ?thesis using IsAhomeomorphism_def by simp

qed

moreover have "∀k∈nat.

IsContinuous(SeqProductTopology(succ(k),T),T,{⟨x,∑x⟩.x∈succ(k)->G})

-->

IsContinuous(SeqProductTopology(succ(succ(k)),T),T,{⟨x,∑x⟩.x∈succ(succ(k))->G})"

proof -

{ fix k assume "k ∈ nat"

let ?s = "{⟨x,∑x⟩.x∈succ(k)->G}"

let ?g = "{⟨p,⟨?s`(fst(p)),snd(p)⟩⟩. p ∈ (succ(k)->G)×G}"

let ?h = "{⟨x,⟨Init(x),x`(succ(k))⟩⟩. x ∈ succ(succ(k))->G}"

let ?φ = "SeqProductTopology(succ(k),T)"

let ?ψ = "SeqProductTopology(succ(succ(k)),T)"

assume "IsContinuous(?φ,T,?s)"

from `k ∈ nat` have "?s: (succ(k)->G) -> G"

using sum_list_in_group ZF_fun_from_total by simp

have "?h: (succ(succ(k))->G)->(succ(k)->G)×G"

proof -

{ fix x assume "x ∈ succ(succ(k))->G"

with `k ∈ nat` have "Init(x) ∈ (succ(k)->G)"

using init_props by simp

with `k ∈ nat` `x : succ(succ(k))->G`

have "⟨Init(x),x`(succ(k))⟩ ∈ (succ(k)->G)×G"

using apply_funtype by blast

} then show ?thesis using ZF_fun_from_total by simp

qed

moreover have "?g:((succ(k)->G)×G)->(G×G)"

proof -

{ fix p assume "p ∈ (succ(k)->G)×G"

hence "fst(p): succ(k)->G" and "snd(p) ∈ G" by auto

with `?s: (succ(k)->G) -> G` have "⟨?s`(fst(p)),snd(p)⟩ ∈ G×G"

using apply_funtype by blast

} then show "?g:((succ(k)->G)×G)->(G×G)" using ZF_fun_from_total

by simp

qed

moreover have "f : G×G -> G" using topgroup_f_binop by simp

ultimately have "f O ?g O ?h :(succ(succ(k))->G)->G" using comp_fun

by blast

from `k ∈ nat` have "IsContinuous(?ψ,ProductTopology(?φ,T),?h)"

using topSpaceAssum finite_top_prod_homeo IsAhomeomorphism_def

by simp

moreover have "IsContinuous(ProductTopology(?φ,T),τ,?g)"

proof -

from topSpaceAssum have

"T {is a topology}" "?φ {is a topology}" "\<Union>?φ = succ(k)->G"

using seq_prod_top_is_top by auto

moreover from `\<Union>?φ = succ(k)->G` `?s: (succ(k)->G) -> G`

have "?s:\<Union>?φ->\<Union>T" by simp

moreover note `IsContinuous(?φ,T,?s)`

moreover from `\<Union>?φ = succ(k)->G`

have "?g = {⟨p,⟨?s`(fst(p)),snd(p)⟩⟩. p ∈ \<Union>?φ×\<Union>T}"

by simp

ultimately have "IsContinuous(ProductTopology(?φ,T),ProductTopology(T,T),?g)"

using cart_prod_cont1 by blast

thus ?thesis by simp

qed

moreover have "IsContinuous(τ,T,f)" using fcon by simp

moreover have "{⟨x,∑x⟩.x∈succ(succ(k))->G} = f O ?g O ?h"

proof -

let ?d = "{⟨x,∑x⟩.x∈succ(succ(k))->G}"

from `k∈nat` have "∀x∈succ(succ(k))->G. (∑x) ∈ G"

using sum_list_in_group by blast

then have "?d:(succ(succ(k))->G)->G"

using sum_list_in_group ZF_fun_from_total by simp

moreover note `f O ?g O ?h :(succ(succ(k))->G)->G`

moreover have "∀x∈succ(succ(k))->G. ?d`(x) = (f O ?g O ?h)`(x)"

proof

fix x assume "x∈succ(succ(k))->G"

then have I: "?h`(x) = ⟨Init(x),x`(succ(k))⟩"

using ZF_fun_from_tot_val1 by simp

moreover from `k∈nat` `x∈succ(succ(k))->G`

have "Init(x): succ(k)->G"

using init_props by simp

moreover from `k∈nat` `x:succ(succ(k))->G`

have II: "x`(succ(k)) ∈ G"

using apply_funtype by blast

ultimately have "?h`(x) ∈ (succ(k)->G)×G" by simp

then have "?g`(?h`(x)) = ⟨?s`(fst(?h`(x))),snd(?h`(x))⟩"

using ZF_fun_from_tot_val1 by simp

with I have "?g`(?h`(x)) = ⟨?s`(Init(x)),x`(succ(k))⟩"

by simp

with `Init(x): succ(k)->G` have "?g`(?h`(x)) = ⟨∑Init(x),x`(succ(k))⟩"

using ZF_fun_from_tot_val1 by simp

with `k ∈ nat` `x: succ(succ(k))->G`

have "f`(?g`(?h`(x))) = (∑x)"

using shorter_set_add by simp

with `x ∈ succ(succ(k))->G` have "f`(?g`(?h`(x))) = ?d`(x)"

using ZF_fun_from_tot_val1 by simp

moreover from

`?h: (succ(succ(k))->G)->(succ(k)->G)×G`

`?g:((succ(k)->G)×G)->(G×G)`

`f:(G×G)->G` `x∈succ(succ(k))->G`

have "(f O ?g O ?h)`(x) = f`(?g`(?h`(x)))" by (rule func1_1_L18)

ultimately show "?d`(x) = (f O ?g O ?h)`(x)" by simp

qed

ultimately show "{⟨x,∑x⟩.x∈succ(succ(k))->G} = f O ?g O ?h"

using func_eq by simp

qed

moreover note `IsContinuous(τ,T,f)`

ultimately have "IsContinuous(?ψ,T,{⟨x,∑x⟩.x∈succ(succ(k))->G})"

using comp_cont3 by simp

} thus ?thesis by simp

qed

ultimately show ?thesis by (rule ind_on_nat)

qed

end