Metamath Proof Explorer

Theorem tendoconid

Description: The composition (product) of trace-preserving endormorphisms is nonzero when each argument is nonzero. (Contributed by NM, 8-Aug-2013)

Ref Expression
Hypotheses tendoid0.b 
|- B = ( Base ` K )
tendoid0.h 
|- H = ( LHyp ` K )
tendoid0.t 
|- T = ( ( LTrn ` K ) ` W )
tendoid0.e 
|- E = ( ( TEndo ` K ) ` W )
tendoid0.o 
|- O = ( f e. T |-> ( _I |` B ) )
Assertion tendoconid 
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) -> ( U o. V ) =/= O )

Proof

Step Hyp Ref Expression
1 tendoid0.b 
 |-  B = ( Base ` K )
2 tendoid0.h 
 |-  H = ( LHyp ` K )
3 tendoid0.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 tendoid0.e 
 |-  E = ( ( TEndo ` K ) ` W )
5 tendoid0.o 
 |-  O = ( f e. T |-> ( _I |` B ) )
6 1 2 3 cdlemftr0 
 |-  ( ( K e. HL /\ W e. H ) -> E. g e. T g =/= ( _I |` B ) )
7 6 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) -> E. g e. T g =/= ( _I |` B ) )
8 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> ( K e. HL /\ W e. H ) )
9 simpl3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> V e. E )
10 2 3 4 tendof 
 |-  ( ( ( K e. HL /\ W e. H ) /\ V e. E ) -> V : T --> T )
11 8 9 10 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> V : T --> T )
12 simprl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> g e. T )
13 fvco3 
 |-  ( ( V : T --> T /\ g e. T ) -> ( ( U o. V ) ` g ) = ( U ` ( V ` g ) ) )
14 11 12 13 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> ( ( U o. V ) ` g ) = ( U ` ( V ` g ) ) )
15 simpl2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> U =/= O )
16 simpl2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> U e. E )
17 2 3 4 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ V e. E /\ g e. T ) -> ( V ` g ) e. T )
18 8 9 12 17 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> ( V ` g ) e. T )
19 simpl3r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> V =/= O )
20 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> ( g e. T /\ g =/= ( _I |` B ) ) )
21 1 2 3 4 5 tendoid0 
 |-  ( ( ( K e. HL /\ W e. H ) /\ V e. E /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> ( ( V ` g ) = ( _I |` B ) <-> V = O ) )
22 8 9 20 21 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> ( ( V ` g ) = ( _I |` B ) <-> V = O ) )
23 22 necon3bid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> ( ( V ` g ) =/= ( _I |` B ) <-> V =/= O ) )
24 19 23 mpbird 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> ( V ` g ) =/= ( _I |` B ) )
25 1 2 3 4 5 tendoid0 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ ( ( V ` g ) e. T /\ ( V ` g ) =/= ( _I |` B ) ) ) -> ( ( U ` ( V ` g ) ) = ( _I |` B ) <-> U = O ) )
26 8 16 18 24 25 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> ( ( U ` ( V ` g ) ) = ( _I |` B ) <-> U = O ) )
27 26 necon3bid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> ( ( U ` ( V ` g ) ) =/= ( _I |` B ) <-> U =/= O ) )
28 15 27 mpbird 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> ( U ` ( V ` g ) ) =/= ( _I |` B ) )
29 14 28 eqnetrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> ( ( U o. V ) ` g ) =/= ( _I |` B ) )
30 2 4 tendococl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) -> ( U o. V ) e. E )
31 8 16 9 30 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> ( U o. V ) e. E )
32 1 2 3 4 5 tendoid0 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U o. V ) e. E /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> ( ( ( U o. V ) ` g ) = ( _I |` B ) <-> ( U o. V ) = O ) )
33 8 31 20 32 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> ( ( ( U o. V ) ` g ) = ( _I |` B ) <-> ( U o. V ) = O ) )
34 33 necon3bid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> ( ( ( U o. V ) ` g ) =/= ( _I |` B ) <-> ( U o. V ) =/= O ) )
35 29 34 mpbid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) /\ ( g e. T /\ g =/= ( _I |` B ) ) ) -> ( U o. V ) =/= O )
36 7 35 rexlimddv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) -> ( U o. V ) =/= O )