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

Metamath Proof Explorer

Theorem paddasslem11

Description: Lemma for paddass . The case when p = z . (Contributed by NM, 11-Jan-2012)

		Ref	Expression
	Hypotheses	paddasslem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		paddasslem.j	$⊢ \underset{˙}{\lor} = join (K)$
		paddasslem.a	$⊢ A = Atoms (K)$
		paddasslem.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
	Assertion	paddasslem11	$⊢ (((K \in HL \land p = z) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \land z \in Z) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)$

Proof

Step	Hyp	Ref	Expression
1		paddasslem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		paddasslem.j	$⊢ \underset{˙}{\lor} = join (K)$
3		paddasslem.a	$⊢ A = Atoms (K)$
4		paddasslem.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
5		simplll	$⊢ (((K \in HL \land p = z) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \land z \in Z) \to K \in HL$
6		simplr3	$⊢ (((K \in HL \land p = z) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \land z \in Z) \to Z \subseteq A$
7		simplr1	$⊢ (((K \in HL \land p = z) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \land z \in Z) \to X \subseteq A$
8		simplr2	$⊢ (((K \in HL \land p = z) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \land z \in Z) \to Y \subseteq A$
9	3 4	paddssat	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq A) \to X \underset{˙}{+} Y \subseteq A$
10	5 7 8 9	syl3anc	$⊢ (((K \in HL \land p = z) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \land z \in Z) \to X \underset{˙}{+} Y \subseteq A$
11	3 4	sspadd2	$⊢ (K \in HL \land Z \subseteq A \land X \underset{˙}{+} Y \subseteq A) \to Z \subseteq (X \underset{˙}{+} Y) \underset{˙}{+} Z$
12	5 6 10 11	syl3anc	$⊢ (((K \in HL \land p = z) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \land z \in Z) \to Z \subseteq (X \underset{˙}{+} Y) \underset{˙}{+} Z$
13		simpllr	$⊢ (((K \in HL \land p = z) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \land z \in Z) \to p = z$
14		simpr	$⊢ (((K \in HL \land p = z) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \land z \in Z) \to z \in Z$
15	13 14	eqeltrd	$⊢ (((K \in HL \land p = z) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \land z \in Z) \to p \in Z$
16	12 15	sseldd	$⊢ (((K \in HL \land p = z) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \land z \in Z) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)$