Metamath Proof Explorer

Theorem erngdv

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

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

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 3 1 4 cdlemftr0 ⊢K∈HL∧W∈H→∃f∈LTrn⁡K⁡Wf≠I↾BaseK
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↾BaseK=f∈LTrn⁡K⁡W⟼I↾BaseK
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⟼a∘b=a∈TEndo⁡K⁡W,b∈TEndo⁡K⁡W⟼a∘b
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⁡Wjoin⁡KtrL⁡K⁡W⁡bmeet⁡Kf⁡oc⁡K⁡Wjoin⁡KtrL⁡K⁡W⁡b∘s⁡f-1=oc⁡K⁡Wjoin⁡KtrL⁡K⁡W⁡bmeet⁡Kf⁡oc⁡K⁡Wjoin⁡KtrL⁡K⁡W⁡b∘s⁡f-1
16 eqid ⊢oc⁡K⁡Wjoin⁡KtrL⁡K⁡W⁡gmeet⁡Koc⁡K⁡Wjoin⁡KtrL⁡K⁡W⁡bmeet⁡Kf⁡oc⁡K⁡Wjoin⁡KtrL⁡K⁡W⁡b∘s⁡f-1join⁡KtrL⁡K⁡W⁡g∘b-1=oc⁡K⁡Wjoin⁡KtrL⁡K⁡W⁡gmeet⁡Koc⁡K⁡Wjoin⁡KtrL⁡K⁡W⁡bmeet⁡Kf⁡oc⁡K⁡Wjoin⁡KtrL⁡K⁡W⁡b∘s⁡f-1join⁡KtrL⁡K⁡W⁡g∘b-1
17 eqid ⊢ιz∈LTrn⁡K⁡W|∀b∈LTrn⁡K⁡Wb≠I↾BaseK∧trL⁡K⁡W⁡b≠trL⁡K⁡W⁡s⁡f∧trL⁡K⁡W⁡b≠trL⁡K⁡W⁡g→z⁡oc⁡K⁡W=oc⁡K⁡Wjoin⁡KtrL⁡K⁡W⁡gmeet⁡Koc⁡K⁡Wjoin⁡KtrL⁡K⁡W⁡bmeet⁡Kf⁡oc⁡K⁡Wjoin⁡KtrL⁡K⁡W⁡b∘s⁡f-1join⁡KtrL⁡K⁡W⁡g∘b-1=ιz∈LTrn⁡K⁡W|∀b∈LTrn⁡K⁡Wb≠I↾BaseK∧trL⁡K⁡W⁡b≠trL⁡K⁡W⁡s⁡f∧trL⁡K⁡W⁡b≠trL⁡K⁡W⁡g→z⁡oc⁡K⁡W=oc⁡K⁡Wjoin⁡KtrL⁡K⁡W⁡gmeet⁡Koc⁡K⁡Wjoin⁡KtrL⁡K⁡W⁡bmeet⁡Kf⁡oc⁡K⁡Wjoin⁡KtrL⁡K⁡W⁡b∘s⁡f-1join⁡KtrL⁡K⁡W⁡g∘b-1
18 eqid ⊢g∈LTrn⁡K⁡W⟼ifs⁡f=fgιz∈LTrn⁡K⁡W|∀b∈LTrn⁡K⁡Wb≠I↾BaseK∧trL⁡K⁡W⁡b≠trL⁡K⁡W⁡s⁡f∧trL⁡K⁡W⁡b≠trL⁡K⁡W⁡g→z⁡oc⁡K⁡W=oc⁡K⁡Wjoin⁡KtrL⁡K⁡W⁡gmeet⁡Koc⁡K⁡Wjoin⁡KtrL⁡K⁡W⁡bmeet⁡Kf⁡oc⁡K⁡Wjoin⁡KtrL⁡K⁡W⁡b∘s⁡f-1join⁡KtrL⁡K⁡W⁡g∘b-1=g∈LTrn⁡K⁡W⟼ifs⁡f=fgιz∈LTrn⁡K⁡W|∀b∈LTrn⁡K⁡Wb≠I↾BaseK∧trL⁡K⁡W⁡b≠trL⁡K⁡W⁡s⁡f∧trL⁡K⁡W⁡b≠trL⁡K⁡W⁡g→z⁡oc⁡K⁡W=oc⁡K⁡Wjoin⁡KtrL⁡K⁡W⁡gmeet⁡Koc⁡K⁡Wjoin⁡KtrL⁡K⁡W⁡bmeet⁡Kf⁡oc⁡K⁡Wjoin⁡KtrL⁡K⁡W⁡b∘s⁡f-1join⁡KtrL⁡K⁡W⁡g∘b-1
19 1 2 3 4 6 7 8 9 10 11 12 13 14 15 16 17 18 erngdvlem4 ⊢K∈HL∧W∈H∧f∈LTrn⁡K⁡W∧f≠I↾BaseK→D∈DivRing
20 5 19 rexlimddv ⊢K∈HL∧W∈H→D∈DivRing