Metamath Proof Explorer


Theorem 4atlem4b

Description: Lemma for 4at . Frequently used associative law. (Contributed by NM, 9-Jul-2012)

Ref Expression
Hypotheses 4at.l ˙ = K
4at.j ˙ = join K
4at.a A = Atoms K
Assertion 4atlem4b K HL P A Q A R A S A P ˙ Q ˙ R ˙ S = Q ˙ P ˙ R ˙ S

Proof

Step Hyp Ref Expression
1 4at.l ˙ = K
2 4at.j ˙ = join K
3 4at.a A = Atoms K
4 simpl1 K HL P A Q A R A S A K HL
5 simpl2 K HL P A Q A R A S A P A
6 simpl3 K HL P A Q A R A S A Q A
7 simprl K HL P A Q A R A S A R A
8 simprr K HL P A Q A R A S A S A
9 2 3 hlatj4 K HL P A Q A R A S A P ˙ Q ˙ R ˙ S = P ˙ R ˙ Q ˙ S
10 4 5 6 7 8 9 syl122anc K HL P A Q A R A S A P ˙ Q ˙ R ˙ S = P ˙ R ˙ Q ˙ S
11 4 hllatd K HL P A Q A R A S A K Lat
12 eqid Base K = Base K
13 12 2 3 hlatjcl K HL P A R A P ˙ R Base K
14 4 5 7 13 syl3anc K HL P A Q A R A S A P ˙ R Base K
15 12 3 atbase Q A Q Base K
16 6 15 syl K HL P A Q A R A S A Q Base K
17 12 3 atbase S A S Base K
18 17 ad2antll K HL P A Q A R A S A S Base K
19 12 2 latj12 K Lat P ˙ R Base K Q Base K S Base K P ˙ R ˙ Q ˙ S = Q ˙ P ˙ R ˙ S
20 11 14 16 18 19 syl13anc K HL P A Q A R A S A P ˙ R ˙ Q ˙ S = Q ˙ P ˙ R ˙ S
21 10 20 eqtrd K HL P A Q A R A S A P ˙ Q ˙ R ˙ S = Q ˙ P ˙ R ˙ S