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 ˙ = join K
2atmat.m ˙ = meet K
2atmat.a A = Atoms K
Assertion 2atmat K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R P ˙ Q ˙ R ˙ S A

Proof

Step Hyp Ref Expression
1 2atmat.l ˙ = K
2 2atmat.j ˙ = join K
3 2atmat.m ˙ = meet K
4 2atmat.a A = Atoms K
5 simp11 K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R K HL
6 5 hllatd K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R K Lat
7 eqid Base K = Base K
8 7 2 4 hlatjcl K HL P A Q A P ˙ Q Base K
9 8 3ad2ant1 K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R P ˙ Q Base K
10 simp21 K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R R A
11 7 4 atbase R A R Base K
12 10 11 syl K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R R Base K
13 simp22 K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R S A
14 7 4 atbase S A S Base K
15 13 14 syl K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R S Base K
16 7 2 latjass K Lat P ˙ Q Base K R Base K S Base K P ˙ Q ˙ R ˙ S = P ˙ Q ˙ R ˙ S
17 6 9 12 15 16 syl13anc K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R P ˙ Q ˙ R ˙ S = P ˙ Q ˙ R ˙ S
18 simp33 K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R S ˙ P ˙ Q ˙ R
19 7 2 latjcl K Lat P ˙ Q Base K R Base K P ˙ Q ˙ R Base K
20 6 9 12 19 syl3anc K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R P ˙ Q ˙ R Base K
21 7 1 2 latleeqj2 K Lat S Base K P ˙ Q ˙ R Base K S ˙ P ˙ Q ˙ R P ˙ Q ˙ R ˙ S = P ˙ Q ˙ R
22 6 15 20 21 syl3anc K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R S ˙ P ˙ Q ˙ R P ˙ Q ˙ R ˙ S = P ˙ Q ˙ R
23 18 22 mpbid K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R P ˙ Q ˙ R ˙ S = P ˙ Q ˙ R
24 17 23 eqtr3d K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R P ˙ Q ˙ R ˙ S = P ˙ Q ˙ R
25 simp23 K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R P Q
26 simp32 K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R ¬ R ˙ P ˙ Q
27 simp12 K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R P A
28 simp13 K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R Q A
29 eqid LPlanes K = LPlanes K
30 1 2 4 29 islpln2a K HL P A Q A R A P ˙ Q ˙ R LPlanes K P Q ¬ R ˙ P ˙ Q
31 5 27 28 10 30 syl13anc K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R P ˙ Q ˙ R LPlanes K P Q ¬ R ˙ P ˙ Q
32 25 26 31 mpbir2and K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R P ˙ Q ˙ R LPlanes K
33 24 32 eqeltrd K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R P ˙ Q ˙ R ˙ S LPlanes K
34 eqid LLines K = LLines K
35 2 4 34 llni2 K HL P A Q A P Q P ˙ Q LLines K
36 5 27 28 25 35 syl31anc K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R P ˙ Q LLines K
37 simp31 K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R R S
38 2 4 34 llni2 K HL R A S A R S R ˙ S LLines K
39 5 10 13 37 38 syl31anc K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R R ˙ S LLines K
40 2 3 4 34 29 2llnmj K HL P ˙ Q LLines K R ˙ S LLines K P ˙ Q ˙ R ˙ S A P ˙ Q ˙ R ˙ S LPlanes K
41 5 36 39 40 syl3anc K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R P ˙ Q ˙ R ˙ S A P ˙ Q ˙ R ˙ S LPlanes K
42 33 41 mpbird K HL P A Q A R A S A P Q R S ¬ R ˙ P ˙ Q S ˙ P ˙ Q ˙ R P ˙ Q ˙ R ˙ S A