Metamath Proof Explorer

Theorem ascldimul

Description: The algebra scalar lifting function distributes over multiplication. (Contributed by Mario Carneiro, 8-Mar-2015) (Proof shortened by SN, 5-Nov-2023)

Ref Expression
Hypotheses ascldimul.a 
|- A = ( algSc ` W )
ascldimul.f 
|- F = ( Scalar ` W )
ascldimul.k 
|- K = ( Base ` F )
ascldimul.t 
|- .X. = ( .r ` W )
ascldimul.s 
|- .x. = ( .r ` F )
Assertion ascldimul 
|- ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( A ` ( R .x. S ) ) = ( ( A ` R ) .X. ( A ` S ) ) )

Proof

Step Hyp Ref Expression
1 ascldimul.a 
 |-  A = ( algSc ` W )
2 ascldimul.f 
 |-  F = ( Scalar ` W )
3 ascldimul.k 
 |-  K = ( Base ` F )
4 ascldimul.t 
 |-  .X. = ( .r ` W )
5 ascldimul.s 
 |-  .x. = ( .r ` F )
6 assalmod 
 |-  ( W e. AssAlg -> W e. LMod )
7 6 3ad2ant1 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> W e. LMod )
8 simp2 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> R e. K )
9 simp3 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> S e. K )
10 assaring 
 |-  ( W e. AssAlg -> W e. Ring )
11 10 3ad2ant1 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> W e. Ring )
12 eqid 
 |-  ( Base ` W ) = ( Base ` W )
13 eqid 
 |-  ( 1r ` W ) = ( 1r ` W )
14 12 13 ringidcl 
 |-  ( W e. Ring -> ( 1r ` W ) e. ( Base ` W ) )
15 11 14 syl 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( 1r ` W ) e. ( Base ` W ) )
16 eqid 
 |-  ( .s ` W ) = ( .s ` W )
17 12 2 16 3 5 lmodvsass 
 |-  ( ( W e. LMod /\ ( R e. K /\ S e. K /\ ( 1r ` W ) e. ( Base ` W ) ) ) -> ( ( R .x. S ) ( .s ` W ) ( 1r ` W ) ) = ( R ( .s ` W ) ( S ( .s ` W ) ( 1r ` W ) ) ) )
18 7 8 9 15 17 syl13anc 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( ( R .x. S ) ( .s ` W ) ( 1r ` W ) ) = ( R ( .s ` W ) ( S ( .s ` W ) ( 1r ` W ) ) ) )
19 2 lmodring 
 |-  ( W e. LMod -> F e. Ring )
20 6 19 syl 
 |-  ( W e. AssAlg -> F e. Ring )
21 3 5 ringcl 
 |-  ( ( F e. Ring /\ R e. K /\ S e. K ) -> ( R .x. S ) e. K )
22 20 21 syl3an1 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( R .x. S ) e. K )
23 1 2 3 16 13 asclval 
 |-  ( ( R .x. S ) e. K -> ( A ` ( R .x. S ) ) = ( ( R .x. S ) ( .s ` W ) ( 1r ` W ) ) )
24 22 23 syl 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( A ` ( R .x. S ) ) = ( ( R .x. S ) ( .s ` W ) ( 1r ` W ) ) )
25 1 2 10 6 3 12 asclf 
 |-  ( W e. AssAlg -> A : K --> ( Base ` W ) )
26 25 ffvelcdmda 
 |-  ( ( W e. AssAlg /\ S e. K ) -> ( A ` S ) e. ( Base ` W ) )
27 26 3adant2 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( A ` S ) e. ( Base ` W ) )
28 1 2 3 12 4 16 asclmul1 
 |-  ( ( W e. AssAlg /\ R e. K /\ ( A ` S ) e. ( Base ` W ) ) -> ( ( A ` R ) .X. ( A ` S ) ) = ( R ( .s ` W ) ( A ` S ) ) )
29 27 28 syld3an3 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( ( A ` R ) .X. ( A ` S ) ) = ( R ( .s ` W ) ( A ` S ) ) )
30 1 2 3 16 13 asclval 
 |-  ( S e. K -> ( A ` S ) = ( S ( .s ` W ) ( 1r ` W ) ) )
31 30 3ad2ant3 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( A ` S ) = ( S ( .s ` W ) ( 1r ` W ) ) )
32 31 oveq2d 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( R ( .s ` W ) ( A ` S ) ) = ( R ( .s ` W ) ( S ( .s ` W ) ( 1r ` W ) ) ) )
33 29 32 eqtrd 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( ( A ` R ) .X. ( A ` S ) ) = ( R ( .s ` W ) ( S ( .s ` W ) ( 1r ` W ) ) ) )
34 18 24 33 3eqtr4d 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( A ` ( R .x. S ) ) = ( ( A ` R ) .X. ( A ` S ) ) )