Database
BASIC ORDER THEORY
Posets and lattices using extensible structures
Lattices
latj4rot
Next ⟩
latjjdi
Metamath Proof Explorer
Ascii
Unicode
Theorem
latj4rot
Description:
Rotate lattice join of 4 classes.
(Contributed by
NM
, 11-Jul-2012)
Ref
Expression
Hypotheses
latjass.b
⊢
B
=
Base
K
latjass.j
⊢
∨
˙
=
join
⁡
K
Assertion
latj4rot
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
∧
W
∈
B
→
X
∨
˙
Y
∨
˙
Z
∨
˙
W
=
W
∨
˙
X
∨
˙
Y
∨
˙
Z
Proof
Step
Hyp
Ref
Expression
1
latjass.b
⊢
B
=
Base
K
2
latjass.j
⊢
∨
˙
=
join
⁡
K
3
simp1
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
∧
W
∈
B
→
K
∈
Lat
4
simp3l
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
∧
W
∈
B
→
Z
∈
B
5
simp3r
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
∧
W
∈
B
→
W
∈
B
6
1
2
latjcom
⊢
K
∈
Lat
∧
Z
∈
B
∧
W
∈
B
→
Z
∨
˙
W
=
W
∨
˙
Z
7
3
4
5
6
syl3anc
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
∧
W
∈
B
→
Z
∨
˙
W
=
W
∨
˙
Z
8
7
oveq2d
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
∧
W
∈
B
→
X
∨
˙
Y
∨
˙
Z
∨
˙
W
=
X
∨
˙
Y
∨
˙
W
∨
˙
Z
9
5
4
jca
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
∧
W
∈
B
→
W
∈
B
∧
Z
∈
B
10
1
2
latj4
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
∧
W
∈
B
∧
Z
∈
B
→
X
∨
˙
Y
∨
˙
W
∨
˙
Z
=
X
∨
˙
W
∨
˙
Y
∨
˙
Z
11
9
10
syld3an3
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
∧
W
∈
B
→
X
∨
˙
Y
∨
˙
W
∨
˙
Z
=
X
∨
˙
W
∨
˙
Y
∨
˙
Z
12
simp2l
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
∧
W
∈
B
→
X
∈
B
13
1
2
latjcom
⊢
K
∈
Lat
∧
X
∈
B
∧
W
∈
B
→
X
∨
˙
W
=
W
∨
˙
X
14
3
12
5
13
syl3anc
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
∧
W
∈
B
→
X
∨
˙
W
=
W
∨
˙
X
15
14
oveq1d
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
∧
W
∈
B
→
X
∨
˙
W
∨
˙
Y
∨
˙
Z
=
W
∨
˙
X
∨
˙
Y
∨
˙
Z
16
8
11
15
3eqtrd
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
∧
W
∈
B
→
X
∨
˙
Y
∨
˙
Z
∨
˙
W
=
W
∨
˙
X
∨
˙
Y
∨
˙
Z