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 ⊢ 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 ⟼ 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 ⁡ 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 ⊢ K ∈ HL ∧ W ∈ H ∧ f ∈ LTrn ⁡ K ⁡ W ∧ f ≠ I ↾ Base K → D ∈ DivRing
20 5 19 rexlimddv ⊢ K ∈ HL ∧ W ∈ H → D ∈ DivRing