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 | |
|
trljat.j | |
||
trljat.a | |
||
trljat.h | |
||
trljat.t | |
||
trljat.r | |
||
Assertion | trljat3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | trljat.l | |
|
2 | trljat.j | |
|
3 | trljat.a | |
|
4 | trljat.h | |
|
5 | trljat.t | |
|
6 | trljat.r | |
|
7 | 1 2 3 4 5 6 | trljat1 | |
8 | 1 2 3 4 5 6 | trljat2 | |
9 | 7 8 | eqtr4d | |