asclrhm

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

Step	Hyp	Ref	Expression
1		asclrhm.a	$⊢ A = algSc (W)$
2		asclrhm.f	$⊢ F = Scalar (W)$
3		eqid	$⊢ {Base}_{F} = {Base}_{F}$
4		eqid	$⊢ 1_{F} = 1_{F}$
5		eqid	$⊢ 1_{W} = 1_{W}$
6		eqid	$⊢ \cdot_{F} = \cdot_{F}$
7		eqid	$⊢ \cdot_{W} = \cdot_{W}$
8	2	assasca	$⊢ W \in AssAlg \to F \in Ring$
9		assaring	$⊢ W \in AssAlg \to W \in Ring$
10		assalmod	$⊢ W \in AssAlg \to W \in LMod$
11	1 2 10 9	ascl1	$⊢ W \in AssAlg \to A (1_{F}) = 1_{W}$
12	1 2 3 7 6	ascldimul	$⊢ (W \in AssAlg \land x \in {Base}_{F} \land y \in {Base}_{F}) \to A (x \cdot_{F} y) = A (x) \cdot_{W} A (y)$
13	12	3expb	$⊢ (W \in AssAlg \land (x \in {Base}_{F} \land y \in {Base}_{F})) \to A (x \cdot_{F} y) = A (x) \cdot_{W} A (y)$
14	1 2 9 10	asclghm	$⊢ W \in AssAlg \to A \in (F GrpHom W)$
15	3 4 5 6 7 8 9 11 13 14	isrhm2d	$⊢ W \in AssAlg \to A \in (F RingHom W)$

Metamath Proof Explorer