Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  assalem Structured version   Unicode version

Theorem assalem 16369
 Description: The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.)
Hypotheses
Ref Expression
isassa.v
isassa.f Scalar
isassa.b
isassa.s
isassa.t
Assertion
Ref Expression
assalem AssAlg

Proof of Theorem assalem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isassa.v . . . 4
2 isassa.f . . . 4 Scalar
3 isassa.b . . . 4
4 isassa.s . . . 4
5 isassa.t . . . 4
61, 2, 3, 4, 5isassa 16368 . . 3 AssAlg
76simprbi 451 . 2 AssAlg
8 oveq1 6081 . . . . . 6
98oveq1d 6089 . . . . 5
10 oveq1 6081 . . . . 5
119, 10eqeq12d 2450 . . . 4
12 oveq1 6081 . . . . . 6
1312oveq2d 6090 . . . . 5
1413, 10eqeq12d 2450 . . . 4
1511, 14anbi12d 692 . . 3
16 oveq2 6082 . . . . . 6
1716oveq1d 6089 . . . . 5
18 oveq1 6081 . . . . . 6
1918oveq2d 6090 . . . . 5
2017, 19eqeq12d 2450 . . . 4
21 oveq1 6081 . . . . 5
2221, 19eqeq12d 2450 . . . 4
2320, 22anbi12d 692 . . 3
24 oveq2 6082 . . . . 5
25 oveq2 6082 . . . . . 6
2625oveq2d 6090 . . . . 5
2724, 26eqeq12d 2450 . . . 4
28 oveq2 6082 . . . . . 6
2928oveq2d 6090 . . . . 5
3029, 26eqeq12d 2450 . . . 4
3127, 30anbi12d 692 . . 3
3215, 23, 31rspc3v 3054 . 2
337, 32mpan9 456 1 AssAlg
 Colors of variables: wff set class Syntax hints:   wi 4   wa 359   w3a 936   wceq 1652   wcel 1725  wral 2698  cfv 5447  (class class class)co 6074  cbs 13462  cmulr 13523  Scalarcsca 13525  cvsca 13526  crg 15653  ccrg 15654  clmod 15943  AssAlgcasa 16362 This theorem is referenced by:  assaass  16370  assaassr  16371 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-nul 4331 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2703  df-rex 2704  df-rab 2707  df-v 2951  df-sbc 3155  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-nul 3622  df-if 3733  df-sn 3813  df-pr 3814  df-op 3816  df-uni 4009  df-br 4206  df-iota 5411  df-fv 5455  df-ov 6077  df-assa 16365
 Copyright terms: Public domain W3C validator