Description: The cyclic subgroup generated by A includes its generator. Although this theorem holds for any class G , the definition of F is only meaningful if G is a group. (Contributed by Rohan Ridenour, 3-Aug-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cycsubggend.1 | ⊢ 𝐵 = ( Base ‘ 𝐺 ) | |
| cycsubggend.2 | ⊢ · = ( .g ‘ 𝐺 ) | ||
| cycsubggend.3 | ⊢ 𝐹 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐴 ) ) | ||
| cycsubggend.4 | ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 ) | ||
| Assertion | cycsubggend | ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐹 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cycsubggend.1 | ⊢ 𝐵 = ( Base ‘ 𝐺 ) | |
| 2 | cycsubggend.2 | ⊢ · = ( .g ‘ 𝐺 ) | |
| 3 | cycsubggend.3 | ⊢ 𝐹 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐴 ) ) | |
| 4 | cycsubggend.4 | ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 ) | |
| 5 | 1zzd | ⊢ ( 𝜑 → 1 ∈ ℤ ) | |
| 6 | simpr | ⊢ ( ( 𝜑 ∧ 𝑛 = 1 ) → 𝑛 = 1 ) | |
| 7 | 6 | oveq1d | ⊢ ( ( 𝜑 ∧ 𝑛 = 1 ) → ( 𝑛 · 𝐴 ) = ( 1 · 𝐴 ) ) |
| 8 | 4 | adantr | ⊢ ( ( 𝜑 ∧ 𝑛 = 1 ) → 𝐴 ∈ 𝐵 ) |
| 9 | 1 2 | mulg1 | ⊢ ( 𝐴 ∈ 𝐵 → ( 1 · 𝐴 ) = 𝐴 ) |
| 10 | 8 9 | syl | ⊢ ( ( 𝜑 ∧ 𝑛 = 1 ) → ( 1 · 𝐴 ) = 𝐴 ) |
| 11 | 7 10 | eqtr2d | ⊢ ( ( 𝜑 ∧ 𝑛 = 1 ) → 𝐴 = ( 𝑛 · 𝐴 ) ) |
| 12 | 3 5 4 11 | elrnmptdv | ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐹 ) |