Theorem iscyggen2

Description: The property of being a cyclic generator for a group. (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	iscyg.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
	iscyg.2	⊢ · = ( .g ‘ 𝐺 )
	iscyg3.e	⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 }
Assertion	iscyggen2	⊢ ( 𝐺 ∈ Grp → ( 𝑋 ∈ 𝐸 ↔ ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑋 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscyg.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		iscyg.2	⊢ · = ( .g ‘ 𝐺 )
3		iscyg3.e	⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 }
4	1 2 3	iscyggen	⊢ ( 𝑋 ∈ 𝐸 ↔ ( 𝑋 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = 𝐵 ) )
5	1 2	mulgcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑛 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑛 · 𝑋 ) ∈ 𝐵 )
6	5	3expa	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑛 ∈ ℤ ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝑛 · 𝑋 ) ∈ 𝐵 )
7	6	an32s	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℤ ) → ( 𝑛 · 𝑋 ) ∈ 𝐵 )
8	7	fmpttd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) : ℤ ⟶ 𝐵 )
9		frn	⊢ ( ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) : ℤ ⟶ 𝐵 → ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ⊆ 𝐵 )
10		eqss	⊢ ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = 𝐵 ↔ ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ⊆ 𝐵 ∧ 𝐵 ⊆ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ) )
11	10	baib	⊢ ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ⊆ 𝐵 → ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = 𝐵 ↔ 𝐵 ⊆ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ) )
12	8 9 11	3syl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = 𝐵 ↔ 𝐵 ⊆ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ) )
13		dfss3	⊢ ( 𝐵 ⊆ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ↔ ∀ 𝑦 ∈ 𝐵 𝑦 ∈ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) )
14		eqid	⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) )
15		ovex	⊢ ( 𝑛 · 𝑋 ) ∈ V
16	14 15	elrnmpti	⊢ ( 𝑦 ∈ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ↔ ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑋 ) )
17	16	ralbii	⊢ ( ∀ 𝑦 ∈ 𝐵 𝑦 ∈ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑋 ) )
18	13 17	bitri	⊢ ( 𝐵 ⊆ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑋 ) )
19	12 18	bitrdi	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑋 ) ) )
20	19	pm5.32da	⊢ ( 𝐺 ∈ Grp → ( ( 𝑋 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = 𝐵 ) ↔ ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑋 ) ) ) )
21	4 20	syl5bb	⊢ ( 𝐺 ∈ Grp → ( 𝑋 ∈ 𝐸 ↔ ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑋 ) ) ) )