Metamath Proof Explorer

Theorem asclrhm

Description: The scalar injection 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 → 𝐹 ∈ CRing )
9 crngring ⊢ ( 𝐹 ∈ CRing → 𝐹 ∈ Ring )
10 8 9 syl ⊢ ( 𝑊 ∈ AssAlg → 𝐹 ∈ Ring )
11 assaring ⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ Ring )
12 3 4 ringidcl ⊢ ( 𝐹 ∈ Ring → ( 1r ‘ 𝐹 ) ∈ ( Base ‘ 𝐹 ) )
13 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
14 1 2 3 13 5 asclval ⊢ ( ( 1r ‘ 𝐹 ) ∈ ( Base ‘ 𝐹 ) → ( 𝐴 ‘ ( 1r ‘ 𝐹 ) ) = ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
15 10 12 14 3syl ⊢ ( 𝑊 ∈ AssAlg → ( 𝐴 ‘ ( 1r ‘ 𝐹 ) ) = ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
16 assalmod ⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ LMod )
17 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
18 17 5 ringidcl ⊢ ( 𝑊 ∈ Ring → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
19 11 18 syl ⊢ ( 𝑊 ∈ AssAlg → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
20 17 2 13 4 lmodvs1 ⊢ ( ( 𝑊 ∈ LMod ∧ ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) ) → ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) = ( 1r ‘ 𝑊 ) )
21 16 19 20 syl2anc ⊢ ( 𝑊 ∈ AssAlg → ( ( 1r ‘ 𝐹 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) = ( 1r ‘ 𝑊 ) )
22 15 21 eqtrd ⊢ ( 𝑊 ∈ AssAlg → ( 𝐴 ‘ ( 1r ‘ 𝐹 ) ) = ( 1r ‘ 𝑊 ) )
23 1 2 3 7 6 ascldimul ⊢ ( ( 𝑊 ∈ AssAlg ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) → ( 𝐴 ‘ ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) ( .r ‘ 𝑊 ) ( 𝐴 ‘ 𝑦 ) ) )
24 23 3expb ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ) → ( 𝐴 ‘ ( 𝑥 ( .r ‘ 𝐹 ) 𝑦 ) ) = ( ( 𝐴 ‘ 𝑥 ) ( .r ‘ 𝑊 ) ( 𝐴 ‘ 𝑦 ) ) )
25 1 2 11 16 asclghm ⊢ ( 𝑊 ∈ AssAlg → 𝐴 ∈ ( 𝐹 GrpHom 𝑊 ) )
26 3 4 5 6 7 10 11 22 24 25 isrhm2d ⊢ ( 𝑊 ∈ AssAlg → 𝐴 ∈ ( 𝐹 RingHom 𝑊 ) )