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

Metamath Proof Explorer

Theorem trljat3

Description: The value of a translation of an atom P not under the fiducial co-atom W , joined with trace. Equation above Lemma C in Crawley p. 112. (Contributed by NM, 22-May-2012)

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

Proof

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