Metamath Proof Explorer

Theorem cycsubgcl

Description: The set of integer powers of an element A of a group forms a subgroup containing A , called the cyclic group generated by the element A . (Contributed by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses cycsubg.x 
|- X = ( Base ` G )
cycsubg.t 
|- .x. = ( .g ` G )
cycsubg.f 
|- F = ( x e. ZZ |-> ( x .x. A ) )
Assertion cycsubgcl 
|- ( ( G e. Grp /\ A e. X ) -> ( ran F e. ( SubGrp ` G ) /\ A e. ran F ) )

Proof

Step Hyp Ref Expression
1 cycsubg.x 
 |-  X = ( Base ` G )
2 cycsubg.t 
 |-  .x. = ( .g ` G )
3 cycsubg.f 
 |-  F = ( x e. ZZ |-> ( x .x. A ) )
4 1 2 mulgcl 
 |-  ( ( G e. Grp /\ x e. ZZ /\ A e. X ) -> ( x .x. A ) e. X )
5 4 3expa 
 |-  ( ( ( G e. Grp /\ x e. ZZ ) /\ A e. X ) -> ( x .x. A ) e. X )
6 5 an32s 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ x e. ZZ ) -> ( x .x. A ) e. X )
7 6 3 fmptd 
 |-  ( ( G e. Grp /\ A e. X ) -> F : ZZ --> X )
8 7 frnd 
 |-  ( ( G e. Grp /\ A e. X ) -> ran F C_ X )
9 7 ffnd 
 |-  ( ( G e. Grp /\ A e. X ) -> F Fn ZZ )
10 1z 
 |-  1 e. ZZ
11 fnfvelrn 
 |-  ( ( F Fn ZZ /\ 1 e. ZZ ) -> ( F ` 1 ) e. ran F )
12 9 10 11 sylancl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( F ` 1 ) e. ran F )
13 12 ne0d 
 |-  ( ( G e. Grp /\ A e. X ) -> ran F =/= (/) )
14 df-3an 
 |-  ( ( m e. ZZ /\ n e. ZZ /\ A e. X ) <-> ( ( m e. ZZ /\ n e. ZZ ) /\ A e. X ) )
15 eqid 
 |-  ( +g ` G ) = ( +g ` G )
16 1 2 15 mulgdir 
 |-  ( ( G e. Grp /\ ( m e. ZZ /\ n e. ZZ /\ A e. X ) ) -> ( ( m + n ) .x. A ) = ( ( m .x. A ) ( +g ` G ) ( n .x. A ) ) )
17 14 16 sylan2br 
 |-  ( ( G e. Grp /\ ( ( m e. ZZ /\ n e. ZZ ) /\ A e. X ) ) -> ( ( m + n ) .x. A ) = ( ( m .x. A ) ( +g ` G ) ( n .x. A ) ) )
18 17 anass1rs 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> ( ( m + n ) .x. A ) = ( ( m .x. A ) ( +g ` G ) ( n .x. A ) ) )
19 zaddcl 
 |-  ( ( m e. ZZ /\ n e. ZZ ) -> ( m + n ) e. ZZ )
20 19 adantl 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> ( m + n ) e. ZZ )
21 oveq1 
 |-  ( x = ( m + n ) -> ( x .x. A ) = ( ( m + n ) .x. A ) )
22 ovex 
 |-  ( ( m + n ) .x. A ) e. _V
23 21 3 22 fvmpt 
 |-  ( ( m + n ) e. ZZ -> ( F ` ( m + n ) ) = ( ( m + n ) .x. A ) )
24 20 23 syl 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> ( F ` ( m + n ) ) = ( ( m + n ) .x. A ) )
25 oveq1 
 |-  ( x = m -> ( x .x. A ) = ( m .x. A ) )
26 ovex 
 |-  ( m .x. A ) e. _V
27 25 3 26 fvmpt 
 |-  ( m e. ZZ -> ( F ` m ) = ( m .x. A ) )
28 27 ad2antrl 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> ( F ` m ) = ( m .x. A ) )
29 oveq1 
 |-  ( x = n -> ( x .x. A ) = ( n .x. A ) )
30 ovex 
 |-  ( n .x. A ) e. _V
31 29 3 30 fvmpt 
 |-  ( n e. ZZ -> ( F ` n ) = ( n .x. A ) )
32 31 ad2antll 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> ( F ` n ) = ( n .x. A ) )
33 28 32 oveq12d 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> ( ( F ` m ) ( +g ` G ) ( F ` n ) ) = ( ( m .x. A ) ( +g ` G ) ( n .x. A ) ) )
34 18 24 33 3eqtr4d 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> ( F ` ( m + n ) ) = ( ( F ` m ) ( +g ` G ) ( F ` n ) ) )
35 fnfvelrn 
 |-  ( ( F Fn ZZ /\ ( m + n ) e. ZZ ) -> ( F ` ( m + n ) ) e. ran F )
36 9 19 35 syl2an 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> ( F ` ( m + n ) ) e. ran F )
37 34 36 eqeltrrd 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ ( m e. ZZ /\ n e. ZZ ) ) -> ( ( F ` m ) ( +g ` G ) ( F ` n ) ) e. ran F )
38 37 anassrs 
 |-  ( ( ( ( G e. Grp /\ A e. X ) /\ m e. ZZ ) /\ n e. ZZ ) -> ( ( F ` m ) ( +g ` G ) ( F ` n ) ) e. ran F )
39 38 ralrimiva 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ m e. ZZ ) -> A. n e. ZZ ( ( F ` m ) ( +g ` G ) ( F ` n ) ) e. ran F )
40 oveq2 
 |-  ( v = ( F ` n ) -> ( ( F ` m ) ( +g ` G ) v ) = ( ( F ` m ) ( +g ` G ) ( F ` n ) ) )
41 40 eleq1d 
 |-  ( v = ( F ` n ) -> ( ( ( F ` m ) ( +g ` G ) v ) e. ran F <-> ( ( F ` m ) ( +g ` G ) ( F ` n ) ) e. ran F ) )
42 41 ralrn 
 |-  ( F Fn ZZ -> ( A. v e. ran F ( ( F ` m ) ( +g ` G ) v ) e. ran F <-> A. n e. ZZ ( ( F ` m ) ( +g ` G ) ( F ` n ) ) e. ran F ) )
43 9 42 syl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( A. v e. ran F ( ( F ` m ) ( +g ` G ) v ) e. ran F <-> A. n e. ZZ ( ( F ` m ) ( +g ` G ) ( F ` n ) ) e. ran F ) )
44 43 adantr 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ m e. ZZ ) -> ( A. v e. ran F ( ( F ` m ) ( +g ` G ) v ) e. ran F <-> A. n e. ZZ ( ( F ` m ) ( +g ` G ) ( F ` n ) ) e. ran F ) )
45 39 44 mpbird 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ m e. ZZ ) -> A. v e. ran F ( ( F ` m ) ( +g ` G ) v ) e. ran F )
46 eqid 
 |-  ( invg ` G ) = ( invg ` G )
47 1 2 46 mulgneg 
 |-  ( ( G e. Grp /\ m e. ZZ /\ A e. X ) -> ( -u m .x. A ) = ( ( invg ` G ) ` ( m .x. A ) ) )
48 47 3expa 
 |-  ( ( ( G e. Grp /\ m e. ZZ ) /\ A e. X ) -> ( -u m .x. A ) = ( ( invg ` G ) ` ( m .x. A ) ) )
49 48 an32s 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ m e. ZZ ) -> ( -u m .x. A ) = ( ( invg ` G ) ` ( m .x. A ) ) )
50 znegcl 
 |-  ( m e. ZZ -> -u m e. ZZ )
51 50 adantl 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ m e. ZZ ) -> -u m e. ZZ )
52 oveq1 
 |-  ( x = -u m -> ( x .x. A ) = ( -u m .x. A ) )
53 ovex 
 |-  ( -u m .x. A ) e. _V
54 52 3 53 fvmpt 
 |-  ( -u m e. ZZ -> ( F ` -u m ) = ( -u m .x. A ) )
55 51 54 syl 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ m e. ZZ ) -> ( F ` -u m ) = ( -u m .x. A ) )
56 27 adantl 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ m e. ZZ ) -> ( F ` m ) = ( m .x. A ) )
57 56 fveq2d 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ m e. ZZ ) -> ( ( invg ` G ) ` ( F ` m ) ) = ( ( invg ` G ) ` ( m .x. A ) ) )
58 49 55 57 3eqtr4d 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ m e. ZZ ) -> ( F ` -u m ) = ( ( invg ` G ) ` ( F ` m ) ) )
59 fnfvelrn 
 |-  ( ( F Fn ZZ /\ -u m e. ZZ ) -> ( F ` -u m ) e. ran F )
60 9 50 59 syl2an 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ m e. ZZ ) -> ( F ` -u m ) e. ran F )
61 58 60 eqeltrrd 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ m e. ZZ ) -> ( ( invg ` G ) ` ( F ` m ) ) e. ran F )
62 45 61 jca 
 |-  ( ( ( G e. Grp /\ A e. X ) /\ m e. ZZ ) -> ( A. v e. ran F ( ( F ` m ) ( +g ` G ) v ) e. ran F /\ ( ( invg ` G ) ` ( F ` m ) ) e. ran F ) )
63 62 ralrimiva 
 |-  ( ( G e. Grp /\ A e. X ) -> A. m e. ZZ ( A. v e. ran F ( ( F ` m ) ( +g ` G ) v ) e. ran F /\ ( ( invg ` G ) ` ( F ` m ) ) e. ran F ) )
64 oveq1 
 |-  ( u = ( F ` m ) -> ( u ( +g ` G ) v ) = ( ( F ` m ) ( +g ` G ) v ) )
65 64 eleq1d 
 |-  ( u = ( F ` m ) -> ( ( u ( +g ` G ) v ) e. ran F <-> ( ( F ` m ) ( +g ` G ) v ) e. ran F ) )
66 65 ralbidv 
 |-  ( u = ( F ` m ) -> ( A. v e. ran F ( u ( +g ` G ) v ) e. ran F <-> A. v e. ran F ( ( F ` m ) ( +g ` G ) v ) e. ran F ) )
67 fveq2 
 |-  ( u = ( F ` m ) -> ( ( invg ` G ) ` u ) = ( ( invg ` G ) ` ( F ` m ) ) )
68 67 eleq1d 
 |-  ( u = ( F ` m ) -> ( ( ( invg ` G ) ` u ) e. ran F <-> ( ( invg ` G ) ` ( F ` m ) ) e. ran F ) )
69 66 68 anbi12d 
 |-  ( u = ( F ` m ) -> ( ( A. v e. ran F ( u ( +g ` G ) v ) e. ran F /\ ( ( invg ` G ) ` u ) e. ran F ) <-> ( A. v e. ran F ( ( F ` m ) ( +g ` G ) v ) e. ran F /\ ( ( invg ` G ) ` ( F ` m ) ) e. ran F ) ) )
70 69 ralrn 
 |-  ( F Fn ZZ -> ( A. u e. ran F ( A. v e. ran F ( u ( +g ` G ) v ) e. ran F /\ ( ( invg ` G ) ` u ) e. ran F ) <-> A. m e. ZZ ( A. v e. ran F ( ( F ` m ) ( +g ` G ) v ) e. ran F /\ ( ( invg ` G ) ` ( F ` m ) ) e. ran F ) ) )
71 9 70 syl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( A. u e. ran F ( A. v e. ran F ( u ( +g ` G ) v ) e. ran F /\ ( ( invg ` G ) ` u ) e. ran F ) <-> A. m e. ZZ ( A. v e. ran F ( ( F ` m ) ( +g ` G ) v ) e. ran F /\ ( ( invg ` G ) ` ( F ` m ) ) e. ran F ) ) )
72 63 71 mpbird 
 |-  ( ( G e. Grp /\ A e. X ) -> A. u e. ran F ( A. v e. ran F ( u ( +g ` G ) v ) e. ran F /\ ( ( invg ` G ) ` u ) e. ran F ) )
73 1 15 46 issubg2 
 |-  ( G e. Grp -> ( ran F e. ( SubGrp ` G ) <-> ( ran F C_ X /\ ran F =/= (/) /\ A. u e. ran F ( A. v e. ran F ( u ( +g ` G ) v ) e. ran F /\ ( ( invg ` G ) ` u ) e. ran F ) ) ) )
74 73 adantr 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ran F e. ( SubGrp ` G ) <-> ( ran F C_ X /\ ran F =/= (/) /\ A. u e. ran F ( A. v e. ran F ( u ( +g ` G ) v ) e. ran F /\ ( ( invg ` G ) ` u ) e. ran F ) ) ) )
75 8 13 72 74 mpbir3and 
 |-  ( ( G e. Grp /\ A e. X ) -> ran F e. ( SubGrp ` G ) )
76 oveq1 
 |-  ( x = 1 -> ( x .x. A ) = ( 1 .x. A ) )
77 ovex 
 |-  ( 1 .x. A ) e. _V
78 76 3 77 fvmpt 
 |-  ( 1 e. ZZ -> ( F ` 1 ) = ( 1 .x. A ) )
79 10 78 ax-mp 
 |-  ( F ` 1 ) = ( 1 .x. A )
80 1 2 mulg1 
 |-  ( A e. X -> ( 1 .x. A ) = A )
81 80 adantl 
 |-  ( ( G e. Grp /\ A e. X ) -> ( 1 .x. A ) = A )
82 79 81 syl5eq 
 |-  ( ( G e. Grp /\ A e. X ) -> ( F ` 1 ) = A )
83 82 12 eqeltrrd 
 |-  ( ( G e. Grp /\ A e. X ) -> A e. ran F )
84 75 83 jca 
 |-  ( ( G e. Grp /\ A e. X ) -> ( ran F e. ( SubGrp ` G ) /\ A e. ran F ) )