Theorem ncvsprp

Description: Proportionality property of the norm of a scalar product in a normed subcomplex vector space. (Contributed by NM, 11-Nov-2006) (Revised by AV, 8-Oct-2021)

	Ref	Expression
Hypotheses	ncvsprp.v	|- V = ( Base ` W )
	ncvsprp.n	|- N = ( norm ` W )
	ncvsprp.s	|- .x. = ( .s ` W )
	ncvsprp.f	|- F = ( Scalar ` W )
	ncvsprp.k	|- K = ( Base ` F )
Assertion	ncvsprp	|- ( ( W e. ( NrmVec i^i CVec ) /\ A e. K /\ B e. V ) -> ( N ` ( A .x. B ) ) = ( ( abs ` A ) x. ( N ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		ncvsprp.v	|- V = ( Base ` W )
2		ncvsprp.n	|- N = ( norm ` W )
3		ncvsprp.s	|- .x. = ( .s ` W )
4		ncvsprp.f	|- F = ( Scalar ` W )
5		ncvsprp.k	|- K = ( Base ` F )
6		elin	|- ( W e. ( NrmVec i^i CVec ) <-> ( W e. NrmVec /\ W e. CVec ) )
7		nvcnlm	|- ( W e. NrmVec -> W e. NrmMod )
8	7	adantr	|- ( ( W e. NrmVec /\ W e. CVec ) -> W e. NrmMod )
9	6 8	sylbi	|- ( W e. ( NrmVec i^i CVec ) -> W e. NrmMod )
10		eqid	|- ( norm ` F ) = ( norm ` F )
11	1 2 3 4 5 10	nmvs	|- ( ( W e. NrmMod /\ A e. K /\ B e. V ) -> ( N ` ( A .x. B ) ) = ( ( ( norm ` F ) ` A ) x. ( N ` B ) ) )
12	9 11	syl3an1	|- ( ( W e. ( NrmVec i^i CVec ) /\ A e. K /\ B e. V ) -> ( N ` ( A .x. B ) ) = ( ( ( norm ` F ) ` A ) x. ( N ` B ) ) )
13		id	|- ( W e. CVec -> W e. CVec )
14	13	cvsclm	|- ( W e. CVec -> W e. CMod )
15	6 14	simplbiim	|- ( W e. ( NrmVec i^i CVec ) -> W e. CMod )
16	4 5	clmabs	|- ( ( W e. CMod /\ A e. K ) -> ( abs ` A ) = ( ( norm ` F ) ` A ) )
17	15 16	sylan	|- ( ( W e. ( NrmVec i^i CVec ) /\ A e. K ) -> ( abs ` A ) = ( ( norm ` F ) ` A ) )
18	17	3adant3	|- ( ( W e. ( NrmVec i^i CVec ) /\ A e. K /\ B e. V ) -> ( abs ` A ) = ( ( norm ` F ) ` A ) )
19	18	eqcomd	|- ( ( W e. ( NrmVec i^i CVec ) /\ A e. K /\ B e. V ) -> ( ( norm ` F ) ` A ) = ( abs ` A ) )
20	19	oveq1d	|- ( ( W e. ( NrmVec i^i CVec ) /\ A e. K /\ B e. V ) -> ( ( ( norm ` F ) ` A ) x. ( N ` B ) ) = ( ( abs ` A ) x. ( N ` B ) ) )
21	12 20	eqtrd	|- ( ( W e. ( NrmVec i^i CVec ) /\ A e. K /\ B e. V ) -> ( N ` ( A .x. B ) ) = ( ( abs ` A ) x. ( N ` B ) ) )