Metamath Proof Explorer

Theorem assalem

Description: The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses isassa.v 
|- V = ( Base ` W )
isassa.f 
|- F = ( Scalar ` W )
isassa.b 
|- B = ( Base ` F )
isassa.s 
|- .x. = ( .s ` W )
isassa.t 
|- .X. = ( .r ` W )
Assertion assalem 
|- ( ( W e. AssAlg /\ ( A e. B /\ X e. V /\ Y e. V ) ) -> ( ( ( A .x. X ) .X. Y ) = ( A .x. ( X .X. Y ) ) /\ ( X .X. ( A .x. Y ) ) = ( A .x. ( X .X. Y ) ) ) )

Proof

Step Hyp Ref Expression
1 isassa.v 
 |-  V = ( Base ` W )
2 isassa.f 
 |-  F = ( Scalar ` W )
3 isassa.b 
 |-  B = ( Base ` F )
4 isassa.s 
 |-  .x. = ( .s ` W )
5 isassa.t 
 |-  .X. = ( .r ` W )
6 1 2 3 4 5 isassa 
 |-  ( W e. AssAlg <-> ( ( W e. LMod /\ W e. Ring /\ F e. CRing ) /\ A. r e. B A. x e. V A. y e. V ( ( ( r .x. x ) .X. y ) = ( r .x. ( x .X. y ) ) /\ ( x .X. ( r .x. y ) ) = ( r .x. ( x .X. y ) ) ) ) )
7 6 simprbi 
 |-  ( W e. AssAlg -> A. r e. B A. x e. V A. y e. V ( ( ( r .x. x ) .X. y ) = ( r .x. ( x .X. y ) ) /\ ( x .X. ( r .x. y ) ) = ( r .x. ( x .X. y ) ) ) )
8 oveq1 
 |-  ( r = A -> ( r .x. x ) = ( A .x. x ) )
9 8 oveq1d 
 |-  ( r = A -> ( ( r .x. x ) .X. y ) = ( ( A .x. x ) .X. y ) )
10 oveq1 
 |-  ( r = A -> ( r .x. ( x .X. y ) ) = ( A .x. ( x .X. y ) ) )
11 9 10 eqeq12d 
 |-  ( r = A -> ( ( ( r .x. x ) .X. y ) = ( r .x. ( x .X. y ) ) <-> ( ( A .x. x ) .X. y ) = ( A .x. ( x .X. y ) ) ) )
12 oveq1 
 |-  ( r = A -> ( r .x. y ) = ( A .x. y ) )
13 12 oveq2d 
 |-  ( r = A -> ( x .X. ( r .x. y ) ) = ( x .X. ( A .x. y ) ) )
14 13 10 eqeq12d 
 |-  ( r = A -> ( ( x .X. ( r .x. y ) ) = ( r .x. ( x .X. y ) ) <-> ( x .X. ( A .x. y ) ) = ( A .x. ( x .X. y ) ) ) )
15 11 14 anbi12d 
 |-  ( r = A -> ( ( ( ( r .x. x ) .X. y ) = ( r .x. ( x .X. y ) ) /\ ( x .X. ( r .x. y ) ) = ( r .x. ( x .X. y ) ) ) <-> ( ( ( A .x. x ) .X. y ) = ( A .x. ( x .X. y ) ) /\ ( x .X. ( A .x. y ) ) = ( A .x. ( x .X. y ) ) ) ) )
16 oveq2 
 |-  ( x = X -> ( A .x. x ) = ( A .x. X ) )
17 16 oveq1d 
 |-  ( x = X -> ( ( A .x. x ) .X. y ) = ( ( A .x. X ) .X. y ) )
18 oveq1 
 |-  ( x = X -> ( x .X. y ) = ( X .X. y ) )
19 18 oveq2d 
 |-  ( x = X -> ( A .x. ( x .X. y ) ) = ( A .x. ( X .X. y ) ) )
20 17 19 eqeq12d 
 |-  ( x = X -> ( ( ( A .x. x ) .X. y ) = ( A .x. ( x .X. y ) ) <-> ( ( A .x. X ) .X. y ) = ( A .x. ( X .X. y ) ) ) )
21 oveq1 
 |-  ( x = X -> ( x .X. ( A .x. y ) ) = ( X .X. ( A .x. y ) ) )
22 21 19 eqeq12d 
 |-  ( x = X -> ( ( x .X. ( A .x. y ) ) = ( A .x. ( x .X. y ) ) <-> ( X .X. ( A .x. y ) ) = ( A .x. ( X .X. y ) ) ) )
23 20 22 anbi12d 
 |-  ( x = X -> ( ( ( ( A .x. x ) .X. y ) = ( A .x. ( x .X. y ) ) /\ ( x .X. ( A .x. y ) ) = ( A .x. ( x .X. y ) ) ) <-> ( ( ( A .x. X ) .X. y ) = ( A .x. ( X .X. y ) ) /\ ( X .X. ( A .x. y ) ) = ( A .x. ( X .X. y ) ) ) ) )
24 oveq2 
 |-  ( y = Y -> ( ( A .x. X ) .X. y ) = ( ( A .x. X ) .X. Y ) )
25 oveq2 
 |-  ( y = Y -> ( X .X. y ) = ( X .X. Y ) )
26 25 oveq2d 
 |-  ( y = Y -> ( A .x. ( X .X. y ) ) = ( A .x. ( X .X. Y ) ) )
27 24 26 eqeq12d 
 |-  ( y = Y -> ( ( ( A .x. X ) .X. y ) = ( A .x. ( X .X. y ) ) <-> ( ( A .x. X ) .X. Y ) = ( A .x. ( X .X. Y ) ) ) )
28 oveq2 
 |-  ( y = Y -> ( A .x. y ) = ( A .x. Y ) )
29 28 oveq2d 
 |-  ( y = Y -> ( X .X. ( A .x. y ) ) = ( X .X. ( A .x. Y ) ) )
30 29 26 eqeq12d 
 |-  ( y = Y -> ( ( X .X. ( A .x. y ) ) = ( A .x. ( X .X. y ) ) <-> ( X .X. ( A .x. Y ) ) = ( A .x. ( X .X. Y ) ) ) )
31 27 30 anbi12d 
 |-  ( y = Y -> ( ( ( ( A .x. X ) .X. y ) = ( A .x. ( X .X. y ) ) /\ ( X .X. ( A .x. y ) ) = ( A .x. ( X .X. y ) ) ) <-> ( ( ( A .x. X ) .X. Y ) = ( A .x. ( X .X. Y ) ) /\ ( X .X. ( A .x. Y ) ) = ( A .x. ( X .X. Y ) ) ) ) )
32 15 23 31 rspc3v 
 |-  ( ( A e. B /\ X e. V /\ Y e. V ) -> ( A. r e. B A. x e. V A. y e. V ( ( ( r .x. x ) .X. y ) = ( r .x. ( x .X. y ) ) /\ ( x .X. ( r .x. y ) ) = ( r .x. ( x .X. y ) ) ) -> ( ( ( A .x. X ) .X. Y ) = ( A .x. ( X .X. Y ) ) /\ ( X .X. ( A .x. Y ) ) = ( A .x. ( X .X. Y ) ) ) ) )
33 7 32 mpan9 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ X e. V /\ Y e. V ) ) -> ( ( ( A .x. X ) .X. Y ) = ( A .x. ( X .X. Y ) ) /\ ( X .X. ( A .x. Y ) ) = ( A .x. ( X .X. Y ) ) ) )