paddssat

Description: A projective subspace sum is a set of atoms. (Contributed by NM, 3-Jan-2012)

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

Step	Hyp	Ref	Expression
1		padd0.a	$⊢ A = Atoms (K)$
2		padd0.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
3		eqid	$⊢ \leq_{K} = \leq_{K}$
4		eqid	$⊢ join (K) = join (K)$
5	3 4 1 2	paddval	$⊢ (K \in B \land X \subseteq A \land Y \subseteq A) \to X \underset{˙}{+} Y = (X \cup Y) \cup \{p \in A \| \exists q \in X \exists r \in Y p \leq_{K} (q join (K) r)\}$
6		unss	$⊢ (X \subseteq A \land Y \subseteq A) \leftrightarrow X \cup Y \subseteq A$
7	6	biimpi	$⊢ (X \subseteq A \land Y \subseteq A) \to X \cup Y \subseteq A$
8		ssrab2	$⊢ \{p \in A \| \exists q \in X \exists r \in Y p \leq_{K} (q join (K) r)\} \subseteq A$
9	7 8	jctir	$⊢ (X \subseteq A \land Y \subseteq A) \to (X \cup Y \subseteq A \land \{p \in A \| \exists q \in X \exists r \in Y p \leq_{K} (q join (K) r)\} \subseteq A)$
10		unss	$⊢ (X \cup Y \subseteq A \land \{p \in A \| \exists q \in X \exists r \in Y p \leq_{K} (q join (K) r)\} \subseteq A) \leftrightarrow (X \cup Y) \cup \{p \in A \| \exists q \in X \exists r \in Y p \leq_{K} (q join (K) r)\} \subseteq A$
11	9 10	sylib	$⊢ (X \subseteq A \land Y \subseteq A) \to (X \cup Y) \cup \{p \in A \| \exists q \in X \exists r \in Y p \leq_{K} (q join (K) r)\} \subseteq A$
12	11	3adant1	$⊢ (K \in B \land X \subseteq A \land Y \subseteq A) \to (X \cup Y) \cup \{p \in A \| \exists q \in X \exists r \in Y p \leq_{K} (q join (K) r)\} \subseteq A$
13	5 12	eqsstrd	$⊢ (K \in B \land X \subseteq A \land Y \subseteq A) \to X \underset{˙}{+} Y \subseteq A$

Metamath Proof Explorer