Theorem circsubm

Description: The circle group T is a submonoid of the multiplicative group of CCfld . (Contributed by Thierry Arnoux, 26-Jan-2020)

	Ref	Expression
Hypotheses	circgrp.1	⊢ 𝐶 = ( ◡ abs “ { 1 } )
	circgrp.2	⊢ 𝑇 = ( ( mulGrp ‘ ℂfld ) ↾s 𝐶 )
Assertion	circsubm	⊢ 𝐶 ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) )

Proof

Step	Hyp	Ref	Expression
1		circgrp.1	⊢ 𝐶 = ( ◡ abs “ { 1 } )
2		circgrp.2	⊢ 𝑇 = ( ( mulGrp ‘ ℂfld ) ↾s 𝐶 )
3		oveq2	⊢ ( 𝑥 = 𝑦 → ( i · 𝑥 ) = ( i · 𝑦 ) )
4	3	fveq2d	⊢ ( 𝑥 = 𝑦 → ( exp ‘ ( i · 𝑥 ) ) = ( exp ‘ ( i · 𝑦 ) ) )
5	4	cbvmptv	⊢ ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( i · 𝑥 ) ) ) = ( 𝑦 ∈ ℝ ↦ ( exp ‘ ( i · 𝑦 ) ) )
6	5 1	efifo	⊢ ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( i · 𝑥 ) ) ) : ℝ –onto→ 𝐶
7		forn	⊢ ( ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( i · 𝑥 ) ) ) : ℝ –onto→ 𝐶 → ran ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( i · 𝑥 ) ) ) = 𝐶 )
8	6 7	ax-mp	⊢ ran ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( i · 𝑥 ) ) ) = 𝐶
9	8	eqcomi	⊢ 𝐶 = ran ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( i · 𝑥 ) ) )
10	9	oveq2i	⊢ ( ( mulGrp ‘ ℂfld ) ↾s 𝐶 ) = ( ( mulGrp ‘ ℂfld ) ↾s ran ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( i · 𝑥 ) ) ) )
11		ax-icn	⊢ i ∈ ℂ
12	11	a1i	⊢ ( ⊤ → i ∈ ℂ )
13		resubdrg	⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) ∧ ℝfld ∈ DivRing )
14	13	simpli	⊢ ℝ ∈ ( SubRing ‘ ℂfld )
15		subrgsubg	⊢ ( ℝ ∈ ( SubRing ‘ ℂfld ) → ℝ ∈ ( SubGrp ‘ ℂfld ) )
16	14 15	ax-mp	⊢ ℝ ∈ ( SubGrp ‘ ℂfld )
17	16	a1i	⊢ ( ⊤ → ℝ ∈ ( SubGrp ‘ ℂfld ) )
18	5 10 12 17	efsubm	⊢ ( ⊤ → ran ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( i · 𝑥 ) ) ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) ) )
19	18	mptru	⊢ ran ( 𝑥 ∈ ℝ ↦ ( exp ‘ ( i · 𝑥 ) ) ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) )
20	9 19	eqeltri	⊢ 𝐶 ∈ ( SubMnd ‘ ( mulGrp ‘ ℂfld ) )