Metamath Proof Explorer

Theorem erng1r

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

Ref Expression
Hypotheses erng1r.h ⊢H=LHyp⁡K
erng1r.t ⊢T=LTrn⁡K⁡W
erng1r.d ⊢D=EDRing⁡K⁡W
erng1r.r ⊢1˙=1D
Assertion erng1r ⊢K∈HL∧W∈H→1˙=I↾T

Proof

Step Hyp Ref Expression
1 erng1r.h ⊢H=LHyp⁡K
2 erng1r.t ⊢T=LTrn⁡K⁡W
3 erng1r.d ⊢D=EDRing⁡K⁡W
4 erng1r.r ⊢1˙=1D
5 eqid ⊢TEndo⁡K⁡W=TEndo⁡K⁡W
6 1 2 5 tendoidcl ⊢K∈HL∧W∈H→I↾T∈TEndo⁡K⁡W
7 eqid ⊢BaseD=BaseD
8 1 2 5 3 7 erngbase ⊢K∈HL∧W∈H→BaseD=TEndo⁡K⁡W
9 6 8 eleqtrrd ⊢K∈HL∧W∈H→I↾T∈BaseD
10 eqid ⊢BaseK=BaseK
11 eqid ⊢f∈T⟼I↾BaseK=f∈T⟼I↾BaseK
12 10 1 2 5 11 tendo1ne0 ⊢K∈HL∧W∈H→I↾T≠f∈T⟼I↾BaseK
13 eqid ⊢0D=0D
14 10 1 2 3 11 13 erng0g ⊢K∈HL∧W∈H→0D=f∈T⟼I↾BaseK
15 12 14 neeqtrrd ⊢K∈HL∧W∈H→I↾T≠0D
16 id ⊢K∈HL∧W∈H→K∈HL∧W∈H
17 eqid ⊢⋅D=⋅D
18 1 2 5 3 17 erngmul ⊢K∈HL∧W∈H∧I↾T∈TEndo⁡K⁡W∧I↾T∈TEndo⁡K⁡W→I↾T⋅DI↾T=I↾T∘I↾T
19 16 6 6 18 syl12anc ⊢K∈HL∧W∈H→I↾T⋅DI↾T=I↾T∘I↾T
20 f1oi ⊢I↾T:T⟶1-1 ontoT
21 f1of ⊢I↾T:T⟶1-1 ontoT→I↾T:T⟶T
22 fcoi2 ⊢I↾T:T⟶T→I↾T∘I↾T=I↾T
23 20 21 22 mp2b ⊢I↾T∘I↾T=I↾T
24 19 23 eqtrdi ⊢K∈HL∧W∈H→I↾T⋅DI↾T=I↾T
25 9 15 24 3jca ⊢K∈HL∧W∈H→I↾T∈BaseD∧I↾T≠0D∧I↾T⋅DI↾T=I↾T
26 1 3 erngdv ⊢K∈HL∧W∈H→D∈DivRing
27 7 17 13 4 drngid2 ⊢D∈DivRing→I↾T∈BaseD∧I↾T≠0D∧I↾T⋅DI↾T=I↾T↔1˙=I↾T
28 26 27 syl ⊢K∈HL∧W∈H→I↾T∈BaseD∧I↾T≠0D∧I↾T⋅DI↾T=I↾T↔1˙=I↾T
29 25 28 mpbid ⊢K∈HL∧W∈H→1˙=I↾T