Database
BASIC ORDER THEORY
Posets and lattices using extensible structures
Lattices
latjrot
Next ⟩
latj4
Metamath Proof Explorer
Ascii
Unicode
Theorem
latjrot
Description:
Rotate lattice join of 3 classes.
(Contributed by
NM
, 23-Jul-2012)
Ref
Expression
Hypotheses
latjass.b
⊢
B
=
Base
K
latjass.j
⊢
∨
˙
=
join
⁡
K
Assertion
latjrot
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
→
X
∨
˙
Y
∨
˙
Z
=
Z
∨
˙
X
∨
˙
Y
Proof
Step
Hyp
Ref
Expression
1
latjass.b
⊢
B
=
Base
K
2
latjass.j
⊢
∨
˙
=
join
⁡
K
3
1
2
latj31
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
→
X
∨
˙
Y
∨
˙
Z
=
Z
∨
˙
Y
∨
˙
X
4
simpl
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
→
K
∈
Lat
5
simpr3
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
→
Z
∈
B
6
simpr2
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
→
Y
∈
B
7
simpr1
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
→
X
∈
B
8
1
2
latj32
⊢
K
∈
Lat
∧
Z
∈
B
∧
Y
∈
B
∧
X
∈
B
→
Z
∨
˙
Y
∨
˙
X
=
Z
∨
˙
X
∨
˙
Y
9
4
5
6
7
8
syl13anc
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
→
Z
∨
˙
Y
∨
˙
X
=
Z
∨
˙
X
∨
˙
Y
10
3
9
eqtrd
⊢
K
∈
Lat
∧
X
∈
B
∧
Y
∈
B
∧
Z
∈
B
→
X
∨
˙
Y
∨
˙
Z
=
Z
∨
˙
X
∨
˙
Y