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