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 
|- ( ph -> W e. Ring )
asclf.l 
|- ( ph -> W e. LMod )
asclf.k 
|- K = ( Base ` F )
asclf.b 
|- B = ( Base ` W )
Assertion asclf 
|- ( ph -> A : K --> B )

Proof

Step Hyp Ref Expression
1 asclf.a 
 |-  A = ( algSc ` W )
2 asclf.f 
 |-  F = ( Scalar ` W )
3 asclf.r 
 |-  ( ph -> W e. Ring )
4 asclf.l 
 |-  ( ph -> W e. LMod )
5 asclf.k 
 |-  K = ( Base ` F )
6 asclf.b 
 |-  B = ( Base ` W )
7 4 adantr 
 |-  ( ( ph /\ x e. K ) -> W e. LMod )
8 simpr 
 |-  ( ( ph /\ x e. K ) -> x e. K )
9 eqid 
 |-  ( 1r ` W ) = ( 1r ` W )
10 6 9 ringidcl 
 |-  ( W e. Ring -> ( 1r ` W ) e. B )
11 3 10 syl 
 |-  ( ph -> ( 1r ` W ) e. B )
12 11 adantr 
 |-  ( ( ph /\ x e. K ) -> ( 1r ` W ) e. B )
13 eqid 
 |-  ( .s ` W ) = ( .s ` W )
14 6 2 13 5 lmodvscl 
 |-  ( ( W e. LMod /\ x e. K /\ ( 1r ` W ) e. B ) -> ( x ( .s ` W ) ( 1r ` W ) ) e. B )
15 7 8 12 14 syl3anc 
 |-  ( ( ph /\ x e. K ) -> ( x ( .s ` W ) ( 1r ` W ) ) e. B )
16 1 2 5 13 9 asclfval 
 |-  A = ( x e. K |-> ( x ( .s ` W ) ( 1r ` W ) ) )
17 15 16 fmptd 
 |-  ( ph -> A : K --> B )