# Metamath Proof Explorer

## Theorem tendocan

Description: Cancellation law: if the values of two trace-preserving endormorphisms are equal, so are the endormorphisms. Lemma J of Crawley p. 118. (Contributed by NM, 21-Jun-2013)

Ref Expression
Hypotheses tendocan.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
tendocan.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
tendocan.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
tendocan.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
Assertion tendocan ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {U}={V}$

### Proof

Step Hyp Ref Expression
1 tendocan.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 tendocan.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 tendocan.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
4 tendocan.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
5 simp1l ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {K}\in \mathrm{HL}$
6 simp1r ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {W}\in {H}$
7 simp21 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {U}\in {E}$
8 simp22 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {V}\in {E}$
9 simp11 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\right)\right)\wedge {h}\in {T}\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
10 simp12 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\right)\right)\wedge {h}\in {T}\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\to \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)$
11 simp13l ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\right)\right)\wedge {h}\in {T}\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\to {F}\in {T}$
12 simp13r ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\right)\right)\wedge {h}\in {T}\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\to {F}\ne {\mathrm{I}↾}_{{B}}$
13 simp2 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\right)\right)\wedge {h}\in {T}\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\to {h}\in {T}$
14 11 12 13 3jca ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\right)\right)\wedge {h}\in {T}\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\to \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)$
15 simp3 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\right)\right)\wedge {h}\in {T}\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\to {h}\ne {\mathrm{I}↾}_{{B}}$
16 eqid ${⊢}\mathrm{trL}\left({K}\right)\left({W}\right)=\mathrm{trL}\left({K}\right)\left({W}\right)$
17 1 2 3 16 4 cdlemj3 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\to {U}\left({h}\right)={V}\left({h}\right)$
18 9 10 14 15 17 syl31anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\right)\right)\wedge {h}\in {T}\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\to {U}\left({h}\right)={V}\left({h}\right)$
19 18 3exp ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to \left({h}\in {T}\to \left({h}\ne {\mathrm{I}↾}_{{B}}\to {U}\left({h}\right)={V}\left({h}\right)\right)\right)$
20 19 ralrimiv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to \forall {h}\in {T}\phantom{\rule{.4em}{0ex}}\left({h}\ne {\mathrm{I}↾}_{{B}}\to {U}\left({h}\right)={V}\left({h}\right)\right)$
21 1 2 3 4 tendoeq2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\right)\wedge \forall {h}\in {T}\phantom{\rule{.4em}{0ex}}\left({h}\ne {\mathrm{I}↾}_{{B}}\to {U}\left({h}\right)={V}\left({h}\right)\right)\right)\to {U}={V}$
22 5 6 7 8 20 21 syl221anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {U}={V}$