Metamath Proof Explorer

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 ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐴 ‘ 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) )