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 
|- ( ph -> V = ( Base ` W ) )
isassad.f 
|- ( ph -> F = ( Scalar ` W ) )
isassad.b 
|- ( ph -> B = ( Base ` F ) )
isassad.s 
|- ( ph -> .x. = ( .s ` W ) )
isassad.t 
|- ( ph -> .X. = ( .r ` W ) )
isassad.1 
|- ( ph -> W e. LMod )
isassad.2 
|- ( ph -> W e. Ring )
isassad.4 
|- ( ( ph /\ ( r e. B /\ x e. V /\ y e. V ) ) -> ( ( r .x. x ) .X. y ) = ( r .x. ( x .X. y ) ) )
isassad.5 
|- ( ( ph /\ ( r e. B /\ x e. V /\ y e. V ) ) -> ( x .X. ( r .x. y ) ) = ( r .x. ( x .X. y ) ) )
Assertion isassad 
|- ( ph -> W e. AssAlg )

Proof

Step Hyp Ref Expression
1 isassad.v 
 |-  ( ph -> V = ( Base ` W ) )
2 isassad.f 
 |-  ( ph -> F = ( Scalar ` W ) )
3 isassad.b 
 |-  ( ph -> B = ( Base ` F ) )
4 isassad.s 
 |-  ( ph -> .x. = ( .s ` W ) )
5 isassad.t 
 |-  ( ph -> .X. = ( .r ` W ) )
6 isassad.1 
 |-  ( ph -> W e. LMod )
7 isassad.2 
 |-  ( ph -> W e. Ring )
8 isassad.4 
 |-  ( ( ph /\ ( r e. B /\ x e. V /\ y e. V ) ) -> ( ( r .x. x ) .X. y ) = ( r .x. ( x .X. y ) ) )
9 isassad.5 
 |-  ( ( ph /\ ( r e. B /\ x e. V /\ y e. V ) ) -> ( x .X. ( r .x. y ) ) = ( r .x. ( x .X. y ) ) )
10 6 7 jca 
 |-  ( ph -> ( W e. LMod /\ W e. Ring ) )
11 8 9 jca 
 |-  ( ( ph /\ ( r e. B /\ x e. V /\ y e. V ) ) -> ( ( ( r .x. x ) .X. y ) = ( r .x. ( x .X. y ) ) /\ ( x .X. ( r .x. y ) ) = ( r .x. ( x .X. y ) ) ) )
12 11 ralrimivvva 
 |-  ( ph -> 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 ) ) ) )
13 2 fveq2d 
 |-  ( ph -> ( Base ` F ) = ( Base ` ( Scalar ` W ) ) )
14 3 13 eqtrd 
 |-  ( ph -> B = ( Base ` ( Scalar ` W ) ) )
15 4 oveqd 
 |-  ( ph -> ( r .x. x ) = ( r ( .s ` W ) x ) )
16 eqidd 
 |-  ( ph -> y = y )
17 5 15 16 oveq123d 
 |-  ( ph -> ( ( r .x. x ) .X. y ) = ( ( r ( .s ` W ) x ) ( .r ` W ) y ) )
18 eqidd 
 |-  ( ph -> r = r )
19 5 oveqd 
 |-  ( ph -> ( x .X. y ) = ( x ( .r ` W ) y ) )
20 4 18 19 oveq123d 
 |-  ( ph -> ( r .x. ( x .X. y ) ) = ( r ( .s ` W ) ( x ( .r ` W ) y ) ) )
21 17 20 eqeq12d 
 |-  ( ph -> ( ( ( r .x. x ) .X. y ) = ( r .x. ( x .X. y ) ) <-> ( ( r ( .s ` W ) x ) ( .r ` W ) y ) = ( r ( .s ` W ) ( x ( .r ` W ) y ) ) ) )
22 eqidd 
 |-  ( ph -> x = x )
23 4 oveqd 
 |-  ( ph -> ( r .x. y ) = ( r ( .s ` W ) y ) )
24 5 22 23 oveq123d 
 |-  ( ph -> ( x .X. ( r .x. y ) ) = ( x ( .r ` W ) ( r ( .s ` W ) y ) ) )
25 24 20 eqeq12d 
 |-  ( ph -> ( ( x .X. ( r .x. y ) ) = ( r .x. ( x .X. y ) ) <-> ( x ( .r ` W ) ( r ( .s ` W ) y ) ) = ( r ( .s ` W ) ( x ( .r ` W ) y ) ) ) )
26 21 25 anbi12d 
 |-  ( ph -> ( ( ( ( r .x. x ) .X. y ) = ( r .x. ( x .X. y ) ) /\ ( x .X. ( r .x. y ) ) = ( r .x. ( x .X. y ) ) ) <-> ( ( ( r ( .s ` W ) x ) ( .r ` W ) y ) = ( r ( .s ` W ) ( x ( .r ` W ) y ) ) /\ ( x ( .r ` W ) ( r ( .s ` W ) y ) ) = ( r ( .s ` W ) ( x ( .r ` W ) y ) ) ) ) )
27 1 26 raleqbidv 
 |-  ( ph -> ( A. y e. V ( ( ( r .x. x ) .X. y ) = ( r .x. ( x .X. y ) ) /\ ( x .X. ( r .x. y ) ) = ( r .x. ( x .X. y ) ) ) <-> A. y e. ( Base ` W ) ( ( ( r ( .s ` W ) x ) ( .r ` W ) y ) = ( r ( .s ` W ) ( x ( .r ` W ) y ) ) /\ ( x ( .r ` W ) ( r ( .s ` W ) y ) ) = ( r ( .s ` W ) ( x ( .r ` W ) y ) ) ) ) )
28 1 27 raleqbidv 
 |-  ( ph -> ( 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 ) ) ) <-> A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( ( ( r ( .s ` W ) x ) ( .r ` W ) y ) = ( r ( .s ` W ) ( x ( .r ` W ) y ) ) /\ ( x ( .r ` W ) ( r ( .s ` W ) y ) ) = ( r ( .s ` W ) ( x ( .r ` W ) y ) ) ) ) )
29 14 28 raleqbidv 
 |-  ( ph -> ( 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 ) ) ) <-> A. r e. ( Base ` ( Scalar ` W ) ) A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( ( ( r ( .s ` W ) x ) ( .r ` W ) y ) = ( r ( .s ` W ) ( x ( .r ` W ) y ) ) /\ ( x ( .r ` W ) ( r ( .s ` W ) y ) ) = ( r ( .s ` W ) ( x ( .r ` W ) y ) ) ) ) )
30 12 29 mpbid 
 |-  ( ph -> A. r e. ( Base ` ( Scalar ` W ) ) A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( ( ( r ( .s ` W ) x ) ( .r ` W ) y ) = ( r ( .s ` W ) ( x ( .r ` W ) y ) ) /\ ( x ( .r ` W ) ( r ( .s ` W ) y ) ) = ( r ( .s ` W ) ( x ( .r ` W ) y ) ) ) )
31 eqid 
 |-  ( Base ` W ) = ( Base ` W )
32 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
33 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
34 eqid 
 |-  ( .s ` W ) = ( .s ` W )
35 eqid 
 |-  ( .r ` W ) = ( .r ` W )
36 31 32 33 34 35 isassa 
 |-  ( W e. AssAlg <-> ( ( W e. LMod /\ W e. Ring ) /\ A. r e. ( Base ` ( Scalar ` W ) ) A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( ( ( r ( .s ` W ) x ) ( .r ` W ) y ) = ( r ( .s ` W ) ( x ( .r ` W ) y ) ) /\ ( x ( .r ` W ) ( r ( .s ` W ) y ) ) = ( r ( .s ` W ) ( x ( .r ` W ) y ) ) ) ) )
37 10 30 36 sylanbrc 
 |-  ( ph -> W e. AssAlg )