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 eqid 
 |-  ( Base ` W ) = ( Base ` W )
11 eqid 
 |-  ( 1r ` W ) = ( 1r ` W )
12 assaring 
 |-  ( W e. AssAlg -> W e. Ring )
13 12 3ad2ant1 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> W e. Ring )
14 10 11 13 ringidcld 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( 1r ` W ) e. ( Base ` W ) )
15 eqid 
 |-  ( .s ` W ) = ( .s ` W )
16 10 2 15 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 ) ) ) )
17 7 8 9 14 16 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 ) ) ) )
18 2 assasca 
 |-  ( W e. AssAlg -> F e. Ring )
19 3 5 ringcl 
 |-  ( ( F e. Ring /\ R e. K /\ S e. K ) -> ( R .x. S ) e. K )
20 18 19 syl3an1 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( R .x. S ) e. K )
21 1 2 3 15 11 asclval 
 |-  ( ( R .x. S ) e. K -> ( A ` ( R .x. S ) ) = ( ( R .x. S ) ( .s ` W ) ( 1r ` W ) ) )
22 20 21 syl 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( A ` ( R .x. S ) ) = ( ( R .x. S ) ( .s ` W ) ( 1r ` W ) ) )
23 1 2 12 6 3 10 asclf 
 |-  ( W e. AssAlg -> A : K --> ( Base ` W ) )
24 23 ffvelcdmda 
 |-  ( ( W e. AssAlg /\ S e. K ) -> ( A ` S ) e. ( Base ` W ) )
25 24 3adant2 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( A ` S ) e. ( Base ` W ) )
26 1 2 3 10 4 15 asclmul1 
 |-  ( ( W e. AssAlg /\ R e. K /\ ( A ` S ) e. ( Base ` W ) ) -> ( ( A ` R ) .X. ( A ` S ) ) = ( R ( .s ` W ) ( A ` S ) ) )
27 25 26 syld3an3 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( ( A ` R ) .X. ( A ` S ) ) = ( R ( .s ` W ) ( A ` S ) ) )
28 1 2 3 15 11 asclval 
 |-  ( S e. K -> ( A ` S ) = ( S ( .s ` W ) ( 1r ` W ) ) )
29 28 3ad2ant3 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( A ` S ) = ( S ( .s ` W ) ( 1r ` W ) ) )
30 29 oveq2d 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( R ( .s ` W ) ( A ` S ) ) = ( R ( .s ` W ) ( S ( .s ` W ) ( 1r ` W ) ) ) )
31 27 30 eqtrd 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( ( A ` R ) .X. ( A ` S ) ) = ( R ( .s ` W ) ( S ( .s ` W ) ( 1r ` W ) ) ) )
32 17 22 31 3eqtr4d 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( A ` ( R .x. S ) ) = ( ( A ` R ) .X. ( A ` S ) ) )