Metamath Proof Explorer


Theorem lplnri2N

Description: Property of a lattice plane expressed as the join of 3 atoms. (Contributed by NM, 30-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lplnri1.j ˙ = join K
lplnri1.a A = Atoms K
lplnri1.p P = LPlanes K
lplnri1.y Y = Q ˙ R ˙ S
Assertion lplnri2N K HL Q A R A S A Y P Q S

Proof

Step Hyp Ref Expression
1 lplnri1.j ˙ = join K
2 lplnri1.a A = Atoms K
3 lplnri1.p P = LPlanes K
4 lplnri1.y Y = Q ˙ R ˙ S
5 eqid K = K
6 5 1 2 3 4 lplnriaN K HL Q A R A S A Y P ¬ Q K R ˙ S
7 5 1 2 atnlej2 K HL Q A R A S A ¬ Q K R ˙ S Q S
8 6 7 syld3an3 K HL Q A R A S A Y P Q S