paddasslem16

Description: Lemma for paddass . Use elpaddn0 to eliminate x and r from paddasslem15 . (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	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$

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		hllat	$⊢ K \in HL \to K \in Lat$
6	5	3ad2ant1	$⊢ (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 K \in Lat$
7		simp21	$⊢ (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 \subseteq A$
8		simp1	$⊢ (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 K \in HL$
9		simp22	$⊢ (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 Y \subseteq A$
10		simp23	$⊢ (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 Z \subseteq A$
11	3 4	paddssat	$⊢ (K \in HL \land Y \subseteq A \land Z \subseteq A) \to Y \underset{˙}{+} Z \subseteq A$
12	8 9 10 11	syl3anc	$⊢ (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 Y \underset{˙}{+} Z \subseteq A$
13		simp3l	$⊢ (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 \neq \emptyset \land Y \underset{˙}{+} Z \neq \emptyset)$
14	1 2 3 4	elpaddn0	$⊢ ((K \in Lat \land X \subseteq A \land Y \underset{˙}{+} Z \subseteq A) \land (X \neq \emptyset \land Y \underset{˙}{+} Z \neq \emptyset)) \to (p \in (X \underset{˙}{+} (Y \underset{˙}{+} Z)) \leftrightarrow (p \in A \land \exists x \in X \exists r \in (Y \underset{˙}{+} Z) p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))$
15	6 7 12 13 14	syl31anc	$⊢ (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 (p \in (X \underset{˙}{+} (Y \underset{˙}{+} Z)) \leftrightarrow (p \in A \land \exists x \in X \exists r \in (Y \underset{˙}{+} Z) p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))$
16		simpr	$⊢ ((X \neq \emptyset \land Y \underset{˙}{+} Z \neq \emptyset) \land (Y \neq \emptyset \land Z \neq \emptyset)) \to (Y \neq \emptyset \land Z \neq \emptyset)$
17	1 2 3 4	paddasslem15	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (Y \neq \emptyset \land Z \neq \emptyset)) \land (p \in A \land (x \in X \land r \in (Y \underset{˙}{+} Z)) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)$
18	16 17	syl3anl3	$⊢ ((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))) \land (p \in A \land (x \in X \land r \in (Y \underset{˙}{+} Z)) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)$
19	18	3exp2	$⊢ (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 (p \in A \to ((x \in X \land r \in (Y \underset{˙}{+} Z)) \to (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z))))$
20	19	imp	$⊢ ((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))) \land p \in A) \to ((x \in X \land r \in (Y \underset{˙}{+} Z)) \to (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)))$
21	20	rexlimdvv	$⊢ ((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))) \land p \in A) \to (\exists x \in X \exists r \in (Y \underset{˙}{+} Z) p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z))$
22	21	expimpd	$⊢ (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 ((p \in A \land \exists x \in X \exists r \in (Y \underset{˙}{+} Z) p \underset{˙}{\leq} (x \underset{˙}{\lor} r)) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z))$
23	15 22	sylbid	$⊢ (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 (p \in (X \underset{˙}{+} (Y \underset{˙}{+} Z)) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z))$
24	23	ssrdv	$⊢ (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$

Metamath Proof Explorer

Theorem paddasslem16

Proof