This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi ⊢ ( ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝐹 ∈ 𝑇 → ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) )
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 ⊢ ( ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) = ( ( 𝑄 ∨ ( 𝐹 ‘ 𝑄 ) ) ∧ 𝑊 ) )