Metamath Proof Explorer

Theorem erng0g

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

Ref Expression
Hypotheses erng0g.b 
|- B = ( Base ` K )
erng0g.h 
|- H = ( LHyp ` K )
erng0g.t 
|- T = ( ( LTrn ` K ) ` W )
erng0g.d 
|- D = ( ( EDRing ` K ) ` W )
erng0g.o 
|- O = ( f e. T |-> ( _I |` B ) )
erng0g.z 
|- .0. = ( 0g ` D )
Assertion erng0g 
|- ( ( K e. HL /\ W e. H ) -> .0. = O )

Proof

Step Hyp Ref Expression
1 erng0g.b 
 |-  B = ( Base ` K )
2 erng0g.h 
 |-  H = ( LHyp ` K )
3 erng0g.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 erng0g.d 
 |-  D = ( ( EDRing ` K ) ` W )
5 erng0g.o 
 |-  O = ( f e. T |-> ( _I |` B ) )
6 erng0g.z 
 |-  .0. = ( 0g ` D )
7 eqid 
 |-  ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
8 eqid 
 |-  ( +g ` D ) = ( +g ` D )
9 2 3 7 4 8 erngfplus 
 |-  ( ( K e. HL /\ W e. H ) -> ( +g ` D ) = ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) )
10 9 oveqd 
 |-  ( ( K e. HL /\ W e. H ) -> ( O ( +g ` D ) O ) = ( O ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) O ) )
11 1 2 3 7 5 tendo0cl 
 |-  ( ( K e. HL /\ W e. H ) -> O e. ( ( TEndo ` K ) ` W ) )
12 eqid 
 |-  ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) = ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )
13 1 2 3 7 5 12 tendo0pl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ O e. ( ( TEndo ` K ) ` W ) ) -> ( O ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) O ) = O )
14 11 13 mpdan 
 |-  ( ( K e. HL /\ W e. H ) -> ( O ( s e. ( ( TEndo ` K ) ` W ) , t e. ( ( TEndo ` K ) ` W ) |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) O ) = O )
15 10 14 eqtrd 
 |-  ( ( K e. HL /\ W e. H ) -> ( O ( +g ` D ) O ) = O )
16 2 4 eringring 
 |-  ( ( K e. HL /\ W e. H ) -> D e. Ring )
17 ringgrp 
 |-  ( D e. Ring -> D e. Grp )
18 16 17 syl 
 |-  ( ( K e. HL /\ W e. H ) -> D e. Grp )
19 eqid 
 |-  ( Base ` D ) = ( Base ` D )
20 2 3 7 4 19 erngbase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` D ) = ( ( TEndo ` K ) ` W ) )
21 11 20 eleqtrrd 
 |-  ( ( K e. HL /\ W e. H ) -> O e. ( Base ` D ) )
22 19 8 6 grpid 
 |-  ( ( D e. Grp /\ O e. ( Base ` D ) ) -> ( ( O ( +g ` D ) O ) = O <-> .0. = O ) )
23 18 21 22 syl2anc 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( O ( +g ` D ) O ) = O <-> .0. = O ) )
24 15 23 mpbid 
 |-  ( ( K e. HL /\ W e. H ) -> .0. = O )