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 
|- H = ( LHyp ` K )
erng1r.t 
|- T = ( ( LTrn ` K ) ` W )
erng1r.d 
|- D = ( ( EDRing ` K ) ` W )
erng1r.r 
|- .1. = ( 1r ` D )
Assertion erng1r 
|- ( ( K e. HL /\ W e. 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. = ( 1r ` D )
5 eqid 
 |-  ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
6 1 2 5 tendoidcl 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` T ) e. ( ( TEndo ` K ) ` W ) )
7 eqid 
 |-  ( Base ` D ) = ( Base ` D )
8 1 2 5 3 7 erngbase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` D ) = ( ( TEndo ` K ) ` W ) )
9 6 8 eleqtrrd 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` T ) e. ( Base ` D ) )
10 eqid 
 |-  ( Base ` K ) = ( Base ` K )
11 eqid 
 |-  ( f e. T |-> ( _I |` ( Base ` K ) ) ) = ( f e. T |-> ( _I |` ( Base ` K ) ) )
12 10 1 2 5 11 tendo1ne0 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` T ) =/= ( f e. T |-> ( _I |` ( Base ` K ) ) ) )
13 eqid 
 |-  ( 0g ` D ) = ( 0g ` D )
14 10 1 2 3 11 13 erng0g 
 |-  ( ( K e. HL /\ W e. H ) -> ( 0g ` D ) = ( f e. T |-> ( _I |` ( Base ` K ) ) ) )
15 12 14 neeqtrrd 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` T ) =/= ( 0g ` D ) )
16 id 
 |-  ( ( K e. HL /\ W e. H ) -> ( K e. HL /\ W e. H ) )
17 eqid 
 |-  ( .r ` D ) = ( .r ` D )
18 1 2 5 3 17 erngmul 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( _I |` T ) e. ( ( TEndo ` K ) ` W ) /\ ( _I |` T ) e. ( ( TEndo ` K ) ` W ) ) ) -> ( ( _I |` T ) ( .r ` D ) ( _I |` T ) ) = ( ( _I |` T ) o. ( _I |` T ) ) )
19 16 6 6 18 syl12anc 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( _I |` T ) ( .r ` D ) ( _I |` T ) ) = ( ( _I |` T ) o. ( _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 ) o. ( _I |` T ) ) = ( _I |` T ) )
23 20 21 22 mp2b 
 |-  ( ( _I |` T ) o. ( _I |` T ) ) = ( _I |` T )
24 19 23 eqtrdi 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( _I |` T ) ( .r ` D ) ( _I |` T ) ) = ( _I |` T ) )
25 9 15 24 3jca 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( _I |` T ) e. ( Base ` D ) /\ ( _I |` T ) =/= ( 0g ` D ) /\ ( ( _I |` T ) ( .r ` D ) ( _I |` T ) ) = ( _I |` T ) ) )
26 1 3 erngdv 
 |-  ( ( K e. HL /\ W e. H ) -> D e. DivRing )
27 7 17 13 4 drngid2 
 |-  ( D e. DivRing -> ( ( ( _I |` T ) e. ( Base ` D ) /\ ( _I |` T ) =/= ( 0g ` D ) /\ ( ( _I |` T ) ( .r ` D ) ( _I |` T ) ) = ( _I |` T ) ) <-> .1. = ( _I |` T ) ) )
28 26 27 syl 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( _I |` T ) e. ( Base ` D ) /\ ( _I |` T ) =/= ( 0g ` D ) /\ ( ( _I |` T ) ( .r ` D ) ( _I |` T ) ) = ( _I |` T ) ) <-> .1. = ( _I |` T ) ) )
29 25 28 mpbid 
 |-  ( ( K e. HL /\ W e. H ) -> .1. = ( _I |` T ) )