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

Metamath Proof Explorer

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 ‘ 𝐺 ) ∣ 𝐴 ∈ 𝑠 } )