Metamath Proof Explorer

Theorem tendoicl

Description: Closure of the additive inverse endomorphism. (Contributed by NM, 12-Jun-2013)

Ref Expression
Hypotheses tendoicl.h 
|- H = ( LHyp ` K )
tendoicl.t 
|- T = ( ( LTrn ` K ) ` W )
tendoicl.e 
|- E = ( ( TEndo ` K ) ` W )
tendoicl.i 
|- I = ( s e. E |-> ( f e. T |-> `' ( s ` f ) ) )
Assertion tendoicl 
|- ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( I ` S ) e. E )

Proof

Step Hyp Ref Expression
1 tendoicl.h 
 |-  H = ( LHyp ` K )
2 tendoicl.t 
 |-  T = ( ( LTrn ` K ) ` W )
3 tendoicl.e 
 |-  E = ( ( TEndo ` K ) ` W )
4 tendoicl.i 
 |-  I = ( s e. E |-> ( f e. T |-> `' ( s ` f ) ) )
5 eqid 
 |-  ( le ` K ) = ( le ` K )
6 eqid 
 |-  ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W )
7 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( K e. HL /\ W e. H ) )
8 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( K e. HL /\ W e. H ) )
9 1 2 3 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ g e. T ) -> ( S ` g ) e. T )
10 9 3expa 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( S ` g ) e. T )
11 1 2 ltrncnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S ` g ) e. T ) -> `' ( S ` g ) e. T )
12 8 10 11 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> `' ( S ` g ) e. T )
13 12 fmpttd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( g e. T |-> `' ( S ` g ) ) : T --> T )
14 4 2 tendoi 
 |-  ( S e. E -> ( I ` S ) = ( g e. T |-> `' ( S ` g ) ) )
15 14 adantl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( I ` S ) = ( g e. T |-> `' ( S ` g ) ) )
16 15 feq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( ( I ` S ) : T --> T <-> ( g e. T |-> `' ( S ` g ) ) : T --> T ) )
17 13 16 mpbird 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( I ` S ) : T --> T )
18 simp1r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T /\ h e. T ) -> S e. E )
19 1 2 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ g e. T /\ h e. T ) -> ( g o. h ) e. T )
20 19 3adant1r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T /\ h e. T ) -> ( g o. h ) e. T )
21 4 2 tendoi2 
 |-  ( ( S e. E /\ ( g o. h ) e. T ) -> ( ( I ` S ) ` ( g o. h ) ) = `' ( S ` ( g o. h ) ) )
22 18 20 21 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T /\ h e. T ) -> ( ( I ` S ) ` ( g o. h ) ) = `' ( S ` ( g o. h ) ) )
23 cnvco 
 |-  `' ( ( S ` h ) o. ( S ` g ) ) = ( `' ( S ` g ) o. `' ( S ` h ) )
24 1 2 ltrncom 
 |-  ( ( ( K e. HL /\ W e. H ) /\ g e. T /\ h e. T ) -> ( g o. h ) = ( h o. g ) )
25 24 3adant1r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T /\ h e. T ) -> ( g o. h ) = ( h o. g ) )
26 25 fveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T /\ h e. T ) -> ( S ` ( g o. h ) ) = ( S ` ( h o. g ) ) )
27 simp1ll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T /\ h e. T ) -> K e. HL )
28 simp1lr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T /\ h e. T ) -> W e. H )
29 simp3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T /\ h e. T ) -> h e. T )
30 simp2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T /\ h e. T ) -> g e. T )
31 1 2 3 tendovalco 
 |-  ( ( ( K e. HL /\ W e. H /\ S e. E ) /\ ( h e. T /\ g e. T ) ) -> ( S ` ( h o. g ) ) = ( ( S ` h ) o. ( S ` g ) ) )
32 27 28 18 29 30 31 syl32anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T /\ h e. T ) -> ( S ` ( h o. g ) ) = ( ( S ` h ) o. ( S ` g ) ) )
33 26 32 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T /\ h e. T ) -> ( S ` ( g o. h ) ) = ( ( S ` h ) o. ( S ` g ) ) )
34 33 cnveqd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T /\ h e. T ) -> `' ( S ` ( g o. h ) ) = `' ( ( S ` h ) o. ( S ` g ) ) )
35 4 2 tendoi2 
 |-  ( ( S e. E /\ g e. T ) -> ( ( I ` S ) ` g ) = `' ( S ` g ) )
36 18 30 35 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T /\ h e. T ) -> ( ( I ` S ) ` g ) = `' ( S ` g ) )
37 4 2 tendoi2 
 |-  ( ( S e. E /\ h e. T ) -> ( ( I ` S ) ` h ) = `' ( S ` h ) )
38 18 29 37 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T /\ h e. T ) -> ( ( I ` S ) ` h ) = `' ( S ` h ) )
39 36 38 coeq12d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T /\ h e. T ) -> ( ( ( I ` S ) ` g ) o. ( ( I ` S ) ` h ) ) = ( `' ( S ` g ) o. `' ( S ` h ) ) )
40 23 34 39 3eqtr4a 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T /\ h e. T ) -> `' ( S ` ( g o. h ) ) = ( ( ( I ` S ) ` g ) o. ( ( I ` S ) ` h ) ) )
41 22 40 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T /\ h e. T ) -> ( ( I ` S ) ` ( g o. h ) ) = ( ( ( I ` S ) ` g ) o. ( ( I ` S ) ` h ) ) )
42 35 adantll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( ( I ` S ) ` g ) = `' ( S ` g ) )
43 42 fveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( ( ( trL ` K ) ` W ) ` ( ( I ` S ) ` g ) ) = ( ( ( trL ` K ) ` W ) ` `' ( S ` g ) ) )
44 1 2 6 trlcnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S ` g ) e. T ) -> ( ( ( trL ` K ) ` W ) ` `' ( S ` g ) ) = ( ( ( trL ` K ) ` W ) ` ( S ` g ) ) )
45 8 10 44 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( ( ( trL ` K ) ` W ) ` `' ( S ` g ) ) = ( ( ( trL ` K ) ` W ) ` ( S ` g ) ) )
46 43 45 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( ( ( trL ` K ) ` W ) ` ( ( I ` S ) ` g ) ) = ( ( ( trL ` K ) ` W ) ` ( S ` g ) ) )
47 5 1 2 6 3 tendotp 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ g e. T ) -> ( ( ( trL ` K ) ` W ) ` ( S ` g ) ) ( le ` K ) ( ( ( trL ` K ) ` W ) ` g ) )
48 47 3expa 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( ( ( trL ` K ) ` W ) ` ( S ` g ) ) ( le ` K ) ( ( ( trL ` K ) ` W ) ` g ) )
49 46 48 eqbrtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E ) /\ g e. T ) -> ( ( ( trL ` K ) ` W ) ` ( ( I ` S ) ` g ) ) ( le ` K ) ( ( ( trL ` K ) ` W ) ` g ) )
50 5 1 2 6 3 7 17 41 49 istendod 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( I ` S ) e. E )