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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
tendoid0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
tendoid0.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendoid0.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
tendoid0.o ⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
Assertion tendo1ne0 ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ≠ 𝑂 )

Proof

Step Hyp Ref Expression
1 tendoid0.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 tendoid0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 tendoid0.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 tendoid0.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
5 tendoid0.o ⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
6 1 2 3 cdlemftr0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑔 ∈ 𝑇 𝑔 ≠ ( I ↾ 𝐵 ) )
7 simp3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) → 𝑔 ≠ ( I ↾ 𝐵 ) )
8 fveq1 ⊢ ( ( I ↾ 𝑇 ) = 𝑂 → ( ( I ↾ 𝑇 ) ‘ 𝑔 ) = ( 𝑂 ‘ 𝑔 ) )
9 8 adantl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( I ↾ 𝑇 ) = 𝑂 ) → ( ( I ↾ 𝑇 ) ‘ 𝑔 ) = ( 𝑂 ‘ 𝑔 ) )
10 simpl2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( I ↾ 𝑇 ) = 𝑂 ) → 𝑔 ∈ 𝑇 )
11 fvresi ⊢ ( 𝑔 ∈ 𝑇 → ( ( I ↾ 𝑇 ) ‘ 𝑔 ) = 𝑔 )
12 10 11 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( I ↾ 𝑇 ) = 𝑂 ) → ( ( I ↾ 𝑇 ) ‘ 𝑔 ) = 𝑔 )
13 5 1 tendo02 ⊢ ( 𝑔 ∈ 𝑇 → ( 𝑂 ‘ 𝑔 ) = ( I ↾ 𝐵 ) )
14 10 13 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( I ↾ 𝑇 ) = 𝑂 ) → ( 𝑂 ‘ 𝑔 ) = ( I ↾ 𝐵 ) )
15 9 12 14 3eqtr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) ∧ ( I ↾ 𝑇 ) = 𝑂 ) → 𝑔 = ( I ↾ 𝐵 ) )
16 15 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) → ( ( I ↾ 𝑇 ) = 𝑂 → 𝑔 = ( I ↾ 𝐵 ) ) )
17 16 necon3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) → ( 𝑔 ≠ ( I ↾ 𝐵 ) → ( I ↾ 𝑇 ) ≠ 𝑂 ) )
18 7 17 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝑇 ∧ 𝑔 ≠ ( I ↾ 𝐵 ) ) → ( I ↾ 𝑇 ) ≠ 𝑂 )
19 18 rexlimdv3a ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ∃ 𝑔 ∈ 𝑇 𝑔 ≠ ( I ↾ 𝐵 ) → ( I ↾ 𝑇 ) ≠ 𝑂 ) )
20 6 19 mpd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝑇 ) ≠ 𝑂 )