Metamath Proof Explorer

Theorem isassa

Description: The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014) (Revised by SN, 2-Mar-2025)

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 ) /\ 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 fveq2 
 |-  ( f = F -> ( Base ` f ) = ( Base ` F ) )
10 9 3 eqtr4di 
 |-  ( f = F -> ( Base ` f ) = B )
11 10 adantl 
 |-  ( ( w = W /\ f = F ) -> ( Base ` f ) = B )
12 fveq2 
 |-  ( w = W -> ( Base ` w ) = ( Base ` W ) )
13 12 1 eqtr4di 
 |-  ( w = W -> ( Base ` w ) = V )
14 simpr 
 |-  ( ( s = .x. /\ t = .X. ) -> t = .X. )
15 simpl 
 |-  ( ( s = .x. /\ t = .X. ) -> s = .x. )
16 15 oveqd 
 |-  ( ( s = .x. /\ t = .X. ) -> ( r s x ) = ( r .x. x ) )
17 eqidd 
 |-  ( ( s = .x. /\ t = .X. ) -> y = y )
18 14 16 17 oveq123d 
 |-  ( ( s = .x. /\ t = .X. ) -> ( ( r s x ) t y ) = ( ( r .x. x ) .X. y ) )
19 eqidd 
 |-  ( ( s = .x. /\ t = .X. ) -> r = r )
20 14 oveqd 
 |-  ( ( s = .x. /\ t = .X. ) -> ( x t y ) = ( x .X. y ) )
21 15 19 20 oveq123d 
 |-  ( ( s = .x. /\ t = .X. ) -> ( r s ( x t y ) ) = ( r .x. ( x .X. y ) ) )
22 18 21 eqeq12d 
 |-  ( ( s = .x. /\ t = .X. ) -> ( ( ( r s x ) t y ) = ( r s ( x t y ) ) <-> ( ( r .x. x ) .X. y ) = ( r .x. ( x .X. y ) ) ) )
23 eqidd 
 |-  ( ( s = .x. /\ t = .X. ) -> x = x )
24 15 oveqd 
 |-  ( ( s = .x. /\ t = .X. ) -> ( r s y ) = ( r .x. y ) )
25 14 23 24 oveq123d 
 |-  ( ( s = .x. /\ t = .X. ) -> ( x t ( r s y ) ) = ( x .X. ( r .x. y ) ) )
26 25 21 eqeq12d 
 |-  ( ( s = .x. /\ t = .X. ) -> ( ( x t ( r s y ) ) = ( r s ( x t y ) ) <-> ( x .X. ( r .x. y ) ) = ( r .x. ( x .X. y ) ) ) )
27 22 26 anbi12d 
 |-  ( ( s = .x. /\ t = .X. ) -> ( ( ( ( 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 ) ) ) ) )
28 4 5 27 sbcie2s 
 |-  ( 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 ) ) ) ) )
29 13 28 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 ) ) ) ) )
30 13 29 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 ) ) ) ) )
31 30 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 ) ) ) ) )
32 11 31 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 ) ) ) ) )
33 6 8 32 sbcied2 
 |-  ( w = W -> ( [. ( Scalar ` w ) / 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 ) ) ) ) )
34 df-assa 
 |-  AssAlg = { w e. ( LMod i^i Ring ) | [. ( Scalar ` w ) / 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 ) ) ) }
35 33 34 elrab2 
 |-  ( W e. AssAlg <-> ( W e. ( LMod i^i Ring ) /\ 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 ) ) ) ) )
36 elin 
 |-  ( W e. ( LMod i^i Ring ) <-> ( W e. LMod /\ W e. Ring ) )
37 36 anbi1i 
 |-  ( ( W e. ( LMod i^i Ring ) /\ 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 ) /\ 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 ) ) ) ) )
38 35 37 bitri 
 |-  ( W e. AssAlg <-> ( ( W e. LMod /\ W e. Ring ) /\ 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 ) ) ) ) )