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

Metamath Proof Explorer

Theorem asclrhm

Description: The algebra scalar lifting function is a ring homomorphism. (Contributed by Mario Carneiro, 8-Mar-2015)

Ref Expression
Hypotheses asclrhm.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
asclrhm.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
Assertion asclrhm ( 𝑊 ∈ AssAlg → 𝐴 ∈ ( 𝐹 RingHom 𝑊 ) )

Proof

Step Hyp Ref Expression
1 asclrhm.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
2 asclrhm.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
4 eqid ⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
5 eqid ⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
6 eqid ⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
7 eqid ⊢ ( .r ‘ 𝑊 ) = ( .r ‘ 𝑊 )
8 2 assasca ⊢ ( 𝑊 ∈ AssAlg → 𝐹 ∈ Ring )
9 assaring ⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ Ring )
10 assalmod ⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ LMod )
11 1 2 10 9 ascl1 ⊢ ( 𝑊 ∈ AssAlg → ( 𝐴 ‘ ( 1r ‘ 𝐹 ) ) = ( 1r ‘ 𝑊 ) )
12 1 2 3 7 6 ascldimul ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) → ( 𝐴 ‘ ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) ( .r ‘ 𝑊 ) ( 𝐴 ‘ 𝑦 ) ) )
13 12 3expb ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ) → ( 𝐴 ‘ ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) ( .r ‘ 𝑊 ) ( 𝐴 ‘ 𝑦 ) ) )
14 1 2 9 10 asclghm ⊢ ( 𝑊 ∈ AssAlg → 𝐴 ∈ ( 𝐹 GrpHom 𝑊 ) )
15 3 4 5 6 7 8 9 11 13 14 isrhm2d ⊢ ( 𝑊 ∈ AssAlg → 𝐴 ∈ ( 𝐹 RingHom 𝑊 ) )