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 ˙=joinK
trljat.a A=AtomsK
trljat.h H=LHypK
trljat.t T=LTrnKW
trljat.r R=trLKW
Assertion trljat3 KHLWHFTPA¬P˙WP˙RF=FP˙RF

Proof

Step Hyp Ref Expression
1 trljat.l ˙=K
2 trljat.j ˙=joinK
3 trljat.a A=AtomsK
4 trljat.h H=LHypK
5 trljat.t T=LTrnKW
6 trljat.r R=trLKW
7 1 2 3 4 5 6 trljat1 KHLWHFTPA¬P˙WP˙RF=P˙FP
8 1 2 3 4 5 6 trljat2 KHLWHFTPA¬P˙WFP˙RF=P˙FP
9 7 8 eqtr4d KHLWHFTPA¬P˙WP˙RF=FP˙RF