Theorem 3atnelvolN

Description: The join of 3 atoms is not a lattice volume. (Contributed by NM, 17-Jul-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	3atnelvol.j	⊢ ∨ = ( join ‘ 𝐾 )
	3atnelvol.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	3atnelvol.v	⊢ 𝑉 = ( LVols ‘ 𝐾 )
Assertion	3atnelvolN	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ¬ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		3atnelvol.j	⊢ ∨ = ( join ‘ 𝐾 )
2		3atnelvol.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		3atnelvol.v	⊢ 𝑉 = ( LVols ‘ 𝐾 )
4		hllat	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
5	4	adantr	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝐾 ∈ Lat )
6		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7	6 1 2	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
8	7	3adant3r3	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
9		simpr3	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑅 ∈ 𝐴 )
10	6 2	atbase	⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
11	9 10	syl	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
12	6 1	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
13	5 8 11 12	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
14		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
15	6 14	latref	⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ( le ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
16	5 13 15	syl2anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ( le ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
17	14 1 2 3	lvolnle3at	⊢ ( ( ( 𝐾 ∈ HL ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ¬ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ( le ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
18	17	an32s	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑉 ) → ¬ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ( le ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
19	18	ex	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑉 → ¬ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ( le ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
20	16 19	mt2d	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ¬ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ 𝑉 )