Metamath Proof Explorer


Theorem lplnllnneN

Description: Two lattice lines defined by atoms defining a lattice plane are not equal. (Contributed by NM, 9-Oct-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 lplnllnneN K HL Q A R A S A Y P Q ˙ S R ˙ 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 simpl1 K HL Q A R A S A Y P Q ˙ S = R ˙ S K HL
8 simpl21 K HL Q A R A S A Y P Q ˙ S = R ˙ S Q A
9 simpl23 K HL Q A R A S A Y P Q ˙ S = R ˙ S S A
10 5 1 2 hlatlej1 K HL Q A S A Q K Q ˙ S
11 7 8 9 10 syl3anc K HL Q A R A S A Y P Q ˙ S = R ˙ S Q K Q ˙ S
12 simpr K HL Q A R A S A Y P Q ˙ S = R ˙ S Q ˙ S = R ˙ S
13 11 12 breqtrd K HL Q A R A S A Y P Q ˙ S = R ˙ S Q K R ˙ S
14 13 ex K HL Q A R A S A Y P Q ˙ S = R ˙ S Q K R ˙ S
15 14 necon3bd K HL Q A R A S A Y P ¬ Q K R ˙ S Q ˙ S R ˙ S
16 6 15 mpd K HL Q A R A S A Y P Q ˙ S R ˙ S