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 · ˙ = W
isassa.t × ˙ = W
Assertion assaass W AssAlg A B X V Y V A · ˙ X × ˙ Y = A · ˙ 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 · ˙ = W
5 isassa.t × ˙ = W
6 1 2 3 4 5 assalem W AssAlg A B X V Y V A · ˙ X × ˙ Y = A · ˙ X × ˙ Y X × ˙ A · ˙ Y = A · ˙ X × ˙ Y
7 6 simpld W AssAlg A B X V Y V A · ˙ X × ˙ Y = A · ˙ X × ˙ Y