Metamath Proof Explorer

Theorem erng1lem

Description: Value of the endomorphism division ring unity. (Contributed by NM, 12-Oct-2013)

Ref Expression
Hypotheses erng1.h ⊢H=LHyp⁡K
erng1.t ⊢T=LTrn⁡K⁡W
erng1.e ⊢E=TEndo⁡K⁡W
erng1.d ⊢D=EDRing⁡K⁡W
erng1.r ⊢K∈HL∧W∈H→D∈Ring
Assertion erng1lem ⊢K∈HL∧W∈H→1D=I↾T

Proof

Step Hyp Ref Expression
1 erng1.h ⊢H=LHyp⁡K
2 erng1.t ⊢T=LTrn⁡K⁡W
3 erng1.e ⊢E=TEndo⁡K⁡W
4 erng1.d ⊢D=EDRing⁡K⁡W
5 erng1.r ⊢K∈HL∧W∈H→D∈Ring
6 1 2 3 tendoidcl ⊢K∈HL∧W∈H→I↾T∈E
7 eqid ⊢BaseD=BaseD
8 1 2 3 4 7 erngbase ⊢K∈HL∧W∈H→BaseD=E
9 6 8 eleqtrrd ⊢K∈HL∧W∈H→I↾T∈BaseD
10 8 eleq2d ⊢K∈HL∧W∈H→u∈BaseD↔u∈E
11 simpl ⊢K∈HL∧W∈H∧u∈E→K∈HL∧W∈H
12 6 adantr ⊢K∈HL∧W∈H∧u∈E→I↾T∈E
13 simpr ⊢K∈HL∧W∈H∧u∈E→u∈E
14 eqid ⊢⋅D=⋅D
15 1 2 3 4 14 erngmul ⊢K∈HL∧W∈H∧I↾T∈E∧u∈E→I↾T⋅Du=I↾T∘u
16 11 12 13 15 syl12anc ⊢K∈HL∧W∈H∧u∈E→I↾T⋅Du=I↾T∘u
17 1 2 3 tendo1mul ⊢K∈HL∧W∈H∧u∈E→I↾T∘u=u
18 16 17 eqtrd ⊢K∈HL∧W∈H∧u∈E→I↾T⋅Du=u
19 1 2 3 4 14 erngmul ⊢K∈HL∧W∈H∧u∈E∧I↾T∈E→u⋅DI↾T=u∘I↾T
20 11 13 12 19 syl12anc ⊢K∈HL∧W∈H∧u∈E→u⋅DI↾T=u∘I↾T
21 1 2 3 tendo1mulr ⊢K∈HL∧W∈H∧u∈E→u∘I↾T=u
22 20 21 eqtrd ⊢K∈HL∧W∈H∧u∈E→u⋅DI↾T=u
23 18 22 jca ⊢K∈HL∧W∈H∧u∈E→I↾T⋅Du=u∧u⋅DI↾T=u
24 23 ex ⊢K∈HL∧W∈H→u∈E→I↾T⋅Du=u∧u⋅DI↾T=u
25 10 24 sylbid ⊢K∈HL∧W∈H→u∈BaseD→I↾T⋅Du=u∧u⋅DI↾T=u
26 25 ralrimiv ⊢K∈HL∧W∈H→∀u∈BaseDI↾T⋅Du=u∧u⋅DI↾T=u
27 eqid ⊢1D=1D
28 7 14 27 isringid ⊢D∈Ring→I↾T∈BaseD∧∀u∈BaseDI↾T⋅Du=u∧u⋅DI↾T=u↔1D=I↾T
29 5 28 syl ⊢K∈HL∧W∈H→I↾T∈BaseD∧∀u∈BaseDI↾T⋅Du=u∧u⋅DI↾T=u↔1D=I↾T
30 9 26 29 mpbi2and ⊢K∈HL∧W∈H→1D=I↾T