Theorem cnmgpid

Description: The group identity element of nonzero complex number multiplication is one. (Contributed by Steve Rodriguez, 23-Feb-2007) (Revised by AV, 26-Aug-2021)

	Ref	Expression
Hypothesis	cnmgpabl.m	⊢ 𝑀 = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
Assertion	cnmgpid	⊢ ( 0g ‘ 𝑀 ) = 1

Proof

Step	Hyp	Ref	Expression
1		cnmgpabl.m	⊢ 𝑀 = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
2		cnring	⊢ ℂfld ∈ Ring
3		difss	⊢ ( ℂ ∖ { 0 } ) ⊆ ℂ
4		ax-1cn	⊢ 1 ∈ ℂ
5		ax-1ne0	⊢ 1 ≠ 0
6		eldifsn	⊢ ( 1 ∈ ( ℂ ∖ { 0 } ) ↔ ( 1 ∈ ℂ ∧ 1 ≠ 0 ) )
7	4 5 6	mpbir2an	⊢ 1 ∈ ( ℂ ∖ { 0 } )
8		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
9		cnfld1	⊢ 1 = ( 1r ‘ ℂfld )
10	1 8 9	ringidss	⊢ ( ( ℂfld ∈ Ring ∧ ( ℂ ∖ { 0 } ) ⊆ ℂ ∧ 1 ∈ ( ℂ ∖ { 0 } ) ) → 1 = ( 0g ‘ 𝑀 ) )
11	10	eqcomd	⊢ ( ( ℂfld ∈ Ring ∧ ( ℂ ∖ { 0 } ) ⊆ ℂ ∧ 1 ∈ ( ℂ ∖ { 0 } ) ) → ( 0g ‘ 𝑀 ) = 1 )
12	2 3 7 11	mp3an	⊢ ( 0g ‘ 𝑀 ) = 1