This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem assaring

Description: An associative algebra is a ring. (Contributed by Mario Carneiro, 5-Dec-2014)

Ref Expression
Assertion assaring ( 𝑊 ∈ AssAlg → 𝑊 ∈ Ring )

Proof

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