Metamath Proof Explorer


Theorem dalawlem5

Description: Lemma for dalaw . Special case to eliminate the requirement -. ( P .\/ S ) ./\ ( Q .\/ T ) ) .<_ ( P .\/ Q ) in dalawlem1 . (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 dalawlem5 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 ˙ S ˙ T ˙ 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 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
9 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
10 5 2 4 hlatjcl K HL P A Q A P ˙ Q 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 P ˙ Q Base K
12 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
13 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
14 5 2 4 hlatjcl K HL S A T A S ˙ T Base K
15 6 12 13 14 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 ˙ T Base K
16 5 3 latmcl K Lat P ˙ Q Base K S ˙ T Base K P ˙ Q ˙ S ˙ T Base K
17 7 11 15 16 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 ˙ S ˙ T Base K
18 5 4 atbase T A T Base K
19 13 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 T Base K
20 5 2 latjcl K Lat P ˙ Q Base K T Base K P ˙ Q ˙ T Base K
21 7 11 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 P ˙ Q ˙ T Base K
22 5 4 atbase S A S Base K
23 12 22 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
24 5 3 latmcl K Lat P ˙ Q ˙ T Base K S Base K P ˙ Q ˙ T ˙ S Base K
25 7 21 23 24 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 ˙ T ˙ S Base K
26 5 2 latjcl K Lat P ˙ Q Base K S Base K P ˙ Q ˙ S Base K
27 7 11 23 26 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 ˙ S Base K
28 5 3 latmcl K Lat P ˙ Q ˙ S Base K T Base K P ˙ Q ˙ S ˙ T Base K
29 7 27 19 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 P ˙ Q ˙ S ˙ T Base K
30 5 2 latjcl K Lat P ˙ Q ˙ T ˙ S Base K P ˙ Q ˙ S ˙ T Base K P ˙ Q ˙ T ˙ S ˙ P ˙ Q ˙ S ˙ T Base K
31 7 25 29 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 P ˙ Q ˙ T ˙ S ˙ P ˙ Q ˙ S ˙ T Base K
32 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
33 5 2 4 hlatjcl K HL Q A R A Q ˙ R Base K
34 6 9 32 33 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
35 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
36 5 2 4 hlatjcl K HL T A U A T ˙ U Base K
37 6 13 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 T ˙ U Base K
38 5 3 latmcl K Lat Q ˙ R Base K T ˙ U Base K Q ˙ R ˙ T ˙ U Base K
39 7 34 37 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 Q ˙ R ˙ T ˙ U Base K
40 5 2 4 hlatjcl K HL R A P A R ˙ P Base K
41 6 32 8 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 R ˙ P Base K
42 5 2 4 hlatjcl K HL U A S A U ˙ S Base K
43 6 35 12 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 U ˙ S Base K
44 5 3 latmcl K Lat R ˙ P Base K U ˙ S Base K R ˙ P ˙ U ˙ S Base K
45 7 41 43 44 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
46 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
47 7 39 45 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 ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S Base K
48 1 2 3 4 dalawlem2 K HL P A Q A S A T A P ˙ Q ˙ S ˙ T ˙ P ˙ Q ˙ T ˙ S ˙ P ˙ Q ˙ S ˙ T
49 6 8 9 12 13 48 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 P ˙ Q ˙ S ˙ T ˙ P ˙ Q ˙ T ˙ S ˙ P ˙ Q ˙ S ˙ T
50 2 4 hlatjcom K HL P A Q A P ˙ Q = Q ˙ P
51 6 8 9 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 ˙ Q = Q ˙ P
52 51 oveq1d 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 ˙ T = Q ˙ P ˙ T
53 2 4 hlatj32 K HL Q A P A T A Q ˙ P ˙ T = Q ˙ T ˙ P
54 6 9 8 13 53 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 ˙ P ˙ T = Q ˙ T ˙ P
55 52 54 eqtrd 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 ˙ T = Q ˙ T ˙ P
56 55 oveq1d 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 ˙ T ˙ S = Q ˙ T ˙ P ˙ S
57 1 2 3 4 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
58 56 57 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 P ˙ Q ˙ T ˙ S ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
59 2 4 hlatj32 K HL P A Q A S A P ˙ Q ˙ S = P ˙ S ˙ Q
60 6 8 9 12 59 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 ˙ Q ˙ S = P ˙ S ˙ Q
61 60 oveq1d 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 ˙ S ˙ T = P ˙ S ˙ Q ˙ T
62 1 2 3 4 dalawlem4 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 ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
63 61 62 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 P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
64 5 1 2 latjle12 K Lat P ˙ Q ˙ T ˙ S Base K P ˙ Q ˙ S ˙ T Base K Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S Base K P ˙ Q ˙ T ˙ S ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S P ˙ Q ˙ T ˙ S ˙ P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
65 7 25 29 47 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 P ˙ Q ˙ T ˙ S ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S P ˙ Q ˙ T ˙ S ˙ P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
66 58 63 65 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 P ˙ Q ˙ T ˙ S ˙ P ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S
67 5 1 7 17 31 47 49 66 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 ˙ Q ˙ S ˙ T ˙ Q ˙ R ˙ T ˙ U ˙ R ˙ P ˙ U ˙ S