Metamath Proof Explorer

Theorem erng1lem

Description: Value of the endomorphism division ring unit. (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 e. HL /\ W e. H ) -> D e. Ring )
Assertion erng1lem 
|- ( ( K e. HL /\ W e. H ) -> ( 1r ` D ) = ( _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 e. HL /\ W e. H ) -> D e. Ring )
6 1 2 3 tendoidcl 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` T ) e. E )
7 eqid 
 |-  ( Base ` D ) = ( Base ` D )
8 1 2 3 4 7 erngbase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` D ) = E )
9 6 8 eleqtrrd 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` T ) e. ( Base ` D ) )
10 8 eleq2d 
 |-  ( ( K e. HL /\ W e. H ) -> ( u e. ( Base ` D ) <-> u e. E ) )
11 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ u e. E ) -> ( K e. HL /\ W e. H ) )
12 6 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ u e. E ) -> ( _I |` T ) e. E )
13 simpr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ u e. E ) -> u e. E )
14 eqid 
 |-  ( .r ` D ) = ( .r ` D )
15 1 2 3 4 14 erngmul 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( _I |` T ) e. E /\ u e. E ) ) -> ( ( _I |` T ) ( .r ` D ) u ) = ( ( _I |` T ) o. u ) )
16 11 12 13 15 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ u e. E ) -> ( ( _I |` T ) ( .r ` D ) u ) = ( ( _I |` T ) o. u ) )
17 1 2 3 tendo1mul 
 |-  ( ( ( K e. HL /\ W e. H ) /\ u e. E ) -> ( ( _I |` T ) o. u ) = u )
18 16 17 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ u e. E ) -> ( ( _I |` T ) ( .r ` D ) u ) = u )
19 1 2 3 4 14 erngmul 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( u e. E /\ ( _I |` T ) e. E ) ) -> ( u ( .r ` D ) ( _I |` T ) ) = ( u o. ( _I |` T ) ) )
20 11 13 12 19 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ u e. E ) -> ( u ( .r ` D ) ( _I |` T ) ) = ( u o. ( _I |` T ) ) )
21 1 2 3 tendo1mulr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ u e. E ) -> ( u o. ( _I |` T ) ) = u )
22 20 21 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ u e. E ) -> ( u ( .r ` D ) ( _I |` T ) ) = u )
23 18 22 jca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ u e. E ) -> ( ( ( _I |` T ) ( .r ` D ) u ) = u /\ ( u ( .r ` D ) ( _I |` T ) ) = u ) )
24 23 ex 
 |-  ( ( K e. HL /\ W e. H ) -> ( u e. E -> ( ( ( _I |` T ) ( .r ` D ) u ) = u /\ ( u ( .r ` D ) ( _I |` T ) ) = u ) ) )
25 10 24 sylbid 
 |-  ( ( K e. HL /\ W e. H ) -> ( u e. ( Base ` D ) -> ( ( ( _I |` T ) ( .r ` D ) u ) = u /\ ( u ( .r ` D ) ( _I |` T ) ) = u ) ) )
26 25 ralrimiv 
 |-  ( ( K e. HL /\ W e. H ) -> A. u e. ( Base ` D ) ( ( ( _I |` T ) ( .r ` D ) u ) = u /\ ( u ( .r ` D ) ( _I |` T ) ) = u ) )
27 eqid 
 |-  ( 1r ` D ) = ( 1r ` D )
28 7 14 27 isringid 
 |-  ( D e. Ring -> ( ( ( _I |` T ) e. ( Base ` D ) /\ A. u e. ( Base ` D ) ( ( ( _I |` T ) ( .r ` D ) u ) = u /\ ( u ( .r ` D ) ( _I |` T ) ) = u ) ) <-> ( 1r ` D ) = ( _I |` T ) ) )
29 5 28 syl 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( _I |` T ) e. ( Base ` D ) /\ A. u e. ( Base ` D ) ( ( ( _I |` T ) ( .r ` D ) u ) = u /\ ( u ( .r ` D ) ( _I |` T ) ) = u ) ) <-> ( 1r ` D ) = ( _I |` T ) ) )
30 9 26 29 mpbi2and 
 |-  ( ( K e. HL /\ W e. H ) -> ( 1r ` D ) = ( _I |` T ) )