Metamath Proof Explorer

Theorem isassad

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

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