let F be Group; :: thesis: for G being strict Group

for g being Homomorphism of G,F st G is cyclic holds

Image g is cyclic

let G be strict Group; :: thesis: for g being Homomorphism of G,F st G is cyclic holds

Image g is cyclic

let g be Homomorphism of G,F; :: thesis: ( G is cyclic implies Image g is cyclic )

assume G is cyclic ; :: thesis: Image g is cyclic

then consider a being Element of G such that

A1: G = gr {a} ;

ex f1 being Element of (Image g) st Image g = gr {f1}

for g being Homomorphism of G,F st G is cyclic holds

Image g is cyclic

let G be strict Group; :: thesis: for g being Homomorphism of G,F st G is cyclic holds

Image g is cyclic

let g be Homomorphism of G,F; :: thesis: ( G is cyclic implies Image g is cyclic )

assume G is cyclic ; :: thesis: Image g is cyclic

then consider a being Element of G such that

A1: G = gr {a} ;

ex f1 being Element of (Image g) st Image g = gr {f1}

proof

hence
Image g is cyclic
; :: thesis: verum
g . a in Image g
by GROUP_6:45;

then reconsider f = g . a as Element of (Image g) by STRUCT_0:def 5;

take f ; :: thesis: Image g = gr {f}

for d being Element of (Image g) ex i being Integer st d = f |^ i

end;then reconsider f = g . a as Element of (Image g) by STRUCT_0:def 5;

take f ; :: thesis: Image g = gr {f}

for d being Element of (Image g) ex i being Integer st d = f |^ i

proof

hence
Image g = gr {f}
by Th5; :: thesis: verum
let d be Element of (Image g); :: thesis: ex i being Integer st d = f |^ i

d in Image g by STRUCT_0:def 5;

then consider b being Element of G such that

A2: d = g . b by GROUP_6:45;

b in gr {a} by A1, STRUCT_0:def 5;

then consider i being Integer such that

A3: b = a |^ i by GR_CY_1:5;

take i ; :: thesis: d = f |^ i

d = (g . a) |^ i by A2, A3, GROUP_6:37

.= f |^ i by GROUP_4:2 ;

hence d = f |^ i ; :: thesis: verum

end;d in Image g by STRUCT_0:def 5;

then consider b being Element of G such that

A2: d = g . b by GROUP_6:45;

b in gr {a} by A1, STRUCT_0:def 5;

then consider i being Integer such that

A3: b = a |^ i by GR_CY_1:5;

take i ; :: thesis: d = f |^ i

d = (g . a) |^ i by A2, A3, GROUP_6:37

.= f |^ i by GROUP_4:2 ;

hence d = f |^ i ; :: thesis: verum