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 ↾ 𝑇 ) ≠ 𝑂 )