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

Metamath Proof Explorer

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 𝐹 )