Theorem asclf

Description: The algebra scalars 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	⊢ ( 𝜑 → 𝐴 : 𝐾 ⟶ 𝐵 )