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

Metamath Proof Explorer

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