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 = LHyp K
ernggrp.d-r D = EDRing R K W
Assertion erngdv-rN K HL W H D DivRing

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 3 1 4 cdlemftr0 K HL W H f LTrn K W f I Base K
6 eqid TEndo K W = TEndo K W
7 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
8 eqid f LTrn K W I Base K = f LTrn K W I Base K
9 eqid a TEndo K W f LTrn K W a f -1 = a TEndo K W f LTrn K W a f -1
10 eqid a TEndo K W , b TEndo K W b a = a TEndo K W , b TEndo K W b a
11 eqid join K = join K
12 eqid meet K = meet K
13 eqid trL K W = trL K W
14 eqid oc K W = oc K W
15 eqid oc K W join K trL K W b meet K f oc K W join K trL K W b s f -1 = oc K W join K trL K W b meet K f oc K W join K trL K W b s f -1
16 eqid oc K W join K trL K W g meet K oc K W join K trL K W b meet K f oc K W join K trL K W b s f -1 join K trL K W g b -1 = oc K W join K trL K W g meet K oc K W join K trL K W b meet K f oc K W join K trL K W b s f -1 join K trL K W g b -1
17 eqid ι z LTrn K W | b LTrn K W b I Base K trL K W b trL K W s f trL K W b trL K W g z oc K W = oc K W join K trL K W g meet K oc K W join K trL K W b meet K f oc K W join K trL K W b s f -1 join K trL K W g b -1 = ι z LTrn K W | b LTrn K W b I Base K trL K W b trL K W s f trL K W b trL K W g z oc K W = oc K W join K trL K W g meet K oc K W join K trL K W b meet K f oc K W join K trL K W b s f -1 join K trL K W g b -1
18 eqid g LTrn K W if s f = f g ι z LTrn K W | b LTrn K W b I Base K trL K W b trL K W s f trL K W b trL K W g z oc K W = oc K W join K trL K W g meet K oc K W join K trL K W b meet K f oc K W join K trL K W b s f -1 join K trL K W g b -1 = g LTrn K W if s f = f g ι z LTrn K W | b LTrn K W b I Base K trL K W b trL K W s f trL K W b trL K W g z oc K W = oc K W join K trL K W g meet K oc K W join K trL K W b meet K f oc K W join K trL K W b s f -1 join K trL K W g b -1
19 1 2 3 4 6 7 8 9 10 11 12 13 14 15 16 17 18 erngdvlem4-rN K HL W H f LTrn K W f I Base K D DivRing
20 5 19 rexlimddv K HL W H D DivRing