Metamath Proof Explorer

Theorem trlnidatb

Description: A lattice translation is not the identity iff its trace is an atom. TODO: Can proofs be reorganized so this goes with trlnidat ? Why do both this and ltrnideq need trlnidat ? (Contributed by NM, 4-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 trlnidatb.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 trlnidatb.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 trlnidatb.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 trlnidatb.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5 trlnidatb.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
6 1 2 3 4 5 trlnidat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 )
7 6 3expia ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) )
8 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
9 8 2 3 lhpexnle ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 )
10 9 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ∃ 𝑝 ∈ 𝐴 ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 )
11 1 8 2 3 4 ltrnideq ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐹 = ( I ↾ 𝐵 ) ↔ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) )
12 11 3expa ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐹 = ( I ↾ 𝐵 ) ↔ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) )
13 simp1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
14 simp2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) )
15 simp1r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → 𝐹 ∈ 𝑇 )
16 simp3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ( 𝐹 ‘ 𝑝 ) = 𝑝 )
17 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
18 8 17 2 3 4 5 trl0 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ) → ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) )
19 13 14 15 16 18 syl112anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) )
20 19 3expia ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( 𝐹 ‘ 𝑝 ) = 𝑝 → ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) )
21 simplll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → 𝐾 ∈ HL )
22 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
23 17 2 atn0 ⊢ ( ( 𝐾 ∈ AtLat ∧ ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 0. ‘ 𝐾 ) )
24 23 ex ⊢ ( 𝐾 ∈ AtLat → ( ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 → ( 𝑅 ‘ 𝐹 ) ≠ ( 0. ‘ 𝐾 ) ) )
25 21 22 24 3syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 → ( 𝑅 ‘ 𝐹 ) ≠ ( 0. ‘ 𝐾 ) ) )
26 25 necon2bd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) → ¬ ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) )
27 20 26 syld ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( 𝐹 ‘ 𝑝 ) = 𝑝 → ¬ ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) )
28 12 27 sylbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐹 = ( I ↾ 𝐵 ) → ¬ ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) )
29 10 28 rexlimddv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐹 = ( I ↾ 𝐵 ) → ¬ ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) )
30 29 necon2ad ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 → 𝐹 ≠ ( I ↾ 𝐵 ) ) )
31 7 30 impbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) ↔ ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ) )