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

Metamath Proof Explorer

Theorem tendospcanN

Description: Cancellation law for trace-preserving endomorphism values (used as scalar product). (Contributed by NM, 7-Apr-2014) (New usage is discouraged.)

Ref Expression
Hypotheses tendospcan.b 
|- B = ( Base ` K )
tendospcan.h 
|- H = ( LHyp ` K )
tendospcan.t 
|- T = ( ( LTrn ` K ) ` W )
tendospcan.e 
|- E = ( ( TEndo ` K ) ` W )
tendospcan.o 
|- O = ( f e. T |-> ( _I |` B ) )
Assertion tendospcanN 
|- ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ S =/= O ) /\ ( F e. T /\ G e. T ) ) -> ( ( S ` F ) = ( S ` G ) <-> F = G ) )

Proof

Step Hyp Ref Expression
1 tendospcan.b 
 |-  B = ( Base ` K )
2 tendospcan.h 
 |-  H = ( LHyp ` K )
3 tendospcan.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 tendospcan.e 
 |-  E = ( ( TEndo ` K ) ` W )
5 tendospcan.o 
 |-  O = ( f e. T |-> ( _I |` B ) )
6 2 3 4 tendocnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ G e. T ) -> `' ( S ` G ) = ( S ` `' G ) )
7 6 3adant3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) -> `' ( S ` G ) = ( S ` `' G ) )
8 7 coeq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) -> ( ( S ` F ) o. `' ( S ` G ) ) = ( ( S ` F ) o. ( S ` `' G ) ) )
9 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) -> ( K e. HL /\ W e. H ) )
10 simp2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) -> S e. E )
11 simp3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) -> F e. T )
12 simp3r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) -> G e. T )
13 2 3 ltrncnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> `' G e. T )
14 9 12 13 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) -> `' G e. T )
15 2 3 4 tendospdi1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ F e. T /\ `' G e. T ) ) -> ( S ` ( F o. `' G ) ) = ( ( S ` F ) o. ( S ` `' G ) ) )
16 9 10 11 14 15 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) -> ( S ` ( F o. `' G ) ) = ( ( S ` F ) o. ( S ` `' G ) ) )
17 8 16 eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) -> ( ( S ` F ) o. `' ( S ` G ) ) = ( S ` ( F o. `' G ) ) )
18 17 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) /\ ( F o. `' G ) =/= ( _I |` B ) ) -> ( ( S ` F ) o. `' ( S ` G ) ) = ( S ` ( F o. `' G ) ) )
19 18 eqeq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) /\ ( F o. `' G ) =/= ( _I |` B ) ) -> ( ( ( S ` F ) o. `' ( S ` G ) ) = ( _I |` B ) <-> ( S ` ( F o. `' G ) ) = ( _I |` B ) ) )
20 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) /\ ( F o. `' G ) =/= ( _I |` B ) ) -> ( K e. HL /\ W e. H ) )
21 simpl2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) /\ ( F o. `' G ) =/= ( _I |` B ) ) -> S e. E )
22 simpl3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) /\ ( F o. `' G ) =/= ( _I |` B ) ) -> F e. T )
23 2 3 4 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ F e. T ) -> ( S ` F ) e. T )
24 20 21 22 23 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) /\ ( F o. `' G ) =/= ( _I |` B ) ) -> ( S ` F ) e. T )
25 simpl3r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) /\ ( F o. `' G ) =/= ( _I |` B ) ) -> G e. T )
26 2 3 4 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ G e. T ) -> ( S ` G ) e. T )
27 20 21 25 26 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) /\ ( F o. `' G ) =/= ( _I |` B ) ) -> ( S ` G ) e. T )
28 1 2 3 ltrncoidN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S ` F ) e. T /\ ( S ` G ) e. T ) -> ( ( ( S ` F ) o. `' ( S ` G ) ) = ( _I |` B ) <-> ( S ` F ) = ( S ` G ) ) )
29 20 24 27 28 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) /\ ( F o. `' G ) =/= ( _I |` B ) ) -> ( ( ( S ` F ) o. `' ( S ` G ) ) = ( _I |` B ) <-> ( S ` F ) = ( S ` G ) ) )
30 20 25 13 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) /\ ( F o. `' G ) =/= ( _I |` B ) ) -> `' G e. T )
31 2 3 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ `' G e. T ) -> ( F o. `' G ) e. T )
32 20 22 30 31 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) /\ ( F o. `' G ) =/= ( _I |` B ) ) -> ( F o. `' G ) e. T )
33 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) /\ ( F o. `' G ) =/= ( _I |` B ) ) -> ( F o. `' G ) =/= ( _I |` B ) )
34 1 2 3 4 5 tendoid0 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( ( F o. `' G ) e. T /\ ( F o. `' G ) =/= ( _I |` B ) ) ) -> ( ( S ` ( F o. `' G ) ) = ( _I |` B ) <-> S = O ) )
35 20 21 32 33 34 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) /\ ( F o. `' G ) =/= ( _I |` B ) ) -> ( ( S ` ( F o. `' G ) ) = ( _I |` B ) <-> S = O ) )
36 19 29 35 3bitr3d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) /\ ( F o. `' G ) =/= ( _I |` B ) ) -> ( ( S ` F ) = ( S ` G ) <-> S = O ) )
37 36 biimpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) /\ ( F o. `' G ) =/= ( _I |` B ) ) -> ( ( S ` F ) = ( S ` G ) -> S = O ) )
38 37 impancom 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) /\ ( S ` F ) = ( S ` G ) ) -> ( ( F o. `' G ) =/= ( _I |` B ) -> S = O ) )
39 38 necon1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) /\ ( S ` F ) = ( S ` G ) ) -> ( S =/= O -> ( F o. `' G ) = ( _I |` B ) ) )
40 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) /\ ( S ` F ) = ( S ` G ) ) -> ( K e. HL /\ W e. H ) )
41 simpl3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) /\ ( S ` F ) = ( S ` G ) ) -> F e. T )
42 simpl3r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) /\ ( S ` F ) = ( S ` G ) ) -> G e. T )
43 1 2 3 ltrncoidN 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( ( F o. `' G ) = ( _I |` B ) <-> F = G ) )
44 40 41 42 43 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) /\ ( S ` F ) = ( S ` G ) ) -> ( ( F o. `' G ) = ( _I |` B ) <-> F = G ) )
45 39 44 sylibd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ ( F e. T /\ G e. T ) ) /\ ( S ` F ) = ( S ` G ) ) -> ( S =/= O -> F = G ) )
46 45 3exp1 
 |-  ( ( K e. HL /\ W e. H ) -> ( S e. E -> ( ( F e. T /\ G e. T ) -> ( ( S ` F ) = ( S ` G ) -> ( S =/= O -> F = G ) ) ) ) )
47 46 com24 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( S ` F ) = ( S ` G ) -> ( ( F e. T /\ G e. T ) -> ( S e. E -> ( S =/= O -> F = G ) ) ) ) )
48 47 imp5a 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( S ` F ) = ( S ` G ) -> ( ( F e. T /\ G e. T ) -> ( ( S e. E /\ S =/= O ) -> F = G ) ) ) )
49 48 com24 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( S e. E /\ S =/= O ) -> ( ( F e. T /\ G e. T ) -> ( ( S ` F ) = ( S ` G ) -> F = G ) ) ) )
50 49 3imp 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ S =/= O ) /\ ( F e. T /\ G e. T ) ) -> ( ( S ` F ) = ( S ` G ) -> F = G ) )
51 fveq2 
 |-  ( F = G -> ( S ` F ) = ( S ` G ) )
52 50 51 impbid1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ S =/= O ) /\ ( F e. T /\ G e. T ) ) -> ( ( S ` F ) = ( S ` G ) <-> F = G ) )