Metamath Proof Explorer

Theorem isltrn2N

Description: The predicate "is a lattice translation". Version of isltrn that considers only different p and q . TODO: Can this eliminate some separate proofs for the p = q case? (Contributed by NM, 22-Apr-2013) (New usage is discouraged.)

Ref Expression
Hypotheses ltrnset.l ⊢ ≤ = ( le ‘ 𝐾 )
ltrnset.j ⊢ ∨ = ( join ‘ 𝐾 )
ltrnset.m ⊢ ∧ = ( meet ‘ 𝐾 )
ltrnset.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
ltrnset.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
ltrnset.d ⊢ 𝐷 = ( ( LDil ‘ 𝐾 ) ‘ 𝑊 )
ltrnset.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion isltrn2N ( ( 𝐾 ∈ 𝐵 ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 ∈ 𝑇 ↔ ( 𝐹 ∈ 𝐷 ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ltrnset.l ⊢ ≤ = ( le ‘ 𝐾 )
2 ltrnset.j ⊢ ∨ = ( join ‘ 𝐾 )
3 ltrnset.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 ltrnset.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 ltrnset.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 ltrnset.d ⊢ 𝐷 = ( ( LDil ‘ 𝐾 ) ‘ 𝑊 )
7 ltrnset.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
8 1 2 3 4 5 6 7 isltrn ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 ∈ 𝑇 ↔ ( 𝐹 ∈ 𝐷 ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) ) )
9 3simpa ⊢ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) → ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) )
10 9 imim1i ⊢ ( ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) )
11 3anass ⊢ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ↔ ( 𝑝 ≠ 𝑞 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ) )
12 3anrot ⊢ ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ↔ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) )
13 df-ne ⊢ ( 𝑝 ≠ 𝑞 ↔ ¬ 𝑝 = 𝑞 )
14 13 anbi1i ⊢ ( ( 𝑝 ≠ 𝑞 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ) ↔ ( ¬ 𝑝 = 𝑞 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ) )
15 11 12 14 3bitr3i ⊢ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) ↔ ( ¬ 𝑝 = 𝑞 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ) )
16 15 imbi1i ⊢ ( ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ↔ ( ( ¬ 𝑝 = 𝑞 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) )
17 impexp ⊢ ( ( ( ¬ 𝑝 = 𝑞 ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ↔ ( ¬ 𝑝 = 𝑞 → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) )
18 16 17 bitri ⊢ ( ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ↔ ( ¬ 𝑝 = 𝑞 → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) )
19 id ⊢ ( 𝑝 = 𝑞 → 𝑝 = 𝑞 )
20 fveq2 ⊢ ( 𝑝 = 𝑞 → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) )
21 19 20 oveq12d ⊢ ( 𝑝 = 𝑞 → ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) = ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) )
22 21 oveq1d ⊢ ( 𝑝 = 𝑞 → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) )
23 22 a1d ⊢ ( 𝑝 = 𝑞 → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) )
24 pm2.61 ⊢ ( ( 𝑝 = 𝑞 → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) → ( ( ¬ 𝑝 = 𝑞 → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) )
25 23 24 ax-mp ⊢ ( ( ¬ 𝑝 = 𝑞 → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) )
26 18 25 sylbi ⊢ ( ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) )
27 10 26 impbii ⊢ ( ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ↔ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) )
28 27 2ralbii ⊢ ( ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ↔ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) )
29 28 anbi2i ⊢ ( ( 𝐹 ∈ 𝐷 ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) ↔ ( 𝐹 ∈ 𝐷 ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) )
30 8 29 bitrdi ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 ∈ 𝑇 ↔ ( 𝐹 ∈ 𝐷 ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) ) )