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	$⊢ \underset{˙}{\lor} = join (K)$
	3atnelvol.a	$⊢ A = Atoms (K)$
	3atnelvol.v	$⊢ V = LVols (K)$
Assertion	3atnelvolN	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in V$

Proof

Step	Hyp	Ref	Expression
1		3atnelvol.j	$⊢ \underset{˙}{\lor} = join (K)$
2		3atnelvol.a	$⊢ A = Atoms (K)$
3		3atnelvol.v	$⊢ V = LVols (K)$
4		hllat	$⊢ K \in HL \to K \in Lat$
5	4	adantr	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to K \in Lat$
6		eqid	$⊢ {Base}_{K} = {Base}_{K}$
7	6 1 2	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
8	7	3adant3r3	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
9		simpr3	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to R \in A$
10	6 2	atbase	$⊢ R \in A \to R \in {Base}_{K}$
11	9 10	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to R \in {Base}_{K}$
12	6 1	latjcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land R \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in {Base}_{K}$
13	5 8 11 12	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in {Base}_{K}$
14		eqid	$⊢ \leq_{K} = \leq_{K}$
15	6 14	latref	$⊢ (K \in Lat \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in {Base}_{K}) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \leq_{K} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
16	5 13 15	syl2anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \leq_{K} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
17	14 1 2 3	lvolnle3at	$⊢ ((K \in HL \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in V) \land (P \in A \land Q \in A \land R \in A)) \to \neg ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \leq_{K} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
18	17	an32s	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in V) \to \neg ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \leq_{K} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
19	18	ex	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in V \to \neg ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \leq_{K} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
20	16 19	mt2d	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in V$

Metamath Proof Explorer

Theorem 3atnelvolN

Proof