Theorem assasca

Description: An associative algebra's scalar field is a commutative ring. (Contributed by Mario Carneiro, 7-Jan-2015)

	Ref	Expression
Hypothesis	assasca.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
Assertion	assasca	⊢ ( 𝑊 ∈ AssAlg → 𝐹 ∈ CRing )

Proof

Step	Hyp	Ref	Expression
1		assasca.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
3		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
4		eqid	⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
5		eqid	⊢ ( .r ‘ 𝑊 ) = ( .r ‘ 𝑊 )
6	2 1 3 4 5	isassa	⊢ ( 𝑊 ∈ AssAlg ↔ ( ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐹 ) ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ( .r ‘ 𝑊 ) 𝑦 ) = ( 𝑧 ( ·𝑠 ‘ 𝑊 ) ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) ) ∧ ( 𝑥 ( .r ‘ 𝑊 ) ( 𝑧 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ) = ( 𝑧 ( ·𝑠 ‘ 𝑊 ) ( 𝑥 ( .r ‘ 𝑊 ) 𝑦 ) ) ) ) )
7	6	simplbi	⊢ ( 𝑊 ∈ AssAlg → ( 𝑊 ∈ LMod ∧ 𝑊 ∈ Ring ∧ 𝐹 ∈ CRing ) )
8	7	simp3d	⊢ ( 𝑊 ∈ AssAlg → 𝐹 ∈ CRing )