Metamath Proof Explorer

Theorem erng1r

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

Ref Expression
Hypotheses erng1r.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
erng1r.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
erng1r.d ⊢ 𝐷 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
erng1r.r ⊢ 1 = ( 1r ‘ 𝐷 )
Assertion erng1r ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 1 = ( I ↾ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 erng1r.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 erng1r.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 erng1r.d ⊢ 𝐷 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
4 erng1r.r ⊢ 1 = ( 1r ‘ 𝐷 )
5 eqid ⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
6 1 2 5 tendoidcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
7 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
8 1 2 5 3 7 erngbase ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝐷 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
9 6 8 eleqtrrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ∈ ( Base ‘ 𝐷 ) )
10 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11 eqid ⊢ ( 𝑓 ∈ 𝑇 ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ ( Base ‘ 𝐾 ) ) )
12 10 1 2 5 11 tendo1ne0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ≠ ( 𝑓 ∈ 𝑇 ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) )
13 eqid ⊢ ( 0g ‘ 𝐷 ) = ( 0g ‘ 𝐷 )
14 10 1 2 3 11 13 erng0g ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 0g ‘ 𝐷 ) = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) )
15 12 14 neeqtrrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ≠ ( 0g ‘ 𝐷 ) )
16 id ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
17 eqid ⊢ ( .r ‘ 𝐷 ) = ( .r ‘ 𝐷 )
18 1 2 5 3 17 erngmul ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( I ↾ 𝑇 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( I ↾ 𝑇 ) ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( ( I ↾ 𝑇 ) ( .r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = ( ( I ↾ 𝑇 ) ∘ ( I ↾ 𝑇 ) ) )
19 16 6 6 18 syl12anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( I ↾ 𝑇 ) ( .r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = ( ( I ↾ 𝑇 ) ∘ ( I ↾ 𝑇 ) ) )
20 f1oi ⊢ ( I ↾ 𝑇 ) : 𝑇 –1-1-onto→ 𝑇
21 f1of ⊢ ( ( I ↾ 𝑇 ) : 𝑇 –1-1-onto→ 𝑇 → ( I ↾ 𝑇 ) : 𝑇 ⟶ 𝑇 )
22 fcoi2 ⊢ ( ( I ↾ 𝑇 ) : 𝑇 ⟶ 𝑇 → ( ( I ↾ 𝑇 ) ∘ ( I ↾ 𝑇 ) ) = ( I ↾ 𝑇 ) )
23 20 21 22 mp2b ⊢ ( ( I ↾ 𝑇 ) ∘ ( I ↾ 𝑇 ) ) = ( I ↾ 𝑇 )
24 19 23 eqtrdi ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( I ↾ 𝑇 ) ( .r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = ( I ↾ 𝑇 ) )
25 9 15 24 3jca ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( I ↾ 𝑇 ) ∈ ( Base ‘ 𝐷 ) ∧ ( I ↾ 𝑇 ) ≠ ( 0g ‘ 𝐷 ) ∧ ( ( I ↾ 𝑇 ) ( .r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = ( I ↾ 𝑇 ) ) )
26 1 3 erngdv ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 ∈ DivRing )
27 7 17 13 4 drngid2 ⊢ ( 𝐷 ∈ DivRing → ( ( ( I ↾ 𝑇 ) ∈ ( Base ‘ 𝐷 ) ∧ ( I ↾ 𝑇 ) ≠ ( 0g ‘ 𝐷 ) ∧ ( ( I ↾ 𝑇 ) ( .r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = ( I ↾ 𝑇 ) ) ↔ 1 = ( I ↾ 𝑇 ) ) )
28 26 27 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( I ↾ 𝑇 ) ∈ ( Base ‘ 𝐷 ) ∧ ( I ↾ 𝑇 ) ≠ ( 0g ‘ 𝐷 ) ∧ ( ( I ↾ 𝑇 ) ( .r ‘ 𝐷 ) ( I ↾ 𝑇 ) ) = ( I ↾ 𝑇 ) ) ↔ 1 = ( I ↾ 𝑇 ) ) )
29 25 28 mpbid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 1 = ( I ↾ 𝑇 ) )