This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
cycsubg.t ⊢ · = ( .g ‘ 𝐺 )
cycsubg.f ⊢ 𝐹 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) )
Assertion cycsubgcl ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ran 𝐹 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ran 𝐹 ) )

Proof

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