# Metamath Proof Explorer

## Theorem tendoid0

Description: A trace-preserving endomorphism is the additive identity iff at least one of its values (at a non-identity translation) is the identity translation. (Contributed by NM, 1-Aug-2013)

Ref Expression
Hypotheses tendoid0.b 𝐵 = ( Base ‘ 𝐾 )
tendoid0.h 𝐻 = ( LHyp ‘ 𝐾 )
tendoid0.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendoid0.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
tendoid0.o 𝑂 = ( 𝑓𝑇 ↦ ( I ↾ 𝐵 ) )
Assertion tendoid0 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸 ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) → ( ( 𝑈𝐹 ) = ( 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 simp3l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸 ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) → 𝐹𝑇 )
7 5 1 tendo02 ( 𝐹𝑇 → ( 𝑂𝐹 ) = ( I ↾ 𝐵 ) )
8 6 7 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸 ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑂𝐹 ) = ( I ↾ 𝐵 ) )
9 8 eqeq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸 ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) → ( ( 𝑈𝐹 ) = ( 𝑂𝐹 ) ↔ ( 𝑈𝐹 ) = ( I ↾ 𝐵 ) ) )
10 simpl1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸 ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑈𝐹 ) = ( 𝑂𝐹 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
11 simpl2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸 ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑈𝐹 ) = ( 𝑂𝐹 ) ) → 𝑈𝐸 )
12 1 2 3 4 5 tendo0cl ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑂𝐸 )
13 10 12 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸 ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑈𝐹 ) = ( 𝑂𝐹 ) ) → 𝑂𝐸 )
14 simpr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸 ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑈𝐹 ) = ( 𝑂𝐹 ) ) → ( 𝑈𝐹 ) = ( 𝑂𝐹 ) )
15 simpl3l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸 ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑈𝐹 ) = ( 𝑂𝐹 ) ) → 𝐹𝑇 )
16 simpl3r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸 ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑈𝐹 ) = ( 𝑂𝐹 ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) )
17 1 2 3 4 tendocan ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝑂𝐸 ∧ ( 𝑈𝐹 ) = ( 𝑂𝐹 ) ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) → 𝑈 = 𝑂 )
18 10 11 13 14 15 16 17 syl132anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸 ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑈𝐹 ) = ( 𝑂𝐹 ) ) → 𝑈 = 𝑂 )
19 18 ex ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸 ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) → ( ( 𝑈𝐹 ) = ( 𝑂𝐹 ) → 𝑈 = 𝑂 ) )
20 9 19 sylbird ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸 ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) → ( ( 𝑈𝐹 ) = ( I ↾ 𝐵 ) → 𝑈 = 𝑂 ) )
21 fveq1 ( 𝑈 = 𝑂 → ( 𝑈𝐹 ) = ( 𝑂𝐹 ) )
22 21 eqeq1d ( 𝑈 = 𝑂 → ( ( 𝑈𝐹 ) = ( I ↾ 𝐵 ) ↔ ( 𝑂𝐹 ) = ( I ↾ 𝐵 ) ) )
23 8 22 syl5ibrcom ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸 ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) → ( 𝑈 = 𝑂 → ( 𝑈𝐹 ) = ( I ↾ 𝐵 ) ) )
24 20 23 impbid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸 ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ) → ( ( 𝑈𝐹 ) = ( I ↾ 𝐵 ) ↔ 𝑈 = 𝑂 ) )