This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem trlval5

Description: The value of the trace of a lattice translation in terms of itself. (Contributed by NM, 19-Jul-2013)

Ref Expression
Hypotheses trlval3.l ⊢ ≤ ˙ = ≤ K
trlval3.j ⊢ ∨ ˙ = join ⁡ K
trlval3.m ⊢ ∧ ˙ = meet ⁡ K
trlval3.a ⊢ A = Atoms ⁡ K
trlval3.h ⊢ H = LHyp ⁡ K
trlval3.t ⊢ T = LTrn ⁡ K ⁡ W
trlval3.r ⊢ R = trL ⁡ K ⁡ W
Assertion trlval5 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → R ⁡ F = P ∨ ˙ R ⁡ F ∧ ˙ W

Proof

Step Hyp Ref Expression
1 trlval3.l ⊢ ≤ ˙ = ≤ K
2 trlval3.j ⊢ ∨ ˙ = join ⁡ K
3 trlval3.m ⊢ ∧ ˙ = meet ⁡ K
4 trlval3.a ⊢ A = Atoms ⁡ K
5 trlval3.h ⊢ H = LHyp ⁡ K
6 trlval3.t ⊢ T = LTrn ⁡ K ⁡ W
7 trlval3.r ⊢ R = trL ⁡ K ⁡ W
8 1 2 3 4 5 6 7 trlval2 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → R ⁡ F = P ∨ ˙ F ⁡ P ∧ ˙ W
9 1 2 4 5 6 7 trljat1 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ R ⁡ F = P ∨ ˙ F ⁡ P
10 9 oveq1d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → P ∨ ˙ R ⁡ F ∧ ˙ W = P ∨ ˙ F ⁡ P ∧ ˙ W
11 8 10 eqtr4d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → R ⁡ F = P ∨ ˙ R ⁡ F ∧ ˙ W