Theorem isnvc2

Description: A normed vector space is just a normed module whose scalar ring is a division ring. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypothesis	isnvc2.1	|- F = ( Scalar ` W )
Assertion	isnvc2	|- ( W e. NrmVec <-> ( W e. NrmMod /\ F e. DivRing ) )

Proof

Step	Hyp	Ref	Expression
1		isnvc2.1	|- F = ( Scalar ` W )
2		isnvc	|- ( W e. NrmVec <-> ( W e. NrmMod /\ W e. LVec ) )
3		nlmlmod	|- ( W e. NrmMod -> W e. LMod )
4	1	islvec	|- ( W e. LVec <-> ( W e. LMod /\ F e. DivRing ) )
5	4	baib	|- ( W e. LMod -> ( W e. LVec <-> F e. DivRing ) )
6	3 5	syl	|- ( W e. NrmMod -> ( W e. LVec <-> F e. DivRing ) )
7	6	pm5.32i	|- ( ( W e. NrmMod /\ W e. LVec ) <-> ( W e. NrmMod /\ F e. DivRing ) )
8	2 7	bitri	|- ( W e. NrmVec <-> ( W e. NrmMod /\ F e. DivRing ) )