islpln2

Description: The predicate "is a lattice plane" in terms of atoms. (Contributed by NM, 25-Jun-2012)

	Ref	Expression
Hypotheses	islpln5.b	$⊢ B = {Base}_{K}$
	islpln5.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	islpln5.j	$⊢ \underset{˙}{\lor} = join (K)$
	islpln5.a	$⊢ A = Atoms (K)$
	islpln5.p	$⊢ P = LPlanes (K)$
Assertion	islpln2	$⊢ K \in HL \to (X \in P \leftrightarrow (X \in B \land \exists p \in A \exists q \in A \exists r \in A (p \neq q \land \neg r \underset{˙}{\leq} (p \underset{˙}{\lor} q) \land X = (p \underset{˙}{\lor} q) \underset{˙}{\lor} r)))$

Step	Hyp	Ref	Expression
1		islpln5.b	$⊢ B = {Base}_{K}$
2		islpln5.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		islpln5.j	$⊢ \underset{˙}{\lor} = join (K)$
4		islpln5.a	$⊢ A = Atoms (K)$
5		islpln5.p	$⊢ P = LPlanes (K)$
6	1 5	lplnbase	$⊢ X \in P \to X \in B$
7	6	pm4.71ri	$⊢ X \in P \leftrightarrow (X \in B \land X \in P)$
8	1 2 3 4 5	islpln5	$⊢ (K \in HL \land X \in B) \to (X \in P \leftrightarrow \exists p \in A \exists q \in A \exists r \in A (p \neq q \land \neg r \underset{˙}{\leq} (p \underset{˙}{\lor} q) \land X = (p \underset{˙}{\lor} q) \underset{˙}{\lor} r))$
9	8	pm5.32da	$⊢ K \in HL \to ((X \in B \land X \in P) \leftrightarrow (X \in B \land \exists p \in A \exists q \in A \exists r \in A (p \neq q \land \neg r \underset{˙}{\leq} (p \underset{˙}{\lor} q) \land X = (p \underset{˙}{\lor} q) \underset{˙}{\lor} r)))$
10	7 9	bitrid	$⊢ K \in HL \to (X \in P \leftrightarrow (X \in B \land \exists p \in A \exists q \in A \exists r \in A (p \neq q \land \neg r \underset{˙}{\leq} (p \underset{˙}{\lor} q) \land X = (p \underset{˙}{\lor} q) \underset{˙}{\lor} r)))$

Metamath Proof Explorer