Metamath Proof Explorer


Theorem 2llnma2rN

Description: Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 2-May-2013) (New usage is discouraged.)

Ref Expression
Hypotheses 2llnm.l ˙ = K
2llnm.j ˙ = join K
2llnm.m ˙ = meet K
2llnm.a A = Atoms K
Assertion 2llnma2rN K HL P A Q A R A P Q ¬ R ˙ P ˙ Q P ˙ R ˙ Q ˙ R = R

Proof

Step Hyp Ref Expression
1 2llnm.l ˙ = K
2 2llnm.j ˙ = join K
3 2llnm.m ˙ = meet K
4 2llnm.a A = Atoms K
5 simp1 K HL P A Q A R A P Q ¬ R ˙ P ˙ Q K HL
6 simp21 K HL P A Q A R A P Q ¬ R ˙ P ˙ Q P A
7 simp23 K HL P A Q A R A P Q ¬ R ˙ P ˙ Q R A
8 2 4 hlatjcom K HL P A R A P ˙ R = R ˙ P
9 5 6 7 8 syl3anc K HL P A Q A R A P Q ¬ R ˙ P ˙ Q P ˙ R = R ˙ P
10 simp22 K HL P A Q A R A P Q ¬ R ˙ P ˙ Q Q A
11 2 4 hlatjcom K HL Q A R A Q ˙ R = R ˙ Q
12 5 10 7 11 syl3anc K HL P A Q A R A P Q ¬ R ˙ P ˙ Q Q ˙ R = R ˙ Q
13 9 12 oveq12d K HL P A Q A R A P Q ¬ R ˙ P ˙ Q P ˙ R ˙ Q ˙ R = R ˙ P ˙ R ˙ Q
14 1 2 3 4 2llnma2 K HL P A Q A R A P Q ¬ R ˙ P ˙ Q R ˙ P ˙ R ˙ Q = R
15 13 14 eqtrd K HL P A Q A R A P Q ¬ R ˙ P ˙ Q P ˙ R ˙ Q ˙ R = R