Theorem trlid0b

Description: A lattice translation is the identity iff its trace is zero. (Contributed by NM, 14-Jun-2013)

	Ref	Expression
Hypotheses	trlid0b.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	trlid0b.z	⊢ 0 = ( 0. ‘ 𝐾 )
	trlid0b.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	trlid0b.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	trlid0b.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion	trlid0b	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐹 = ( I ↾ 𝐵 ) ↔ ( 𝑅 ‘ 𝐹 ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		trlid0b.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		trlid0b.z	⊢ 0 = ( 0. ‘ 𝐾 )
3		trlid0b.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		trlid0b.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5		trlid0b.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
6		eqid	⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
7	1 6 3 4 5	trlnidatb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) ↔ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) )
8	2 6 3 4 5	trlatn0	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ↔ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) )
9	7 8	bitrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) ↔ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) )
10	9	necon4bid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐹 = ( I ↾ 𝐵 ) ↔ ( 𝑅 ‘ 𝐹 ) = 0 ) )