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 ˙ = 1 D
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 ˙ = 1 D
5 eqid ⊢ TEndo ⁡ K ⁡ W = TEndo ⁡ K ⁡ W
6 1 2 5 tendoidcl ⊢ K ∈ HL ∧ W ∈ H → I ↾ T ∈ TEndo ⁡ K ⁡ W
7 eqid ⊢ Base D = Base D
8 1 2 5 3 7 erngbase ⊢ K ∈ HL ∧ W ∈ H → Base D = TEndo ⁡ K ⁡ W
9 6 8 eleqtrrd ⊢ K ∈ HL ∧ W ∈ H → I ↾ T ∈ Base D
10 eqid ⊢ Base K = Base K
11 eqid ⊢ f ∈ T ⟼ I ↾ Base K = f ∈ T ⟼ I ↾ Base K
12 10 1 2 5 11 tendo1ne0 ⊢ K ∈ HL ∧ W ∈ H → I ↾ T ≠ f ∈ T ⟼ I ↾ Base K
13 eqid ⊢ 0 D = 0 D
14 10 1 2 3 11 13 erng0g ⊢ K ∈ HL ∧ W ∈ H → 0 D = f ∈ T ⟼ I ↾ Base K
15 12 14 neeqtrrd ⊢ K ∈ HL ∧ W ∈ H → I ↾ T ≠ 0 D
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 ⋅ D I ↾ T = I ↾ T ∘ I ↾ T
19 16 6 6 18 syl12anc ⊢ K ∈ HL ∧ W ∈ H → I ↾ T ⋅ D I ↾ T = I ↾ T ∘ I ↾ T
20 f1oi ⊢ I ↾ T : T ⟶ 1-1 onto T
21 f1of ⊢ I ↾ T : T ⟶ 1-1 onto T → 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 ⋅ D I ↾ T = I ↾ T
25 9 15 24 3jca ⊢ K ∈ HL ∧ W ∈ H → I ↾ T ∈ Base D ∧ I ↾ T ≠ 0 D ∧ I ↾ T ⋅ D I ↾ T = I ↾ T
26 1 3 erngdv ⊢ K ∈ HL ∧ W ∈ H → D ∈ DivRing
27 7 17 13 4 drngid2 ⊢ D ∈ DivRing → I ↾ T ∈ Base D ∧ I ↾ T ≠ 0 D ∧ I ↾ T ⋅ D I ↾ T = I ↾ T ↔ 1 ˙ = I ↾ T
28 26 27 syl ⊢ K ∈ HL ∧ W ∈ H → I ↾ T ∈ Base D ∧ I ↾ T ≠ 0 D ∧ I ↾ T ⋅ D I ↾ T = I ↾ T ↔ 1 ˙ = I ↾ T
29 25 28 mpbid ⊢ K ∈ HL ∧ W ∈ H → 1 ˙ = I ↾ T