This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem paddssw2

Description: Subset law for projective subspace sum valid for all subsets of atoms. (Contributed by NM, 14-Mar-2012)

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

Proof

Step	Hyp	Ref	Expression
1		paddssw.a	$⊢ A = Atoms (K)$
2		paddssw.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
3	1 2	sspadd1	$⊢ (K \in B \land X \subseteq A \land Y \subseteq A) \to X \subseteq X \underset{˙}{+} Y$
4	3	3adant3r3	$⊢ (K \in B \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to X \subseteq X \underset{˙}{+} Y$
5		sstr	$⊢ (X \subseteq X \underset{˙}{+} Y \land X \underset{˙}{+} Y \subseteq Z) \to X \subseteq Z$
6	4 5	sylan	$⊢ ((K \in B \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \land X \underset{˙}{+} Y \subseteq Z) \to X \subseteq Z$
7	6	ex	$⊢ (K \in B \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to (X \underset{˙}{+} Y \subseteq Z \to X \subseteq Z)$
8		simpl	$⊢ (K \in B \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to K \in B$
9		simpr2	$⊢ (K \in B \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to Y \subseteq A$
10		simpr1	$⊢ (K \in B \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to X \subseteq A$
11	1 2	sspadd2	$⊢ (K \in B \land Y \subseteq A \land X \subseteq A) \to Y \subseteq X \underset{˙}{+} Y$
12	8 9 10 11	syl3anc	$⊢ (K \in B \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to Y \subseteq X \underset{˙}{+} Y$
13		sstr	$⊢ (Y \subseteq X \underset{˙}{+} Y \land X \underset{˙}{+} Y \subseteq Z) \to Y \subseteq Z$
14	12 13	sylan	$⊢ ((K \in B \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \land X \underset{˙}{+} Y \subseteq Z) \to Y \subseteq Z$
15	14	ex	$⊢ (K \in B \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to (X \underset{˙}{+} Y \subseteq Z \to Y \subseteq Z)$
16	7 15	jcad	$⊢ (K \in B \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to (X \underset{˙}{+} Y \subseteq Z \to (X \subseteq Z \land Y \subseteq Z))$