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 ⊢ M = mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0
Assertion cnmgpid ⊢ 0 M = 1

Proof

Step Hyp Ref Expression
1 cnmgpabl.m ⊢ M = mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 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 = 1 ℂ fld
10 1 8 9 ringidss ⊢ ℂ fld ∈ Ring ∧ ℂ ∖ 0 ⊆ ℂ ∧ 1 ∈ ℂ ∖ 0 → 1 = 0 M
11 10 eqcomd ⊢ ℂ fld ∈ Ring ∧ ℂ ∖ 0 ⊆ ℂ ∧ 1 ∈ ℂ ∖ 0 → 0 M = 1
12 2 3 7 11 mp3an ⊢ 0 M = 1