Theorem cycsubg

Description: The cyclic group generated by A is the smallest subgroup containing A . (Contributed by Mario Carneiro, 13-Jan-2015)

	Ref	Expression
Hypotheses	cycsubg.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	cycsubg.t	⊢ · = ( .g ‘ 𝐺 )
	cycsubg.f	⊢ 𝐹 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) )
Assertion	cycsubg	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ran 𝐹 = ∩ { 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∣ 𝐴 ∈ 𝑠 } )

Proof

Step	Hyp	Ref	Expression
1		cycsubg.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		cycsubg.t	⊢ · = ( .g ‘ 𝐺 )
3		cycsubg.f	⊢ 𝐹 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 · 𝐴 ) )
4		ssintab	⊢ ( ran 𝐹 ⊆ ∩ { 𝑠 ∣ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) } ↔ ∀ 𝑠 ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) → ran 𝐹 ⊆ 𝑠 ) )
5	1 2 3	cycsubgss	⊢ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) → ran 𝐹 ⊆ 𝑠 )
6	4 5	mpgbir	⊢ ran 𝐹 ⊆ ∩ { 𝑠 ∣ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) }
7		df-rab	⊢ { 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∣ 𝐴 ∈ 𝑠 } = { 𝑠 ∣ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) }
8	7	inteqi	⊢ ∩ { 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∣ 𝐴 ∈ 𝑠 } = ∩ { 𝑠 ∣ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑠 ) }
9	6 8	sseqtrri	⊢ ran 𝐹 ⊆ ∩ { 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∣ 𝐴 ∈ 𝑠 }
10	9	a1i	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ran 𝐹 ⊆ ∩ { 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∣ 𝐴 ∈ 𝑠 } )
11	1 2 3	cycsubgcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ran 𝐹 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ran 𝐹 ) )
12		eleq2	⊢ ( 𝑠 = ran 𝐹 → ( 𝐴 ∈ 𝑠 ↔ 𝐴 ∈ ran 𝐹 ) )
13	12	elrab	⊢ ( ran 𝐹 ∈ { 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∣ 𝐴 ∈ 𝑠 } ↔ ( ran 𝐹 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ ran 𝐹 ) )
14	11 13	sylibr	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ran 𝐹 ∈ { 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∣ 𝐴 ∈ 𝑠 } )
15		intss1	⊢ ( ran 𝐹 ∈ { 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∣ 𝐴 ∈ 𝑠 } → ∩ { 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∣ 𝐴 ∈ 𝑠 } ⊆ ran 𝐹 )
16	14 15	syl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ∩ { 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∣ 𝐴 ∈ 𝑠 } ⊆ ran 𝐹 )
17	10 16	eqssd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ran 𝐹 = ∩ { 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∣ 𝐴 ∈ 𝑠 } )