Metamath Proof Explorer


Theorem lplnri3N

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 ˙=joinK
lplnri1.a A=AtomsK
lplnri1.p P=LPlanesK
lplnri1.y Y=Q˙R˙S
Assertion lplnri3N KHLQARASAYPRS

Proof

Step Hyp Ref Expression
1 lplnri1.j ˙=joinK
2 lplnri1.a A=AtomsK
3 lplnri1.p P=LPlanesK
4 lplnri1.y Y=Q˙R˙S
5 simp1 KHLQARASAYPKHL
6 simp22 KHLQARASAYPRA
7 simp21 KHLQARASAYPQA
8 simp23 KHLQARASAYPSA
9 eqid K=K
10 9 1 2 3 4 lplnribN KHLQARASAYP¬RKQ˙S
11 9 1 2 atnlej2 KHLRAQASA¬RKQ˙SRS
12 5 6 7 8 10 11 syl131anc KHLQARASAYPRS