This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ≤ = ( le ‘ 𝐾 )
2atmat.j ⊢ ∨ = ( join ‘ 𝐾 )
2atmat.m ⊢ ∧ = ( meet ‘ 𝐾 )
2atmat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 2atmat ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 2atmat.l ⊢ ≤ = ( le ‘ 𝐾 )
2 2atmat.j ⊢ ∨ = ( join ‘ 𝐾 )
3 2atmat.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 2atmat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝐾 ∈ HL )
6 5 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝐾 ∈ Lat )
7 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8 7 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
9 8 3ad2ant1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
10 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑅 ∈ 𝐴 )
11 7 4 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
12 10 11 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
13 simp22 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑆 ∈ 𝐴 )
14 7 4 atbase ⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
15 13 14 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
16 7 2 latjass ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) )
17 6 9 12 15 16 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) )
18 simp33 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
19 7 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
20 6 9 12 19 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
21 7 1 2 latleeqj2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
22 6 15 20 21 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
23 18 22 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∨ 𝑆 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
24 17 23 eqtr3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
25 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑃 ≠ 𝑄 )
26 simp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
27 simp12 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑃 ∈ 𝐴 )
28 simp13 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑄 ∈ 𝐴 )
29 eqid ⊢ ( LPlanes ‘ 𝐾 ) = ( LPlanes ‘ 𝐾 )
30 1 2 4 29 islpln2a ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) ↔ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
31 5 27 28 10 30 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) ↔ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
32 25 26 31 mpbir2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) )
33 24 32 eqeltrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) ∈ ( LPlanes ‘ 𝐾 ) )
34 eqid ⊢ ( LLines ‘ 𝐾 ) = ( LLines ‘ 𝐾 )
35 2 4 34 llni2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( LLines ‘ 𝐾 ) )
36 5 27 28 25 35 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( LLines ‘ 𝐾 ) )
37 simp31 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → 𝑅 ≠ 𝑆 )
38 2 4 34 llni2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ 𝑅 ≠ 𝑆 ) → ( 𝑅 ∨ 𝑆 ) ∈ ( LLines ‘ 𝐾 ) )
39 5 10 13 37 38 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( 𝑅 ∨ 𝑆 ) ∈ ( LLines ‘ 𝐾 ) )
40 2 3 4 34 29 2llnmj ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( LLines ‘ 𝐾 ) ∧ ( 𝑅 ∨ 𝑆 ) ∈ ( LLines ‘ 𝐾 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) ∈ ( LPlanes ‘ 𝐾 ) ) )
41 5 36 39 40 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) ∈ ( LPlanes ‘ 𝐾 ) ) )
42 33 41 mpbird ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ≠ 𝑆 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑅 ∨ 𝑆 ) ) ∈ 𝐴 )