Metamath Proof Explorer


Theorem 2llnma1

Description: Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 11-Oct-2012)

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

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 ¬ R ˙ P ˙ Q K HL
6 simp21 K HL P A Q A R A ¬ R ˙ P ˙ Q P A
7 eqid Base K = Base K
8 7 4 atbase P A P Base K
9 6 8 syl K HL P A Q A R A ¬ R ˙ P ˙ Q P Base K
10 simp22 K HL P A Q A R A ¬ R ˙ P ˙ Q Q A
11 simp23 K HL P A Q A R A ¬ R ˙ P ˙ Q R A
12 simp3 K HL P A Q A R A ¬ R ˙ P ˙ Q ¬ R ˙ P ˙ Q
13 2 4 hlatjcom K HL P A Q A P ˙ Q = Q ˙ P
14 5 6 10 13 syl3anc K HL P A Q A R A ¬ R ˙ P ˙ Q P ˙ Q = Q ˙ P
15 14 breq2d K HL P A Q A R A ¬ R ˙ P ˙ Q R ˙ P ˙ Q R ˙ Q ˙ P
16 12 15 mtbid K HL P A Q A R A ¬ R ˙ P ˙ Q ¬ R ˙ Q ˙ P
17 7 1 2 3 4 2llnma1b K HL P Base K Q A R A ¬ R ˙ Q ˙ P Q ˙ P ˙ Q ˙ R = Q
18 5 9 10 11 16 17 syl131anc K HL P A Q A R A ¬ R ˙ P ˙ Q Q ˙ P ˙ Q ˙ R = Q