Metamath Proof Explorer

Theorem tendorinv

Description: Right multiplicative inverse for endomorphism. (Contributed by NM, 10-Apr-2014) (Revised by Mario Carneiro, 23-Jun-2014)

Ref Expression
Hypotheses tendoinv.b 
|- B = ( Base ` K )
tendoinv.h 
|- H = ( LHyp ` K )
tendoinv.t 
|- T = ( ( LTrn ` K ) ` W )
tendoinv.e 
|- E = ( ( TEndo ` K ) ` W )
tendoinv.o 
|- O = ( h e. T |-> ( _I |` B ) )
tendoinv.u 
|- U = ( ( DVecH ` K ) ` W )
tendoinv.f 
|- F = ( Scalar ` U )
tendoinv.n 
|- N = ( invr ` F )
Assertion tendorinv 
|- ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> ( S o. ( N ` S ) ) = ( _I |` T ) )

Proof

Step Hyp Ref Expression
1 tendoinv.b 
 |-  B = ( Base ` K )
2 tendoinv.h 
 |-  H = ( LHyp ` K )
3 tendoinv.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 tendoinv.e 
 |-  E = ( ( TEndo ` K ) ` W )
5 tendoinv.o 
 |-  O = ( h e. T |-> ( _I |` B ) )
6 tendoinv.u 
 |-  U = ( ( DVecH ` K ) ` W )
7 tendoinv.f 
 |-  F = ( Scalar ` U )
8 tendoinv.n 
 |-  N = ( invr ` F )
9 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> ( K e. HL /\ W e. H ) )
10 eqid 
 |-  ( ( EDRing ` K ) ` W ) = ( ( EDRing ` K ) ` W )
11 2 10 6 7 dvhsca 
 |-  ( ( K e. HL /\ W e. H ) -> F = ( ( EDRing ` K ) ` W ) )
12 9 11 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> F = ( ( EDRing ` K ) ` W ) )
13 2 10 erngdv 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( EDRing ` K ) ` W ) e. DivRing )
14 9 13 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> ( ( EDRing ` K ) ` W ) e. DivRing )
15 12 14 eqeltrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> F e. DivRing )
16 simp2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> S e. E )
17 eqid 
 |-  ( Base ` F ) = ( Base ` F )
18 2 4 6 7 17 dvhbase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` F ) = E )
19 9 18 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> ( Base ` F ) = E )
20 16 19 eleqtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> S e. ( Base ` F ) )
21 simp3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> S =/= O )
22 11 fveq2d 
 |-  ( ( K e. HL /\ W e. H ) -> ( 0g ` F ) = ( 0g ` ( ( EDRing ` K ) ` W ) ) )
23 eqid 
 |-  ( 0g ` ( ( EDRing ` K ) ` W ) ) = ( 0g ` ( ( EDRing ` K ) ` W ) )
24 1 2 3 10 5 23 erng0g 
 |-  ( ( K e. HL /\ W e. H ) -> ( 0g ` ( ( EDRing ` K ) ` W ) ) = O )
25 22 24 eqtrd 
 |-  ( ( K e. HL /\ W e. H ) -> ( 0g ` F ) = O )
26 9 25 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> ( 0g ` F ) = O )
27 21 26 neeqtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> S =/= ( 0g ` F ) )
28 eqid 
 |-  ( 0g ` F ) = ( 0g ` F )
29 eqid 
 |-  ( .r ` F ) = ( .r ` F )
30 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
31 17 28 29 30 8 drnginvrr 
 |-  ( ( F e. DivRing /\ S e. ( Base ` F ) /\ S =/= ( 0g ` F ) ) -> ( S ( .r ` F ) ( N ` S ) ) = ( 1r ` F ) )
32 15 20 27 31 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> ( S ( .r ` F ) ( N ` S ) ) = ( 1r ` F ) )
33 1 2 3 4 5 6 7 8 tendoinvcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> ( ( N ` S ) e. E /\ ( N ` S ) =/= O ) )
34 33 simpld 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> ( N ` S ) e. E )
35 2 3 4 6 7 29 dvhmulr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ ( N ` S ) e. E ) ) -> ( S ( .r ` F ) ( N ` S ) ) = ( S o. ( N ` S ) ) )
36 9 16 34 35 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> ( S ( .r ` F ) ( N ` S ) ) = ( S o. ( N ` S ) ) )
37 11 fveq2d 
 |-  ( ( K e. HL /\ W e. H ) -> ( 1r ` F ) = ( 1r ` ( ( EDRing ` K ) ` W ) ) )
38 eqid 
 |-  ( 1r ` ( ( EDRing ` K ) ` W ) ) = ( 1r ` ( ( EDRing ` K ) ` W ) )
39 2 3 10 38 erng1r 
 |-  ( ( K e. HL /\ W e. H ) -> ( 1r ` ( ( EDRing ` K ) ` W ) ) = ( _I |` T ) )
40 37 39 eqtrd 
 |-  ( ( K e. HL /\ W e. H ) -> ( 1r ` F ) = ( _I |` T ) )
41 9 40 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> ( 1r ` F ) = ( _I |` T ) )
42 32 36 41 3eqtr3d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> ( S o. ( N ` S ) ) = ( _I |` T ) )