Metamath Proof Explorer

Theorem eringring

Description: An endomorphism ring is a ring. TODO: fix comment. (Contributed by NM, 4-Aug-2013)

Ref Expression
Hypotheses ernggrp.h ⊢H=LHyp⁡K
ernggrp.d ⊢D=EDRing⁡K⁡W
Assertion eringring ⊢K∈HL∧W∈H→D∈Ring

Proof

Step Hyp Ref Expression
1 ernggrp.h ⊢H=LHyp⁡K
2 ernggrp.d ⊢D=EDRing⁡K⁡W
3 eqid ⊢BaseK=BaseK
4 eqid ⊢LTrn⁡K⁡W=LTrn⁡K⁡W
5 eqid ⊢TEndo⁡K⁡W=TEndo⁡K⁡W
6 eqid ⊢a∈TEndo⁡K⁡W,b∈TEndo⁡K⁡W⟼f∈LTrn⁡K⁡W⟼a⁡f∘b⁡f=a∈TEndo⁡K⁡W,b∈TEndo⁡K⁡W⟼f∈LTrn⁡K⁡W⟼a⁡f∘b⁡f
7 eqid ⊢f∈LTrn⁡K⁡W⟼I↾BaseK=f∈LTrn⁡K⁡W⟼I↾BaseK
8 eqid ⊢a∈TEndo⁡K⁡W⟼f∈LTrn⁡K⁡W⟼a⁡f-1=a∈TEndo⁡K⁡W⟼f∈LTrn⁡K⁡W⟼a⁡f-1
9 eqid ⊢a∈TEndo⁡K⁡W,b∈TEndo⁡K⁡W⟼a∘b=a∈TEndo⁡K⁡W,b∈TEndo⁡K⁡W⟼a∘b
10 1 2 3 4 5 6 7 8 9 erngdvlem3 ⊢K∈HL∧W∈H→D∈Ring