Metamath Proof Explorer

Theorem erng0g

Description: The division ring zero of an endomorphism ring. (Contributed by NM, 5-Nov-2013) (Revised by Mario Carneiro, 23-Jun-2014)

Ref Expression
Hypotheses erng0g.b ⊢B=BaseK
erng0g.h ⊢H=LHyp⁡K
erng0g.t ⊢T=LTrn⁡K⁡W
erng0g.d ⊢D=EDRing⁡K⁡W
erng0g.o ⊢O=f∈T⟼I↾B
erng0g.z ⊢0˙=0D
Assertion erng0g ⊢K∈HL∧W∈H→0˙=O

Proof

Step Hyp Ref Expression
1 erng0g.b ⊢B=BaseK
2 erng0g.h ⊢H=LHyp⁡K
3 erng0g.t ⊢T=LTrn⁡K⁡W
4 erng0g.d ⊢D=EDRing⁡K⁡W
5 erng0g.o ⊢O=f∈T⟼I↾B
6 erng0g.z ⊢0˙=0D
7 eqid ⊢TEndo⁡K⁡W=TEndo⁡K⁡W
8 eqid ⊢+D=+D
9 2 3 7 4 8 erngfplus ⊢K∈HL∧W∈H→+D=s∈TEndo⁡K⁡W,t∈TEndo⁡K⁡W⟼f∈T⟼s⁡f∘t⁡f
10 9 oveqd ⊢K∈HL∧W∈H→O+DO=Os∈TEndo⁡K⁡W,t∈TEndo⁡K⁡W⟼f∈T⟼s⁡f∘t⁡fO
11 1 2 3 7 5 tendo0cl ⊢K∈HL∧W∈H→O∈TEndo⁡K⁡W
12 eqid ⊢s∈TEndo⁡K⁡W,t∈TEndo⁡K⁡W⟼f∈T⟼s⁡f∘t⁡f=s∈TEndo⁡K⁡W,t∈TEndo⁡K⁡W⟼f∈T⟼s⁡f∘t⁡f
13 1 2 3 7 5 12 tendo0pl ⊢K∈HL∧W∈H∧O∈TEndo⁡K⁡W→Os∈TEndo⁡K⁡W,t∈TEndo⁡K⁡W⟼f∈T⟼s⁡f∘t⁡fO=O
14 11 13 mpdan ⊢K∈HL∧W∈H→Os∈TEndo⁡K⁡W,t∈TEndo⁡K⁡W⟼f∈T⟼s⁡f∘t⁡fO=O
15 10 14 eqtrd ⊢K∈HL∧W∈H→O+DO=O
16 2 4 eringring ⊢K∈HL∧W∈H→D∈Ring
17 ringgrp ⊢D∈Ring→D∈Grp
18 16 17 syl ⊢K∈HL∧W∈H→D∈Grp
19 eqid ⊢BaseD=BaseD
20 2 3 7 4 19 erngbase ⊢K∈HL∧W∈H→BaseD=TEndo⁡K⁡W
21 11 20 eleqtrrd ⊢K∈HL∧W∈H→O∈BaseD
22 19 8 6 grpid ⊢D∈Grp∧O∈BaseD→O+DO=O↔0˙=O
23 18 21 22 syl2anc ⊢K∈HL∧W∈H→O+DO=O↔0˙=O
24 15 23 mpbid ⊢K∈HL∧W∈H→0˙=O