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

Metamath Proof Explorer

Theorem tendoid0

Proof