elpadd2at2

Description: Membership in a projective subspace sum of two points. (Contributed by NM, 8-Mar-2012)

	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	elpadd2at2	$⊢ (K \in Lat \land (Q \in A \land R \in A \land S \in A)) \to (S \in (\{Q\} \underset{˙}{+} \{R\}) \leftrightarrow S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$

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	elpadd2at	$⊢ (K \in Lat \land Q \in A \land R \in A) \to (S \in (\{Q\} \underset{˙}{+} \{R\}) \leftrightarrow (S \in A \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))$
6	5	3adant3r3	$⊢ (K \in Lat \land (Q \in A \land R \in A \land S \in A)) \to (S \in (\{Q\} \underset{˙}{+} \{R\}) \leftrightarrow (S \in A \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))$
7		simpr3	$⊢ (K \in Lat \land (Q \in A \land R \in A \land S \in A)) \to S \in A$
8	7	biantrurd	$⊢ (K \in Lat \land (Q \in A \land R \in A \land S \in A)) \to (S \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \leftrightarrow (S \in A \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))$
9	6 8	bitr4d	$⊢ (K \in Lat \land (Q \in A \land R \in A \land S \in A)) \to (S \in (\{Q\} \underset{˙}{+} \{R\}) \leftrightarrow S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$

Metamath Proof Explorer