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