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 ` CCfld ) |`s ( CC \ { 0 } ) ) |
|
| Assertion | cnmgpid | |- ( 0g ` M ) = 1 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnmgpabl.m | |- M = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) |
|
| 2 | cnring | |- CCfld e. Ring |
|
| 3 | difss | |- ( CC \ { 0 } ) C_ CC |
|
| 4 | ax-1cn | |- 1 e. CC |
|
| 5 | ax-1ne0 | |- 1 =/= 0 |
|
| 6 | eldifsn | |- ( 1 e. ( CC \ { 0 } ) <-> ( 1 e. CC /\ 1 =/= 0 ) ) |
|
| 7 | 4 5 6 | mpbir2an | |- 1 e. ( CC \ { 0 } ) |
| 8 | cnfldbas | |- CC = ( Base ` CCfld ) |
|
| 9 | cnfld1 | |- 1 = ( 1r ` CCfld ) |
|
| 10 | 1 8 9 | ringidss | |- ( ( CCfld e. Ring /\ ( CC \ { 0 } ) C_ CC /\ 1 e. ( CC \ { 0 } ) ) -> 1 = ( 0g ` M ) ) |
| 11 | 10 | eqcomd | |- ( ( CCfld e. Ring /\ ( CC \ { 0 } ) C_ CC /\ 1 e. ( CC \ { 0 } ) ) -> ( 0g ` M ) = 1 ) |
| 12 | 2 3 7 11 | mp3an | |- ( 0g ` M ) = 1 |