Metamath Proof Explorer

Theorem hlatjass

Description: Lattice join is associative. Frequently-used special case of latjass for atoms. (Contributed by NM, 27-Jul-2012)

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

Proof

Step Hyp Ref Expression
1 hlatjcom.j ⊢ ∨ ˙ = join ⁡ K
2 hlatjcom.a ⊢ A = Atoms ⁡ K
3 hllat ⊢ K ∈ HL → K ∈ Lat
4 3 adantr ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → K ∈ Lat
5 simpr1 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → P ∈ A
6 eqid ⊢ Base K = Base K
7 6 2 atbase ⊢ P ∈ A → P ∈ Base K
8 5 7 syl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → P ∈ Base K
9 simpr2 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → Q ∈ A
10 6 2 atbase ⊢ Q ∈ A → Q ∈ Base K
11 9 10 syl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → Q ∈ Base K
12 simpr3 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → R ∈ A
13 6 2 atbase ⊢ R ∈ A → R ∈ Base K
14 12 13 syl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → R ∈ Base K
15 6 1 latjass ⊢ K ∈ Lat ∧ P ∈ Base K ∧ Q ∈ Base K ∧ R ∈ Base K → P ∨ ˙ Q ∨ ˙ R = P ∨ ˙ Q ∨ ˙ R
16 4 8 11 14 15 syl13anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → P ∨ ˙ Q ∨ ˙ R = P ∨ ˙ Q ∨ ˙ R