elpaddatiN

Description: Consequence of membership in a projective subspace sum with a point. (Contributed by NM, 2-Feb-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	paddfval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	paddfval.j	$⊢ \underset{˙}{\lor} = join (K)$
	paddfval.a	$⊢ A = Atoms (K)$
	paddfval.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
Assertion	elpaddatiN	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land (X \neq \emptyset \land R \in (X \underset{˙}{+} \{Q\}))) \to \exists p \in X R \underset{˙}{\leq} (p \underset{˙}{\lor} Q)$

Step	Hyp	Ref	Expression
1		paddfval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		paddfval.j	$⊢ \underset{˙}{\lor} = join (K)$
3		paddfval.a	$⊢ A = Atoms (K)$
4		paddfval.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
5	1 2 3 4	elpaddat	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land X \neq \emptyset) \to (R \in (X \underset{˙}{+} \{Q\}) \leftrightarrow (R \in A \land \exists p \in X R \underset{˙}{\leq} (p \underset{˙}{\lor} Q)))$
6		simpr	$⊢ (R \in A \land \exists p \in X R \underset{˙}{\leq} (p \underset{˙}{\lor} Q)) \to \exists p \in X R \underset{˙}{\leq} (p \underset{˙}{\lor} Q)$
7	5 6	biimtrdi	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land X \neq \emptyset) \to (R \in (X \underset{˙}{+} \{Q\}) \to \exists p \in X R \underset{˙}{\leq} (p \underset{˙}{\lor} Q))$
8	7	impr	$⊢ ((K \in Lat \land X \subseteq A \land Q \in A) \land (X \neq \emptyset \land R \in (X \underset{˙}{+} \{Q\}))) \to \exists p \in X R \underset{˙}{\leq} (p \underset{˙}{\lor} Q)$

Metamath Proof Explorer