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 ) )