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 · ˙ = G
cycsubg.f F = x x · ˙ A
Assertion cycsubgcl G Grp A X ran F SubGrp G A ran F

Proof

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