Metamath Proof Explorer


Theorem ltrnu

Description: Uniqueness property of a lattice translation value for atoms not under the fiducial co-atom W . Similar to definition of translation in Crawley p. 111. (Contributed by NM, 20-May-2012)

Ref Expression
Hypotheses ltrnu.l = ( le ‘ 𝐾 )
ltrnu.j = ( join ‘ 𝐾 )
ltrnu.m = ( meet ‘ 𝐾 )
ltrnu.a 𝐴 = ( Atoms ‘ 𝐾 )
ltrnu.h 𝐻 = ( LHyp ‘ 𝐾 )
ltrnu.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion ltrnu ( ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) → ( ( 𝑃 ( 𝐹𝑃 ) ) 𝑊 ) = ( ( 𝑄 ( 𝐹𝑄 ) ) 𝑊 ) )

Proof

Step Hyp Ref Expression
1 ltrnu.l = ( le ‘ 𝐾 )
2 ltrnu.j = ( join ‘ 𝐾 )
3 ltrnu.m = ( meet ‘ 𝐾 )
4 ltrnu.a 𝐴 = ( Atoms ‘ 𝐾 )
5 ltrnu.h 𝐻 = ( LHyp ‘ 𝐾 )
6 ltrnu.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7 an4 ( ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ↔ ( ( 𝑃𝐴𝑄𝐴 ) ∧ ( ¬ 𝑃 𝑊 ∧ ¬ 𝑄 𝑊 ) ) )
8 simpr ( ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝑇 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ) → ( 𝑃𝐴𝑄𝐴 ) )
9 simplr ( ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝑇 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ) → 𝐹𝑇 )
10 eqid ( ( LDil ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LDil ‘ 𝐾 ) ‘ 𝑊 )
11 1 2 3 4 5 10 6 isltrn ( ( 𝐾𝑉𝑊𝐻 ) → ( 𝐹𝑇 ↔ ( 𝐹 ∈ ( ( LDil ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∀ 𝑝𝐴𝑞𝐴 ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ) ) )
12 11 ad2antrr ( ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝑇 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ) → ( 𝐹𝑇 ↔ ( 𝐹 ∈ ( ( LDil ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∀ 𝑝𝐴𝑞𝐴 ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ) ) )
13 simpr ( ( 𝐹 ∈ ( ( LDil ‘ 𝐾 ) ‘ 𝑊 ) ∧ ∀ 𝑝𝐴𝑞𝐴 ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ) → ∀ 𝑝𝐴𝑞𝐴 ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) )
14 12 13 syl6bi ( ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝑇 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ) → ( 𝐹𝑇 → ∀ 𝑝𝐴𝑞𝐴 ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ) )
15 9 14 mpd ( ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝑇 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ) → ∀ 𝑝𝐴𝑞𝐴 ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) )
16 breq1 ( 𝑝 = 𝑃 → ( 𝑝 𝑊𝑃 𝑊 ) )
17 16 notbid ( 𝑝 = 𝑃 → ( ¬ 𝑝 𝑊 ↔ ¬ 𝑃 𝑊 ) )
18 17 anbi1d ( 𝑝 = 𝑃 → ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) ↔ ( ¬ 𝑃 𝑊 ∧ ¬ 𝑞 𝑊 ) ) )
19 id ( 𝑝 = 𝑃𝑝 = 𝑃 )
20 fveq2 ( 𝑝 = 𝑃 → ( 𝐹𝑝 ) = ( 𝐹𝑃 ) )
21 19 20 oveq12d ( 𝑝 = 𝑃 → ( 𝑝 ( 𝐹𝑝 ) ) = ( 𝑃 ( 𝐹𝑃 ) ) )
22 21 oveq1d ( 𝑝 = 𝑃 → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑃 ( 𝐹𝑃 ) ) 𝑊 ) )
23 22 eqeq1d ( 𝑝 = 𝑃 → ( ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ↔ ( ( 𝑃 ( 𝐹𝑃 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) )
24 18 23 imbi12d ( 𝑝 = 𝑃 → ( ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ↔ ( ( ¬ 𝑃 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑃 ( 𝐹𝑃 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ) )
25 breq1 ( 𝑞 = 𝑄 → ( 𝑞 𝑊𝑄 𝑊 ) )
26 25 notbid ( 𝑞 = 𝑄 → ( ¬ 𝑞 𝑊 ↔ ¬ 𝑄 𝑊 ) )
27 26 anbi2d ( 𝑞 = 𝑄 → ( ( ¬ 𝑃 𝑊 ∧ ¬ 𝑞 𝑊 ) ↔ ( ¬ 𝑃 𝑊 ∧ ¬ 𝑄 𝑊 ) ) )
28 id ( 𝑞 = 𝑄𝑞 = 𝑄 )
29 fveq2 ( 𝑞 = 𝑄 → ( 𝐹𝑞 ) = ( 𝐹𝑄 ) )
30 28 29 oveq12d ( 𝑞 = 𝑄 → ( 𝑞 ( 𝐹𝑞 ) ) = ( 𝑄 ( 𝐹𝑄 ) ) )
31 30 oveq1d ( 𝑞 = 𝑄 → ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) = ( ( 𝑄 ( 𝐹𝑄 ) ) 𝑊 ) )
32 31 eqeq2d ( 𝑞 = 𝑄 → ( ( ( 𝑃 ( 𝐹𝑃 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ↔ ( ( 𝑃 ( 𝐹𝑃 ) ) 𝑊 ) = ( ( 𝑄 ( 𝐹𝑄 ) ) 𝑊 ) ) )
33 27 32 imbi12d ( 𝑞 = 𝑄 → ( ( ( ¬ 𝑃 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑃 ( 𝐹𝑃 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) ↔ ( ( ¬ 𝑃 𝑊 ∧ ¬ 𝑄 𝑊 ) → ( ( 𝑃 ( 𝐹𝑃 ) ) 𝑊 ) = ( ( 𝑄 ( 𝐹𝑄 ) ) 𝑊 ) ) ) )
34 24 33 rspc2v ( ( 𝑃𝐴𝑄𝐴 ) → ( ∀ 𝑝𝐴𝑞𝐴 ( ( ¬ 𝑝 𝑊 ∧ ¬ 𝑞 𝑊 ) → ( ( 𝑝 ( 𝐹𝑝 ) ) 𝑊 ) = ( ( 𝑞 ( 𝐹𝑞 ) ) 𝑊 ) ) → ( ( ¬ 𝑃 𝑊 ∧ ¬ 𝑄 𝑊 ) → ( ( 𝑃 ( 𝐹𝑃 ) ) 𝑊 ) = ( ( 𝑄 ( 𝐹𝑄 ) ) 𝑊 ) ) ) )
35 8 15 34 sylc ( ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝑇 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ) → ( ( ¬ 𝑃 𝑊 ∧ ¬ 𝑄 𝑊 ) → ( ( 𝑃 ( 𝐹𝑃 ) ) 𝑊 ) = ( ( 𝑄 ( 𝐹𝑄 ) ) 𝑊 ) ) )
36 35 impr ( ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝑇 ) ∧ ( ( 𝑃𝐴𝑄𝐴 ) ∧ ( ¬ 𝑃 𝑊 ∧ ¬ 𝑄 𝑊 ) ) ) → ( ( 𝑃 ( 𝐹𝑃 ) ) 𝑊 ) = ( ( 𝑄 ( 𝐹𝑄 ) ) 𝑊 ) )
37 7 36 sylan2b ( ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝑇 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ) → ( ( 𝑃 ( 𝐹𝑃 ) ) 𝑊 ) = ( ( 𝑄 ( 𝐹𝑄 ) ) 𝑊 ) )
38 37 3impb ( ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) → ( ( 𝑃 ( 𝐹𝑃 ) ) 𝑊 ) = ( ( 𝑄 ( 𝐹𝑄 ) ) 𝑊 ) )