Metamath Proof Explorer


Theorem dalawlem3

Description: Lemma for dalaw . First piece of dalawlem5 . (Contributed by NM, 4-Oct-2012)

Ref Expression
Hypotheses dalawlem.l ˙ = K
dalawlem.j ˙ = join K
dalawlem.m ˙ = meet K
dalawlem.a A = Atoms K
Assertion dalawlem3 K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S

Proof

Step Hyp Ref Expression
1 dalawlem.l ˙ = K
2 dalawlem.j ˙ = join K
3 dalawlem.m ˙ = meet K
4 dalawlem.a A = Atoms K
5 eqid Base K = Base K
6 simp11 K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A K HL
7 6 hllatd K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A K Lat
8 simp22 K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q A
9 simp32 K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A T A
10 5 2 4 hlatjcl K HL Q A T A Q ˙ T Base K
11 6 8 9 10 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T Base K
12 simp21 K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P A
13 5 4 atbase P A P Base K
14 12 13 syl K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P Base K
15 5 2 latjcl K Lat Q ˙ T Base K P Base K Q ˙ T ˙ P Base K
16 7 11 14 15 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P Base K
17 simp31 K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A S A
18 5 4 atbase S A S Base K
19 17 18 syl K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A S Base K
20 5 3 latmcl K Lat Q ˙ T ˙ P Base K S Base K Q ˙ T ˙ P ˙ S Base K
21 7 16 19 20 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S Base K
22 simp23 K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A R A
23 5 2 4 hlatjcl K HL Q A R A Q ˙ R Base K
24 6 8 22 23 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ R Base K
25 simp33 K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A U A
26 5 4 atbase U A U Base K
27 25 26 syl K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A U Base K
28 5 3 latmcl K Lat Q ˙ R Base K U Base K Q ˙ R ˙ U Base K
29 7 24 27 28 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ R ˙ U Base K
30 5 2 4 hlatjcl K HL R A P A R ˙ P Base K
31 6 22 12 30 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A R ˙ P Base K
32 5 2 4 hlatjcl K HL U A S A U ˙ S Base K
33 6 25 17 32 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A U ˙ S Base K
34 5 3 latmcl K Lat R ˙ P Base K U ˙ S Base K R ˙ P ˙ U ˙ S Base K
35 7 31 33 34 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A R ˙ P ˙ U ˙ S Base K
36 5 2 latjcl K Lat Q ˙ R ˙ U Base K R ˙ P ˙ U ˙ S Base K Q ˙ R ˙ U ˙ R ˙ P ˙ U ˙ S Base K
37 7 29 35 36 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ R ˙ U ˙ R ˙ P ˙ U ˙ S Base K
38 5 2 4 hlatjcl K HL T A U A T ˙ U Base K
39 6 9 25 38 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A T ˙ U Base K
40 5 3 latmcl K Lat Q ˙ R Base K T ˙ U Base K Q ˙ R ˙ T ˙ U Base K
41 7 24 39 40 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ R ˙ T ˙ U Base K
42 5 2 latjcl K Lat Q ˙ R ˙ T ˙ U Base K R ˙ P ˙ U ˙ S Base K Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S Base K
43 7 41 35 42 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S Base K
44 5 4 atbase Q A Q Base K
45 8 44 syl K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q Base K
46 5 3 latmcl K Lat Q Base K U Base K Q ˙ U Base K
47 7 45 27 46 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ U Base K
48 5 2 4 hlatjcl K HL P A S A P ˙ S Base K
49 6 12 17 48 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ S Base K
50 5 3 latmcl K Lat P ˙ S Base K Q Base K P ˙ S ˙ Q Base K
51 7 49 45 50 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ S ˙ Q Base K
52 5 2 latjcl K Lat Q ˙ U Base K P ˙ S ˙ Q Base K Q ˙ U ˙ P ˙ S ˙ Q Base K
53 7 47 51 52 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ U ˙ P ˙ S ˙ Q Base K
54 5 2 latjcl K Lat P Base K Q ˙ U ˙ P ˙ S ˙ Q Base K P ˙ Q ˙ U ˙ P ˙ S ˙ Q Base K
55 7 14 53 54 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ U ˙ P ˙ S ˙ Q Base K
56 5 4 atbase R A R Base K
57 22 56 syl K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A R Base K
58 5 2 latjcl K Lat R Base K Q ˙ R ˙ U Base K R ˙ Q ˙ R ˙ U Base K
59 7 57 29 58 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A R ˙ Q ˙ R ˙ U Base K
60 5 2 latjcl K Lat P Base K R ˙ Q ˙ R ˙ U Base K P ˙ R ˙ Q ˙ R ˙ U Base K
61 7 14 59 60 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ R ˙ Q ˙ R ˙ U Base K
62 5 2 latjcl K Lat Q ˙ U Base K P Base K Q ˙ U ˙ P Base K
63 7 47 14 62 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ U ˙ P Base K
64 5 1 2 3 latmlej22 K Lat S Base K Q ˙ T ˙ P Base K Q ˙ U ˙ P Base K Q ˙ T ˙ P ˙ S ˙ Q ˙ U ˙ P ˙ S
65 7 19 16 63 64 syl13anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S ˙ Q ˙ U ˙ P ˙ S
66 5 2 latjass K Lat Q ˙ U Base K P Base K S Base K Q ˙ U ˙ P ˙ S = Q ˙ U ˙ P ˙ S
67 7 47 14 19 66 syl13anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ U ˙ P ˙ S = Q ˙ U ˙ P ˙ S
68 65 67 breqtrd K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S ˙ Q ˙ U ˙ P ˙ S
69 5 3 latmcl K Lat Q ˙ T Base K P ˙ S Base K Q ˙ T ˙ P ˙ S Base K
70 7 11 49 69 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S Base K
71 5 2 latjcl K Lat Q ˙ T ˙ P ˙ S Base K P Base K Q ˙ T ˙ P ˙ S ˙ P Base K
72 7 70 14 71 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S ˙ P Base K
73 5 2 4 hlatjcl K HL P A Q A P ˙ Q Base K
74 6 12 8 73 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q Base K
75 1 2 4 hlatlej2 K HL P A S A S ˙ P ˙ S
76 6 12 17 75 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A S ˙ P ˙ S
77 5 1 3 latmlem2 K Lat S Base K P ˙ S Base K Q ˙ T ˙ P Base K S ˙ P ˙ S Q ˙ T ˙ P ˙ S ˙ Q ˙ T ˙ P ˙ P ˙ S
78 7 19 49 16 77 syl13anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A S ˙ P ˙ S Q ˙ T ˙ P ˙ S ˙ Q ˙ T ˙ P ˙ P ˙ S
79 76 78 mpd K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S ˙ Q ˙ T ˙ P ˙ P ˙ S
80 1 2 4 hlatlej1 K HL P A S A P ˙ P ˙ S
81 6 12 17 80 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ P ˙ S
82 5 1 2 3 4 atmod4i1 K HL P A Q ˙ T Base K P ˙ S Base K P ˙ P ˙ S Q ˙ T ˙ P ˙ S ˙ P = Q ˙ T ˙ P ˙ P ˙ S
83 6 12 11 49 81 82 syl131anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S ˙ P = Q ˙ T ˙ P ˙ P ˙ S
84 79 83 breqtrrd K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S ˙ Q ˙ T ˙ P ˙ S ˙ P
85 5 3 latmcom K Lat Q ˙ T Base K P ˙ S Base K Q ˙ T ˙ P ˙ S = P ˙ S ˙ Q ˙ T
86 7 11 49 85 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S = P ˙ S ˙ Q ˙ T
87 simp12 K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ S ˙ Q ˙ T ˙ P ˙ Q
88 86 87 eqbrtrd K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S ˙ P ˙ Q
89 1 2 4 hlatlej1 K HL P A Q A P ˙ P ˙ Q
90 6 12 8 89 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ P ˙ Q
91 5 1 2 latjle12 K Lat Q ˙ T ˙ P ˙ S Base K P Base K P ˙ Q Base K Q ˙ T ˙ P ˙ S ˙ P ˙ Q P ˙ P ˙ Q Q ˙ T ˙ P ˙ S ˙ P ˙ P ˙ Q
92 7 70 14 74 91 syl13anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S ˙ P ˙ Q P ˙ P ˙ Q Q ˙ T ˙ P ˙ S ˙ P ˙ P ˙ Q
93 88 90 92 mpbi2and K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S ˙ P ˙ P ˙ Q
94 5 1 7 21 72 74 84 93 lattrd K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S ˙ P ˙ Q
95 5 2 latjcl K Lat Q ˙ U Base K P ˙ S Base K Q ˙ U ˙ P ˙ S Base K
96 7 47 49 95 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ U ˙ P ˙ S Base K
97 5 1 3 latlem12 K Lat Q ˙ T ˙ P ˙ S Base K Q ˙ U ˙ P ˙ S Base K P ˙ Q Base K Q ˙ T ˙ P ˙ S ˙ Q ˙ U ˙ P ˙ S Q ˙ T ˙ P ˙ S ˙ P ˙ Q Q ˙ T ˙ P ˙ S ˙ Q ˙ U ˙ P ˙ S ˙ P ˙ Q
98 7 21 96 74 97 syl13anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S ˙ Q ˙ U ˙ P ˙ S Q ˙ T ˙ P ˙ S ˙ P ˙ Q Q ˙ T ˙ P ˙ S ˙ Q ˙ U ˙ P ˙ S ˙ P ˙ Q
99 68 94 98 mpbi2and K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S ˙ Q ˙ U ˙ P ˙ S ˙ P ˙ Q
100 5 1 2 3 4 atmod3i1 K HL P A P ˙ S Base K Q Base K P ˙ P ˙ S P ˙ P ˙ S ˙ Q = P ˙ S ˙ P ˙ Q
101 6 12 49 45 81 100 syl131anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ P ˙ S ˙ Q = P ˙ S ˙ P ˙ Q
102 101 oveq2d K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ U ˙ P ˙ P ˙ S ˙ Q = Q ˙ U ˙ P ˙ S ˙ P ˙ Q
103 5 2 latj12 K Lat Q ˙ U Base K P Base K P ˙ S ˙ Q Base K Q ˙ U ˙ P ˙ P ˙ S ˙ Q = P ˙ Q ˙ U ˙ P ˙ S ˙ Q
104 7 47 14 51 103 syl13anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ U ˙ P ˙ P ˙ S ˙ Q = P ˙ Q ˙ U ˙ P ˙ S ˙ Q
105 5 1 2 3 latmlej12 K Lat Q Base K U Base K P Base K Q ˙ U ˙ P ˙ Q
106 7 45 27 14 105 syl13anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ U ˙ P ˙ Q
107 5 1 2 3 4 atmod1i1m K HL U A Q Base K P ˙ S Base K P ˙ Q Base K Q ˙ U ˙ P ˙ Q Q ˙ U ˙ P ˙ S ˙ P ˙ Q = Q ˙ U ˙ P ˙ S ˙ P ˙ Q
108 6 25 45 49 74 106 107 syl231anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ U ˙ P ˙ S ˙ P ˙ Q = Q ˙ U ˙ P ˙ S ˙ P ˙ Q
109 102 104 108 3eqtr3rd K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ U ˙ P ˙ S ˙ P ˙ Q = P ˙ Q ˙ U ˙ P ˙ S ˙ Q
110 99 109 breqtrd K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S ˙ P ˙ Q ˙ U ˙ P ˙ S ˙ Q
111 1 2 4 hlatlej1 K HL Q A R A Q ˙ Q ˙ R
112 6 8 22 111 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ Q ˙ R
113 1 2 4 hlatlej2 K HL R A U A U ˙ R ˙ U
114 6 22 25 113 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A U ˙ R ˙ U
115 5 3 latmcl K Lat P ˙ S Base K Q ˙ T Base K P ˙ S ˙ Q ˙ T Base K
116 7 49 11 115 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ S ˙ Q ˙ T Base K
117 5 2 4 hlatjcl K HL R A U A R ˙ U Base K
118 6 22 25 117 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A R ˙ U Base K
119 1 2 4 hlatlej1 K HL Q A T A Q ˙ Q ˙ T
120 6 8 9 119 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ Q ˙ T
121 5 1 3 latmlem2 K Lat Q Base K Q ˙ T Base K P ˙ S Base K Q ˙ Q ˙ T P ˙ S ˙ Q ˙ P ˙ S ˙ Q ˙ T
122 7 45 11 49 121 syl13anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ Q ˙ T P ˙ S ˙ Q ˙ P ˙ S ˙ Q ˙ T
123 120 122 mpd K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ S ˙ Q ˙ P ˙ S ˙ Q ˙ T
124 simp13 K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ S ˙ Q ˙ T ˙ R ˙ U
125 5 1 7 51 116 118 123 124 lattrd K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ S ˙ Q ˙ R ˙ U
126 5 1 2 latjle12 K Lat U Base K P ˙ S ˙ Q Base K R ˙ U Base K U ˙ R ˙ U P ˙ S ˙ Q ˙ R ˙ U U ˙ P ˙ S ˙ Q ˙ R ˙ U
127 7 27 51 118 126 syl13anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A U ˙ R ˙ U P ˙ S ˙ Q ˙ R ˙ U U ˙ P ˙ S ˙ Q ˙ R ˙ U
128 114 125 127 mpbi2and K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A U ˙ P ˙ S ˙ Q ˙ R ˙ U
129 5 2 latjcl K Lat U Base K P ˙ S ˙ Q Base K U ˙ P ˙ S ˙ Q Base K
130 7 27 51 129 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A U ˙ P ˙ S ˙ Q Base K
131 5 1 3 latmlem12 K Lat Q Base K Q ˙ R Base K U ˙ P ˙ S ˙ Q Base K R ˙ U Base K Q ˙ Q ˙ R U ˙ P ˙ S ˙ Q ˙ R ˙ U Q ˙ U ˙ P ˙ S ˙ Q ˙ Q ˙ R ˙ R ˙ U
132 7 45 24 130 118 131 syl122anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ Q ˙ R U ˙ P ˙ S ˙ Q ˙ R ˙ U Q ˙ U ˙ P ˙ S ˙ Q ˙ Q ˙ R ˙ R ˙ U
133 112 128 132 mp2and K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ U ˙ P ˙ S ˙ Q ˙ Q ˙ R ˙ R ˙ U
134 5 1 3 latmle2 K Lat P ˙ S Base K Q Base K P ˙ S ˙ Q ˙ Q
135 7 49 45 134 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ S ˙ Q ˙ Q
136 5 1 2 3 4 atmod2i2 K HL U A Q Base K P ˙ S ˙ Q Base K P ˙ S ˙ Q ˙ Q Q ˙ U ˙ P ˙ S ˙ Q = Q ˙ U ˙ P ˙ S ˙ Q
137 6 25 45 51 135 136 syl131anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ U ˙ P ˙ S ˙ Q = Q ˙ U ˙ P ˙ S ˙ Q
138 1 2 4 hlatlej2 K HL Q A R A R ˙ Q ˙ R
139 6 8 22 138 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A R ˙ Q ˙ R
140 5 1 2 3 4 atmod3i2 K HL U A R Base K Q ˙ R Base K R ˙ Q ˙ R R ˙ Q ˙ R ˙ U = Q ˙ R ˙ R ˙ U
141 6 25 57 24 139 140 syl131anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A R ˙ Q ˙ R ˙ U = Q ˙ R ˙ R ˙ U
142 133 137 141 3brtr4d K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ U ˙ P ˙ S ˙ Q ˙ R ˙ Q ˙ R ˙ U
143 5 1 2 latjlej2 K Lat Q ˙ U ˙ P ˙ S ˙ Q Base K R ˙ Q ˙ R ˙ U Base K P Base K Q ˙ U ˙ P ˙ S ˙ Q ˙ R ˙ Q ˙ R ˙ U P ˙ Q ˙ U ˙ P ˙ S ˙ Q ˙ P ˙ R ˙ Q ˙ R ˙ U
144 7 53 59 14 143 syl13anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ U ˙ P ˙ S ˙ Q ˙ R ˙ Q ˙ R ˙ U P ˙ Q ˙ U ˙ P ˙ S ˙ Q ˙ P ˙ R ˙ Q ˙ R ˙ U
145 142 144 mpd K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ Q ˙ U ˙ P ˙ S ˙ Q ˙ P ˙ R ˙ Q ˙ R ˙ U
146 5 1 7 21 55 61 110 145 lattrd K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S ˙ P ˙ R ˙ Q ˙ R ˙ U
147 5 2 latj13 K Lat P Base K R Base K Q ˙ R ˙ U Base K P ˙ R ˙ Q ˙ R ˙ U = Q ˙ R ˙ U ˙ R ˙ P
148 7 14 57 29 147 syl13anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A P ˙ R ˙ Q ˙ R ˙ U = Q ˙ R ˙ U ˙ R ˙ P
149 146 148 breqtrd K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S ˙ Q ˙ R ˙ U ˙ R ˙ P
150 5 1 2 3 latmlej22 K Lat S Base K Q ˙ T ˙ P Base K U Base K Q ˙ T ˙ P ˙ S ˙ U ˙ S
151 7 19 16 27 150 syl13anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S ˙ U ˙ S
152 5 2 latjcl K Lat Q ˙ R ˙ U Base K R ˙ P Base K Q ˙ R ˙ U ˙ R ˙ P Base K
153 7 29 31 152 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ R ˙ U ˙ R ˙ P Base K
154 5 1 3 latlem12 K Lat Q ˙ T ˙ P ˙ S Base K Q ˙ R ˙ U ˙ R ˙ P Base K U ˙ S Base K Q ˙ T ˙ P ˙ S ˙ Q ˙ R ˙ U ˙ R ˙ P Q ˙ T ˙ P ˙ S ˙ U ˙ S Q ˙ T ˙ P ˙ S ˙ Q ˙ R ˙ U ˙ R ˙ P ˙ U ˙ S
155 7 21 153 33 154 syl13anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S ˙ Q ˙ R ˙ U ˙ R ˙ P Q ˙ T ˙ P ˙ S ˙ U ˙ S Q ˙ T ˙ P ˙ S ˙ Q ˙ R ˙ U ˙ R ˙ P ˙ U ˙ S
156 149 151 155 mpbi2and K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S ˙ Q ˙ R ˙ U ˙ R ˙ P ˙ U ˙ S
157 5 1 2 3 latmlej21 K Lat U Base K Q ˙ R Base K S Base K Q ˙ R ˙ U ˙ U ˙ S
158 7 27 24 19 157 syl13anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ R ˙ U ˙ U ˙ S
159 5 1 2 3 4 atmod1i1m K HL U A Q ˙ R Base K R ˙ P Base K U ˙ S Base K Q ˙ R ˙ U ˙ U ˙ S Q ˙ R ˙ U ˙ R ˙ P ˙ U ˙ S = Q ˙ R ˙ U ˙ R ˙ P ˙ U ˙ S
160 6 25 24 31 33 158 159 syl231anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ R ˙ U ˙ R ˙ P ˙ U ˙ S = Q ˙ R ˙ U ˙ R ˙ P ˙ U ˙ S
161 156 160 breqtrrd K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S ˙ Q ˙ R ˙ U ˙ R ˙ P ˙ U ˙ S
162 1 2 4 hlatlej2 K HL T A U A U ˙ T ˙ U
163 6 9 25 162 syl3anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A U ˙ T ˙ U
164 5 1 3 latmlem2 K Lat U Base K T ˙ U Base K Q ˙ R Base K U ˙ T ˙ U Q ˙ R ˙ U ˙ Q ˙ R ˙ T ˙ U
165 7 27 39 24 164 syl13anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A U ˙ T ˙ U Q ˙ R ˙ U ˙ Q ˙ R ˙ T ˙ U
166 163 165 mpd K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ R ˙ U ˙ Q ˙ R ˙ T ˙ U
167 5 1 2 latjlej1 K Lat Q ˙ R ˙ U Base K Q ˙ R ˙ T ˙ U Base K R ˙ P ˙ U ˙ S Base K Q ˙ R ˙ U ˙ Q ˙ R ˙ T ˙ U Q ˙ R ˙ U ˙ R ˙ P ˙ U ˙ S ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
168 7 29 41 35 167 syl13anc K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ R ˙ U ˙ Q ˙ R ˙ T ˙ U Q ˙ R ˙ U ˙ R ˙ P ˙ U ˙ S ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
169 166 168 mpd K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ R ˙ U ˙ R ˙ P ˙ U ˙ S ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
170 5 1 7 21 37 43 161 169 lattrd K HL P ˙ S ˙ Q ˙ T ˙ P ˙ Q P ˙ S ˙ Q ˙ T ˙ R ˙ U P A Q A R A S A T A U A Q ˙ T ˙ P ˙ S ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S