Theorem nmvs

Description: Defining property of a normed module. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	isnlm.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	isnlm.n	⊢ 𝑁 = ( norm ‘ 𝑊 )
	isnlm.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	isnlm.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	isnlm.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	isnlm.a	⊢ 𝐴 = ( norm ‘ 𝐹 )
Assertion	nmvs	⊢ ( ( 𝑊 ∈ NrmMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐴 ‘ 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isnlm.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		isnlm.n	⊢ 𝑁 = ( norm ‘ 𝑊 )
3		isnlm.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
4		isnlm.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
5		isnlm.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
6		isnlm.a	⊢ 𝐴 = ( norm ‘ 𝐹 )
7	1 2 3 4 5 6	isnlm	⊢ ( 𝑊 ∈ NrmMod ↔ ( ( 𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ∧ ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ) )
8	7	simprbi	⊢ ( 𝑊 ∈ NrmMod → ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) )
9		fvoveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑁 ‘ ( 𝑥 · 𝑦 ) ) = ( 𝑁 ‘ ( 𝑋 · 𝑦 ) ) )
10		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑋 ) )
11	10	oveq1d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐴 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) = ( ( 𝐴 ‘ 𝑋 ) · ( 𝑁 ‘ 𝑦 ) ) )
12	9 11	eqeq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑁 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) ↔ ( 𝑁 ‘ ( 𝑋 · 𝑦 ) ) = ( ( 𝐴 ‘ 𝑋 ) · ( 𝑁 ‘ 𝑦 ) ) ) )
13		oveq2	⊢ ( 𝑦 = 𝑌 → ( 𝑋 · 𝑦 ) = ( 𝑋 · 𝑌 ) )
14	13	fveq2d	⊢ ( 𝑦 = 𝑌 → ( 𝑁 ‘ ( 𝑋 · 𝑦 ) ) = ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) )
15		fveq2	⊢ ( 𝑦 = 𝑌 → ( 𝑁 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑌 ) )
16	15	oveq2d	⊢ ( 𝑦 = 𝑌 → ( ( 𝐴 ‘ 𝑋 ) · ( 𝑁 ‘ 𝑦 ) ) = ( ( 𝐴 ‘ 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) )
17	14 16	eqeq12d	⊢ ( 𝑦 = 𝑌 → ( ( 𝑁 ‘ ( 𝑋 · 𝑦 ) ) = ( ( 𝐴 ‘ 𝑋 ) · ( 𝑁 ‘ 𝑦 ) ) ↔ ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐴 ‘ 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) ) )
18	12 17	rspc2v	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( ∀ 𝑥 ∈ 𝐾 ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) · ( 𝑁 ‘ 𝑦 ) ) → ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐴 ‘ 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) ) )
19	8 18	syl5com	⊢ ( 𝑊 ∈ NrmMod → ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐴 ‘ 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) ) )
20	19	3impib	⊢ ( ( 𝑊 ∈ NrmMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐴 ‘ 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) )