elpadd0

Description: Member of projective subspace sum with at least one empty set. (Contributed by NM, 29-Dec-2011)

	Ref	Expression
Hypotheses	padd0.a	$⊢ A = Atoms (K)$
	padd0.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
Assertion	elpadd0	$⊢ ((K \in B \land X \subseteq A \land Y \subseteq A) \land \neg (X \neq \emptyset \land Y \neq \emptyset)) \to (S \in (X \underset{˙}{+} Y) \leftrightarrow (S \in X \lor S \in Y))$

Proof

Step	Hyp	Ref	Expression
1		padd0.a	$⊢ A = Atoms (K)$
2		padd0.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
3		neanior	$⊢ (X \neq \emptyset \land Y \neq \emptyset) \leftrightarrow \neg (X = \emptyset \lor Y = \emptyset)$
4	3	bicomi	$⊢ \neg (X = \emptyset \lor Y = \emptyset) \leftrightarrow (X \neq \emptyset \land Y \neq \emptyset)$
5	4	con1bii	$⊢ \neg (X \neq \emptyset \land Y \neq \emptyset) \leftrightarrow (X = \emptyset \lor Y = \emptyset)$
6		eqid	$⊢ \leq_{K} = \leq_{K}$
7		eqid	$⊢ join (K) = join (K)$
8	6 7 1 2	elpadd	$⊢ (K \in B \land X \subseteq A \land Y \subseteq A) \to (S \in (X \underset{˙}{+} Y) \leftrightarrow ((S \in X \lor S \in Y) \lor (S \in A \land \exists q \in X \exists r \in Y S \leq_{K} (q join (K) r))))$
9		rex0	$⊢ \neg \exists q \in \emptyset \exists r \in Y S \leq_{K} (q join (K) r)$
10		rexeq	$⊢ X = \emptyset \to (\exists q \in X \exists r \in Y S \leq_{K} (q join (K) r) \leftrightarrow \exists q \in \emptyset \exists r \in Y S \leq_{K} (q join (K) r))$
11	9 10	mtbiri	$⊢ X = \emptyset \to \neg \exists q \in X \exists r \in Y S \leq_{K} (q join (K) r)$
12		rex0	$⊢ \neg \exists r \in \emptyset S \leq_{K} (q join (K) r)$
13	12	a1i	$⊢ q \in X \to \neg \exists r \in \emptyset S \leq_{K} (q join (K) r)$
14	13	nrex	$⊢ \neg \exists q \in X \exists r \in \emptyset S \leq_{K} (q join (K) r)$
15		rexeq	$⊢ Y = \emptyset \to (\exists r \in Y S \leq_{K} (q join (K) r) \leftrightarrow \exists r \in \emptyset S \leq_{K} (q join (K) r))$
16	15	rexbidv	$⊢ Y = \emptyset \to (\exists q \in X \exists r \in Y S \leq_{K} (q join (K) r) \leftrightarrow \exists q \in X \exists r \in \emptyset S \leq_{K} (q join (K) r))$
17	14 16	mtbiri	$⊢ Y = \emptyset \to \neg \exists q \in X \exists r \in Y S \leq_{K} (q join (K) r)$
18	11 17	jaoi	$⊢ (X = \emptyset \lor Y = \emptyset) \to \neg \exists q \in X \exists r \in Y S \leq_{K} (q join (K) r)$
19	18	intnand	$⊢ (X = \emptyset \lor Y = \emptyset) \to \neg (S \in A \land \exists q \in X \exists r \in Y S \leq_{K} (q join (K) r))$
20		biorf	$⊢ \neg (S \in A \land \exists q \in X \exists r \in Y S \leq_{K} (q join (K) r)) \to ((S \in X \lor S \in Y) \leftrightarrow ((S \in A \land \exists q \in X \exists r \in Y S \leq_{K} (q join (K) r)) \lor (S \in X \lor S \in Y)))$
21	19 20	syl	$⊢ (X = \emptyset \lor Y = \emptyset) \to ((S \in X \lor S \in Y) \leftrightarrow ((S \in A \land \exists q \in X \exists r \in Y S \leq_{K} (q join (K) r)) \lor (S \in X \lor S \in Y)))$
22		orcom	$⊢ ((S \in A \land \exists q \in X \exists r \in Y S \leq_{K} (q join (K) r)) \lor (S \in X \lor S \in Y)) \leftrightarrow ((S \in X \lor S \in Y) \lor (S \in A \land \exists q \in X \exists r \in Y S \leq_{K} (q join (K) r)))$
23	21 22	bitr2di	$⊢ (X = \emptyset \lor Y = \emptyset) \to (((S \in X \lor S \in Y) \lor (S \in A \land \exists q \in X \exists r \in Y S \leq_{K} (q join (K) r))) \leftrightarrow (S \in X \lor S \in Y))$
24	8 23	sylan9bb	$⊢ ((K \in B \land X \subseteq A \land Y \subseteq A) \land (X = \emptyset \lor Y = \emptyset)) \to (S \in (X \underset{˙}{+} Y) \leftrightarrow (S \in X \lor S \in Y))$
25	5 24	sylan2b	$⊢ ((K \in B \land X \subseteq A \land Y \subseteq A) \land \neg (X \neq \emptyset \land Y \neq \emptyset)) \to (S \in (X \underset{˙}{+} Y) \leftrightarrow (S \in X \lor S \in Y))$

Metamath Proof Explorer

Theorem elpadd0

Proof