elpaddri

Description: Condition implying membership in a projective subspace sum. (Contributed by NM, 8-Jan-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	elpaddri	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (Q \in X \land R \in Y) \land (S \in A \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to S \in (X \underset{˙}{+} Y)$

Proof

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		simp3l	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (Q \in X \land R \in Y) \land (S \in A \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to S \in A$
6		simp2l	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (Q \in X \land R \in Y) \land (S \in A \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to Q \in X$
7		simp2r	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (Q \in X \land R \in Y) \land (S \in A \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to R \in Y$
8		simp3r	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (Q \in X \land R \in Y) \land (S \in A \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
9		oveq1	$⊢ q = Q \to q \underset{˙}{\lor} r = Q \underset{˙}{\lor} r$
10	9	breq2d	$⊢ q = Q \to (S \underset{˙}{\leq} (q \underset{˙}{\lor} r) \leftrightarrow S \underset{˙}{\leq} (Q \underset{˙}{\lor} r))$
11		oveq2	$⊢ r = R \to Q \underset{˙}{\lor} r = Q \underset{˙}{\lor} R$
12	11	breq2d	$⊢ r = R \to (S \underset{˙}{\leq} (Q \underset{˙}{\lor} r) \leftrightarrow S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
13	10 12	rspc2ev	$⊢ (Q \in X \land R \in Y \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r)$
14	6 7 8 13	syl3anc	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (Q \in X \land R \in Y) \land (S \in A \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r)$
15		ne0i	$⊢ Q \in X \to X \neq \emptyset$
16		ne0i	$⊢ R \in Y \to Y \neq \emptyset$
17	15 16	anim12i	$⊢ (Q \in X \land R \in Y) \to (X \neq \emptyset \land Y \neq \emptyset)$
18	17	anim2i	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (Q \in X \land R \in Y)) \to ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (X \neq \emptyset \land Y \neq \emptyset))$
19	18	3adant3	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (Q \in X \land R \in Y) \land (S \in A \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (X \neq \emptyset \land Y \neq \emptyset))$
20	1 2 3 4	elpaddn0	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (X \neq \emptyset \land Y \neq \emptyset)) \to (S \in (X \underset{˙}{+} Y) \leftrightarrow (S \in A \land \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r)))$
21	19 20	syl	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (Q \in X \land R \in Y) \land (S \in A \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to (S \in (X \underset{˙}{+} Y) \leftrightarrow (S \in A \land \exists q \in X \exists r \in Y S \underset{˙}{\leq} (q \underset{˙}{\lor} r)))$
22	5 14 21	mpbir2and	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (Q \in X \land R \in Y) \land (S \in A \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to S \in (X \underset{˙}{+} Y)$

Metamath Proof Explorer

Theorem elpaddri

Proof