Description: Norm of the identity element. (Contributed by Mario Carneiro, 4-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nm0.n | |- N = ( norm ` G ) |
|
nm0.z | |- .0. = ( 0g ` G ) |
||
Assertion | nm0 | |- ( G e. NrmGrp -> ( N ` .0. ) = 0 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nm0.n | |- N = ( norm ` G ) |
|
2 | nm0.z | |- .0. = ( 0g ` G ) |
|
3 | eqid | |- .0. = .0. |
|
4 | ngpgrp | |- ( G e. NrmGrp -> G e. Grp ) |
|
5 | eqid | |- ( Base ` G ) = ( Base ` G ) |
|
6 | 5 2 | grpidcl | |- ( G e. Grp -> .0. e. ( Base ` G ) ) |
7 | 4 6 | syl | |- ( G e. NrmGrp -> .0. e. ( Base ` G ) ) |
8 | 5 1 2 | nmeq0 | |- ( ( G e. NrmGrp /\ .0. e. ( Base ` G ) ) -> ( ( N ` .0. ) = 0 <-> .0. = .0. ) ) |
9 | 7 8 | mpdan | |- ( G e. NrmGrp -> ( ( N ` .0. ) = 0 <-> .0. = .0. ) ) |
10 | 3 9 | mpbiri | |- ( G e. NrmGrp -> ( N ` .0. ) = 0 ) |