paddss1

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

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

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	orim1d	$⊢ X \subseteq Y \to ((p \in X \lor p \in Z) \to (p \in Y \lor p \in Z))$
5		ssrexv	$⊢ X \subseteq Y \to (\exists q \in X \exists r \in Z p \leq_{K} (q join (K) r) \to \exists q \in Y \exists r \in Z p \leq_{K} (q join (K) r))$
6	5	anim2d	$⊢ X \subseteq Y \to ((p \in A \land \exists q \in X \exists r \in Z p \leq_{K} (q join (K) r)) \to (p \in A \land \exists q \in Y \exists r \in Z p \leq_{K} (q join (K) r)))$
7	4 6	orim12d	$⊢ X \subseteq Y \to (((p \in X \lor p \in Z) \lor (p \in A \land \exists q \in X \exists r \in Z p \leq_{K} (q join (K) r))) \to ((p \in Y \lor p \in Z) \lor (p \in A \land \exists q \in Y \exists r \in Z p \leq_{K} (q join (K) r))))$
8	7	adantl	$⊢ ((K \in B \land Y \subseteq A \land Z \subseteq A) \land X \subseteq Y) \to (((p \in X \lor p \in Z) \lor (p \in A \land \exists q \in X \exists r \in Z p \leq_{K} (q join (K) r))) \to ((p \in Y \lor p \in Z) \lor (p \in A \land \exists q \in Y \exists r \in Z p \leq_{K} (q join (K) r))))$
9		simpl1	$⊢ ((K \in B \land Y \subseteq A \land Z \subseteq A) \land X \subseteq Y) \to K \in B$
10		sstr	$⊢ (X \subseteq Y \land Y \subseteq A) \to X \subseteq A$
11	10	3ad2antr2	$⊢ (X \subseteq Y \land (K \in B \land Y \subseteq A \land Z \subseteq A)) \to X \subseteq A$
12	11	ancoms	$⊢ ((K \in B \land Y \subseteq A \land Z \subseteq A) \land X \subseteq Y) \to X \subseteq A$
13		simpl3	$⊢ ((K \in B \land Y \subseteq A \land Z \subseteq A) \land X \subseteq Y) \to Z \subseteq A$
14		eqid	$⊢ \leq_{K} = \leq_{K}$
15		eqid	$⊢ join (K) = join (K)$
16	14 15 1 2	elpadd	$⊢ (K \in B \land X \subseteq A \land Z \subseteq A) \to (p \in (X \underset{˙}{+} Z) \leftrightarrow ((p \in X \lor p \in Z) \lor (p \in A \land \exists q \in X \exists r \in Z p \leq_{K} (q join (K) r))))$
17	9 12 13 16	syl3anc	$⊢ ((K \in B \land Y \subseteq A \land Z \subseteq A) \land X \subseteq Y) \to (p \in (X \underset{˙}{+} Z) \leftrightarrow ((p \in X \lor p \in Z) \lor (p \in A \land \exists q \in X \exists r \in Z p \leq_{K} (q join (K) r))))$
18	14 15 1 2	elpadd	$⊢ (K \in B \land Y \subseteq A \land Z \subseteq A) \to (p \in (Y \underset{˙}{+} Z) \leftrightarrow ((p \in Y \lor p \in Z) \lor (p \in A \land \exists q \in Y \exists r \in Z p \leq_{K} (q join (K) r))))$
19	18	adantr	$⊢ ((K \in B \land Y \subseteq A \land Z \subseteq A) \land X \subseteq Y) \to (p \in (Y \underset{˙}{+} Z) \leftrightarrow ((p \in Y \lor p \in Z) \lor (p \in A \land \exists q \in Y \exists r \in Z p \leq_{K} (q join (K) r))))$
20	8 17 19	3imtr4d	$⊢ ((K \in B \land Y \subseteq A \land Z \subseteq A) \land X \subseteq Y) \to (p \in (X \underset{˙}{+} Z) \to p \in (Y \underset{˙}{+} Z))$
21	20	ssrdv	$⊢ ((K \in B \land Y \subseteq A \land Z \subseteq A) \land X \subseteq Y) \to X \underset{˙}{+} Z \subseteq Y \underset{˙}{+} Z$
22	21	ex	$⊢ (K \in B \land Y \subseteq A \land Z \subseteq A) \to (X \subseteq Y \to X \underset{˙}{+} Z \subseteq Y \underset{˙}{+} Z)$

Metamath Proof Explorer

Theorem paddss1

Proof