Metamath Proof Explorer

Theorem trlset

Description: The set of traces of lattice translations for a fiducial co-atom W . (Contributed by NM, 20-May-2012)

Ref Expression
Hypotheses trlset.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
trlset.l ⊢ ≤ = ( le ‘ 𝐾 )
trlset.j ⊢ ∨ = ( join ‘ 𝐾 )
trlset.m ⊢ ∧ = ( meet ‘ 𝐾 )
trlset.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
trlset.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
trlset.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
trlset.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion trlset ( ( 𝐾 ∈ 𝐶 ∧ 𝑊 ∈ 𝐻 ) → 𝑅 = ( 𝑓 ∈ 𝑇 ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 trlset.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 trlset.l ⊢ ≤ = ( le ‘ 𝐾 )
3 trlset.j ⊢ ∨ = ( join ‘ 𝐾 )
4 trlset.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 trlset.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 trlset.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 trlset.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
8 trlset.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
9 1 2 3 4 5 6 trlfset ⊢ ( 𝐾 ∈ 𝐶 → ( trL ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑤 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) ) ) ) ) )
10 9 fveq1d ⊢ ( 𝐾 ∈ 𝐶 → ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( 𝑤 ∈ 𝐻 ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑤 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) ) ) ) ) ‘ 𝑊 ) )
11 8 10 eqtrid ⊢ ( 𝐾 ∈ 𝐶 → 𝑅 = ( ( 𝑤 ∈ 𝐻 ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑤 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) ) ) ) ) ‘ 𝑊 ) )
12 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
13 breq2 ⊢ ( 𝑤 = 𝑊 → ( 𝑝 ≤ 𝑤 ↔ 𝑝 ≤ 𝑊 ) )
14 13 notbid ⊢ ( 𝑤 = 𝑊 → ( ¬ 𝑝 ≤ 𝑤 ↔ ¬ 𝑝 ≤ 𝑊 ) )
15 oveq2 ⊢ ( 𝑤 = 𝑊 → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) )
16 15 eqeq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) ↔ 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) ) )
17 14 16 imbi12d ⊢ ( 𝑤 = 𝑊 → ( ( ¬ 𝑝 ≤ 𝑤 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) ) ↔ ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) )
18 17 ralbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑤 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) ) ↔ ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) )
19 18 riotabidv ⊢ ( 𝑤 = 𝑊 → ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑤 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) ) ) = ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) )
20 12 19 mpteq12dv ⊢ ( 𝑤 = 𝑊 → ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑤 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) ) ) ) = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) ) )
21 eqid ⊢ ( 𝑤 ∈ 𝐻 ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑤 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) ) ) ) ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑤 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) ) ) ) )
22 fvex ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∈ V
23 22 mptex ⊢ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) ) ∈ V
24 20 21 23 fvmpt ⊢ ( 𝑊 ∈ 𝐻 → ( ( 𝑤 ∈ 𝐻 ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑤 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) ) ) ) ) ‘ 𝑊 ) = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) ) )
25 7 mpteq1i ⊢ ( 𝑓 ∈ 𝑇 ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) ) = ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) )
26 24 25 eqtr4di ⊢ ( 𝑊 ∈ 𝐻 → ( ( 𝑤 ∈ 𝐻 ↦ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑤 ) ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑤 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑤 ) ) ) ) ) ‘ 𝑊 ) = ( 𝑓 ∈ 𝑇 ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) ) )
27 11 26 sylan9eq ⊢ ( ( 𝐾 ∈ 𝐶 ∧ 𝑊 ∈ 𝐻 ) → 𝑅 = ( 𝑓 ∈ 𝑇 ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) ) )