Metamath Proof Explorer

Theorem paddasslem18

Description: Lemma for paddass . Combine paddasslem16 and paddasslem17 . (Contributed by NM, 12-Jan-2012)

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

Proof

Step	Hyp	Ref	Expression
1		paddass.a	$⊢ A = Atoms (K)$
2		paddass.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
3		eqid	$⊢ \leq_{K} = \leq_{K}$
4		eqid	$⊢ join (K) = join (K)$
5	3 4 1 2	paddasslem16	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land ((X \neq \emptyset \land Y \underset{˙}{+} Z \neq \emptyset) \land (Y \neq \emptyset \land Z \neq \emptyset))) \to X \underset{˙}{+} (Y \underset{˙}{+} Z) \subseteq (X \underset{˙}{+} Y) \underset{˙}{+} Z$
6	5	3expa	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \land ((X \neq \emptyset \land Y \underset{˙}{+} Z \neq \emptyset) \land (Y \neq \emptyset \land Z \neq \emptyset))) \to X \underset{˙}{+} (Y \underset{˙}{+} Z) \subseteq (X \underset{˙}{+} Y) \underset{˙}{+} Z$
7	1 2	paddasslem17	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land \neg ((X \neq \emptyset \land Y \underset{˙}{+} Z \neq \emptyset) \land (Y \neq \emptyset \land Z \neq \emptyset))) \to X \underset{˙}{+} (Y \underset{˙}{+} Z) \subseteq (X \underset{˙}{+} Y) \underset{˙}{+} Z$
8	7	3expa	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \land \neg ((X \neq \emptyset \land Y \underset{˙}{+} Z \neq \emptyset) \land (Y \neq \emptyset \land Z \neq \emptyset))) \to X \underset{˙}{+} (Y \underset{˙}{+} Z) \subseteq (X \underset{˙}{+} Y) \underset{˙}{+} Z$
9	6 8	pm2.61dan	$⊢ (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to X \underset{˙}{+} (Y \underset{˙}{+} Z) \subseteq (X \underset{˙}{+} Y) \underset{˙}{+} Z$