Metamath Proof Explorer


Theorem latjlej12

Description: Add join to both sides of a lattice ordering. ( chlej12i analog.) (Contributed by NM, 8-Nov-2011)

Ref Expression
Hypotheses latlej.b B = Base K
latlej.l ˙ = K
latlej.j ˙ = join K
Assertion latjlej12 K Lat X B Y B Z B W B X ˙ Y Z ˙ W X ˙ Z ˙ Y ˙ W

Proof

Step Hyp Ref Expression
1 latlej.b B = Base K
2 latlej.l ˙ = K
3 latlej.j ˙ = join K
4 simp1 K Lat X B Y B Z B W B K Lat
5 simp2l K Lat X B Y B Z B W B X B
6 simp2r K Lat X B Y B Z B W B Y B
7 simp3l K Lat X B Y B Z B W B Z B
8 1 2 3 latjlej1 K Lat X B Y B Z B X ˙ Y X ˙ Z ˙ Y ˙ Z
9 4 5 6 7 8 syl13anc K Lat X B Y B Z B W B X ˙ Y X ˙ Z ˙ Y ˙ Z
10 simp3r K Lat X B Y B Z B W B W B
11 1 2 3 latjlej2 K Lat Z B W B Y B Z ˙ W Y ˙ Z ˙ Y ˙ W
12 4 7 10 6 11 syl13anc K Lat X B Y B Z B W B Z ˙ W Y ˙ Z ˙ Y ˙ W
13 1 3 latjcl K Lat X B Z B X ˙ Z B
14 4 5 7 13 syl3anc K Lat X B Y B Z B W B X ˙ Z B
15 1 3 latjcl K Lat Y B Z B Y ˙ Z B
16 4 6 7 15 syl3anc K Lat X B Y B Z B W B Y ˙ Z B
17 1 3 latjcl K Lat Y B W B Y ˙ W B
18 4 6 10 17 syl3anc K Lat X B Y B Z B W B Y ˙ W B
19 1 2 lattr K Lat X ˙ Z B Y ˙ Z B Y ˙ W B X ˙ Z ˙ Y ˙ Z Y ˙ Z ˙ Y ˙ W X ˙ Z ˙ Y ˙ W
20 4 14 16 18 19 syl13anc K Lat X B Y B Z B W B X ˙ Z ˙ Y ˙ Z Y ˙ Z ˙ Y ˙ W X ˙ Z ˙ Y ˙ W
21 9 12 20 syl2and K Lat X B Y B Z B W B X ˙ Y Z ˙ W X ˙ Z ˙ Y ˙ W