Theorem cycsubgss

Description: The cyclic subgroup generated by an element A is a subset of any subgroup containing A . (Contributed by Mario Carneiro, 13-Jan-2015)

	Ref	Expression
Hypotheses	cycsubg.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	cycsubg.t	⊢ · = ( .g ‘ 𝐺 )
	cycsubg.f	⊢ 𝐹 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) )
Assertion	cycsubgss	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑆 ) → ran 𝐹 ⊆ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		cycsubg.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		cycsubg.t	⊢ · = ( .g ‘ 𝐺 )
3		cycsubg.f	⊢ 𝐹 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) )
4	2	subgmulgcl	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ℤ ∧ 𝐴 ∈ 𝑆 ) → ( 𝑥 · 𝐴 ) ∈ 𝑆 )
5	4	3expa	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ℤ ) ∧ 𝐴 ∈ 𝑆 ) → ( 𝑥 · 𝐴 ) ∈ 𝑆 )
6	5	an32s	⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 · 𝐴 ) ∈ 𝑆 )
7	6 3	fmptd	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑆 ) → 𝐹 : ℤ ⟶ 𝑆 )
8	7	frnd	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑆 ) → ran 𝐹 ⊆ 𝑆 )