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