Metamath Proof Explorer


Theorem erngdv-rN

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

Ref Expression
Hypotheses ernggrp.h-r H=LHypK
ernggrp.d-r D=EDRingRKW
Assertion erngdv-rN KHLWHDDivRing

Proof

Step Hyp Ref Expression
1 ernggrp.h-r H=LHypK
2 ernggrp.d-r D=EDRingRKW
3 eqid BaseK=BaseK
4 eqid LTrnKW=LTrnKW
5 3 1 4 cdlemftr0 KHLWHfLTrnKWfIBaseK
6 eqid TEndoKW=TEndoKW
7 eqid aTEndoKW,bTEndoKWfLTrnKWafbf=aTEndoKW,bTEndoKWfLTrnKWafbf
8 eqid fLTrnKWIBaseK=fLTrnKWIBaseK
9 eqid aTEndoKWfLTrnKWaf-1=aTEndoKWfLTrnKWaf-1
10 eqid aTEndoKW,bTEndoKWba=aTEndoKW,bTEndoKWba
11 eqid joinK=joinK
12 eqid meetK=meetK
13 eqid trLKW=trLKW
14 eqid ocKW=ocKW
15 eqid ocKWjoinKtrLKWbmeetKfocKWjoinKtrLKWbsf-1=ocKWjoinKtrLKWbmeetKfocKWjoinKtrLKWbsf-1
16 eqid ocKWjoinKtrLKWgmeetKocKWjoinKtrLKWbmeetKfocKWjoinKtrLKWbsf-1joinKtrLKWgb-1=ocKWjoinKtrLKWgmeetKocKWjoinKtrLKWbmeetKfocKWjoinKtrLKWbsf-1joinKtrLKWgb-1
17 eqid ιzLTrnKW|bLTrnKWbIBaseKtrLKWbtrLKWsftrLKWbtrLKWgzocKW=ocKWjoinKtrLKWgmeetKocKWjoinKtrLKWbmeetKfocKWjoinKtrLKWbsf-1joinKtrLKWgb-1=ιzLTrnKW|bLTrnKWbIBaseKtrLKWbtrLKWsftrLKWbtrLKWgzocKW=ocKWjoinKtrLKWgmeetKocKWjoinKtrLKWbmeetKfocKWjoinKtrLKWbsf-1joinKtrLKWgb-1
18 eqid gLTrnKWifsf=fgιzLTrnKW|bLTrnKWbIBaseKtrLKWbtrLKWsftrLKWbtrLKWgzocKW=ocKWjoinKtrLKWgmeetKocKWjoinKtrLKWbmeetKfocKWjoinKtrLKWbsf-1joinKtrLKWgb-1=gLTrnKWifsf=fgιzLTrnKW|bLTrnKWbIBaseKtrLKWbtrLKWsftrLKWbtrLKWgzocKW=ocKWjoinKtrLKWgmeetKocKWjoinKtrLKWbmeetKfocKWjoinKtrLKWbsf-1joinKtrLKWgb-1
19 1 2 3 4 6 7 8 9 10 11 12 13 14 15 16 17 18 erngdvlem4-rN KHLWHfLTrnKWfIBaseKDDivRing
20 5 19 rexlimddv KHLWHDDivRing