This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem asclf

Description: The algebra scalar lifting function is a function into the base set. (Contributed by Mario Carneiro, 4-Jul-2015)

Ref Expression
Hypotheses asclf.a ⊢ A = algSc ⁡ W
asclf.f ⊢ F = Scalar ⁡ W
asclf.r ⊢ φ → W ∈ Ring
asclf.l ⊢ φ → W ∈ LMod
asclf.k ⊢ K = Base F
asclf.b ⊢ B = Base W
Assertion asclf ⊢ φ → A : K ⟶ B

Proof

Step Hyp Ref Expression
1 asclf.a ⊢ A = algSc ⁡ W
2 asclf.f ⊢ F = Scalar ⁡ W
3 asclf.r ⊢ φ → W ∈ Ring
4 asclf.l ⊢ φ → W ∈ LMod
5 asclf.k ⊢ K = Base F
6 asclf.b ⊢ B = Base W
7 4 adantr ⊢ φ ∧ x ∈ K → W ∈ LMod
8 simpr ⊢ φ ∧ x ∈ K → x ∈ K
9 eqid ⊢ 1 W = 1 W
10 6 9 ringidcl ⊢ W ∈ Ring → 1 W ∈ B
11 3 10 syl ⊢ φ → 1 W ∈ B
12 11 adantr ⊢ φ ∧ x ∈ K → 1 W ∈ B
13 eqid ⊢ ⋅ W = ⋅ W
14 6 2 13 5 lmodvscl ⊢ W ∈ LMod ∧ x ∈ K ∧ 1 W ∈ B → x ⋅ W 1 W ∈ B
15 7 8 12 14 syl3anc ⊢ φ ∧ x ∈ K → x ⋅ W 1 W ∈ B
16 1 2 5 13 9 asclfval ⊢ A = x ∈ K ⟼ x ⋅ W 1 W
17 15 16 fmptd ⊢ φ → A : K ⟶ B