lvolex3N

Description: There is an atom outside of a lattice plane i.e. a 3-dimensional lattice volume exists. (Contributed by NM, 28-Jul-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lvolex3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lvolex3.a	$⊢ A = Atoms (K)$
	lvolex3.p	$⊢ P = LPlanes (K)$
Assertion	lvolex3N	$⊢ (K \in HL \land X \in P) \to \exists q \in A \neg q \underset{˙}{\leq} X$

Proof

Step	Hyp	Ref	Expression
1		lvolex3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		lvolex3.a	$⊢ A = Atoms (K)$
3		lvolex3.p	$⊢ P = LPlanes (K)$
4		eqid	$⊢ {Base}_{K} = {Base}_{K}$
5		eqid	$⊢ join (K) = join (K)$
6	4 1 5 2 3	islpln2	$⊢ K \in HL \to (X \in P \leftrightarrow (X \in {Base}_{K} \land \exists r \in A \exists s \in A \exists t \in A (r \neq s \land \neg t \underset{˙}{\leq} (r join (K) s) \land X = (r join (K) s) join (K) t)))$
7		simp1l	$⊢ ((K \in HL \land (r \in A \land s \in A)) \land t \in A \land (r \neq s \land \neg t \underset{˙}{\leq} (r join (K) s) \land X = (r join (K) s) join (K) t)) \to K \in HL$
8		simp1rl	$⊢ ((K \in HL \land (r \in A \land s \in A)) \land t \in A \land (r \neq s \land \neg t \underset{˙}{\leq} (r join (K) s) \land X = (r join (K) s) join (K) t)) \to r \in A$
9		simp1rr	$⊢ ((K \in HL \land (r \in A \land s \in A)) \land t \in A \land (r \neq s \land \neg t \underset{˙}{\leq} (r join (K) s) \land X = (r join (K) s) join (K) t)) \to s \in A$
10		simp2	$⊢ ((K \in HL \land (r \in A \land s \in A)) \land t \in A \land (r \neq s \land \neg t \underset{˙}{\leq} (r join (K) s) \land X = (r join (K) s) join (K) t)) \to t \in A$
11	5 1 2	3dim3	$⊢ (K \in HL \land (r \in A \land s \in A \land t \in A)) \to \exists q \in A \neg q \underset{˙}{\leq} ((r join (K) s) join (K) t)$
12	7 8 9 10 11	syl13anc	$⊢ ((K \in HL \land (r \in A \land s \in A)) \land t \in A \land (r \neq s \land \neg t \underset{˙}{\leq} (r join (K) s) \land X = (r join (K) s) join (K) t)) \to \exists q \in A \neg q \underset{˙}{\leq} ((r join (K) s) join (K) t)$
13		simp33	$⊢ ((K \in HL \land (r \in A \land s \in A)) \land t \in A \land (r \neq s \land \neg t \underset{˙}{\leq} (r join (K) s) \land X = (r join (K) s) join (K) t)) \to X = (r join (K) s) join (K) t$
14		breq2	$⊢ X = (r join (K) s) join (K) t \to (q \underset{˙}{\leq} X \leftrightarrow q \underset{˙}{\leq} ((r join (K) s) join (K) t))$
15	14	notbid	$⊢ X = (r join (K) s) join (K) t \to (\neg q \underset{˙}{\leq} X \leftrightarrow \neg q \underset{˙}{\leq} ((r join (K) s) join (K) t))$
16	15	rexbidv	$⊢ X = (r join (K) s) join (K) t \to (\exists q \in A \neg q \underset{˙}{\leq} X \leftrightarrow \exists q \in A \neg q \underset{˙}{\leq} ((r join (K) s) join (K) t))$
17	13 16	syl	$⊢ ((K \in HL \land (r \in A \land s \in A)) \land t \in A \land (r \neq s \land \neg t \underset{˙}{\leq} (r join (K) s) \land X = (r join (K) s) join (K) t)) \to (\exists q \in A \neg q \underset{˙}{\leq} X \leftrightarrow \exists q \in A \neg q \underset{˙}{\leq} ((r join (K) s) join (K) t))$
18	12 17	mpbird	$⊢ ((K \in HL \land (r \in A \land s \in A)) \land t \in A \land (r \neq s \land \neg t \underset{˙}{\leq} (r join (K) s) \land X = (r join (K) s) join (K) t)) \to \exists q \in A \neg q \underset{˙}{\leq} X$
19	18	rexlimdv3a	$⊢ (K \in HL \land (r \in A \land s \in A)) \to (\exists t \in A (r \neq s \land \neg t \underset{˙}{\leq} (r join (K) s) \land X = (r join (K) s) join (K) t) \to \exists q \in A \neg q \underset{˙}{\leq} X)$
20	19	rexlimdvva	$⊢ K \in HL \to (\exists r \in A \exists s \in A \exists t \in A (r \neq s \land \neg t \underset{˙}{\leq} (r join (K) s) \land X = (r join (K) s) join (K) t) \to \exists q \in A \neg q \underset{˙}{\leq} X)$
21	20	adantld	$⊢ K \in HL \to ((X \in {Base}_{K} \land \exists r \in A \exists s \in A \exists t \in A (r \neq s \land \neg t \underset{˙}{\leq} (r join (K) s) \land X = (r join (K) s) join (K) t)) \to \exists q \in A \neg q \underset{˙}{\leq} X)$
22	6 21	sylbid	$⊢ K \in HL \to (X \in P \to \exists q \in A \neg q \underset{˙}{\leq} X)$
23	22	imp	$⊢ (K \in HL \land X \in P) \to \exists q \in A \neg q \underset{˙}{\leq} X$

Metamath Proof Explorer

Theorem lvolex3N

Proof