This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hlatj12

Description: Swap 1st and 2nd members of lattice join. Frequently-used special case of latj32 for atoms. (Contributed by NM, 4-Jun-2012)

Ref Expression
Hypotheses hlatjcom.j ⊢ ∨ ˙ = join ⁡ K
hlatjcom.a ⊢ A = Atoms ⁡ K
Assertion hlatj12 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → P ∨ ˙ Q ∨ ˙ R = Q ∨ ˙ P ∨ ˙ R

Proof

Step Hyp Ref Expression
1 hlatjcom.j ⊢ ∨ ˙ = join ⁡ K
2 hlatjcom.a ⊢ A = Atoms ⁡ K
3 1 2 hlatjcom ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ Q = Q ∨ ˙ P
4 3 3adant3r3 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → P ∨ ˙ Q = Q ∨ ˙ P
5 4 oveq1d ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → P ∨ ˙ Q ∨ ˙ R = Q ∨ ˙ P ∨ ˙ R
6 1 2 hlatjass ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → P ∨ ˙ Q ∨ ˙ R = P ∨ ˙ Q ∨ ˙ R
7 simpl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → K ∈ HL
8 simpr2 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → Q ∈ A
9 simpr1 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → P ∈ A
10 simpr3 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → R ∈ A
11 1 2 hlatjass ⊢ K ∈ HL ∧ Q ∈ A ∧ P ∈ A ∧ R ∈ A → Q ∨ ˙ P ∨ ˙ R = Q ∨ ˙ P ∨ ˙ R
12 7 8 9 10 11 syl13anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → Q ∨ ˙ P ∨ ˙ R = Q ∨ ˙ P ∨ ˙ R
13 5 6 12 3eqtr3d ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → P ∨ ˙ Q ∨ ˙ R = Q ∨ ˙ P ∨ ˙ R