Theorem isncvsngpd

Description: Properties that determine a normed subcomplex vector space. (Contributed by NM, 15-Apr-2007) (Revised by AV, 7-Oct-2021)

	Ref	Expression
Hypotheses	isncvsngp.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	isncvsngp.n	⊢ 𝑁 = ( norm ‘ 𝑊 )
	isncvsngp.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	isncvsngp.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	isncvsngp.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	isncvsngpd.v	⊢ ( 𝜑 → 𝑊 ∈ ℂVec )
	isncvsngpd.g	⊢ ( 𝜑 → 𝑊 ∈ NrmGrp )
	isncvsngpd.t	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑘 ∈ 𝐾 ) ) → ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) )
Assertion	isncvsngpd	⊢ ( 𝜑 → 𝑊 ∈ ( NrmVec ∩ ℂVec ) )

Proof

Step	Hyp	Ref	Expression
1		isncvsngp.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		isncvsngp.n	⊢ 𝑁 = ( norm ‘ 𝑊 )
3		isncvsngp.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
4		isncvsngp.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
5		isncvsngp.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
6		isncvsngpd.v	⊢ ( 𝜑 → 𝑊 ∈ ℂVec )
7		isncvsngpd.g	⊢ ( 𝜑 → 𝑊 ∈ NrmGrp )
8		isncvsngpd.t	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑘 ∈ 𝐾 ) ) → ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) )
9	8	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) )
10	1 2 3 4 5	isncvsngp	⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ↔ ( 𝑊 ∈ ℂVec ∧ 𝑊 ∈ NrmGrp ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) )
11	6 7 9 10	syl3anbrc	⊢ ( 𝜑 → 𝑊 ∈ ( NrmVec ∩ ℂVec ) )