sspadd2

Description: A projective subspace sum is a superset of its second summand. ( ssun2 analog.) (Contributed by NM, 3-Jan-2012)

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

Step	Hyp	Ref	Expression
1		padd0.a	$⊢ A = Atoms (K)$
2		padd0.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
3		ssun2	$⊢ X \subseteq Y \cup X$
4		ssun1	$⊢ Y \cup X \subseteq (Y \cup X) \cup \{p \in A \| \exists q \in Y \exists r \in X p \leq_{K} (q join (K) r)\}$
5	3 4	sstri	$⊢ X \subseteq (Y \cup X) \cup \{p \in A \| \exists q \in Y \exists r \in X p \leq_{K} (q join (K) r)\}$
6		eqid	$⊢ \leq_{K} = \leq_{K}$
7		eqid	$⊢ join (K) = join (K)$
8	6 7 1 2	paddval	$⊢ (K \in B \land Y \subseteq A \land X \subseteq A) \to Y \underset{˙}{+} X = (Y \cup X) \cup \{p \in A \| \exists q \in Y \exists r \in X p \leq_{K} (q join (K) r)\}$
9	8	3com23	$⊢ (K \in B \land X \subseteq A \land Y \subseteq A) \to Y \underset{˙}{+} X = (Y \cup X) \cup \{p \in A \| \exists q \in Y \exists r \in X p \leq_{K} (q join (K) r)\}$
10	5 9	sseqtrrid	$⊢ (K \in B \land X \subseteq A \land Y \subseteq A) \to X \subseteq Y \underset{˙}{+} X$

Metamath Proof Explorer