Theorem nlmnrg

Description: The scalar component of a left module is a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypothesis	nlmnrg.1	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
Assertion	nlmnrg	⊢ ( 𝑊 ∈ NrmMod → 𝐹 ∈ NrmRing )

Proof

Step	Hyp	Ref	Expression
1		nlmnrg.1	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
3		eqid	⊢ ( norm ‘ 𝑊 ) = ( norm ‘ 𝑊 )
4		eqid	⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
5		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
6		eqid	⊢ ( norm ‘ 𝐹 ) = ( norm ‘ 𝐹 )
7	2 3 4 1 5 6	isnlm	⊢ ( 𝑊 ∈ NrmMod ↔ ( ( 𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐹 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( norm ‘ 𝑊 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑥 ) · ( ( norm ‘ 𝑊 ) ‘ 𝑦 ) ) ) )
8	7	simplbi	⊢ ( 𝑊 ∈ NrmMod → ( 𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) )
9	8	simp3d	⊢ ( 𝑊 ∈ NrmMod → 𝐹 ∈ NrmRing )