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

Metamath Proof Explorer

Theorem paddss12

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

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

Proof

Step	Hyp	Ref	Expression
1		padd0.a	$⊢ A = Atoms (K)$
2		padd0.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
3		simpl1	$⊢ ((K \in B \land Y \subseteq A \land W \subseteq A) \land (X \subseteq Y \land Z \subseteq W)) \to K \in B$
4		simpl2	$⊢ ((K \in B \land Y \subseteq A \land W \subseteq A) \land (X \subseteq Y \land Z \subseteq W)) \to Y \subseteq A$
5		sstr	$⊢ (Z \subseteq W \land W \subseteq A) \to Z \subseteq A$
6	5	ancoms	$⊢ (W \subseteq A \land Z \subseteq W) \to Z \subseteq A$
7	6	ad2ant2l	$⊢ ((Y \subseteq A \land W \subseteq A) \land (X \subseteq Y \land Z \subseteq W)) \to Z \subseteq A$
8	7	3adantl1	$⊢ ((K \in B \land Y \subseteq A \land W \subseteq A) \land (X \subseteq Y \land Z \subseteq W)) \to Z \subseteq A$
9	3 4 8	3jca	$⊢ ((K \in B \land Y \subseteq A \land W \subseteq A) \land (X \subseteq Y \land Z \subseteq W)) \to (K \in B \land Y \subseteq A \land Z \subseteq A)$
10		simprl	$⊢ ((K \in B \land Y \subseteq A \land W \subseteq A) \land (X \subseteq Y \land Z \subseteq W)) \to X \subseteq Y$
11	1 2	paddss1	$⊢ (K \in B \land Y \subseteq A \land Z \subseteq A) \to (X \subseteq Y \to X \underset{˙}{+} Z \subseteq Y \underset{˙}{+} Z)$
12	9 10 11	sylc	$⊢ ((K \in B \land Y \subseteq A \land W \subseteq A) \land (X \subseteq Y \land Z \subseteq W)) \to X \underset{˙}{+} Z \subseteq Y \underset{˙}{+} Z$
13	1 2	paddss2	$⊢ (K \in B \land W \subseteq A \land Y \subseteq A) \to (Z \subseteq W \to Y \underset{˙}{+} Z \subseteq Y \underset{˙}{+} W)$
14	13	3com23	$⊢ (K \in B \land Y \subseteq A \land W \subseteq A) \to (Z \subseteq W \to Y \underset{˙}{+} Z \subseteq Y \underset{˙}{+} W)$
15	14	imp	$⊢ ((K \in B \land Y \subseteq A \land W \subseteq A) \land Z \subseteq W) \to Y \underset{˙}{+} Z \subseteq Y \underset{˙}{+} W$
16	15	adantrl	$⊢ ((K \in B \land Y \subseteq A \land W \subseteq A) \land (X \subseteq Y \land Z \subseteq W)) \to Y \underset{˙}{+} Z \subseteq Y \underset{˙}{+} W$
17	12 16	sstrd	$⊢ ((K \in B \land Y \subseteq A \land W \subseteq A) \land (X \subseteq Y \land Z \subseteq W)) \to X \underset{˙}{+} Z \subseteq Y \underset{˙}{+} W$
18	17	ex	$⊢ (K \in B \land Y \subseteq A \land W \subseteq A) \to ((X \subseteq Y \land Z \subseteq W) \to X \underset{˙}{+} Z \subseteq Y \underset{˙}{+} W)$