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 𝑊 ) )