Metamath Proof Explorer

Theorem istendo

Description: The predicate "is a trace-preserving endomorphism". Similar to definition of trace-preserving endomorphism in Crawley p. 117, penultimate line. (Contributed by NM, 8-Jun-2013)

Ref Expression
Hypotheses tendoset.l 
|- .<_ = ( le ` K )
tendoset.h 
|- H = ( LHyp ` K )
tendoset.t 
|- T = ( ( LTrn ` K ) ` W )
tendoset.r 
|- R = ( ( trL ` K ) ` W )
tendoset.e 
|- E = ( ( TEndo ` K ) ` W )
Assertion istendo 
|- ( ( K e. V /\ W e. H ) -> ( S e. E <-> ( S : T --> T /\ A. f e. T A. g e. T ( S ` ( f o. g ) ) = ( ( S ` f ) o. ( S ` g ) ) /\ A. f e. T ( R ` ( S ` f ) ) .<_ ( R ` f ) ) ) )

Proof

Step Hyp Ref Expression
1 tendoset.l 
 |-  .<_ = ( le ` K )
2 tendoset.h 
 |-  H = ( LHyp ` K )
3 tendoset.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 tendoset.r 
 |-  R = ( ( trL ` K ) ` W )
5 tendoset.e 
 |-  E = ( ( TEndo ` K ) ` W )
6 1 2 3 4 5 tendoset 
 |-  ( ( K e. V /\ W e. H ) -> E = { s | ( s : T --> T /\ A. f e. T A. g e. T ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) /\ A. f e. T ( R ` ( s ` f ) ) .<_ ( R ` f ) ) } )
7 6 eleq2d 
 |-  ( ( K e. V /\ W e. H ) -> ( S e. E <-> S e. { s | ( s : T --> T /\ A. f e. T A. g e. T ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) /\ A. f e. T ( R ` ( s ` f ) ) .<_ ( R ` f ) ) } ) )
8 3 fvexi 
 |-  T e. _V
9 fex 
 |-  ( ( S : T --> T /\ T e. _V ) -> S e. _V )
10 8 9 mpan2 
 |-  ( S : T --> T -> S e. _V )
11 10 3ad2ant1 
 |-  ( ( S : T --> T /\ A. f e. T A. g e. T ( S ` ( f o. g ) ) = ( ( S ` f ) o. ( S ` g ) ) /\ A. f e. T ( R ` ( S ` f ) ) .<_ ( R ` f ) ) -> S e. _V )
12 feq1 
 |-  ( s = S -> ( s : T --> T <-> S : T --> T ) )
13 fveq1 
 |-  ( s = S -> ( s ` ( f o. g ) ) = ( S ` ( f o. g ) ) )
14 fveq1 
 |-  ( s = S -> ( s ` f ) = ( S ` f ) )
15 fveq1 
 |-  ( s = S -> ( s ` g ) = ( S ` g ) )
16 14 15 coeq12d 
 |-  ( s = S -> ( ( s ` f ) o. ( s ` g ) ) = ( ( S ` f ) o. ( S ` g ) ) )
17 13 16 eqeq12d 
 |-  ( s = S -> ( ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) <-> ( S ` ( f o. g ) ) = ( ( S ` f ) o. ( S ` g ) ) ) )
18 17 2ralbidv 
 |-  ( s = S -> ( A. f e. T A. g e. T ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) <-> A. f e. T A. g e. T ( S ` ( f o. g ) ) = ( ( S ` f ) o. ( S ` g ) ) ) )
19 14 fveq2d 
 |-  ( s = S -> ( R ` ( s ` f ) ) = ( R ` ( S ` f ) ) )
20 19 breq1d 
 |-  ( s = S -> ( ( R ` ( s ` f ) ) .<_ ( R ` f ) <-> ( R ` ( S ` f ) ) .<_ ( R ` f ) ) )
21 20 ralbidv 
 |-  ( s = S -> ( A. f e. T ( R ` ( s ` f ) ) .<_ ( R ` f ) <-> A. f e. T ( R ` ( S ` f ) ) .<_ ( R ` f ) ) )
22 12 18 21 3anbi123d 
 |-  ( s = S -> ( ( s : T --> T /\ A. f e. T A. g e. T ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) /\ A. f e. T ( R ` ( s ` f ) ) .<_ ( R ` f ) ) <-> ( S : T --> T /\ A. f e. T A. g e. T ( S ` ( f o. g ) ) = ( ( S ` f ) o. ( S ` g ) ) /\ A. f e. T ( R ` ( S ` f ) ) .<_ ( R ` f ) ) ) )
23 11 22 elab3 
 |-  ( S e. { s | ( s : T --> T /\ A. f e. T A. g e. T ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) /\ A. f e. T ( R ` ( s ` f ) ) .<_ ( R ` f ) ) } <-> ( S : T --> T /\ A. f e. T A. g e. T ( S ` ( f o. g ) ) = ( ( S ` f ) o. ( S ` g ) ) /\ A. f e. T ( R ` ( S ` f ) ) .<_ ( R ` f ) ) )
24 7 23 bitrdi 
 |-  ( ( K e. V /\ W e. H ) -> ( S e. E <-> ( S : T --> T /\ A. f e. T A. g e. T ( S ` ( f o. g ) ) = ( ( S ` f ) o. ( S ` g ) ) /\ A. f e. T ( R ` ( S ` f ) ) .<_ ( R ` f ) ) ) )