Metamath Proof Explorer

Theorem paddss

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

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

Proof

Step	Hyp	Ref	Expression
1		paddss.a	$⊢ A = Atoms (K)$
2		paddss.s	$⊢ S = PSubSp (K)$
3		paddss.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
4		simpl	$⊢ (K \in B \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \to K \in B$
5		simpr1	$⊢ (K \in B \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \to X \subseteq A$
6		simpr2	$⊢ (K \in B \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \to Y \subseteq A$
7	1 2	psubssat	$⊢ (K \in B \land Z \in S) \to Z \subseteq A$
8	7	3ad2antr3	$⊢ (K \in B \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \to Z \subseteq A$
9	1 3	paddssw1	$⊢ (K \in B \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to ((X \subseteq Z \land Y \subseteq Z) \to X \underset{˙}{+} Y \subseteq Z \underset{˙}{+} Z)$
10	4 5 6 8 9	syl13anc	$⊢ (K \in B \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \to ((X \subseteq Z \land Y \subseteq Z) \to X \underset{˙}{+} Y \subseteq Z \underset{˙}{+} Z)$
11	2 3	paddidm	$⊢ (K \in B \land Z \in S) \to Z \underset{˙}{+} Z = Z$
12	11	3ad2antr3	$⊢ (K \in B \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \to Z \underset{˙}{+} Z = Z$
13	12	sseq2d	$⊢ (K \in B \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \to (X \underset{˙}{+} Y \subseteq Z \underset{˙}{+} Z \leftrightarrow X \underset{˙}{+} Y \subseteq Z)$
14	10 13	sylibd	$⊢ (K \in B \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \to ((X \subseteq Z \land Y \subseteq Z) \to X \underset{˙}{+} Y \subseteq Z)$
15	1 3	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))$
16	4 5 6 8 15	syl13anc	$⊢ (K \in B \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \to (X \underset{˙}{+} Y \subseteq Z \to (X \subseteq Z \land Y \subseteq Z))$
17	14 16	impbid	$⊢ (K \in B \land (X \subseteq A \land Y \subseteq A \land Z \in S)) \to ((X \subseteq Z \land Y \subseteq Z) \leftrightarrow X \underset{˙}{+} Y \subseteq Z)$