Metamath Proof Explorer

Theorem isltrn

Description: The predicate "is a lattice translation". Similar to definition of translation in Crawley p. 111. (Contributed by NM, 11-May-2012)

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 isltrn ( ( 𝐾 ∈ 𝐵 ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 ∈ 𝑇 ↔ ( 𝐹 ∈ 𝐷 ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) ) )

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 ltrnset ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑊 ∈ 𝐻 ) → 𝑇 = { 𝑓 ∈ 𝐷 ∣ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) ) } )
9 8 eleq2d ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 ∈ 𝑇 ↔ 𝐹 ∈ { 𝑓 ∈ 𝐷 ∣ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) ) } ) )
10 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑝 ) )
11 10 oveq2d ⊢ ( 𝑓 = 𝐹 → ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) = ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) )
12 11 oveq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) )
13 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑞 ) )
14 13 oveq2d ⊢ ( 𝑓 = 𝐹 → ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) = ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) )
15 14 oveq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) )
16 12 15 eqeq12d ⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) ↔ ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) )
17 16 imbi2d ⊢ ( 𝑓 = 𝐹 → ( ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ↔ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) )
18 17 2ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ↔ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) )
19 18 elrab ⊢ ( 𝐹 ∈ { 𝑓 ∈ 𝐷 ∣ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) ) } ↔ ( 𝐹 ∈ 𝐷 ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) )
20 9 19 bitrdi ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 ∈ 𝑇 ↔ ( 𝐹 ∈ 𝐷 ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) ) )