Step |
Hyp |
Ref |
Expression |
1 |
|
nmgt0.x |
|- X = ( Base ` G ) |
2 |
|
nmgt0.n |
|- N = ( norm ` G ) |
3 |
|
nmgt0.z |
|- .0. = ( 0g ` G ) |
4 |
1 2 3
|
nmeq0 |
|- ( ( G e. NrmGrp /\ A e. X ) -> ( ( N ` A ) = 0 <-> A = .0. ) ) |
5 |
4
|
necon3bid |
|- ( ( G e. NrmGrp /\ A e. X ) -> ( ( N ` A ) =/= 0 <-> A =/= .0. ) ) |
6 |
1 2
|
nmcl |
|- ( ( G e. NrmGrp /\ A e. X ) -> ( N ` A ) e. RR ) |
7 |
1 2
|
nmge0 |
|- ( ( G e. NrmGrp /\ A e. X ) -> 0 <_ ( N ` A ) ) |
8 |
|
ne0gt0 |
|- ( ( ( N ` A ) e. RR /\ 0 <_ ( N ` A ) ) -> ( ( N ` A ) =/= 0 <-> 0 < ( N ` A ) ) ) |
9 |
6 7 8
|
syl2anc |
|- ( ( G e. NrmGrp /\ A e. X ) -> ( ( N ` A ) =/= 0 <-> 0 < ( N ` A ) ) ) |
10 |
5 9
|
bitr3d |
|- ( ( G e. NrmGrp /\ A e. X ) -> ( A =/= .0. <-> 0 < ( N ` A ) ) ) |