Metamath Proof Explorer

Theorem ascldimulOLD

Description: Obsolete version of ascldimul as of 5-Nov-2023. (Contributed by Mario Carneiro, 8-Mar-2015) (Proof modification is discouraged.) (New usage is discouraged.)

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 ascldimulOLD 
|- ( ( 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 assaring 
 |-  ( W e. AssAlg -> W e. Ring )
7 eqid 
 |-  ( Base ` W ) = ( Base ` W )
8 eqid 
 |-  ( 1r ` W ) = ( 1r ` W )
9 7 8 ringidcl 
 |-  ( W e. Ring -> ( 1r ` W ) e. ( Base ` W ) )
10 6 9 syl 
 |-  ( W e. AssAlg -> ( 1r ` W ) e. ( Base ` W ) )
11 7 4 8 ringlidm 
 |-  ( ( W e. Ring /\ ( 1r ` W ) e. ( Base ` W ) ) -> ( ( 1r ` W ) .X. ( 1r ` W ) ) = ( 1r ` W ) )
12 6 10 11 syl2anc 
 |-  ( W e. AssAlg -> ( ( 1r ` W ) .X. ( 1r ` W ) ) = ( 1r ` W ) )
13 12 oveq2d 
 |-  ( W e. AssAlg -> ( S ( .s ` W ) ( ( 1r ` W ) .X. ( 1r ` W ) ) ) = ( S ( .s ` W ) ( 1r ` W ) ) )
14 13 oveq2d 
 |-  ( W e. AssAlg -> ( R ( .s ` W ) ( S ( .s ` W ) ( ( 1r ` W ) .X. ( 1r ` W ) ) ) ) = ( R ( .s ` W ) ( S ( .s ` W ) ( 1r ` W ) ) ) )
15 14 3ad2ant1 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( R ( .s ` W ) ( S ( .s ` W ) ( ( 1r ` W ) .X. ( 1r ` W ) ) ) ) = ( R ( .s ` W ) ( S ( .s ` W ) ( 1r ` W ) ) ) )
16 simp1 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> W e. AssAlg )
17 simp2 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> R e. K )
18 10 3ad2ant1 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( 1r ` W ) e. ( Base ` W ) )
19 assalmod 
 |-  ( W e. AssAlg -> W e. LMod )
20 19 3ad2ant1 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> W e. LMod )
21 simp3 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> S e. K )
22 eqid 
 |-  ( .s ` W ) = ( .s ` W )
23 7 2 22 3 lmodvscl 
 |-  ( ( W e. LMod /\ S e. K /\ ( 1r ` W ) e. ( Base ` W ) ) -> ( S ( .s ` W ) ( 1r ` W ) ) e. ( Base ` W ) )
24 20 21 18 23 syl3anc 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( S ( .s ` W ) ( 1r ` W ) ) e. ( Base ` W ) )
25 7 2 3 22 4 assaass 
 |-  ( ( W e. AssAlg /\ ( R e. K /\ ( 1r ` W ) e. ( Base ` W ) /\ ( S ( .s ` W ) ( 1r ` W ) ) e. ( Base ` W ) ) ) -> ( ( R ( .s ` W ) ( 1r ` W ) ) .X. ( S ( .s ` W ) ( 1r ` W ) ) ) = ( R ( .s ` W ) ( ( 1r ` W ) .X. ( S ( .s ` W ) ( 1r ` W ) ) ) ) )
26 16 17 18 24 25 syl13anc 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( ( R ( .s ` W ) ( 1r ` W ) ) .X. ( S ( .s ` W ) ( 1r ` W ) ) ) = ( R ( .s ` W ) ( ( 1r ` W ) .X. ( S ( .s ` W ) ( 1r ` W ) ) ) ) )
27 7 2 3 22 4 assaassr 
 |-  ( ( W e. AssAlg /\ ( S e. K /\ ( 1r ` W ) e. ( Base ` W ) /\ ( 1r ` W ) e. ( Base ` W ) ) ) -> ( ( 1r ` W ) .X. ( S ( .s ` W ) ( 1r ` W ) ) ) = ( S ( .s ` W ) ( ( 1r ` W ) .X. ( 1r ` W ) ) ) )
28 16 21 18 18 27 syl13anc 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( ( 1r ` W ) .X. ( S ( .s ` W ) ( 1r ` W ) ) ) = ( S ( .s ` W ) ( ( 1r ` W ) .X. ( 1r ` W ) ) ) )
29 28 oveq2d 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( R ( .s ` W ) ( ( 1r ` W ) .X. ( S ( .s ` W ) ( 1r ` W ) ) ) ) = ( R ( .s ` W ) ( S ( .s ` W ) ( ( 1r ` W ) .X. ( 1r ` W ) ) ) ) )
30 26 29 eqtrd 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( ( R ( .s ` W ) ( 1r ` W ) ) .X. ( S ( .s ` W ) ( 1r ` W ) ) ) = ( R ( .s ` W ) ( S ( .s ` W ) ( ( 1r ` W ) .X. ( 1r ` W ) ) ) ) )
31 7 2 22 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 ) ) ) )
32 20 17 21 18 31 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 ) ) ) )
33 15 30 32 3eqtr4rd 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( ( R .x. S ) ( .s ` W ) ( 1r ` W ) ) = ( ( R ( .s ` W ) ( 1r ` W ) ) .X. ( S ( .s ` W ) ( 1r ` W ) ) ) )
34 2 assasca 
 |-  ( W e. AssAlg -> F e. CRing )
35 crngring 
 |-  ( F e. CRing -> F e. Ring )
36 34 35 syl 
 |-  ( W e. AssAlg -> F e. Ring )
37 3 5 ringcl 
 |-  ( ( F e. Ring /\ R e. K /\ S e. K ) -> ( R .x. S ) e. K )
38 36 37 syl3an1 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( R .x. S ) e. K )
39 1 2 3 22 8 asclval 
 |-  ( ( R .x. S ) e. K -> ( A ` ( R .x. S ) ) = ( ( R .x. S ) ( .s ` W ) ( 1r ` W ) ) )
40 38 39 syl 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( A ` ( R .x. S ) ) = ( ( R .x. S ) ( .s ` W ) ( 1r ` W ) ) )
41 1 2 3 22 8 asclval 
 |-  ( R e. K -> ( A ` R ) = ( R ( .s ` W ) ( 1r ` W ) ) )
42 17 41 syl 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( A ` R ) = ( R ( .s ` W ) ( 1r ` W ) ) )
43 1 2 3 22 8 asclval 
 |-  ( S e. K -> ( A ` S ) = ( S ( .s ` W ) ( 1r ` W ) ) )
44 21 43 syl 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( A ` S ) = ( S ( .s ` W ) ( 1r ` W ) ) )
45 42 44 oveq12d 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( ( A ` R ) .X. ( A ` S ) ) = ( ( R ( .s ` W ) ( 1r ` W ) ) .X. ( S ( .s ` W ) ( 1r ` W ) ) ) )
46 33 40 45 3eqtr4d 
 |-  ( ( W e. AssAlg /\ R e. K /\ S e. K ) -> ( A ` ( R .x. S ) ) = ( ( A ` R ) .X. ( A ` S ) ) )