Database
BASIC ORDER THEORY
Lattices
Lattices
latdisdlem
Next ⟩
latdisd
Metamath Proof Explorer
Ascii
Unicode
Theorem
latdisdlem
Description:
Lemma for
latdisd
.
(Contributed by
Stefan O'Rear
, 30-Jan-2015)
Ref
Expression
Hypotheses
latdisd.b
⊢
B
=
Base
K
latdisd.j
⊢
∨
˙
=
join
K
latdisd.m
⊢
∧
˙
=
meet
K
Assertion
latdisdlem
⊢
K
∈
Lat
→
∀
u
∈
B
∀
v
∈
B
∀
w
∈
B
u
∨
˙
v
∧
˙
w
=
u
∨
˙
v
∧
˙
u
∨
˙
w
→
∀
x
∈
B
∀
y
∈
B
∀
z
∈
B
x
∧
˙
y
∨
˙
z
=
x
∧
˙
y
∨
˙
x
∧
˙
z
Proof
Step
Hyp
Ref
Expression
1
latdisd.b
⊢
B
=
Base
K
2
latdisd.j
⊢
∨
˙
=
join
K
3
latdisd.m
⊢
∧
˙
=
meet
K
4
1
3
latmcl
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
→
x
∧
˙
y
∈
B
5
4
3adant3r3
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
x
∧
˙
y
∈
B
6
simpr1
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
x
∈
B
7
simpr3
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
z
∈
B
8
oveq1
⊢
u
=
x
∧
˙
y
→
u
∨
˙
v
∧
˙
w
=
x
∧
˙
y
∨
˙
v
∧
˙
w
9
oveq1
⊢
u
=
x
∧
˙
y
→
u
∨
˙
v
=
x
∧
˙
y
∨
˙
v
10
oveq1
⊢
u
=
x
∧
˙
y
→
u
∨
˙
w
=
x
∧
˙
y
∨
˙
w
11
9
10
oveq12d
⊢
u
=
x
∧
˙
y
→
u
∨
˙
v
∧
˙
u
∨
˙
w
=
x
∧
˙
y
∨
˙
v
∧
˙
x
∧
˙
y
∨
˙
w
12
8
11
eqeq12d
⊢
u
=
x
∧
˙
y
→
u
∨
˙
v
∧
˙
w
=
u
∨
˙
v
∧
˙
u
∨
˙
w
↔
x
∧
˙
y
∨
˙
v
∧
˙
w
=
x
∧
˙
y
∨
˙
v
∧
˙
x
∧
˙
y
∨
˙
w
13
oveq1
⊢
v
=
x
→
v
∧
˙
w
=
x
∧
˙
w
14
13
oveq2d
⊢
v
=
x
→
x
∧
˙
y
∨
˙
v
∧
˙
w
=
x
∧
˙
y
∨
˙
x
∧
˙
w
15
oveq2
⊢
v
=
x
→
x
∧
˙
y
∨
˙
v
=
x
∧
˙
y
∨
˙
x
16
15
oveq1d
⊢
v
=
x
→
x
∧
˙
y
∨
˙
v
∧
˙
x
∧
˙
y
∨
˙
w
=
x
∧
˙
y
∨
˙
x
∧
˙
x
∧
˙
y
∨
˙
w
17
14
16
eqeq12d
⊢
v
=
x
→
x
∧
˙
y
∨
˙
v
∧
˙
w
=
x
∧
˙
y
∨
˙
v
∧
˙
x
∧
˙
y
∨
˙
w
↔
x
∧
˙
y
∨
˙
x
∧
˙
w
=
x
∧
˙
y
∨
˙
x
∧
˙
x
∧
˙
y
∨
˙
w
18
oveq2
⊢
w
=
z
→
x
∧
˙
w
=
x
∧
˙
z
19
18
oveq2d
⊢
w
=
z
→
x
∧
˙
y
∨
˙
x
∧
˙
w
=
x
∧
˙
y
∨
˙
x
∧
˙
z
20
oveq2
⊢
w
=
z
→
x
∧
˙
y
∨
˙
w
=
x
∧
˙
y
∨
˙
z
21
20
oveq2d
⊢
w
=
z
→
x
∧
˙
y
∨
˙
x
∧
˙
x
∧
˙
y
∨
˙
w
=
x
∧
˙
y
∨
˙
x
∧
˙
x
∧
˙
y
∨
˙
z
22
19
21
eqeq12d
⊢
w
=
z
→
x
∧
˙
y
∨
˙
x
∧
˙
w
=
x
∧
˙
y
∨
˙
x
∧
˙
x
∧
˙
y
∨
˙
w
↔
x
∧
˙
y
∨
˙
x
∧
˙
z
=
x
∧
˙
y
∨
˙
x
∧
˙
x
∧
˙
y
∨
˙
z
23
12
17
22
rspc3v
⊢
x
∧
˙
y
∈
B
∧
x
∈
B
∧
z
∈
B
→
∀
u
∈
B
∀
v
∈
B
∀
w
∈
B
u
∨
˙
v
∧
˙
w
=
u
∨
˙
v
∧
˙
u
∨
˙
w
→
x
∧
˙
y
∨
˙
x
∧
˙
z
=
x
∧
˙
y
∨
˙
x
∧
˙
x
∧
˙
y
∨
˙
z
24
5
6
7
23
syl3anc
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
∀
u
∈
B
∀
v
∈
B
∀
w
∈
B
u
∨
˙
v
∧
˙
w
=
u
∨
˙
v
∧
˙
u
∨
˙
w
→
x
∧
˙
y
∨
˙
x
∧
˙
z
=
x
∧
˙
y
∨
˙
x
∧
˙
x
∧
˙
y
∨
˙
z
25
24
imp
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
∧
∀
u
∈
B
∀
v
∈
B
∀
w
∈
B
u
∨
˙
v
∧
˙
w
=
u
∨
˙
v
∧
˙
u
∨
˙
w
→
x
∧
˙
y
∨
˙
x
∧
˙
z
=
x
∧
˙
y
∨
˙
x
∧
˙
x
∧
˙
y
∨
˙
z
26
simpl
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
K
∈
Lat
27
1
2
latjcom
⊢
K
∈
Lat
∧
x
∧
˙
y
∈
B
∧
x
∈
B
→
x
∧
˙
y
∨
˙
x
=
x
∨
˙
x
∧
˙
y
28
26
5
6
27
syl3anc
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
x
∧
˙
y
∨
˙
x
=
x
∨
˙
x
∧
˙
y
29
1
2
3
latabs1
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
→
x
∨
˙
x
∧
˙
y
=
x
30
29
3adant3r3
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
x
∨
˙
x
∧
˙
y
=
x
31
28
30
eqtrd
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
x
∧
˙
y
∨
˙
x
=
x
32
1
2
latjcom
⊢
K
∈
Lat
∧
x
∧
˙
y
∈
B
∧
z
∈
B
→
x
∧
˙
y
∨
˙
z
=
z
∨
˙
x
∧
˙
y
33
26
5
7
32
syl3anc
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
x
∧
˙
y
∨
˙
z
=
z
∨
˙
x
∧
˙
y
34
31
33
oveq12d
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
x
∧
˙
y
∨
˙
x
∧
˙
x
∧
˙
y
∨
˙
z
=
x
∧
˙
z
∨
˙
x
∧
˙
y
35
34
adantr
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
∧
∀
u
∈
B
∀
v
∈
B
∀
w
∈
B
u
∨
˙
v
∧
˙
w
=
u
∨
˙
v
∧
˙
u
∨
˙
w
→
x
∧
˙
y
∨
˙
x
∧
˙
x
∧
˙
y
∨
˙
z
=
x
∧
˙
z
∨
˙
x
∧
˙
y
36
simpr2
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
y
∈
B
37
oveq1
⊢
u
=
z
→
u
∨
˙
v
∧
˙
w
=
z
∨
˙
v
∧
˙
w
38
oveq1
⊢
u
=
z
→
u
∨
˙
v
=
z
∨
˙
v
39
oveq1
⊢
u
=
z
→
u
∨
˙
w
=
z
∨
˙
w
40
38
39
oveq12d
⊢
u
=
z
→
u
∨
˙
v
∧
˙
u
∨
˙
w
=
z
∨
˙
v
∧
˙
z
∨
˙
w
41
37
40
eqeq12d
⊢
u
=
z
→
u
∨
˙
v
∧
˙
w
=
u
∨
˙
v
∧
˙
u
∨
˙
w
↔
z
∨
˙
v
∧
˙
w
=
z
∨
˙
v
∧
˙
z
∨
˙
w
42
13
oveq2d
⊢
v
=
x
→
z
∨
˙
v
∧
˙
w
=
z
∨
˙
x
∧
˙
w
43
oveq2
⊢
v
=
x
→
z
∨
˙
v
=
z
∨
˙
x
44
43
oveq1d
⊢
v
=
x
→
z
∨
˙
v
∧
˙
z
∨
˙
w
=
z
∨
˙
x
∧
˙
z
∨
˙
w
45
42
44
eqeq12d
⊢
v
=
x
→
z
∨
˙
v
∧
˙
w
=
z
∨
˙
v
∧
˙
z
∨
˙
w
↔
z
∨
˙
x
∧
˙
w
=
z
∨
˙
x
∧
˙
z
∨
˙
w
46
oveq2
⊢
w
=
y
→
x
∧
˙
w
=
x
∧
˙
y
47
46
oveq2d
⊢
w
=
y
→
z
∨
˙
x
∧
˙
w
=
z
∨
˙
x
∧
˙
y
48
oveq2
⊢
w
=
y
→
z
∨
˙
w
=
z
∨
˙
y
49
48
oveq2d
⊢
w
=
y
→
z
∨
˙
x
∧
˙
z
∨
˙
w
=
z
∨
˙
x
∧
˙
z
∨
˙
y
50
47
49
eqeq12d
⊢
w
=
y
→
z
∨
˙
x
∧
˙
w
=
z
∨
˙
x
∧
˙
z
∨
˙
w
↔
z
∨
˙
x
∧
˙
y
=
z
∨
˙
x
∧
˙
z
∨
˙
y
51
41
45
50
rspc3v
⊢
z
∈
B
∧
x
∈
B
∧
y
∈
B
→
∀
u
∈
B
∀
v
∈
B
∀
w
∈
B
u
∨
˙
v
∧
˙
w
=
u
∨
˙
v
∧
˙
u
∨
˙
w
→
z
∨
˙
x
∧
˙
y
=
z
∨
˙
x
∧
˙
z
∨
˙
y
52
7
6
36
51
syl3anc
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
∀
u
∈
B
∀
v
∈
B
∀
w
∈
B
u
∨
˙
v
∧
˙
w
=
u
∨
˙
v
∧
˙
u
∨
˙
w
→
z
∨
˙
x
∧
˙
y
=
z
∨
˙
x
∧
˙
z
∨
˙
y
53
52
imp
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
∧
∀
u
∈
B
∀
v
∈
B
∀
w
∈
B
u
∨
˙
v
∧
˙
w
=
u
∨
˙
v
∧
˙
u
∨
˙
w
→
z
∨
˙
x
∧
˙
y
=
z
∨
˙
x
∧
˙
z
∨
˙
y
54
53
oveq2d
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
∧
∀
u
∈
B
∀
v
∈
B
∀
w
∈
B
u
∨
˙
v
∧
˙
w
=
u
∨
˙
v
∧
˙
u
∨
˙
w
→
x
∧
˙
z
∨
˙
x
∧
˙
y
=
x
∧
˙
z
∨
˙
x
∧
˙
z
∨
˙
y
55
1
2
latjcl
⊢
K
∈
Lat
∧
z
∈
B
∧
x
∈
B
→
z
∨
˙
x
∈
B
56
26
7
6
55
syl3anc
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
z
∨
˙
x
∈
B
57
1
2
latjcl
⊢
K
∈
Lat
∧
z
∈
B
∧
y
∈
B
→
z
∨
˙
y
∈
B
58
26
7
36
57
syl3anc
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
z
∨
˙
y
∈
B
59
1
3
latmass
⊢
K
∈
Lat
∧
x
∈
B
∧
z
∨
˙
x
∈
B
∧
z
∨
˙
y
∈
B
→
x
∧
˙
z
∨
˙
x
∧
˙
z
∨
˙
y
=
x
∧
˙
z
∨
˙
x
∧
˙
z
∨
˙
y
60
26
6
56
58
59
syl13anc
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
x
∧
˙
z
∨
˙
x
∧
˙
z
∨
˙
y
=
x
∧
˙
z
∨
˙
x
∧
˙
z
∨
˙
y
61
1
2
latjcom
⊢
K
∈
Lat
∧
z
∈
B
∧
x
∈
B
→
z
∨
˙
x
=
x
∨
˙
z
62
26
7
6
61
syl3anc
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
z
∨
˙
x
=
x
∨
˙
z
63
62
oveq2d
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
x
∧
˙
z
∨
˙
x
=
x
∧
˙
x
∨
˙
z
64
1
2
3
latabs2
⊢
K
∈
Lat
∧
x
∈
B
∧
z
∈
B
→
x
∧
˙
x
∨
˙
z
=
x
65
26
6
7
64
syl3anc
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
x
∧
˙
x
∨
˙
z
=
x
66
63
65
eqtrd
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
x
∧
˙
z
∨
˙
x
=
x
67
1
2
latjcom
⊢
K
∈
Lat
∧
z
∈
B
∧
y
∈
B
→
z
∨
˙
y
=
y
∨
˙
z
68
26
7
36
67
syl3anc
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
z
∨
˙
y
=
y
∨
˙
z
69
66
68
oveq12d
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
x
∧
˙
z
∨
˙
x
∧
˙
z
∨
˙
y
=
x
∧
˙
y
∨
˙
z
70
60
69
eqtr3d
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
x
∧
˙
z
∨
˙
x
∧
˙
z
∨
˙
y
=
x
∧
˙
y
∨
˙
z
71
70
adantr
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
∧
∀
u
∈
B
∀
v
∈
B
∀
w
∈
B
u
∨
˙
v
∧
˙
w
=
u
∨
˙
v
∧
˙
u
∨
˙
w
→
x
∧
˙
z
∨
˙
x
∧
˙
z
∨
˙
y
=
x
∧
˙
y
∨
˙
z
72
54
71
eqtrd
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
∧
∀
u
∈
B
∀
v
∈
B
∀
w
∈
B
u
∨
˙
v
∧
˙
w
=
u
∨
˙
v
∧
˙
u
∨
˙
w
→
x
∧
˙
z
∨
˙
x
∧
˙
y
=
x
∧
˙
y
∨
˙
z
73
25
35
72
3eqtrrd
⊢
K
∈
Lat
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
∧
∀
u
∈
B
∀
v
∈
B
∀
w
∈
B
u
∨
˙
v
∧
˙
w
=
u
∨
˙
v
∧
˙
u
∨
˙
w
→
x
∧
˙
y
∨
˙
z
=
x
∧
˙
y
∨
˙
x
∧
˙
z
74
73
an32s
⊢
K
∈
Lat
∧
∀
u
∈
B
∀
v
∈
B
∀
w
∈
B
u
∨
˙
v
∧
˙
w
=
u
∨
˙
v
∧
˙
u
∨
˙
w
∧
x
∈
B
∧
y
∈
B
∧
z
∈
B
→
x
∧
˙
y
∨
˙
z
=
x
∧
˙
y
∨
˙
x
∧
˙
z
75
74
ralrimivvva
⊢
K
∈
Lat
∧
∀
u
∈
B
∀
v
∈
B
∀
w
∈
B
u
∨
˙
v
∧
˙
w
=
u
∨
˙
v
∧
˙
u
∨
˙
w
→
∀
x
∈
B
∀
y
∈
B
∀
z
∈
B
x
∧
˙
y
∨
˙
z
=
x
∧
˙
y
∨
˙
x
∧
˙
z
76
75
ex
⊢
K
∈
Lat
→
∀
u
∈
B
∀
v
∈
B
∀
w
∈
B
u
∨
˙
v
∧
˙
w
=
u
∨
˙
v
∧
˙
u
∨
˙
w
→
∀
x
∈
B
∀
y
∈
B
∀
z
∈
B
x
∧
˙
y
∨
˙
z
=
x
∧
˙
y
∨
˙
x
∧
˙
z