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 ⊢ 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 ⟼ 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