Metamath Proof Explorer


Theorem trljat2

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, 25-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 trljat2 K HL W H F T P A ¬ P ˙ W F P ˙ R F = P ˙ F P

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 simp1l K HL W H F T P A ¬ P ˙ W K HL
8 1 3 4 5 ltrnat K HL W H F T P A F P A
9 8 3adant3r K HL W H F T P A ¬ P ˙ W F P A
10 7 hllatd K HL W H F T P A ¬ P ˙ W K Lat
11 simp3l K HL W H F T P A ¬ P ˙ W P A
12 eqid Base K = Base K
13 12 3 atbase P A P Base K
14 11 13 syl K HL W H F T P A ¬ P ˙ W P Base K
15 simp1 K HL W H F T P A ¬ P ˙ W K HL W H
16 simp2 K HL W H F T P A ¬ P ˙ W F T
17 12 4 5 ltrncl K HL W H F T P Base K F P Base K
18 15 16 14 17 syl3anc K HL W H F T P A ¬ P ˙ W F P Base K
19 12 2 latjcl K Lat P Base K F P Base K P ˙ F P Base K
20 10 14 18 19 syl3anc K HL W H F T P A ¬ P ˙ W P ˙ F P Base K
21 simp1r K HL W H F T P A ¬ P ˙ W W H
22 12 4 lhpbase W H W Base K
23 21 22 syl K HL W H F T P A ¬ P ˙ W W Base K
24 12 1 2 latlej2 K Lat P Base K F P Base K F P ˙ P ˙ F P
25 10 14 18 24 syl3anc K HL W H F T P A ¬ P ˙ W F P ˙ P ˙ F P
26 eqid meet K = meet K
27 12 1 2 26 3 atmod2i1 K HL F P A P ˙ F P Base K W Base K F P ˙ P ˙ F P P ˙ F P meet K W ˙ F P = P ˙ F P meet K W ˙ F P
28 7 9 20 23 25 27 syl131anc K HL W H F T P A ¬ P ˙ W P ˙ F P meet K W ˙ F P = P ˙ F P meet K W ˙ F P
29 1 3 4 5 ltrnel K HL W H F T P A ¬ P ˙ W F P A ¬ F P ˙ W
30 eqid 1. K = 1. K
31 1 2 30 3 4 lhpjat1 K HL W H F P A ¬ F P ˙ W W ˙ F P = 1. K
32 7 21 29 31 syl21anc K HL W H F T P A ¬ P ˙ W W ˙ F P = 1. K
33 32 oveq2d K HL W H F T P A ¬ P ˙ W P ˙ F P meet K W ˙ F P = P ˙ F P meet K 1. K
34 hlol K HL K OL
35 7 34 syl K HL W H F T P A ¬ P ˙ W K OL
36 12 26 30 olm11 K OL P ˙ F P Base K P ˙ F P meet K 1. K = P ˙ F P
37 35 20 36 syl2anc K HL W H F T P A ¬ P ˙ W P ˙ F P meet K 1. K = P ˙ F P
38 28 33 37 3eqtrrd K HL W H F T P A ¬ P ˙ W P ˙ F P = P ˙ F P meet K W ˙ F P
39 1 2 26 3 4 5 6 trlval2 K HL W H F T P A ¬ P ˙ W R F = P ˙ F P meet K W
40 39 oveq1d K HL W H F T P A ¬ P ˙ W R F ˙ F P = P ˙ F P meet K W ˙ F P
41 12 4 5 6 trlcl K HL W H F T R F Base K
42 15 16 41 syl2anc K HL W H F T P A ¬ P ˙ W R F Base K
43 12 2 latjcom K Lat R F Base K F P Base K R F ˙ F P = F P ˙ R F
44 10 42 18 43 syl3anc K HL W H F T P A ¬ P ˙ W R F ˙ F P = F P ˙ R F
45 38 40 44 3eqtr2rd K HL W H F T P A ¬ P ˙ W F P ˙ R F = P ˙ F P