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 ⊢ A = algSc ⁡ W
asclrhm.f ⊢ F = Scalar ⁡ W
Assertion asclrhm ⊢ W ∈ AssAlg → A ∈ F RingHom W

Proof

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 ⊢ ⋅ F = ⋅ F
7 eqid ⊢ ⋅ W = ⋅ W
8 2 assasca ⊢ W ∈ AssAlg → F ∈ CRing
9 8 crngringd ⊢ W ∈ AssAlg → F ∈ Ring
10 assaring ⊢ W ∈ AssAlg → W ∈ Ring
11 assalmod ⊢ W ∈ AssAlg → W ∈ LMod
12 1 2 11 10 ascl1 ⊢ W ∈ AssAlg → A ⁡ 1 F = 1 W
13 1 2 3 7 6 ascldimul ⊢ W ∈ AssAlg ∧ x ∈ Base F ∧ y ∈ Base F → A ⁡ x ⋅ F y = A ⁡ x ⋅ W A ⁡ y
14 13 3expb ⊢ W ∈ AssAlg ∧ x ∈ Base F ∧ y ∈ Base F → A ⁡ x ⋅ F y = A ⁡ x ⋅ W A ⁡ y
15 1 2 10 11 asclghm ⊢ W ∈ AssAlg → A ∈ F GrpHom W
16 3 4 5 6 7 9 10 12 14 15 isrhm2d ⊢ W ∈ AssAlg → A ∈ F RingHom W