MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  assalem Structured version   Visualization version   Unicode version
Theorem assalem 19316
Description: The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.)
Hypotheses
Ref Expression
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
Ref Expression
assalem |- ( ( W e. AssAlg /\ ( A e. B /\ X e. V /\ Y e. V ) ) -> ( ( ( A .x. X ) .X. Y ) = ( A .x. ( X .X. Y ) ) /\ ( X .X. ( A .x. Y ) ) = ( A .x. ( X .X. Y ) ) ) )
Proof of Theorem assalem
Dummy variables x r y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isassa.v . . . 4 |- V = ( Base ` W )
2 isassa.f . . . 4 |- F = (Scalar ` W )
3 isassa.b . . . 4 |- B = ( Base ` F )
4 isassa.s . . . 4 |- .x. = ( .s ` W )
5 isassa.t . . . 4 |- .X. = ( .r ` W )
61, 2, 3, 4, 5isassa 19315 . . 3 |- ( 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 ) ) ) ) )
76simprbi 480 . 2 |- ( W e. AssAlg -> 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 ) ) ) )
8 oveq1 6657 . . . . . 6 |- ( r = A -> ( r .x. x ) = ( A .x. x ) )
98oveq1d 6665 . . . . 5 |- ( r = A -> ( ( r .x. x ) .X. y ) = ( ( A .x. x ) .X. y ) )
10 oveq1 6657 . . . . 5 |- ( r = A -> ( r .x. ( x .X. y ) ) = ( A .x. ( x .X. y ) ) )
119, 10eqeq12d 2637 . . . 4 |- ( r = A -> ( ( ( r .x. x ) .X. y ) = ( r .x. ( x .X. y ) ) <-> ( ( A .x. x ) .X. y ) = ( A .x. ( x .X. y ) ) ) )
12 oveq1 6657 . . . . . 6 |- ( r = A -> ( r .x. y ) = ( A .x. y ) )
1312oveq2d 6666 . . . . 5 |- ( r = A -> ( x .X. ( r .x. y ) ) = ( x .X. ( A .x. y ) ) )
1413, 10eqeq12d 2637 . . . 4 |- ( r = A -> ( ( x .X. ( r .x. y ) ) = ( r .x. ( x .X. y ) ) <-> ( x .X. ( A .x. y ) ) = ( A .x. ( x .X. y ) ) ) )
1511, 14anbi12d 747 . . 3 |- ( r = A -> ( ( ( ( r .x. x ) .X. y ) = ( r .x. ( x .X. y ) ) /\ ( x .X. ( r .x. y ) ) = ( r .x. ( x .X. y ) ) ) <-> ( ( ( A .x. x ) .X. y ) = ( A .x. ( x .X. y ) ) /\ ( x .X. ( A .x. y ) ) = ( A .x. ( x .X. y ) ) ) ) )
16 oveq2 6658 . . . . . 6 |- ( x = X -> ( A .x. x ) = ( A .x. X ) )
1716oveq1d 6665 . . . . 5 |- ( x = X -> ( ( A .x. x ) .X. y ) = ( ( A .x. X ) .X. y ) )
18 oveq1 6657 . . . . . 6 |- ( x = X -> ( x .X. y ) = ( X .X. y ) )
1918oveq2d 6666 . . . . 5 |- ( x = X -> ( A .x. ( x .X. y ) ) = ( A .x. ( X .X. y ) ) )
2017, 19eqeq12d 2637 . . . 4 |- ( x = X -> ( ( ( A .x. x ) .X. y ) = ( A .x. ( x .X. y ) ) <-> ( ( A .x. X ) .X. y ) = ( A .x. ( X .X. y ) ) ) )
21 oveq1 6657 . . . . 5 |- ( x = X -> ( x .X. ( A .x. y ) ) = ( X .X. ( A .x. y ) ) )
2221, 19eqeq12d 2637 . . . 4 |- ( x = X -> ( ( x .X. ( A .x. y ) ) = ( A .x. ( x .X. y ) ) <-> ( X .X. ( A .x. y ) ) = ( A .x. ( X .X. y ) ) ) )
2320, 22anbi12d 747 . . 3 |- ( x = X -> ( ( ( ( A .x. x ) .X. y ) = ( A .x. ( x .X. y ) ) /\ ( x .X. ( A .x. y ) ) = ( A .x. ( x .X. y ) ) ) <-> ( ( ( A .x. X ) .X. y ) = ( A .x. ( X .X. y ) ) /\ ( X .X. ( A .x. y ) ) = ( A .x. ( X .X. y ) ) ) ) )
24 oveq2 6658 . . . . 5 |- ( y = Y -> ( ( A .x. X ) .X. y ) = ( ( A .x. X ) .X. Y ) )
25 oveq2 6658 . . . . . 6 |- ( y = Y -> ( X .X. y ) = ( X .X. Y ) )
2625oveq2d 6666 . . . . 5 |- ( y = Y -> ( A .x. ( X .X. y ) ) = ( A .x. ( X .X. Y ) ) )
2724, 26eqeq12d 2637 . . . 4 |- ( y = Y -> ( ( ( A .x. X ) .X. y ) = ( A .x. ( X .X. y ) ) <-> ( ( A .x. X ) .X. Y ) = ( A .x. ( X .X. Y ) ) ) )
28 oveq2 6658 . . . . . 6 |- ( y = Y -> ( A .x. y ) = ( A .x. Y ) )
2928oveq2d 6666 . . . . 5 |- ( y = Y -> ( X .X. ( A .x. y ) ) = ( X .X. ( A .x. Y ) ) )
3029, 26eqeq12d 2637 . . . 4 |- ( y = Y -> ( ( X .X. ( A .x. y ) ) = ( A .x. ( X .X. y ) ) <-> ( X .X. ( A .x. Y ) ) = ( A .x. ( X .X. Y ) ) ) )
3127, 30anbi12d 747 . . 3 |- ( y = Y -> ( ( ( ( A .x. X ) .X. y ) = ( A .x. ( X .X. y ) ) /\ ( X .X. ( A .x. y ) ) = ( A .x. ( X .X. y ) ) ) <-> ( ( ( A .x. X ) .X. Y ) = ( A .x. ( X .X. Y ) ) /\ ( X .X. ( A .x. Y ) ) = ( A .x. ( X .X. Y ) ) ) ) )
3215, 23, 31rspc3v 3325 . 2 |- ( ( A e. B /\ X e. V /\ Y e. V ) -> ( 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 .x. X ) .X. Y ) = ( A .x. ( X .X. Y ) ) /\ ( X .X. ( A .x. Y ) ) = ( A .x. ( X .X. Y ) ) ) ) )
337, 32mpan9 486 1 |- ( ( W e. AssAlg /\ ( A e. B /\ X e. V /\ Y e. V ) ) -> ( ( ( A .x. X ) .X. Y ) = ( A .x. ( X .X. Y ) ) /\ ( X .X. ( A .x. Y ) ) = ( A .x. ( X .X. Y ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   A.wral 2912   ` cfv 5888  (class class class)co 6650   Basecbs 15857   .rcmulr 15942  Scalarcsca 15944   .scvsca 15945   Ringcrg 18547   CRingccrg 18548   LModclmod 18863  AssAlgcasa 19309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-assa 19312
This theorem is referenced by:  assaass  19317  assaassr  19318
  Copyright terms: Public domain W3C validator