circsubm

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

Step	Hyp	Ref	Expression
1		circgrp.1	$⊢ C = {abs}^{-1} [\{1\}]$
2		circgrp.2	$⊢ T = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} C$
3		oveq2	$⊢ x = y \to i x = i y$
4	3	fveq2d	$⊢ x = y \to e^{i x} = e^{i y}$
5	4	cbvmptv	$⊢ (x \in ℝ ⟼ e^{i x}) = (y \in ℝ ⟼ e^{i y})$
6	5 1	efifo	$⊢ (x \in ℝ ⟼ e^{i x}) : ℝ \underset{onto}{⟶} C$
7		forn	$⊢ (x \in ℝ ⟼ e^{i x}) : ℝ \underset{onto}{⟶} C \to ran (x \in ℝ ⟼ e^{i x}) = C$
8	6 7	ax-mp	$⊢ ran (x \in ℝ ⟼ e^{i x}) = C$
9	8	eqcomi	$⊢ C = ran (x \in ℝ ⟼ e^{i x})$
10	9	oveq2i	$⊢ {mulGrp}_{ℂ_{fld}} ↾_{𝑠} C = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} ran (x \in ℝ ⟼ e^{i x})$
11		ax-icn	$⊢ i \in ℂ$
12	11	a1i	$⊢ ⊤ \to i \in ℂ$
13		resubdrg	$⊢ (ℝ \in SubRing (ℂ_{fld}) \land ℝ_{fld} \in DivRing)$
14	13	simpli	$⊢ ℝ \in SubRing (ℂ_{fld})$
15		subrgsubg	$⊢ ℝ \in SubRing (ℂ_{fld}) \to ℝ \in SubGrp (ℂ_{fld})$
16	14 15	ax-mp	$⊢ ℝ \in SubGrp (ℂ_{fld})$
17	16	a1i	$⊢ ⊤ \to ℝ \in SubGrp (ℂ_{fld})$
18	5 10 12 17	efsubm	$⊢ ⊤ \to ran (x \in ℝ ⟼ e^{i x}) \in SubMnd ({mulGrp}_{ℂ_{fld}})$
19	18	mptru	$⊢ ran (x \in ℝ ⟼ e^{i x}) \in SubMnd ({mulGrp}_{ℂ_{fld}})$
20	9 19	eqeltri	$⊢ C \in SubMnd ({mulGrp}_{ℂ_{fld}})$

Metamath Proof Explorer