Metamath Proof Explorer


Theorem 2atmat

Description: The meet of two intersecting lines (expressed as joins of atoms) is an atom. (Contributed by NM, 21-Nov-2012)

Ref Expression
Hypotheses 2atmat.l ˙=K
2atmat.j ˙=joinK
2atmat.m ˙=meetK
2atmat.a A=AtomsK
Assertion 2atmat KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RP˙Q˙R˙SA

Proof

Step Hyp Ref Expression
1 2atmat.l ˙=K
2 2atmat.j ˙=joinK
3 2atmat.m ˙=meetK
4 2atmat.a A=AtomsK
5 simp11 KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RKHL
6 5 hllatd KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RKLat
7 eqid BaseK=BaseK
8 7 2 4 hlatjcl KHLPAQAP˙QBaseK
9 8 3ad2ant1 KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RP˙QBaseK
10 simp21 KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RRA
11 7 4 atbase RARBaseK
12 10 11 syl KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RRBaseK
13 simp22 KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RSA
14 7 4 atbase SASBaseK
15 13 14 syl KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RSBaseK
16 7 2 latjass KLatP˙QBaseKRBaseKSBaseKP˙Q˙R˙S=P˙Q˙R˙S
17 6 9 12 15 16 syl13anc KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RP˙Q˙R˙S=P˙Q˙R˙S
18 simp33 KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RS˙P˙Q˙R
19 7 2 latjcl KLatP˙QBaseKRBaseKP˙Q˙RBaseK
20 6 9 12 19 syl3anc KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RP˙Q˙RBaseK
21 7 1 2 latleeqj2 KLatSBaseKP˙Q˙RBaseKS˙P˙Q˙RP˙Q˙R˙S=P˙Q˙R
22 6 15 20 21 syl3anc KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RS˙P˙Q˙RP˙Q˙R˙S=P˙Q˙R
23 18 22 mpbid KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RP˙Q˙R˙S=P˙Q˙R
24 17 23 eqtr3d KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RP˙Q˙R˙S=P˙Q˙R
25 simp23 KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RPQ
26 simp32 KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙R¬R˙P˙Q
27 simp12 KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RPA
28 simp13 KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RQA
29 eqid LPlanesK=LPlanesK
30 1 2 4 29 islpln2a KHLPAQARAP˙Q˙RLPlanesKPQ¬R˙P˙Q
31 5 27 28 10 30 syl13anc KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RP˙Q˙RLPlanesKPQ¬R˙P˙Q
32 25 26 31 mpbir2and KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RP˙Q˙RLPlanesK
33 24 32 eqeltrd KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RP˙Q˙R˙SLPlanesK
34 eqid LLinesK=LLinesK
35 2 4 34 llni2 KHLPAQAPQP˙QLLinesK
36 5 27 28 25 35 syl31anc KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RP˙QLLinesK
37 simp31 KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RRS
38 2 4 34 llni2 KHLRASARSR˙SLLinesK
39 5 10 13 37 38 syl31anc KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RR˙SLLinesK
40 2 3 4 34 29 2llnmj KHLP˙QLLinesKR˙SLLinesKP˙Q˙R˙SAP˙Q˙R˙SLPlanesK
41 5 36 39 40 syl3anc KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RP˙Q˙R˙SAP˙Q˙R˙SLPlanesK
42 33 41 mpbird KHLPAQARASAPQRS¬R˙P˙QS˙P˙Q˙RP˙Q˙R˙SA