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 
|- .x. = ( .s ` W )
isassa.t 
|- .X. = ( .r ` W )
Assertion 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 ) ) ) ) )

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 fvexd 
 |-  ( w = W -> ( Scalar ` w ) e. _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 e. CRing <-> F e. 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 -> ( .s ` w ) e. _V )
16 fvexd 
 |-  ( ( w = W /\ s = ( .s ` w ) ) -> ( .r ` w ) e. _V )
17 simpr 
 |-  ( ( ( w = W /\ s = ( .s ` w ) ) /\ t = ( .r ` w ) ) -> t = ( .r ` w ) )
18 fveq2 
 |-  ( w = W -> ( .r ` w ) = ( .r ` W ) )
19 18 ad2antrr 
 |-  ( ( ( w = W /\ s = ( .s ` w ) ) /\ t = ( .r ` w ) ) -> ( .r ` w ) = ( .r ` W ) )
20 19 5 eqtr4di 
 |-  ( ( ( w = W /\ s = ( .s ` w ) ) /\ t = ( .r ` w ) ) -> ( .r ` w ) = .X. )
21 17 20 eqtrd 
 |-  ( ( ( w = W /\ s = ( .s ` w ) ) /\ t = ( .r ` w ) ) -> t = .X. )
22 simplr 
 |-  ( ( ( w = W /\ s = ( .s ` w ) ) /\ t = ( .r ` w ) ) -> s = ( .s ` w ) )
23 fveq2 
 |-  ( w = W -> ( .s ` w ) = ( .s ` W ) )
24 23 ad2antrr 
 |-  ( ( ( w = W /\ s = ( .s ` w ) ) /\ t = ( .r ` w ) ) -> ( .s ` w ) = ( .s ` W ) )
25 24 4 eqtr4di 
 |-  ( ( ( w = W /\ s = ( .s ` w ) ) /\ t = ( .r ` w ) ) -> ( .s ` w ) = .x. )
26 22 25 eqtrd 
 |-  ( ( ( w = W /\ s = ( .s ` w ) ) /\ t = ( .r ` w ) ) -> s = .x. )
27 26 oveqd 
 |-  ( ( ( w = W /\ s = ( .s ` w ) ) /\ t = ( .r ` w ) ) -> ( r s x ) = ( r .x. x ) )
28 eqidd 
 |-  ( ( ( w = W /\ s = ( .s ` w ) ) /\ t = ( .r ` w ) ) -> y = y )
29 21 27 28 oveq123d 
 |-  ( ( ( w = W /\ s = ( .s ` w ) ) /\ t = ( .r ` w ) ) -> ( ( r s x ) t y ) = ( ( r .x. x ) .X. y ) )
30 eqidd 
 |-  ( ( ( w = W /\ s = ( .s ` w ) ) /\ t = ( .r ` w ) ) -> r = r )
31 21 oveqd 
 |-  ( ( ( w = W /\ s = ( .s ` w ) ) /\ t = ( .r ` w ) ) -> ( x t y ) = ( x .X. y ) )
32 26 30 31 oveq123d 
 |-  ( ( ( w = W /\ s = ( .s ` w ) ) /\ t = ( .r ` w ) ) -> ( r s ( x t y ) ) = ( r .x. ( x .X. y ) ) )
33 29 32 eqeq12d 
 |-  ( ( ( w = W /\ s = ( .s ` w ) ) /\ t = ( .r ` w ) ) -> ( ( ( r s x ) t y ) = ( r s ( x t y ) ) <-> ( ( r .x. x ) .X. y ) = ( r .x. ( x .X. y ) ) ) )
34 eqidd 
 |-  ( ( ( w = W /\ s = ( .s ` w ) ) /\ t = ( .r ` w ) ) -> x = x )
35 26 oveqd 
 |-  ( ( ( w = W /\ s = ( .s ` w ) ) /\ t = ( .r ` w ) ) -> ( r s y ) = ( r .x. y ) )
36 21 34 35 oveq123d 
 |-  ( ( ( w = W /\ s = ( .s ` w ) ) /\ t = ( .r ` w ) ) -> ( x t ( r s y ) ) = ( x .X. ( r .x. y ) ) )
37 36 32 eqeq12d 
 |-  ( ( ( w = W /\ s = ( .s ` w ) ) /\ t = ( .r ` w ) ) -> ( ( x t ( r s y ) ) = ( r s ( x t y ) ) <-> ( x .X. ( r .x. y ) ) = ( r .x. ( x .X. y ) ) ) )
38 33 37 anbi12d 
 |-  ( ( ( w = W /\ s = ( .s ` w ) ) /\ t = ( .r ` w ) ) -> ( ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) ) <-> ( ( ( r .x. x ) .X. y ) = ( r .x. ( x .X. y ) ) /\ ( x .X. ( r .x. y ) ) = ( r .x. ( x .X. y ) ) ) ) )
39 16 38 sbcied 
 |-  ( ( w = W /\ s = ( .s ` w ) ) -> ( [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) ) <-> ( ( ( r .x. x ) .X. y ) = ( r .x. ( x .X. y ) ) /\ ( x .X. ( r .x. y ) ) = ( r .x. ( x .X. y ) ) ) ) )
40 15 39 sbcied 
 |-  ( w = W -> ( [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) ) <-> ( ( ( r .x. x ) .X. y ) = ( r .x. ( x .X. y ) ) /\ ( x .X. ( r .x. y ) ) = ( r .x. ( x .X. y ) ) ) ) )
41 14 40 raleqbidv 
 |-  ( w = W -> ( A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) ) <-> A. y e. V ( ( ( r .x. x ) .X. y ) = ( r .x. ( x .X. y ) ) /\ ( x .X. ( r .x. y ) ) = ( r .x. ( x .X. y ) ) ) ) )
42 14 41 raleqbidv 
 |-  ( w = W -> ( A. x e. ( Base ` w ) A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) ) <-> 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 ) ) ) ) )
43 42 adantr 
 |-  ( ( w = W /\ f = F ) -> ( A. x e. ( Base ` w ) A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) ) <-> 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 ) ) ) ) )
44 12 43 raleqbidv 
 |-  ( ( w = W /\ f = F ) -> ( A. r e. ( Base ` f ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) ) <-> 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 ) ) ) ) )
45 10 44 anbi12d 
 |-  ( ( w = W /\ f = F ) -> ( ( f e. CRing /\ A. r e. ( Base ` f ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) ) ) <-> ( 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 ) ) ) ) ) )
46 6 8 45 sbcied2 
 |-  ( w = W -> ( [. ( Scalar ` w ) / f ]. ( f e. CRing /\ A. r e. ( Base ` f ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` w ) / t ]. ( ( ( r s x ) t y ) = ( r s ( x t y ) ) /\ ( x t ( r s y ) ) = ( r s ( x t y ) ) ) ) <-> ( 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 ) ) ) ) ) )
47 df-assa 
 |-  AssAlg = { w e. ( LMod i^i Ring ) | [. ( Scalar ` w ) / f ]. ( f e. CRing /\ A. r e. ( Base ` f ) A. x e. ( Base ` w ) A. y e. ( Base ` w ) [. ( .s ` w ) / s ]. [. ( .r ` 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 e. AssAlg <-> ( W e. ( LMod i^i 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 ) ) ) ) ) )
49 anass 
 |-  ( ( ( W e. ( LMod i^i 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 ) ) ) ) <-> ( W e. ( LMod i^i 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 ) ) ) ) ) )
50 elin 
 |-  ( W e. ( LMod i^i Ring ) <-> ( W e. LMod /\ W e. Ring ) )
51 50 anbi1i 
 |-  ( ( W e. ( LMod i^i Ring ) /\ F e. CRing ) <-> ( ( W e. LMod /\ W e. Ring ) /\ F e. CRing ) )
52 df-3an 
 |-  ( ( W e. LMod /\ W e. Ring /\ F e. CRing ) <-> ( ( W e. LMod /\ W e. Ring ) /\ F e. CRing ) )
53 51 52 bitr4i 
 |-  ( ( W e. ( LMod i^i Ring ) /\ F e. CRing ) <-> ( W e. LMod /\ W e. Ring /\ F e. CRing ) )
54 53 anbi1i 
 |-  ( ( ( W e. ( LMod i^i 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 ) ) ) ) <-> ( ( 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 ) ) ) ) )
55 48 49 54 3bitr2i 
 |-  ( 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 ) ) ) ) )