Theorem cycsubg2

Description: The subgroup generated by an element is exhausted by its multiples. (Contributed by Stefan O'Rear, 6-Sep-2015)

	Ref	Expression
Hypotheses	cycsubg2.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	cycsubg2.t	⊢ · = ( .g ‘ 𝐺 )
	cycsubg2.f	⊢ 𝐹 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) )
	cycsubg2.k	⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
Assertion	cycsubg2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐾 ‘ { 𝐴 } ) = ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		cycsubg2.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		cycsubg2.t	⊢ · = ( .g ‘ 𝐺 )
3		cycsubg2.f	⊢ 𝐹 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) )
4		cycsubg2.k	⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
5		snssg	⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 ∈ 𝑦 ↔ { 𝐴 } ⊆ 𝑦 ) )
6	5	bicomd	⊢ ( 𝐴 ∈ 𝑋 → ( { 𝐴 } ⊆ 𝑦 ↔ 𝐴 ∈ 𝑦 ) )
7	6	adantl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( { 𝐴 } ⊆ 𝑦 ↔ 𝐴 ∈ 𝑦 ) )
8	7	rabbidv	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ { 𝐴 } ⊆ 𝑦 } = { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ 𝐴 ∈ 𝑦 } )
9	8	inteqd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ∩ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ { 𝐴 } ⊆ 𝑦 } = ∩ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ 𝐴 ∈ 𝑦 } )
10	1	subgacs	⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝑋 ) )
11	10	acsmred	⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝑋 ) )
12		snssi	⊢ ( 𝐴 ∈ 𝑋 → { 𝐴 } ⊆ 𝑋 )
13	4	mrcval	⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝑋 ) ∧ { 𝐴 } ⊆ 𝑋 ) → ( 𝐾 ‘ { 𝐴 } ) = ∩ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ { 𝐴 } ⊆ 𝑦 } )
14	11 12 13	syl2an	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐾 ‘ { 𝐴 } ) = ∩ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ { 𝐴 } ⊆ 𝑦 } )
15	1 2 3	cycsubg	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ran 𝐹 = ∩ { 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∣ 𝐴 ∈ 𝑦 } )
16	9 14 15	3eqtr4d	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐾 ‘ { 𝐴 } ) = ran 𝐹 )