Metamath Proof Explorer

Theorem asclmulg

Description: Apply group multiplication to the algebra scalars. (Contributed by Thierry Arnoux, 24-Jul-2024)

Ref Expression
Hypotheses asclmulg.a 
|- A = ( algSc ` W )
asclmulg.f 
|- F = ( Scalar ` W )
asclmulg.k 
|- K = ( Base ` F )
asclmulg.m 
|- .^ = ( .g ` W )
asclmulg.t 
|- .* = ( .g ` F )
Assertion asclmulg 
|- ( ( W e. AssAlg /\ N e. NN0 /\ X e. K ) -> ( A ` ( N .* X ) ) = ( N .^ ( A ` X ) ) )

Proof

Step Hyp Ref Expression
1 asclmulg.a 
 |-  A = ( algSc ` W )
2 asclmulg.f 
 |-  F = ( Scalar ` W )
3 asclmulg.k 
 |-  K = ( Base ` F )
4 asclmulg.m 
 |-  .^ = ( .g ` W )
5 asclmulg.t 
 |-  .* = ( .g ` F )
6 assalmod 
 |-  ( W e. AssAlg -> W e. LMod )
7 6 3ad2ant1 
 |-  ( ( W e. AssAlg /\ N e. NN0 /\ X e. K ) -> W e. LMod )
8 simp3 
 |-  ( ( W e. AssAlg /\ N e. NN0 /\ X e. K ) -> X e. K )
9 simp2 
 |-  ( ( W e. AssAlg /\ N e. NN0 /\ X e. K ) -> N e. NN0 )
10 assaring 
 |-  ( W e. AssAlg -> W e. Ring )
11 eqid 
 |-  ( Base ` W ) = ( Base ` W )
12 eqid 
 |-  ( 1r ` W ) = ( 1r ` W )
13 11 12 ringidcl 
 |-  ( W e. Ring -> ( 1r ` W ) e. ( Base ` W ) )
14 10 13 syl 
 |-  ( W e. AssAlg -> ( 1r ` W ) e. ( Base ` W ) )
15 14 3ad2ant1 
 |-  ( ( W e. AssAlg /\ N e. NN0 /\ X e. K ) -> ( 1r ` W ) e. ( Base ` W ) )
16 eqid 
 |-  ( .s ` W ) = ( .s ` W )
17 11 2 16 3 4 5 lmodvsmmulgdi 
 |-  ( ( W e. LMod /\ ( X e. K /\ N e. NN0 /\ ( 1r ` W ) e. ( Base ` W ) ) ) -> ( N .^ ( X ( .s ` W ) ( 1r ` W ) ) ) = ( ( N .* X ) ( .s ` W ) ( 1r ` W ) ) )
18 7 8 9 15 17 syl13anc 
 |-  ( ( W e. AssAlg /\ N e. NN0 /\ X e. K ) -> ( N .^ ( X ( .s ` W ) ( 1r ` W ) ) ) = ( ( N .* X ) ( .s ` W ) ( 1r ` W ) ) )
19 1 2 3 16 12 asclval 
 |-  ( X e. K -> ( A ` X ) = ( X ( .s ` W ) ( 1r ` W ) ) )
20 8 19 syl 
 |-  ( ( W e. AssAlg /\ N e. NN0 /\ X e. K ) -> ( A ` X ) = ( X ( .s ` W ) ( 1r ` W ) ) )
21 20 oveq2d 
 |-  ( ( W e. AssAlg /\ N e. NN0 /\ X e. K ) -> ( N .^ ( A ` X ) ) = ( N .^ ( X ( .s ` W ) ( 1r ` W ) ) ) )
22 2 assasca 
 |-  ( W e. AssAlg -> F e. CRing )
23 22 3ad2ant1 
 |-  ( ( W e. AssAlg /\ N e. NN0 /\ X e. K ) -> F e. CRing )
24 23 crnggrpd 
 |-  ( ( W e. AssAlg /\ N e. NN0 /\ X e. K ) -> F e. Grp )
25 9 nn0zd 
 |-  ( ( W e. AssAlg /\ N e. NN0 /\ X e. K ) -> N e. ZZ )
26 3 5 24 25 8 mulgcld 
 |-  ( ( W e. AssAlg /\ N e. NN0 /\ X e. K ) -> ( N .* X ) e. K )
27 1 2 3 16 12 asclval 
 |-  ( ( N .* X ) e. K -> ( A ` ( N .* X ) ) = ( ( N .* X ) ( .s ` W ) ( 1r ` W ) ) )
28 26 27 syl 
 |-  ( ( W e. AssAlg /\ N e. NN0 /\ X e. K ) -> ( A ` ( N .* X ) ) = ( ( N .* X ) ( .s ` W ) ( 1r ` W ) ) )
29 18 21 28 3eqtr4rd 
 |-  ( ( W e. AssAlg /\ N e. NN0 /\ X e. K ) -> ( A ` ( N .* X ) ) = ( N .^ ( A ` X ) ) )