Metamath Proof Explorer

Theorem trlval

Description: The value of the trace of a lattice translation. (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 trlval ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) = ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) )

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 7 8 trlset ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝑅 = ( 𝑓 ∈ 𝑇 ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) ) )
10 9 fveq1d ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑅 ‘ 𝐹 ) = ( ( 𝑓 ∈ 𝑇 ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) ) ‘ 𝐹 ) )
11 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑝 ) )
12 11 oveq2d ⊢ ( 𝑓 = 𝐹 → ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) = ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) )
13 12 oveq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) = ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) )
14 13 eqeq2d ⊢ ( 𝑓 = 𝐹 → ( 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) ↔ 𝑥 = ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) ) )
15 14 imbi2d ⊢ ( 𝑓 = 𝐹 → ( ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ↔ ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) )
16 15 ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ↔ ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) )
17 16 riotabidv ⊢ ( 𝑓 = 𝐹 → ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) = ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) )
18 eqid ⊢ ( 𝑓 ∈ 𝑇 ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) ) = ( 𝑓 ∈ 𝑇 ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) )
19 riotaex ⊢ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) ∈ V
20 17 18 19 fvmpt ⊢ ( 𝐹 ∈ 𝑇 → ( ( 𝑓 ∈ 𝑇 ↦ ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝑓 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) ) ‘ 𝐹 ) = ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) )
21 10 20 sylan9eq ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) = ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → 𝑥 = ( ( 𝑝 ∨ ( 𝐹 ‘ 𝑝 ) ) ∧ 𝑊 ) ) ) )