paddss2

Description: Subset law for projective subspace sum. ( unss2 analog.) (Contributed by NM, 7-Mar-2012)

	Ref	Expression
Hypotheses	padd0.a	$⊢ A = Atoms (K)$
	padd0.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
Assertion	paddss2	$⊢ (K \in B \land Y \subseteq A \land Z \subseteq A) \to (X \subseteq Y \to Z \underset{˙}{+} X \subseteq Z \underset{˙}{+} Y)$

Proof

Step	Hyp	Ref	Expression
1		padd0.a	$⊢ A = Atoms (K)$
2		padd0.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
3		ssel	$⊢ X \subseteq Y \to (p \in X \to p \in Y)$
4	3	orim2d	$⊢ X \subseteq Y \to ((p \in Z \lor p \in X) \to (p \in Z \lor p \in Y))$
5		ssrexv	$⊢ X \subseteq Y \to (\exists r \in X p \leq_{K} (q join (K) r) \to \exists r \in Y p \leq_{K} (q join (K) r))$
6	5	reximdv	$⊢ X \subseteq Y \to (\exists q \in Z \exists r \in X p \leq_{K} (q join (K) r) \to \exists q \in Z \exists r \in Y p \leq_{K} (q join (K) r))$
7	6	anim2d	$⊢ X \subseteq Y \to ((p \in A \land \exists q \in Z \exists r \in X p \leq_{K} (q join (K) r)) \to (p \in A \land \exists q \in Z \exists r \in Y p \leq_{K} (q join (K) r)))$
8	4 7	orim12d	$⊢ X \subseteq Y \to (((p \in Z \lor p \in X) \lor (p \in A \land \exists q \in Z \exists r \in X p \leq_{K} (q join (K) r))) \to ((p \in Z \lor p \in Y) \lor (p \in A \land \exists q \in Z \exists r \in Y p \leq_{K} (q join (K) r))))$
9	8	adantl	$⊢ ((K \in B \land Y \subseteq A \land Z \subseteq A) \land X \subseteq Y) \to (((p \in Z \lor p \in X) \lor (p \in A \land \exists q \in Z \exists r \in X p \leq_{K} (q join (K) r))) \to ((p \in Z \lor p \in Y) \lor (p \in A \land \exists q \in Z \exists r \in Y p \leq_{K} (q join (K) r))))$
10		simpl1	$⊢ ((K \in B \land Y \subseteq A \land Z \subseteq A) \land X \subseteq Y) \to K \in B$
11		simpl3	$⊢ ((K \in B \land Y \subseteq A \land Z \subseteq A) \land X \subseteq Y) \to Z \subseteq A$
12		sstr	$⊢ (X \subseteq Y \land Y \subseteq A) \to X \subseteq A$
13	12	3ad2antr2	$⊢ (X \subseteq Y \land (K \in B \land Y \subseteq A \land Z \subseteq A)) \to X \subseteq A$
14	13	ancoms	$⊢ ((K \in B \land Y \subseteq A \land Z \subseteq A) \land X \subseteq Y) \to X \subseteq A$
15		eqid	$⊢ \leq_{K} = \leq_{K}$
16		eqid	$⊢ join (K) = join (K)$
17	15 16 1 2	elpadd	$⊢ (K \in B \land Z \subseteq A \land X \subseteq A) \to (p \in (Z \underset{˙}{+} X) \leftrightarrow ((p \in Z \lor p \in X) \lor (p \in A \land \exists q \in Z \exists r \in X p \leq_{K} (q join (K) r))))$
18	10 11 14 17	syl3anc	$⊢ ((K \in B \land Y \subseteq A \land Z \subseteq A) \land X \subseteq Y) \to (p \in (Z \underset{˙}{+} X) \leftrightarrow ((p \in Z \lor p \in X) \lor (p \in A \land \exists q \in Z \exists r \in X p \leq_{K} (q join (K) r))))$
19		simpl2	$⊢ ((K \in B \land Y \subseteq A \land Z \subseteq A) \land X \subseteq Y) \to Y \subseteq A$
20	15 16 1 2	elpadd	$⊢ (K \in B \land Z \subseteq A \land Y \subseteq A) \to (p \in (Z \underset{˙}{+} Y) \leftrightarrow ((p \in Z \lor p \in Y) \lor (p \in A \land \exists q \in Z \exists r \in Y p \leq_{K} (q join (K) r))))$
21	10 11 19 20	syl3anc	$⊢ ((K \in B \land Y \subseteq A \land Z \subseteq A) \land X \subseteq Y) \to (p \in (Z \underset{˙}{+} Y) \leftrightarrow ((p \in Z \lor p \in Y) \lor (p \in A \land \exists q \in Z \exists r \in Y p \leq_{K} (q join (K) r))))$
22	9 18 21	3imtr4d	$⊢ ((K \in B \land Y \subseteq A \land Z \subseteq A) \land X \subseteq Y) \to (p \in (Z \underset{˙}{+} X) \to p \in (Z \underset{˙}{+} Y))$
23	22	ssrdv	$⊢ ((K \in B \land Y \subseteq A \land Z \subseteq A) \land X \subseteq Y) \to Z \underset{˙}{+} X \subseteq Z \underset{˙}{+} Y$
24	23	ex	$⊢ (K \in B \land Y \subseteq A \land Z \subseteq A) \to (X \subseteq Y \to Z \underset{˙}{+} X \subseteq Z \underset{˙}{+} Y)$

Metamath Proof Explorer

Theorem paddss2

Proof