Metamath Proof Explorer


Theorem isassad

Description: Sufficient condition for being an associative algebra. (Contributed by Mario Carneiro, 5-Dec-2014) (Revised by SN, 2-Mar-2025)

Ref Expression
Hypotheses isassad.v φ V = Base W
isassad.f φ F = Scalar W
isassad.b φ B = Base F
isassad.s φ · ˙ = W
isassad.t φ × ˙ = W
isassad.1 φ W LMod
isassad.2 φ W Ring
isassad.4 φ r B x V y V r · ˙ x × ˙ y = r · ˙ x × ˙ y
isassad.5 φ r B x V y V x × ˙ r · ˙ y = r · ˙ x × ˙ y
Assertion isassad φ W AssAlg

Proof

Step Hyp Ref Expression
1 isassad.v φ V = Base W
2 isassad.f φ F = Scalar W
3 isassad.b φ B = Base F
4 isassad.s φ · ˙ = W
5 isassad.t φ × ˙ = W
6 isassad.1 φ W LMod
7 isassad.2 φ W Ring
8 isassad.4 φ r B x V y V r · ˙ x × ˙ y = r · ˙ x × ˙ y
9 isassad.5 φ r B x V y V x × ˙ r · ˙ y = r · ˙ x × ˙ y
10 6 7 jca φ W LMod W Ring
11 8 9 jca φ r B x V y V r · ˙ x × ˙ y = r · ˙ x × ˙ y x × ˙ r · ˙ y = r · ˙ x × ˙ y
12 11 ralrimivvva φ r B x V y V r · ˙ x × ˙ y = r · ˙ x × ˙ y x × ˙ r · ˙ y = r · ˙ x × ˙ y
13 2 fveq2d φ Base F = Base Scalar W
14 3 13 eqtrd φ B = Base Scalar W
15 4 oveqd φ r · ˙ x = r W x
16 eqidd φ y = y
17 5 15 16 oveq123d φ r · ˙ x × ˙ y = r W x W y
18 eqidd φ r = r
19 5 oveqd φ x × ˙ y = x W y
20 4 18 19 oveq123d φ r · ˙ x × ˙ y = r W x W y
21 17 20 eqeq12d φ r · ˙ x × ˙ y = r · ˙ x × ˙ y r W x W y = r W x W y
22 eqidd φ x = x
23 4 oveqd φ r · ˙ y = r W y
24 5 22 23 oveq123d φ x × ˙ r · ˙ y = x W r W y
25 24 20 eqeq12d φ x × ˙ r · ˙ y = r · ˙ x × ˙ y x W r W y = r W x W y
26 21 25 anbi12d φ r · ˙ x × ˙ y = r · ˙ x × ˙ y x × ˙ r · ˙ y = r · ˙ x × ˙ y r W x W y = r W x W y x W r W y = r W x W y
27 1 26 raleqbidv φ y V r · ˙ x × ˙ y = r · ˙ x × ˙ y x × ˙ r · ˙ y = r · ˙ x × ˙ y y Base W r W x W y = r W x W y x W r W y = r W x W y
28 1 27 raleqbidv φ x V y V r · ˙ x × ˙ y = r · ˙ x × ˙ y x × ˙ r · ˙ y = r · ˙ x × ˙ y x Base W y Base W r W x W y = r W x W y x W r W y = r W x W y
29 14 28 raleqbidv φ r B x V y V r · ˙ x × ˙ y = r · ˙ x × ˙ y x × ˙ r · ˙ y = r · ˙ x × ˙ y r Base Scalar W x Base W y Base W r W x W y = r W x W y x W r W y = r W x W y
30 12 29 mpbid φ r Base Scalar W x Base W y Base W r W x W y = r W x W y x W r W y = r W x W y
31 eqid Base W = Base W
32 eqid Scalar W = Scalar W
33 eqid Base Scalar W = Base Scalar W
34 eqid W = W
35 eqid W = W
36 31 32 33 34 35 isassa W AssAlg W LMod W Ring r Base Scalar W x Base W y Base W r W x W y = r W x W y x W r W y = r W x W y
37 10 30 36 sylanbrc φ W AssAlg