Metamath Proof Explorer

Theorem ltrnset

Description: The set of lattice translations for a fiducial co-atom W . (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 ltrnset ( ( 𝐾 ∈ 𝐵 ∧ 𝑊 ∈ 𝐻 ) → 𝑇 = { 𝑓 ∈ 𝐷 ∣ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) ) } )

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 ltrnfset ⊢ ( 𝐾 ∈ 𝐵 → ( LTrn ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑓 ∈ ( ( LDil ‘ 𝐾 ) ‘ 𝑤 ) ∣ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑤 ) ) } ) )
9 8 fveq1d ⊢ ( 𝐾 ∈ 𝐵 → ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( 𝑤 ∈ 𝐻 ↦ { 𝑓 ∈ ( ( LDil ‘ 𝐾 ) ‘ 𝑤 ) ∣ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑤 ) ) } ) ‘ 𝑊 ) )
10 7 9 syl5eq ⊢ ( 𝐾 ∈ 𝐵 → 𝑇 = ( ( 𝑤 ∈ 𝐻 ↦ { 𝑓 ∈ ( ( LDil ‘ 𝐾 ) ‘ 𝑤 ) ∣ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑤 ) ) } ) ‘ 𝑊 ) )
11 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ( LDil ‘ 𝐾 ) ‘ 𝑤 ) = ( ( LDil ‘ 𝐾 ) ‘ 𝑊 ) )
12 11 6 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( ( LDil ‘ 𝐾 ) ‘ 𝑤 ) = 𝐷 )
13 breq2 ⊢ ( 𝑤 = 𝑊 → ( 𝑝 ≤ 𝑤 ↔ 𝑝 ≤ 𝑊 ) )
14 13 notbid ⊢ ( 𝑤 = 𝑊 → ( ¬ 𝑝 ≤ 𝑤 ↔ ¬ 𝑝 ≤ 𝑊 ) )
15 breq2 ⊢ ( 𝑤 = 𝑊 → ( 𝑞 ≤ 𝑤 ↔ 𝑞 ≤ 𝑊 ) )
16 15 notbid ⊢ ( 𝑤 = 𝑊 → ( ¬ 𝑞 ≤ 𝑤 ↔ ¬ 𝑞 ≤ 𝑊 ) )
17 14 16 anbi12d ⊢ ( 𝑤 = 𝑊 → ( ( ¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤 ) ↔ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ) )
18 oveq2 ⊢ ( 𝑤 = 𝑊 → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) )
19 oveq2 ⊢ ( 𝑤 = 𝑊 → ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑤 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) )
20 18 19 eqeq12d ⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑤 ) ↔ ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) ) )
21 17 20 imbi12d ⊢ ( 𝑤 = 𝑊 → ( ( ( ¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑤 ) ) ↔ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) )
22 21 2ralbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑤 ) ) ↔ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) ) ) )
23 12 22 rabeqbidv ⊢ ( 𝑤 = 𝑊 → { 𝑓 ∈ ( ( LDil ‘ 𝐾 ) ‘ 𝑤 ) ∣ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑤 ) ) } = { 𝑓 ∈ 𝐷 ∣ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) ) } )
24 eqid ⊢ ( 𝑤 ∈ 𝐻 ↦ { 𝑓 ∈ ( ( LDil ‘ 𝐾 ) ‘ 𝑤 ) ∣ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑤 ) ) } ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑓 ∈ ( ( LDil ‘ 𝐾 ) ‘ 𝑤 ) ∣ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑤 ) ) } )
25 6 fvexi ⊢ 𝐷 ∈ V
26 25 rabex ⊢ { 𝑓 ∈ 𝐷 ∣ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) ) } ∈ V
27 23 24 26 fvmpt ⊢ ( 𝑊 ∈ 𝐻 → ( ( 𝑤 ∈ 𝐻 ↦ { 𝑓 ∈ ( ( LDil ‘ 𝐾 ) ‘ 𝑤 ) ∣ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑤 ∧ ¬ 𝑞 ≤ 𝑤 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑤 ) ) } ) ‘ 𝑊 ) = { 𝑓 ∈ 𝐷 ∣ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) ) } )
28 10 27 sylan9eq ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑊 ∈ 𝐻 ) → 𝑇 = { 𝑓 ∈ 𝐷 ∣ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑞 ∨ ( 𝑓 ‘ 𝑞 ) ) ∧ 𝑊 ) ) } )