# Metamath Proof Explorer

## Theorem tendo1ne0

Description: The identity (unity) is not equal to the zero trace-preserving endomorphism. (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 ∈ T ⟼ I ↾ B$
Assertion tendo1ne0 $⊢ K ∈ HL ∧ W ∈ H → I ↾ T ≠ 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 ∈ T ⟼ I ↾ B$
6 1 2 3 cdlemftr0 $⊢ K ∈ HL ∧ W ∈ H → ∃ g ∈ T g ≠ I ↾ B$
7 simp3 $⊢ K ∈ HL ∧ W ∈ H ∧ g ∈ T ∧ g ≠ I ↾ B → g ≠ I ↾ B$
8 fveq1 $⊢ I ↾ T = O → I ↾ T ⁡ g = O ⁡ g$
9 8 adantl $⊢ K ∈ HL ∧ W ∈ H ∧ g ∈ T ∧ g ≠ I ↾ B ∧ I ↾ T = O → I ↾ T ⁡ g = O ⁡ g$
10 simpl2 $⊢ K ∈ HL ∧ W ∈ H ∧ g ∈ T ∧ g ≠ I ↾ B ∧ I ↾ T = O → g ∈ T$
11 fvresi $⊢ g ∈ T → I ↾ T ⁡ g = g$
12 10 11 syl $⊢ K ∈ HL ∧ W ∈ H ∧ g ∈ T ∧ g ≠ I ↾ B ∧ I ↾ T = O → I ↾ T ⁡ g = g$
13 5 1 tendo02 $⊢ g ∈ T → O ⁡ g = I ↾ B$
14 10 13 syl $⊢ K ∈ HL ∧ W ∈ H ∧ g ∈ T ∧ g ≠ I ↾ B ∧ I ↾ T = O → O ⁡ g = I ↾ B$
15 9 12 14 3eqtr3d $⊢ K ∈ HL ∧ W ∈ H ∧ g ∈ T ∧ g ≠ I ↾ B ∧ I ↾ T = O → g = I ↾ B$
16 15 ex $⊢ K ∈ HL ∧ W ∈ H ∧ g ∈ T ∧ g ≠ I ↾ B → I ↾ T = O → g = I ↾ B$
17 16 necon3d $⊢ K ∈ HL ∧ W ∈ H ∧ g ∈ T ∧ g ≠ I ↾ B → g ≠ I ↾ B → I ↾ T ≠ O$
18 7 17 mpd $⊢ K ∈ HL ∧ W ∈ H ∧ g ∈ T ∧ g ≠ I ↾ B → I ↾ T ≠ O$
19 18 rexlimdv3a $⊢ K ∈ HL ∧ W ∈ H → ∃ g ∈ T g ≠ I ↾ B → I ↾ T ≠ O$
20 6 19 mpd $⊢ K ∈ HL ∧ W ∈ H → I ↾ T ≠ O$