Theorem assaring 21872

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1534   ∈ wcel 2100  ∀wral 3054  ‘cfv 6556  (class class class)co 7427  Basecbs 17226  ._rcmulr 17280  Scalarcsca 17282   ·_𝑠 cvsca 17283  Ringcrg 20228  LModclmod 20848  AssAlgcasa 21861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-ext 2700  ax-nul 5312

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2062  df-clab 2707  df-cleq 2721  df-clel 2806  df-ne 2934  df-ral 3055  df-rab 3429  df-v 3474  df-sbc 3788  df-dif 3961  df-un 3963  df-in 3965  df-ss 3975  df-nul 4334  df-if 4535  df-sn 4635  df-pr 4637  df-op 4641  df-uni 4917  df-br 5155  df-iota 6508  df-fv 6564  df-ov 7430  df-assa 21864

This theorem is referenced by:  issubassa  21877  assapropd  21882  aspval  21883  asclmul1  21896  asclmul2  21897  ascldimul  21898  asclrhm  21900  rnascl  21901  aspval2  21908  assamulgscmlem1  21909  assamulgscmlem2  21910  asclmulg  21912  zlmassa  21913  mplind  22084  evlseu  22097  pf1subrg  22339  matinv  22670  lactlmhm  33592  assalactf1o  33593  assarrginv  33594  irngnzply1lem  33635  assaascl0  47885  assaascl1  47886