Metamath Proof Explorer


Theorem ltrnnidn

Description: If a lattice translation is not the identity, then the translation of any atom not under the fiducial co-atom W is different from the atom. Remark above Lemma C in Crawley p. 112. (Contributed by NM, 24-May-2012)

Ref Expression
Hypotheses ltrnnidn.b 𝐵 = ( Base ‘ 𝐾 )
ltrnnidn.l = ( le ‘ 𝐾 )
ltrnnidn.a 𝐴 = ( Atoms ‘ 𝐾 )
ltrnnidn.h 𝐻 = ( LHyp ‘ 𝐾 )
ltrnnidn.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion ltrnnidn ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝐹𝑃 ) ≠ 𝑃 )

Proof

Step Hyp Ref Expression
1 ltrnnidn.b 𝐵 = ( Base ‘ 𝐾 )
2 ltrnnidn.l = ( le ‘ 𝐾 )
3 ltrnnidn.a 𝐴 = ( Atoms ‘ 𝐾 )
4 ltrnnidn.h 𝐻 = ( LHyp ‘ 𝐾 )
5 ltrnnidn.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝐾 ∈ HL )
7 hlatl ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
8 6 7 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝐾 ∈ AtLat )
9 simp1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
10 simp2l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝐹𝑇 )
11 simp2r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) )
12 eqid ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
13 1 3 4 5 12 trlnidat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝐹 ) ∈ 𝐴 )
14 9 10 11 13 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝐹 ) ∈ 𝐴 )
15 eqid ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
16 15 3 atn0 ( ( 𝐾 ∈ AtLat ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝐹 ) ∈ 𝐴 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝐹 ) ≠ ( 0. ‘ 𝐾 ) )
17 8 14 16 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝐹 ) ≠ ( 0. ‘ 𝐾 ) )
18 simpl1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ∧ ( 𝐹𝑃 ) = 𝑃 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
19 simpl3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ∧ ( 𝐹𝑃 ) = 𝑃 ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
20 simpl2l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ∧ ( 𝐹𝑃 ) = 𝑃 ) → 𝐹𝑇 )
21 simpr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ∧ ( 𝐹𝑃 ) = 𝑃 ) → ( 𝐹𝑃 ) = 𝑃 )
22 2 15 3 4 5 12 trl0 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝐹𝑇 ∧ ( 𝐹𝑃 ) = 𝑃 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) )
23 18 19 20 21 22 syl112anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ∧ ( 𝐹𝑃 ) = 𝑃 ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) )
24 23 ex ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( 𝐹𝑃 ) = 𝑃 → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) )
25 24 necon3d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝐹 ) ≠ ( 0. ‘ 𝐾 ) → ( 𝐹𝑃 ) ≠ 𝑃 ) )
26 17 25 mpd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝐹𝑃 ) ≠ 𝑃 )