Theorem trlatn0

Description: The trace of a lattice translation is an atom iff it is nonzero. (Contributed by NM, 14-Jun-2013)

	Ref	Expression
Hypotheses	trl0a.z	⊢ 0 = ( 0. ‘ 𝐾 )
	trl0a.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	trl0a.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	trl0a.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	trl0a.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion	trlatn0	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ↔ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) )

Proof

Step	Hyp	Ref	Expression
1		trl0a.z	⊢ 0 = ( 0. ‘ 𝐾 )
2		trl0a.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		trl0a.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		trl0a.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5		trl0a.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
6		hlatl	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
7	6	ad3antrrr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) → 𝐾 ∈ AtLat )
8	1 2	atn0	⊢ ( ( 𝐾 ∈ AtLat ∧ ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) → ( 𝑅 ‘ 𝐹 ) ≠ 0 )
9	7 8	sylancom	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) → ( 𝑅 ‘ 𝐹 ) ≠ 0 )
10	9	ex	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 → ( 𝑅 ‘ 𝐹 ) ≠ 0 ) )
11	1 2 3 4 5	trlator0	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ∨ ( 𝑅 ‘ 𝐹 ) = 0 ) )
12	11	ord	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ¬ ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 → ( 𝑅 ‘ 𝐹 ) = 0 ) )
13	12	necon1ad	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ≠ 0 → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) )
14	10 13	impbid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ↔ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) )