This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ↾ 𝐵 ) ↔ 𝑈 = 𝑂 ) )