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 | |- .<_ = ( le ` 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 e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .\/ ( R ` F ) ) = ( ( F ` P ) .\/ ( R ` F ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | trljat.l | |- .<_ = ( le ` 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 e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .\/ ( R ` F ) ) = ( P .\/ ( F ` P ) ) ) |
| 8 | 1 2 3 4 5 6 | trljat2 | |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) .\/ ( R ` F ) ) = ( P .\/ ( F ` P ) ) ) |
| 9 | 7 8 | eqtr4d | |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .\/ ( R ` F ) ) = ( ( F ` P ) .\/ ( R ` F ) ) ) |