Theorem norm-i-i

Description: Theorem 3.3(i) of Beran p. 97. (Contributed by NM, 5-Sep-1999) (New usage is discouraged.)

	Ref	Expression
Hypothesis	normcl.1	|- A e. ~H
Assertion	norm-i-i	|- ( ( normh ` A ) = 0 <-> A = 0h )

Proof

Step	Hyp	Ref	Expression
1		normcl.1	|- A e. ~H
2		norm-i	|- ( A e. ~H -> ( ( normh ` A ) = 0 <-> A = 0h ) )
3	1 2	ax-mp	|- ( ( normh ` A ) = 0 <-> A = 0h )