Theorem ablsimpg1gend

Description: An abelian simple group is generated by any non-identity element. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	ablsimpg1gend.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
	ablsimpg1gend.2	⊢ 0 = ( 0g ‘ 𝐺 )
	ablsimpg1gend.3	⊢ · = ( .g ‘ 𝐺 )
	ablsimpg1gend.4	⊢ ( 𝜑 → 𝐺 ∈ Abel )
	ablsimpg1gend.5	⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )
	ablsimpg1gend.6	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	ablsimpg1gend.7	⊢ ( 𝜑 → ¬ 𝐴 = 0 )
	ablsimpg1gend.8	⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
Assertion	ablsimpg1gend	⊢ ( 𝜑 → ∃ 𝑛 ∈ ℤ 𝐶 = ( 𝑛 · 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ablsimpg1gend.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		ablsimpg1gend.2	⊢ 0 = ( 0g ‘ 𝐺 )
3		ablsimpg1gend.3	⊢ · = ( .g ‘ 𝐺 )
4		ablsimpg1gend.4	⊢ ( 𝜑 → 𝐺 ∈ Abel )
5		ablsimpg1gend.5	⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )
6		ablsimpg1gend.6	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
7		ablsimpg1gend.7	⊢ ( 𝜑 → ¬ 𝐴 = 0 )
8		ablsimpg1gend.8	⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
9		eqid	⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐴 ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐴 ) )
10	5	simpggrpd	⊢ ( 𝜑 → 𝐺 ∈ Grp )
11	1 3 9 10 6	cycsubgcld	⊢ ( 𝜑 → ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐴 ) ) ∈ ( SubGrp ‘ 𝐺 ) )
12	1 3 9 6	cycsubggend	⊢ ( 𝜑 → 𝐴 ∈ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐴 ) ) )
13	1 2 4 5 11 12 7	ablsimpnosubgd	⊢ ( 𝜑 → ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐴 ) ) = 𝐵 )
14	8 13	eleqtrrd	⊢ ( 𝜑 → 𝐶 ∈ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐴 ) ) )
15	9 14	elrnmpt2d	⊢ ( 𝜑 → ∃ 𝑛 ∈ ℤ 𝐶 = ( 𝑛 · 𝐴 ) )