Theorem assaring 21900

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 2761	. . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2761	. . . 4 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
3		eqid 2761	. . . 4 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
4		eqid 2761	. . . 4 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
5		eqid 2761	. . . 4 ⊢ (.r‘𝑊) = (.r‘𝑊)
6	1, 2, 3, 4, 5	isassa 21895	. . 3 ⊢ (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)(((𝑧( ·𝑠 ‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑧( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)) ∧ (𝑥(.r‘𝑊)(𝑧( ·𝑠 ‘𝑊)𝑦)) = (𝑧( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)))))
7	6	simplbi 500	. 2 ⊢ (𝑊 ∈ AssAlg → (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring))
8	7	simprd 499	1 ⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ Ring)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141  ∀wral 3075  ‘cfv 6515  (class class class)co 7390  Basecbs 17235  ._rcmulr 17277  Scalarcsca 17279   ·_𝑠 cvsca 17280  Ringcrg 20269  LModclmod 20914  AssAlgcasa 21889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5253

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rab 3414  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6471  df-fv 6523  df-ov 7393  df-assa 21892

This theorem is referenced by:  issubassa  21906  assapropd  21910  aspval  21911  asclelbas  21922  asclmul1  21925  asclmul2  21926  ascldimul  21927  asclrhm  21929  rnascl  21930  aspval2  21937  assamulgscmlem1  21938  assamulgscmlem2  21939  asclmulg  21941  zlmassa  21942  mplind  22110  evlseu  22123  pf1subrg  22398  matinv  22724  lactlmhm  33891  assalactf1o  33892  assarrginv  33893  irngnzply1lem  33947  assaascl0  48963  assaascl1  48964  asclelbasALT  49587