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

Metamath Proof Explorer

Theorem 2atnelpln

Description: The join of two atoms is not a lattice plane. (Contributed by NM, 16-Jul-2012)

Ref Expression
Hypotheses 2atnelpln.j ⊢ ∨ = ( join ‘ 𝐾 )
2atnelpln.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2atnelpln.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion 2atnelpln ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ¬ ( 𝑄 ∨ 𝑅 ) ∈ 𝑃 )

Proof

Step Hyp Ref Expression
1 2atnelpln.j ⊢ ∨ = ( join ‘ 𝐾 )
2 2atnelpln.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 2atnelpln.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
4 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
5 4 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → 𝐾 ∈ Lat )
6 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 6 1 2 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
8 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
9 6 8 latref ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑄 ∨ 𝑅 ) ( le ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) )
10 5 7 9 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑅 ) ( le ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) )
11 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ 𝑃 ) → 𝐾 ∈ HL )
12 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ 𝑃 ) → ( 𝑄 ∨ 𝑅 ) ∈ 𝑃 )
13 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ 𝑃 ) → 𝑄 ∈ 𝐴 )
14 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ 𝑃 ) → 𝑅 ∈ 𝐴 )
15 8 1 2 3 lplnnle2at ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑄 ∨ 𝑅 ) ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ¬ ( 𝑄 ∨ 𝑅 ) ( le ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) )
16 11 12 13 14 15 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ 𝑃 ) → ¬ ( 𝑄 ∨ 𝑅 ) ( le ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) )
17 16 ex ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( ( 𝑄 ∨ 𝑅 ) ∈ 𝑃 → ¬ ( 𝑄 ∨ 𝑅 ) ( le ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) ) )
18 10 17 mt2d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ¬ ( 𝑄 ∨ 𝑅 ) ∈ 𝑃 )