Metamath Proof Explorer

Theorem assaass

Description: Left-associative property 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 assaass 
|- ( ( W e. AssAlg /\ ( A e. B /\ X e. V /\ Y e. V ) ) -> ( ( A .x. X ) .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 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 ) ) ) )
7 6 simpld 
 |-  ( ( W e. AssAlg /\ ( A e. B /\ X e. V /\ Y e. V ) ) -> ( ( A .x. X ) .X. Y ) = ( A .x. ( X .X. Y ) ) )