Metamath Proof Explorer


Theorem lplnribN

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 islpln2a.l ˙ = K
islpln2a.j ˙ = join K
islpln2a.a A = Atoms K
islpln2a.p P = LPlanes K
islpln2a.y Y = Q ˙ R ˙ S
Assertion lplnribN K HL Q A R A S A Y P ¬ R ˙ Q ˙ S

Proof

Step Hyp Ref Expression
1 islpln2a.l ˙ = K
2 islpln2a.j ˙ = join K
3 islpln2a.a A = Atoms K
4 islpln2a.p P = LPlanes K
5 islpln2a.y Y = Q ˙ R ˙ S
6 1 2 3 3noncolr1N K HL Q A R A S A Q R ¬ S ˙ Q ˙ R S Q ¬ R ˙ S ˙ Q
7 6 simprd K HL Q A R A S A Q R ¬ S ˙ Q ˙ R ¬ R ˙ S ˙ Q
8 7 3expia K HL Q A R A S A Q R ¬ S ˙ Q ˙ R ¬ R ˙ S ˙ Q
9 1 2 3 4 5 islpln2ah K HL Q A R A S A Y P Q R ¬ S ˙ Q ˙ R
10 2 3 hlatjcom K HL Q A S A Q ˙ S = S ˙ Q
11 10 3adant3r2 K HL Q A R A S A Q ˙ S = S ˙ Q
12 11 breq2d K HL Q A R A S A R ˙ Q ˙ S R ˙ S ˙ Q
13 12 notbid K HL Q A R A S A ¬ R ˙ Q ˙ S ¬ R ˙ S ˙ Q
14 8 9 13 3imtr4d K HL Q A R A S A Y P ¬ R ˙ Q ˙ S
15 14 3impia K HL Q A R A S A Y P ¬ R ˙ Q ˙ S