Metamath Proof Explorer

Theorem assamulgscm

Description: Exponentiation of a scalar multiplication in an associative algebra: ( a .x. X ) ^ N = ( a ^ N ) .X. ( X ^ N ) . (Contributed by AV, 26-Aug-2019)

Ref Expression
Hypotheses assamulgscm.v 
|- V = ( Base ` W )
assamulgscm.f 
|- F = ( Scalar ` W )
assamulgscm.b 
|- B = ( Base ` F )
assamulgscm.s 
|- .x. = ( .s ` W )
assamulgscm.g 
|- G = ( mulGrp ` F )
assamulgscm.p 
|- .^ = ( .g ` G )
assamulgscm.h 
|- H = ( mulGrp ` W )
assamulgscm.e 
|- E = ( .g ` H )
Assertion assamulgscm 
|- ( ( W e. AssAlg /\ ( N e. NN0 /\ A e. B /\ X e. V ) ) -> ( N E ( A .x. X ) ) = ( ( N .^ A ) .x. ( N E X ) ) )

Proof

Step Hyp Ref Expression
1 assamulgscm.v 
 |-  V = ( Base ` W )
2 assamulgscm.f 
 |-  F = ( Scalar ` W )
3 assamulgscm.b 
 |-  B = ( Base ` F )
4 assamulgscm.s 
 |-  .x. = ( .s ` W )
5 assamulgscm.g 
 |-  G = ( mulGrp ` F )
6 assamulgscm.p 
 |-  .^ = ( .g ` G )
7 assamulgscm.h 
 |-  H = ( mulGrp ` W )
8 assamulgscm.e 
 |-  E = ( .g ` H )
9 oveq1 
 |-  ( x = 0 -> ( x E ( A .x. X ) ) = ( 0 E ( A .x. X ) ) )
10 oveq1 
 |-  ( x = 0 -> ( x .^ A ) = ( 0 .^ A ) )
11 oveq1 
 |-  ( x = 0 -> ( x E X ) = ( 0 E X ) )
12 10 11 oveq12d 
 |-  ( x = 0 -> ( ( x .^ A ) .x. ( x E X ) ) = ( ( 0 .^ A ) .x. ( 0 E X ) ) )
13 9 12 eqeq12d 
 |-  ( x = 0 -> ( ( x E ( A .x. X ) ) = ( ( x .^ A ) .x. ( x E X ) ) <-> ( 0 E ( A .x. X ) ) = ( ( 0 .^ A ) .x. ( 0 E X ) ) ) )
14 13 imbi2d 
 |-  ( x = 0 -> ( ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( x E ( A .x. X ) ) = ( ( x .^ A ) .x. ( x E X ) ) ) <-> ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( 0 E ( A .x. X ) ) = ( ( 0 .^ A ) .x. ( 0 E X ) ) ) ) )
15 oveq1 
 |-  ( x = y -> ( x E ( A .x. X ) ) = ( y E ( A .x. X ) ) )
16 oveq1 
 |-  ( x = y -> ( x .^ A ) = ( y .^ A ) )
17 oveq1 
 |-  ( x = y -> ( x E X ) = ( y E X ) )
18 16 17 oveq12d 
 |-  ( x = y -> ( ( x .^ A ) .x. ( x E X ) ) = ( ( y .^ A ) .x. ( y E X ) ) )
19 15 18 eqeq12d 
 |-  ( x = y -> ( ( x E ( A .x. X ) ) = ( ( x .^ A ) .x. ( x E X ) ) <-> ( y E ( A .x. X ) ) = ( ( y .^ A ) .x. ( y E X ) ) ) )
20 19 imbi2d 
 |-  ( x = y -> ( ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( x E ( A .x. X ) ) = ( ( x .^ A ) .x. ( x E X ) ) ) <-> ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( y E ( A .x. X ) ) = ( ( y .^ A ) .x. ( y E X ) ) ) ) )
21 oveq1 
 |-  ( x = ( y + 1 ) -> ( x E ( A .x. X ) ) = ( ( y + 1 ) E ( A .x. X ) ) )
22 oveq1 
 |-  ( x = ( y + 1 ) -> ( x .^ A ) = ( ( y + 1 ) .^ A ) )
23 oveq1 
 |-  ( x = ( y + 1 ) -> ( x E X ) = ( ( y + 1 ) E X ) )
24 22 23 oveq12d 
 |-  ( x = ( y + 1 ) -> ( ( x .^ A ) .x. ( x E X ) ) = ( ( ( y + 1 ) .^ A ) .x. ( ( y + 1 ) E X ) ) )
25 21 24 eqeq12d 
 |-  ( x = ( y + 1 ) -> ( ( x E ( A .x. X ) ) = ( ( x .^ A ) .x. ( x E X ) ) <-> ( ( y + 1 ) E ( A .x. X ) ) = ( ( ( y + 1 ) .^ A ) .x. ( ( y + 1 ) E X ) ) ) )
26 25 imbi2d 
 |-  ( x = ( y + 1 ) -> ( ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( x E ( A .x. X ) ) = ( ( x .^ A ) .x. ( x E X ) ) ) <-> ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( ( y + 1 ) E ( A .x. X ) ) = ( ( ( y + 1 ) .^ A ) .x. ( ( y + 1 ) E X ) ) ) ) )
27 oveq1 
 |-  ( x = N -> ( x E ( A .x. X ) ) = ( N E ( A .x. X ) ) )
28 oveq1 
 |-  ( x = N -> ( x .^ A ) = ( N .^ A ) )
29 oveq1 
 |-  ( x = N -> ( x E X ) = ( N E X ) )
30 28 29 oveq12d 
 |-  ( x = N -> ( ( x .^ A ) .x. ( x E X ) ) = ( ( N .^ A ) .x. ( N E X ) ) )
31 27 30 eqeq12d 
 |-  ( x = N -> ( ( x E ( A .x. X ) ) = ( ( x .^ A ) .x. ( x E X ) ) <-> ( N E ( A .x. X ) ) = ( ( N .^ A ) .x. ( N E X ) ) ) )
32 31 imbi2d 
 |-  ( x = N -> ( ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( x E ( A .x. X ) ) = ( ( x .^ A ) .x. ( x E X ) ) ) <-> ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( N E ( A .x. X ) ) = ( ( N .^ A ) .x. ( N E X ) ) ) ) )
33 1 2 3 4 5 6 7 8 assamulgscmlem1 
 |-  ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( 0 E ( A .x. X ) ) = ( ( 0 .^ A ) .x. ( 0 E X ) ) )
34 1 2 3 4 5 6 7 8 assamulgscmlem2 
 |-  ( y e. NN0 -> ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( ( y E ( A .x. X ) ) = ( ( y .^ A ) .x. ( y E X ) ) -> ( ( y + 1 ) E ( A .x. X ) ) = ( ( ( y + 1 ) .^ A ) .x. ( ( y + 1 ) E X ) ) ) ) )
35 34 a2d 
 |-  ( y e. NN0 -> ( ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( y E ( A .x. X ) ) = ( ( y .^ A ) .x. ( y E X ) ) ) -> ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( ( y + 1 ) E ( A .x. X ) ) = ( ( ( y + 1 ) .^ A ) .x. ( ( y + 1 ) E X ) ) ) ) )
36 14 20 26 32 33 35 nn0ind 
 |-  ( N e. NN0 -> ( ( ( A e. B /\ X e. V ) /\ W e. AssAlg ) -> ( N E ( A .x. X ) ) = ( ( N .^ A ) .x. ( N E X ) ) ) )
37 36 exp4c 
 |-  ( N e. NN0 -> ( A e. B -> ( X e. V -> ( W e. AssAlg -> ( N E ( A .x. X ) ) = ( ( N .^ A ) .x. ( N E X ) ) ) ) ) )
38 37 3imp 
 |-  ( ( N e. NN0 /\ A e. B /\ X e. V ) -> ( W e. AssAlg -> ( N E ( A .x. X ) ) = ( ( N .^ A ) .x. ( N E X ) ) ) )
39 38 impcom 
 |-  ( ( W e. AssAlg /\ ( N e. NN0 /\ A e. B /\ X e. V ) ) -> ( N E ( A .x. X ) ) = ( ( N .^ A ) .x. ( N E X ) ) )