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