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