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

Metamath Proof Explorer

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