Metamath Proof Explorer


Theorem isassa

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 · ˙ = W
isassa.t × ˙ = W
Assertion isassa W AssAlg W LMod W Ring F CRing r B x V y V r · ˙ x × ˙ y = r · ˙ x × ˙ y x × ˙ r · ˙ y = r · ˙ 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 fvexd w = W Scalar w V
7 fveq2 w = W Scalar w = Scalar W
8 7 2 eqtr4di w = W Scalar w = F
9 simpr w = W f = F f = F
10 9 eleq1d w = W f = F f CRing F CRing
11 9 fveq2d w = W f = F Base f = Base F
12 11 3 eqtr4di w = W f = F Base f = B
13 fveq2 w = W Base w = Base W
14 13 1 eqtr4di w = W Base w = V
15 fvexd w = W w V
16 fvexd w = W s = w w V
17 simpr w = W s = w t = w t = w
18 fveq2 w = W w = W
19 18 ad2antrr w = W s = w t = w w = W
20 19 5 eqtr4di w = W s = w t = w w = × ˙
21 17 20 eqtrd w = W s = w t = w t = × ˙
22 simplr w = W s = w t = w s = w
23 fveq2 w = W w = W
24 23 ad2antrr w = W s = w t = w w = W
25 24 4 eqtr4di w = W s = w t = w w = · ˙
26 22 25 eqtrd w = W s = w t = w s = · ˙
27 26 oveqd w = W s = w t = w r s x = r · ˙ x
28 eqidd w = W s = w t = w y = y
29 21 27 28 oveq123d w = W s = w t = w r s x t y = r · ˙ x × ˙ y
30 eqidd w = W s = w t = w r = r
31 21 oveqd w = W s = w t = w x t y = x × ˙ y
32 26 30 31 oveq123d w = W s = w t = w r s x t y = r · ˙ x × ˙ y
33 29 32 eqeq12d w = W s = w t = w r s x t y = r s x t y r · ˙ x × ˙ y = r · ˙ x × ˙ y
34 eqidd w = W s = w t = w x = x
35 26 oveqd w = W s = w t = w r s y = r · ˙ y
36 21 34 35 oveq123d w = W s = w t = w x t r s y = x × ˙ r · ˙ y
37 36 32 eqeq12d w = W s = w t = w x t r s y = r s x t y x × ˙ r · ˙ y = r · ˙ x × ˙ y
38 33 37 anbi12d w = W s = w t = w r s x t y = r s x t y x t r s y = r s x t y r · ˙ x × ˙ y = r · ˙ x × ˙ y x × ˙ r · ˙ y = r · ˙ x × ˙ y
39 16 38 sbcied w = W s = w [˙ w / t]˙ r s x t y = r s x t y x t r s y = r s x t y r · ˙ x × ˙ y = r · ˙ x × ˙ y x × ˙ r · ˙ y = r · ˙ x × ˙ y
40 15 39 sbcied w = W [˙ w / s]˙ [˙ w / t]˙ r s x t y = r s x t y x t r s y = r s x t y r · ˙ x × ˙ y = r · ˙ x × ˙ y x × ˙ r · ˙ y = r · ˙ x × ˙ y
41 14 40 raleqbidv w = W y Base w [˙ w / s]˙ [˙ w / t]˙ r s x t y = r s x t y x t r s y = r s x t y y V r · ˙ x × ˙ y = r · ˙ x × ˙ y x × ˙ r · ˙ y = r · ˙ x × ˙ y
42 14 41 raleqbidv w = W x Base w y Base w [˙ w / s]˙ [˙ w / t]˙ r s x t y = r s x t y x t r s y = r s x t y x V y V r · ˙ x × ˙ y = r · ˙ x × ˙ y x × ˙ r · ˙ y = r · ˙ x × ˙ y
43 42 adantr w = W f = F x Base w y Base w [˙ w / s]˙ [˙ w / t]˙ r s x t y = r s x t y x t r s y = r s x t y x V y V r · ˙ x × ˙ y = r · ˙ x × ˙ y x × ˙ r · ˙ y = r · ˙ x × ˙ y
44 12 43 raleqbidv w = W f = F r Base f x Base w y Base w [˙ w / s]˙ [˙ w / t]˙ r s x t y = r s x t y x t r s y = r s x t y r B x V y V r · ˙ x × ˙ y = r · ˙ x × ˙ y x × ˙ r · ˙ y = r · ˙ x × ˙ y
45 10 44 anbi12d w = W f = F f CRing r Base f x Base w y Base w [˙ w / s]˙ [˙ w / t]˙ r s x t y = r s x t y x t r s y = r s x t y F CRing r B x V y V r · ˙ x × ˙ y = r · ˙ x × ˙ y x × ˙ r · ˙ y = r · ˙ x × ˙ y
46 6 8 45 sbcied2 w = W [˙ Scalar w / f]˙ f CRing r Base f x Base w y Base w [˙ w / s]˙ [˙ w / t]˙ r s x t y = r s x t y x t r s y = r s x t y F CRing r B x V y V r · ˙ x × ˙ y = r · ˙ x × ˙ y x × ˙ r · ˙ y = r · ˙ x × ˙ y
47 df-assa AssAlg = w LMod Ring | [˙ Scalar w / f]˙ f CRing r Base f x Base w y Base w [˙ w / s]˙ [˙ w / t]˙ r s x t y = r s x t y x t r s y = r s x t y
48 46 47 elrab2 W AssAlg W LMod Ring F CRing r B x V y V r · ˙ x × ˙ y = r · ˙ x × ˙ y x × ˙ r · ˙ y = r · ˙ x × ˙ y
49 anass W LMod Ring F CRing r B x V y V r · ˙ x × ˙ y = r · ˙ x × ˙ y x × ˙ r · ˙ y = r · ˙ x × ˙ y W LMod Ring F CRing r B x V y V r · ˙ x × ˙ y = r · ˙ x × ˙ y x × ˙ r · ˙ y = r · ˙ x × ˙ y
50 elin W LMod Ring W LMod W Ring
51 50 anbi1i W LMod Ring F CRing W LMod W Ring F CRing
52 df-3an W LMod W Ring F CRing W LMod W Ring F CRing
53 51 52 bitr4i W LMod Ring F CRing W LMod W Ring F CRing
54 53 anbi1i W LMod Ring F CRing r B x V y V r · ˙ x × ˙ y = r · ˙ x × ˙ y x × ˙ r · ˙ y = r · ˙ x × ˙ y W LMod W Ring F CRing r B x V y V r · ˙ x × ˙ y = r · ˙ x × ˙ y x × ˙ r · ˙ y = r · ˙ x × ˙ y
55 48 49 54 3bitr2i W AssAlg W LMod W Ring F CRing r B x V y V r · ˙ x × ˙ y = r · ˙ x × ˙ y x × ˙ r · ˙ y = r · ˙ x × ˙ y