Metamath Proof Explorer

Theorem trlator0

Description: The trace of a lattice translation is an atom or zero. (Contributed by NM, 5-May-2013)

Ref Expression
Hypotheses trl0a.z ⊢ 0 = ( 0. ‘ 𝐾 )
trl0a.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
trl0a.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
trl0a.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
trl0a.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion trlator0 ( ( ( 𝐾 ∈ 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 df-ne ⊢ ( ( 𝑅 ‘ 𝐹 ) ≠ 0 ↔ ¬ ( 𝑅 ‘ 𝐹 ) = 0 )
7 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
8 7 2 3 lhpexnle ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 )
9 8 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) → ∃ 𝑝 ∈ 𝐴 ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 )
10 simplll ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
11 simpr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) )
12 simpllr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → 𝐹 ∈ 𝑇 )
13 simplr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝑅 ‘ 𝐹 ) ≠ 0 )
14 10 adantr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) ∧ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
15 simplr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) ∧ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) )
16 12 adantr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) ∧ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → 𝐹 ∈ 𝑇 )
17 simpr ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) ∧ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ( 𝐹 ‘ 𝑝 ) = 𝑝 )
18 7 1 2 3 4 5 trl0 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ) → ( 𝑅 ‘ 𝐹 ) = 0 )
19 14 15 16 17 18 syl112anc ⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) ∧ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ( 𝑅 ‘ 𝐹 ) = 0 )
20 19 ex ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( 𝐹 ‘ 𝑝 ) = 𝑝 → ( 𝑅 ‘ 𝐹 ) = 0 ) )
21 20 necon3d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( 𝑅 ‘ 𝐹 ) ≠ 0 → ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) )
22 13 21 mpd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 )
23 7 2 3 4 5 trlat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑝 ) ≠ 𝑝 ) ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 )
24 10 11 12 22 23 syl112anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 )
25 9 24 rexlimddv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 0 ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 )
26 25 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ≠ 0 → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) )
27 6 26 syl5bir ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ¬ ( 𝑅 ‘ 𝐹 ) = 0 → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) )
28 27 orrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) = 0 ∨ ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) )
29 28 orcomd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ∨ ( 𝑅 ‘ 𝐹 ) = 0 ) )