Metamath Proof Explorer


Theorem dalawlem2

Description: Lemma for dalaw . Utility lemma that breaks ( ( P .\/ Q ) ./\ ( S .\/ T ) ) into a join of two pieces. (Contributed by NM, 6-Oct-2012)

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

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 simp1 K HL P A Q A S A T A K HL
6 5 hllatd K HL P A Q A S A T A K Lat
7 simp2l K HL P A Q A S A T A P A
8 simp2r K HL P A Q A S A T A Q A
9 eqid Base K = Base K
10 9 2 4 hlatjcl K HL P A Q A P ˙ Q Base K
11 5 7 8 10 syl3anc K HL P A Q A S A T A P ˙ Q Base K
12 simp3r K HL P A Q A S A T A T A
13 9 4 atbase T A T Base K
14 12 13 syl K HL P A Q A S A T A T Base K
15 9 1 2 latlej1 K Lat P ˙ Q Base K T Base K P ˙ Q ˙ P ˙ Q ˙ T
16 6 11 14 15 syl3anc K HL P A Q A S A T A P ˙ Q ˙ P ˙ Q ˙ T
17 simp3l K HL P A Q A S A T A S A
18 9 4 atbase S A S Base K
19 17 18 syl K HL P A Q A S A T A S Base K
20 9 1 2 latlej1 K Lat P ˙ Q Base K S Base K P ˙ Q ˙ P ˙ Q ˙ S
21 6 11 19 20 syl3anc K HL P A Q A S A T A P ˙ Q ˙ P ˙ Q ˙ S
22 9 2 latjcl K Lat P ˙ Q Base K T Base K P ˙ Q ˙ T Base K
23 6 11 14 22 syl3anc K HL P A Q A S A T A P ˙ Q ˙ T Base K
24 9 2 latjcl K Lat P ˙ Q Base K S Base K P ˙ Q ˙ S Base K
25 6 11 19 24 syl3anc K HL P A Q A S A T A P ˙ Q ˙ S Base K
26 9 1 3 latlem12 K Lat P ˙ Q Base K P ˙ Q ˙ T Base K P ˙ Q ˙ S Base K P ˙ Q ˙ P ˙ Q ˙ T P ˙ Q ˙ P ˙ Q ˙ S P ˙ Q ˙ P ˙ Q ˙ T ˙ P ˙ Q ˙ S
27 6 11 23 25 26 syl13anc K HL P A Q A S A T A P ˙ Q ˙ P ˙ Q ˙ T P ˙ Q ˙ P ˙ Q ˙ S P ˙ Q ˙ P ˙ Q ˙ T ˙ P ˙ Q ˙ S
28 16 21 27 mpbi2and K HL P A Q A S A T A P ˙ Q ˙ P ˙ Q ˙ T ˙ P ˙ Q ˙ S
29 9 3 latmcl K Lat P ˙ Q ˙ T Base K P ˙ Q ˙ S Base K P ˙ Q ˙ T ˙ P ˙ Q ˙ S Base K
30 6 23 25 29 syl3anc K HL P A Q A S A T A P ˙ Q ˙ T ˙ P ˙ Q ˙ S Base K
31 9 2 4 hlatjcl K HL S A T A S ˙ T Base K
32 5 17 12 31 syl3anc K HL P A Q A S A T A S ˙ T Base K
33 9 1 3 latmlem1 K Lat P ˙ Q Base K P ˙ Q ˙ T ˙ P ˙ Q ˙ S Base K S ˙ T Base K P ˙ Q ˙ P ˙ Q ˙ T ˙ P ˙ Q ˙ S P ˙ Q ˙ S ˙ T ˙ P ˙ Q ˙ T ˙ P ˙ Q ˙ S ˙ S ˙ T
34 6 11 30 32 33 syl13anc K HL P A Q A S A T A P ˙ Q ˙ P ˙ Q ˙ T ˙ P ˙ Q ˙ S P ˙ Q ˙ S ˙ T ˙ P ˙ Q ˙ T ˙ P ˙ Q ˙ S ˙ S ˙ T
35 28 34 mpd K HL P A Q A S A T A P ˙ Q ˙ S ˙ T ˙ P ˙ Q ˙ T ˙ P ˙ Q ˙ S ˙ S ˙ T
36 9 1 2 latlej2 K Lat P ˙ Q Base K S Base K S ˙ P ˙ Q ˙ S
37 6 11 19 36 syl3anc K HL P A Q A S A T A S ˙ P ˙ Q ˙ S
38 9 1 2 3 4 atmod3i1 K HL S A P ˙ Q ˙ S Base K T Base K S ˙ P ˙ Q ˙ S S ˙ P ˙ Q ˙ S ˙ T = P ˙ Q ˙ S ˙ S ˙ T
39 5 17 25 14 37 38 syl131anc K HL P A Q A S A T A S ˙ P ˙ Q ˙ S ˙ T = P ˙ Q ˙ S ˙ S ˙ T
40 39 oveq2d K HL P A Q A S A T A P ˙ Q ˙ T ˙ S ˙ P ˙ Q ˙ S ˙ T = P ˙ Q ˙ T ˙ P ˙ Q ˙ S ˙ S ˙ T
41 9 3 latmcl K Lat P ˙ Q ˙ S Base K T Base K P ˙ Q ˙ S ˙ T Base K
42 6 25 14 41 syl3anc K HL P A Q A S A T A P ˙ Q ˙ S ˙ T Base K
43 9 1 2 3 latmlej22 K Lat T Base K P ˙ Q ˙ S Base K P ˙ Q Base K P ˙ Q ˙ S ˙ T ˙ P ˙ Q ˙ T
44 6 14 25 11 43 syl13anc K HL P A Q A S A T A P ˙ Q ˙ S ˙ T ˙ P ˙ Q ˙ T
45 9 1 2 3 4 atmod2i2 K HL S A P ˙ Q ˙ T Base K P ˙ Q ˙ S ˙ T Base K P ˙ Q ˙ S ˙ T ˙ P ˙ Q ˙ T P ˙ Q ˙ T ˙ S ˙ P ˙ Q ˙ S ˙ T = P ˙ Q ˙ T ˙ S ˙ P ˙ Q ˙ S ˙ T
46 5 17 23 42 44 45 syl131anc K HL P A Q A S A T A P ˙ Q ˙ T ˙ S ˙ P ˙ Q ˙ S ˙ T = P ˙ Q ˙ T ˙ S ˙ P ˙ Q ˙ S ˙ T
47 hlol K HL K OL
48 5 47 syl K HL P A Q A S A T A K OL
49 9 3 latmassOLD K OL P ˙ Q ˙ T Base K P ˙ Q ˙ S Base K S ˙ T Base K P ˙ Q ˙ T ˙ P ˙ Q ˙ S ˙ S ˙ T = P ˙ Q ˙ T ˙ P ˙ Q ˙ S ˙ S ˙ T
50 48 23 25 32 49 syl13anc K HL P A Q A S A T A P ˙ Q ˙ T ˙ P ˙ Q ˙ S ˙ S ˙ T = P ˙ Q ˙ T ˙ P ˙ Q ˙ S ˙ S ˙ T
51 40 46 50 3eqtr4rd K HL P A Q A S A T A P ˙ Q ˙ T ˙ P ˙ Q ˙ S ˙ S ˙ T = P ˙ Q ˙ T ˙ S ˙ P ˙ Q ˙ S ˙ T
52 35 51 breqtrd K HL P A Q A S A T A P ˙ Q ˙ S ˙ T ˙ P ˙ Q ˙ T ˙ S ˙ P ˙ Q ˙ S ˙ T