Metamath Proof Explorer


Theorem trlval4

Description: The value of the trace of a lattice translation in terms of 2 atoms. (Contributed by NM, 3-May-2013)

Ref Expression
Hypotheses trlval3.l ˙ = K
trlval3.j ˙ = join K
trlval3.m ˙ = meet K
trlval3.a A = Atoms K
trlval3.h H = LHyp K
trlval3.t T = LTrn K W
trlval3.r R = trL K W
Assertion trlval4 K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q R F = P ˙ F P ˙ Q ˙ F Q

Proof

Step Hyp Ref Expression
1 trlval3.l ˙ = K
2 trlval3.j ˙ = join K
3 trlval3.m ˙ = meet K
4 trlval3.a A = Atoms K
5 trlval3.h H = LHyp K
6 trlval3.t T = LTrn K W
7 trlval3.r R = trL K W
8 simp1 K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q K HL W H
9 simp21 K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q F T
10 simp22 K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P A ¬ P ˙ W
11 simp23 K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q Q A ¬ Q ˙ W
12 simp3r K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q ¬ R F ˙ P ˙ Q
13 simpl1l K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q K HL
14 simp23l K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q Q A
15 14 adantr K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q Q A
16 simpl1 K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q K HL W H
17 simpl21 K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q F T
18 1 4 5 6 ltrnat K HL W H F T Q A F Q A
19 16 17 15 18 syl3anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q F Q A
20 1 2 4 hlatlej1 K HL Q A F Q A Q ˙ Q ˙ F Q
21 13 15 19 20 syl3anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q Q ˙ Q ˙ F Q
22 simpl22 K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q P A ¬ P ˙ W
23 1 2 4 5 6 7 trljat1 K HL W H F T P A ¬ P ˙ W P ˙ R F = P ˙ F P
24 16 17 22 23 syl3anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q P ˙ R F = P ˙ F P
25 simpr K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q P ˙ F P = Q ˙ F Q
26 24 25 eqtrd K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q P ˙ R F = Q ˙ F Q
27 21 26 breqtrrd K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q Q ˙ P ˙ R F
28 simpl3r K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q ¬ R F ˙ P ˙ Q
29 simpll1 K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q F P = P K HL W H
30 22 adantr K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q F P = P P A ¬ P ˙ W
31 17 adantr K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q F P = P F T
32 simpr K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q F P = P F P = P
33 eqid 0. K = 0. K
34 1 33 4 5 6 7 trl0 K HL W H P A ¬ P ˙ W F T F P = P R F = 0. K
35 29 30 31 32 34 syl112anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q F P = P R F = 0. K
36 hlatl K HL K AtLat
37 13 36 syl K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q K AtLat
38 simp22l K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P A
39 38 adantr K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q P A
40 eqid Base K = Base K
41 40 2 4 hlatjcl K HL P A Q A P ˙ Q Base K
42 13 39 15 41 syl3anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q P ˙ Q Base K
43 40 1 33 atl0le K AtLat P ˙ Q Base K 0. K ˙ P ˙ Q
44 37 42 43 syl2anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q 0. K ˙ P ˙ Q
45 44 adantr K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q F P = P 0. K ˙ P ˙ Q
46 35 45 eqbrtrd K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q F P = P R F ˙ P ˙ Q
47 46 ex K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q F P = P R F ˙ P ˙ Q
48 47 necon3bd K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q ¬ R F ˙ P ˙ Q F P P
49 28 48 mpd K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q F P P
50 1 4 5 6 7 trlat K HL W H P A ¬ P ˙ W F T F P P R F A
51 16 22 17 49 50 syl112anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q R F A
52 simpl3l K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q P Q
53 52 necomd K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q Q P
54 1 2 4 hlatexch1 K HL Q A R F A P A Q P Q ˙ P ˙ R F R F ˙ P ˙ Q
55 13 15 51 39 53 54 syl131anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q Q ˙ P ˙ R F R F ˙ P ˙ Q
56 27 55 mpd K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q R F ˙ P ˙ Q
57 56 ex K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P = Q ˙ F Q R F ˙ P ˙ Q
58 57 necon3bd K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q ¬ R F ˙ P ˙ Q P ˙ F P Q ˙ F Q
59 12 58 mpd K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q P ˙ F P Q ˙ F Q
60 1 2 3 4 5 6 7 trlval3 K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P ˙ F P Q ˙ F Q R F = P ˙ F P ˙ Q ˙ F Q
61 8 9 10 11 59 60 syl113anc K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ R F ˙ P ˙ Q R F = P ˙ F P ˙ Q ˙ F Q