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 ∧ 𝑄𝐴𝑅𝐴 ) → ¬ ( 𝑄 𝑅 ) ∈ 𝑃 )