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 ⊢ 𝐴 = ( algSc ‘ 𝑊 )
asclf.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
asclf.r ⊢ ( 𝜑 → 𝑊 ∈ Ring )
asclf.l ⊢ ( 𝜑 → 𝑊 ∈ LMod )
asclf.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
asclf.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
Assertion asclf ( 𝜑 → 𝐴 : 𝐾 ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 asclf.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
2 asclf.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 asclf.r ⊢ ( 𝜑 → 𝑊 ∈ Ring )
4 asclf.l ⊢ ( 𝜑 → 𝑊 ∈ LMod )
5 asclf.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
6 asclf.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
7 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → 𝑊 ∈ LMod )
8 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → 𝑥 ∈ 𝐾 )
9 eqid ⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
10 6 9 ringidcl ⊢ ( 𝑊 ∈ Ring → ( 1r ‘ 𝑊 ) ∈ 𝐵 )
11 3 10 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑊 ) ∈ 𝐵 )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( 1r ‘ 𝑊 ) ∈ 𝐵 )
13 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
14 6 2 13 5 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑥 ∈ 𝐾 ∧ ( 1r ‘ 𝑊 ) ∈ 𝐵 ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ∈ 𝐵 )
15 7 8 12 14 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ∈ 𝐵 )
16 1 2 5 13 9 asclfval ⊢ 𝐴 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
17 15 16 fmptd ⊢ ( 𝜑 → 𝐴 : 𝐾 ⟶ 𝐵 )