Metamath Proof Explorer

Theorem hlatj4

Description: Rearrangement of lattice join of 4 classes. Frequently-used special case of latj4 for atoms. (Contributed by NM, 9-Aug-2012)

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

Proof

Step Hyp Ref Expression
1 hlatjcom.j ⊢ ∨ ˙ = join ⁡ K
2 hlatjcom.a ⊢ A = Atoms ⁡ K
3 hllat ⊢ K ∈ HL → K ∈ Lat
4 3 3ad2ant1 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ S ∈ A → K ∈ Lat
5 simp2l ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ S ∈ 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 ∧ S ∈ A → P ∈ Base K
9 simp2r ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ S ∈ A → Q ∈ A
10 6 2 atbase ⊢ Q ∈ A → Q ∈ Base K
11 9 10 syl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ S ∈ A → Q ∈ Base K
12 simp3l ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ S ∈ A → R ∈ A
13 6 2 atbase ⊢ R ∈ A → R ∈ Base K
14 12 13 syl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ S ∈ A → R ∈ Base K
15 simp3r ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ S ∈ A → S ∈ A
16 6 2 atbase ⊢ S ∈ A → S ∈ Base K
17 15 16 syl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ S ∈ A → S ∈ Base K
18 6 1 latj4 ⊢ K ∈ Lat ∧ P ∈ Base K ∧ Q ∈ Base K ∧ R ∈ Base K ∧ S ∈ Base K → P ∨ ˙ Q ∨ ˙ R ∨ ˙ S = P ∨ ˙ R ∨ ˙ Q ∨ ˙ S
19 4 8 11 14 17 18 syl122anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ S ∈ A → P ∨ ˙ Q ∨ ˙ R ∨ ˙ S = P ∨ ˙ R ∨ ˙ Q ∨ ˙ S