Metamath Proof Explorer

Theorem erngring-rN

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

Ref Expression
Hypotheses ernggrp.h-r ⊢ H = LHyp ⁡ K
ernggrp.d-r ⊢ D = EDRing R ⁡ K ⁡ W
Assertion erngring-rN ⊢ K ∈ HL ∧ W ∈ H → D ∈ Ring

Proof

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