Metamath Proof Explorer


Theorem latdisdlem

Description: Lemma for latdisd . (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Hypotheses latdisd.b B=BaseK
latdisd.j ˙=joinK
latdisd.m ˙=meetK
Assertion latdisdlem KLatuBvBwBu˙v˙w=u˙v˙u˙wxByBzBx˙y˙z=x˙y˙x˙z

Proof

Step Hyp Ref Expression
1 latdisd.b B=BaseK
2 latdisd.j ˙=joinK
3 latdisd.m ˙=meetK
4 1 3 latmcl KLatxByBx˙yB
5 4 3adant3r3 KLatxByBzBx˙yB
6 simpr1 KLatxByBzBxB
7 simpr3 KLatxByBzBzB
8 oveq1 u=x˙yu˙v˙w=x˙y˙v˙w
9 oveq1 u=x˙yu˙v=x˙y˙v
10 oveq1 u=x˙yu˙w=x˙y˙w
11 9 10 oveq12d u=x˙yu˙v˙u˙w=x˙y˙v˙x˙y˙w
12 8 11 eqeq12d u=x˙yu˙v˙w=u˙v˙u˙wx˙y˙v˙w=x˙y˙v˙x˙y˙w
13 oveq1 v=xv˙w=x˙w
14 13 oveq2d v=xx˙y˙v˙w=x˙y˙x˙w
15 oveq2 v=xx˙y˙v=x˙y˙x
16 15 oveq1d v=xx˙y˙v˙x˙y˙w=x˙y˙x˙x˙y˙w
17 14 16 eqeq12d v=xx˙y˙v˙w=x˙y˙v˙x˙y˙wx˙y˙x˙w=x˙y˙x˙x˙y˙w
18 oveq2 w=zx˙w=x˙z
19 18 oveq2d w=zx˙y˙x˙w=x˙y˙x˙z
20 oveq2 w=zx˙y˙w=x˙y˙z
21 20 oveq2d w=zx˙y˙x˙x˙y˙w=x˙y˙x˙x˙y˙z
22 19 21 eqeq12d w=zx˙y˙x˙w=x˙y˙x˙x˙y˙wx˙y˙x˙z=x˙y˙x˙x˙y˙z
23 12 17 22 rspc3v x˙yBxBzBuBvBwBu˙v˙w=u˙v˙u˙wx˙y˙x˙z=x˙y˙x˙x˙y˙z
24 5 6 7 23 syl3anc KLatxByBzBuBvBwBu˙v˙w=u˙v˙u˙wx˙y˙x˙z=x˙y˙x˙x˙y˙z
25 24 imp KLatxByBzBuBvBwBu˙v˙w=u˙v˙u˙wx˙y˙x˙z=x˙y˙x˙x˙y˙z
26 simpl KLatxByBzBKLat
27 1 2 latjcom KLatx˙yBxBx˙y˙x=x˙x˙y
28 26 5 6 27 syl3anc KLatxByBzBx˙y˙x=x˙x˙y
29 1 2 3 latabs1 KLatxByBx˙x˙y=x
30 29 3adant3r3 KLatxByBzBx˙x˙y=x
31 28 30 eqtrd KLatxByBzBx˙y˙x=x
32 1 2 latjcom KLatx˙yBzBx˙y˙z=z˙x˙y
33 26 5 7 32 syl3anc KLatxByBzBx˙y˙z=z˙x˙y
34 31 33 oveq12d KLatxByBzBx˙y˙x˙x˙y˙z=x˙z˙x˙y
35 34 adantr KLatxByBzBuBvBwBu˙v˙w=u˙v˙u˙wx˙y˙x˙x˙y˙z=x˙z˙x˙y
36 simpr2 KLatxByBzByB
37 oveq1 u=zu˙v˙w=z˙v˙w
38 oveq1 u=zu˙v=z˙v
39 oveq1 u=zu˙w=z˙w
40 38 39 oveq12d u=zu˙v˙u˙w=z˙v˙z˙w
41 37 40 eqeq12d u=zu˙v˙w=u˙v˙u˙wz˙v˙w=z˙v˙z˙w
42 13 oveq2d v=xz˙v˙w=z˙x˙w
43 oveq2 v=xz˙v=z˙x
44 43 oveq1d v=xz˙v˙z˙w=z˙x˙z˙w
45 42 44 eqeq12d v=xz˙v˙w=z˙v˙z˙wz˙x˙w=z˙x˙z˙w
46 oveq2 w=yx˙w=x˙y
47 46 oveq2d w=yz˙x˙w=z˙x˙y
48 oveq2 w=yz˙w=z˙y
49 48 oveq2d w=yz˙x˙z˙w=z˙x˙z˙y
50 47 49 eqeq12d w=yz˙x˙w=z˙x˙z˙wz˙x˙y=z˙x˙z˙y
51 41 45 50 rspc3v zBxByBuBvBwBu˙v˙w=u˙v˙u˙wz˙x˙y=z˙x˙z˙y
52 7 6 36 51 syl3anc KLatxByBzBuBvBwBu˙v˙w=u˙v˙u˙wz˙x˙y=z˙x˙z˙y
53 52 imp KLatxByBzBuBvBwBu˙v˙w=u˙v˙u˙wz˙x˙y=z˙x˙z˙y
54 53 oveq2d KLatxByBzBuBvBwBu˙v˙w=u˙v˙u˙wx˙z˙x˙y=x˙z˙x˙z˙y
55 1 2 latjcl KLatzBxBz˙xB
56 26 7 6 55 syl3anc KLatxByBzBz˙xB
57 1 2 latjcl KLatzByBz˙yB
58 26 7 36 57 syl3anc KLatxByBzBz˙yB
59 1 3 latmass KLatxBz˙xBz˙yBx˙z˙x˙z˙y=x˙z˙x˙z˙y
60 26 6 56 58 59 syl13anc KLatxByBzBx˙z˙x˙z˙y=x˙z˙x˙z˙y
61 1 2 latjcom KLatzBxBz˙x=x˙z
62 26 7 6 61 syl3anc KLatxByBzBz˙x=x˙z
63 62 oveq2d KLatxByBzBx˙z˙x=x˙x˙z
64 1 2 3 latabs2 KLatxBzBx˙x˙z=x
65 26 6 7 64 syl3anc KLatxByBzBx˙x˙z=x
66 63 65 eqtrd KLatxByBzBx˙z˙x=x
67 1 2 latjcom KLatzByBz˙y=y˙z
68 26 7 36 67 syl3anc KLatxByBzBz˙y=y˙z
69 66 68 oveq12d KLatxByBzBx˙z˙x˙z˙y=x˙y˙z
70 60 69 eqtr3d KLatxByBzBx˙z˙x˙z˙y=x˙y˙z
71 70 adantr KLatxByBzBuBvBwBu˙v˙w=u˙v˙u˙wx˙z˙x˙z˙y=x˙y˙z
72 54 71 eqtrd KLatxByBzBuBvBwBu˙v˙w=u˙v˙u˙wx˙z˙x˙y=x˙y˙z
73 25 35 72 3eqtrrd KLatxByBzBuBvBwBu˙v˙w=u˙v˙u˙wx˙y˙z=x˙y˙x˙z
74 73 an32s KLatuBvBwBu˙v˙w=u˙v˙u˙wxByBzBx˙y˙z=x˙y˙x˙z
75 74 ralrimivvva KLatuBvBwBu˙v˙w=u˙v˙u˙wxByBzBx˙y˙z=x˙y˙x˙z
76 75 ex KLatuBvBwBu˙v˙w=u˙v˙u˙wxByBzBx˙y˙z=x˙y˙x˙z