# 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 𝐵 = ( Base ‘ 𝐾 )
tendocan.h 𝐻 = ( LHyp ‘ 𝐾 )
tendocan.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendocan.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
Assertion tendocan ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸 ∧ ( 𝑈𝐹 ) = ( 𝑉𝐹 ) ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) → 𝑈 = 𝑉 )

### Proof

Step Hyp Ref Expression
1 tendocan.b 𝐵 = ( Base ‘ 𝐾 )
2 tendocan.h 𝐻 = ( LHyp ‘ 𝐾 )
3 tendocan.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 tendocan.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
5 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸 ∧ ( 𝑈𝐹 ) = ( 𝑉𝐹 ) ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) → 𝐾 ∈ HL )
6 simp1r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸 ∧ ( 𝑈𝐹 ) = ( 𝑉𝐹 ) ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) → 𝑊𝐻 )
7 simp21 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸 ∧ ( 𝑈𝐹 ) = ( 𝑉𝐹 ) ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) → 𝑈𝐸 )
8 simp22 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸 ∧ ( 𝑈𝐹 ) = ( 𝑉𝐹 ) ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) → 𝑉𝐸 )
9 simp11 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸 ∧ ( 𝑈𝐹 ) = ( 𝑉𝐹 ) ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) ∧ 𝑇 ≠ ( I ↾ 𝐵 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
10 simp12 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸 ∧ ( 𝑈𝐹 ) = ( 𝑉𝐹 ) ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) ∧ 𝑇 ≠ ( I ↾ 𝐵 ) ) → ( 𝑈𝐸𝑉𝐸 ∧ ( 𝑈𝐹 ) = ( 𝑉𝐹 ) ) )
11 simp13l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸 ∧ ( 𝑈𝐹 ) = ( 𝑉𝐹 ) ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) ∧ 𝑇 ≠ ( I ↾ 𝐵 ) ) → 𝐹𝑇 )
12 simp13r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸 ∧ ( 𝑈𝐹 ) = ( 𝑉𝐹 ) ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) ∧ 𝑇 ≠ ( I ↾ 𝐵 ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) )
13 simp2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸 ∧ ( 𝑈𝐹 ) = ( 𝑉𝐹 ) ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) ∧ 𝑇 ≠ ( I ↾ 𝐵 ) ) → 𝑇 )
14 11 12 13 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸 ∧ ( 𝑈𝐹 ) = ( 𝑉𝐹 ) ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) ∧ 𝑇 ≠ ( I ↾ 𝐵 ) ) → ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑇 ) )
15 simp3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸 ∧ ( 𝑈𝐹 ) = ( 𝑉𝐹 ) ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) ∧ 𝑇 ≠ ( I ↾ 𝐵 ) ) → ≠ ( I ↾ 𝐵 ) )
16 eqid ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
17 1 2 3 16 4 cdlemj3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸 ∧ ( 𝑈𝐹 ) = ( 𝑉𝐹 ) ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑇 ) ) ∧ ≠ ( I ↾ 𝐵 ) ) → ( 𝑈 ) = ( 𝑉 ) )
18 9 10 14 15 17 syl31anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸 ∧ ( 𝑈𝐹 ) = ( 𝑉𝐹 ) ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) ∧ 𝑇 ≠ ( I ↾ 𝐵 ) ) → ( 𝑈 ) = ( 𝑉 ) )
19 18 3exp ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸 ∧ ( 𝑈𝐹 ) = ( 𝑉𝐹 ) ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑇 → ( ≠ ( I ↾ 𝐵 ) → ( 𝑈 ) = ( 𝑉 ) ) ) )
20 19 ralrimiv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸 ∧ ( 𝑈𝐹 ) = ( 𝑉𝐹 ) ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) → ∀ 𝑇 ( ≠ ( I ↾ 𝐵 ) → ( 𝑈 ) = ( 𝑉 ) ) )
21 1 2 3 4 tendoeq2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸 ) ∧ ∀ 𝑇 ( ≠ ( I ↾ 𝐵 ) → ( 𝑈 ) = ( 𝑉 ) ) ) → 𝑈 = 𝑉 )
22 5 6 7 8 20 21 syl221anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑉𝐸 ∧ ( 𝑈𝐹 ) = ( 𝑉𝐹 ) ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) → 𝑈 = 𝑉 )