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 )