Theorem assaring 21808

Description: An associative algebra is a ring. (Contributed by Mario Carneiro, 5-Dec-2014.)

Assertion

Ref	Expression
assaring	⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ Ring)

Proof of Theorem assaring

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2733	. . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2733	. . . 4 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
3		eqid 2733	. . . 4 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
4		eqid 2733	. . . 4 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
5		eqid 2733	. . . 4 ⊢ (.r‘𝑊) = (.r‘𝑊)
6	1, 2, 3, 4, 5	isassa 21803	. . 3 ⊢ (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)(((𝑧( ·𝑠 ‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑧( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)) ∧ (𝑥(.r‘𝑊)(𝑧( ·𝑠 ‘𝑊)𝑦)) = (𝑧( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)))))
7	6	simplbi 497	. 2 ⊢ (𝑊 ∈ AssAlg → (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring))
8	7	simprd 495	1 ⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ Ring)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3049  ‘cfv 6489  (class class class)co 7355  Basecbs 17130  ._rcmulr 17172  Scalarcsca 17174   ·_𝑠 cvsca 17175  Ringcrg 20161  LModclmod 20803  AssAlgcasa 21797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2931  df-ral 3050  df-rab 3398  df-v 3440  df-sbc 3739  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-ov 7358  df-assa 21800

This theorem is referenced by:  issubassa  21814  assapropd  21819  aspval  21820  asclmul1  21833  asclmul2  21834  ascldimul  21835  asclrhm  21837  rnascl  21838  aspval2  21845  assamulgscmlem1  21846  assamulgscmlem2  21847  asclmulg  21849  zlmassa  21850  mplind  22015  evlseu  22028  pf1subrg  22273  matinv  22602  lactlmhm  33658  assalactf1o  33659  assarrginv  33660  irngnzply1lem  33714  assaascl0  48495  assaascl1  48496  asclelbas  49120  asclelbasALT  49121