Metamath Proof Explorer

Theorem tendoinvcl

Description: Closure of multiplicative inverse for endomorphism. We use the scalar inverse of the vector space since it is much simpler than the direct inverse of cdleml8 . (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 tendoinvcl 
|- ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> ( ( N ` S ) e. E /\ ( N ` S ) =/= O ) )

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 eqid 
 |-  ( ( EDRing ` K ) ` W ) = ( ( EDRing ` K ) ` W )
10 2 9 6 7 dvhsca 
 |-  ( ( K e. HL /\ W e. H ) -> F = ( ( EDRing ` K ) ` W ) )
11 2 9 erngdv 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( EDRing ` K ) ` W ) e. DivRing )
12 10 11 eqeltrd 
 |-  ( ( K e. HL /\ W e. H ) -> F e. DivRing )
13 12 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> F e. DivRing )
14 simp2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> S e. E )
15 eqid 
 |-  ( Base ` F ) = ( Base ` F )
16 2 4 6 7 15 dvhbase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` F ) = E )
17 16 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> ( Base ` F ) = E )
18 14 17 eleqtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> S e. ( Base ` F ) )
19 simp3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> S =/= O )
20 10 fveq2d 
 |-  ( ( K e. HL /\ W e. H ) -> ( 0g ` F ) = ( 0g ` ( ( EDRing ` K ) ` W ) ) )
21 eqid 
 |-  ( 0g ` ( ( EDRing ` K ) ` W ) ) = ( 0g ` ( ( EDRing ` K ) ` W ) )
22 1 2 3 9 5 21 erng0g 
 |-  ( ( K e. HL /\ W e. H ) -> ( 0g ` ( ( EDRing ` K ) ` W ) ) = O )
23 20 22 eqtrd 
 |-  ( ( K e. HL /\ W e. H ) -> ( 0g ` F ) = O )
24 23 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> ( 0g ` F ) = O )
25 19 24 neeqtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> S =/= ( 0g ` F ) )
26 eqid 
 |-  ( 0g ` F ) = ( 0g ` F )
27 15 26 8 drnginvrcl 
 |-  ( ( F e. DivRing /\ S e. ( Base ` F ) /\ S =/= ( 0g ` F ) ) -> ( N ` S ) e. ( Base ` F ) )
28 13 18 25 27 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> ( N ` S ) e. ( Base ` F ) )
29 28 17 eleqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> ( N ` S ) e. E )
30 15 26 8 drnginvrn0 
 |-  ( ( F e. DivRing /\ S e. ( Base ` F ) /\ S =/= ( 0g ` F ) ) -> ( N ` S ) =/= ( 0g ` F ) )
31 13 18 25 30 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> ( N ` S ) =/= ( 0g ` F ) )
32 31 24 neeqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> ( N ` S ) =/= O )
33 29 32 jca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ S =/= O ) -> ( ( N ` S ) e. E /\ ( N ` S ) =/= O ) )