This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tendocnv

Description: Converse of a trace-preserving endomorphism value. (Contributed by NM, 7-Apr-2014)

Ref Expression
Hypotheses tendosp.h 
|- H = ( LHyp ` K )
tendosp.t 
|- T = ( ( LTrn ` K ) ` W )
tendosp.e 
|- E = ( ( TEndo ` K ) ` W )
Assertion tendocnv 
|- ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> `' ( S ` F ) = ( S ` `' F ) )

Proof

Step Hyp Ref Expression
1 tendosp.h 
 |-  H = ( LHyp ` K )
2 tendosp.t 
 |-  T = ( ( LTrn ` K ) ` W )
3 tendosp.e 
 |-  E = ( ( TEndo ` K ) ` W )
4 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> ( K e. HL /\ W e. H ) )
5 1 2 3 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> ( S ` F ) e. T )
6 eqid 
 |-  ( Base ` K ) = ( Base ` K )
7 6 1 2 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S ` F ) e. T ) -> ( S ` F ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
8 4 5 7 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> ( S ` F ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
9 f1ococnv1 
 |-  ( ( S ` F ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) -> ( `' ( S ` F ) o. ( S ` F ) ) = ( _I |` ( Base ` K ) ) )
10 8 9 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> ( `' ( S ` F ) o. ( S ` F ) ) = ( _I |` ( Base ` K ) ) )
11 10 coeq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> ( ( `' ( S ` F ) o. ( S ` F ) ) o. `' ( S ` F ) ) = ( ( _I |` ( Base ` K ) ) o. `' ( S ` F ) ) )
12 simp2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> S e. E )
13 6 1 3 tendoid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( S ` ( _I |` ( Base ` K ) ) ) = ( _I |` ( Base ` K ) ) )
14 4 12 13 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> ( S ` ( _I |` ( Base ` K ) ) ) = ( _I |` ( Base ` K ) ) )
15 6 1 2 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
16 15 3adant2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> F : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
17 f1ococnv2 
 |-  ( F : ( Base ` K ) -1-1-onto-> ( Base ` K ) -> ( F o. `' F ) = ( _I |` ( Base ` K ) ) )
18 16 17 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> ( F o. `' F ) = ( _I |` ( Base ` K ) ) )
19 18 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> ( S ` ( F o. `' F ) ) = ( S ` ( _I |` ( Base ` K ) ) ) )
20 f1ococnv2 
 |-  ( ( S ` F ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) -> ( ( S ` F ) o. `' ( S ` F ) ) = ( _I |` ( Base ` K ) ) )
21 8 20 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> ( ( S ` F ) o. `' ( S ` F ) ) = ( _I |` ( Base ` K ) ) )
22 14 19 21 3eqtr4rd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> ( ( S ` F ) o. `' ( S ` F ) ) = ( S ` ( F o. `' F ) ) )
23 simp3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> F e. T )
24 1 2 ltrncnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> `' F e. T )
25 24 3adant2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> `' F e. T )
26 1 2 3 tendospdi1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ F e. T /\ `' F e. T ) ) -> ( S ` ( F o. `' F ) ) = ( ( S ` F ) o. ( S ` `' F ) ) )
27 4 12 23 25 26 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> ( S ` ( F o. `' F ) ) = ( ( S ` F ) o. ( S ` `' F ) ) )
28 22 27 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> ( ( S ` F ) o. `' ( S ` F ) ) = ( ( S ` F ) o. ( S ` `' F ) ) )
29 28 coeq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> ( `' ( S ` F ) o. ( ( S ` F ) o. `' ( S ` F ) ) ) = ( `' ( S ` F ) o. ( ( S ` F ) o. ( S ` `' F ) ) ) )
30 coass 
 |-  ( ( `' ( S ` F ) o. ( S ` F ) ) o. `' ( S ` F ) ) = ( `' ( S ` F ) o. ( ( S ` F ) o. `' ( S ` F ) ) )
31 coass 
 |-  ( ( `' ( S ` F ) o. ( S ` F ) ) o. ( S ` `' F ) ) = ( `' ( S ` F ) o. ( ( S ` F ) o. ( S ` `' F ) ) )
32 29 30 31 3eqtr4g 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> ( ( `' ( S ` F ) o. ( S ` F ) ) o. `' ( S ` F ) ) = ( ( `' ( S ` F ) o. ( S ` F ) ) o. ( S ` `' F ) ) )
33 10 coeq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> ( ( `' ( S ` F ) o. ( S ` F ) ) o. ( S ` `' F ) ) = ( ( _I |` ( Base ` K ) ) o. ( S ` `' F ) ) )
34 1 2 3 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ `' F e. T ) -> ( S ` `' F ) e. T )
35 25 34 syld3an3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> ( S ` `' F ) e. T )
36 6 1 2 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S ` `' F ) e. T ) -> ( S ` `' F ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
37 4 35 36 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> ( S ` `' F ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
38 f1of 
 |-  ( ( S ` `' F ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) -> ( S ` `' F ) : ( Base ` K ) --> ( Base ` K ) )
39 fcoi2 
 |-  ( ( S ` `' F ) : ( Base ` K ) --> ( Base ` K ) -> ( ( _I |` ( Base ` K ) ) o. ( S ` `' F ) ) = ( S ` `' F ) )
40 37 38 39 3syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> ( ( _I |` ( Base ` K ) ) o. ( S ` `' F ) ) = ( S ` `' F ) )
41 32 33 40 3eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> ( ( `' ( S ` F ) o. ( S ` F ) ) o. `' ( S ` F ) ) = ( S ` `' F ) )
42 1 2 ltrncnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S ` F ) e. T ) -> `' ( S ` F ) e. T )
43 4 5 42 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> `' ( S ` F ) e. T )
44 6 1 2 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ `' ( S ` F ) e. T ) -> `' ( S ` F ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
45 4 43 44 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> `' ( S ` F ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
46 f1of 
 |-  ( `' ( S ` F ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) -> `' ( S ` F ) : ( Base ` K ) --> ( Base ` K ) )
47 fcoi2 
 |-  ( `' ( S ` F ) : ( Base ` K ) --> ( Base ` K ) -> ( ( _I |` ( Base ` K ) ) o. `' ( S ` F ) ) = `' ( S ` F ) )
48 45 46 47 3syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> ( ( _I |` ( Base ` K ) ) o. `' ( S ` F ) ) = `' ( S ` F ) )
49 11 41 48 3eqtr3rd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> `' ( S ` F ) = ( S ` `' F ) )