paddasslem15

Description: Lemma for paddass . Use elpaddn0 to eliminate y and z from paddasslem14 . (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	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)$

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		simpr2r	$⊢ ((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 r \in (Y \underset{˙}{+} Z)$
6		simpl1	$⊢ ((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 K \in HL$
7	6	hllatd	$⊢ ((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 K \in Lat$
8		simpl22	$⊢ ((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 Y \subseteq A$
9		simpl23	$⊢ ((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 Z \subseteq A$
10		simpl3	$⊢ ((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 (Y \neq \emptyset \land Z \neq \emptyset)$
11	1 2 3 4	elpaddn0	$⊢ ((K \in Lat \land Y \subseteq A \land Z \subseteq A) \land (Y \neq \emptyset \land Z \neq \emptyset)) \to (r \in (Y \underset{˙}{+} Z) \leftrightarrow (r \in A \land \exists y \in Y \exists z \in Z r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))$
12	7 8 9 10 11	syl31anc	$⊢ ((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 (r \in (Y \underset{˙}{+} Z) \leftrightarrow (r \in A \land \exists y \in Y \exists z \in Z r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))$
13	5 12	mpbid	$⊢ ((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 (r \in A \land \exists y \in Y \exists z \in Z r \underset{˙}{\leq} (y \underset{˙}{\lor} z))$
14		simp11	$⊢ ((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)) \land (r \in A \land (y \in Y \land z \in Z) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to K \in HL$
15		simp12	$⊢ ((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)) \land (r \in A \land (y \in Y \land z \in Z) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to (X \subseteq A \land Y \subseteq A \land Z \subseteq A)$
16		simp21	$⊢ ((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)) \land (r \in A \land (y \in Y \land z \in Z) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to p \in A$
17		simp31	$⊢ ((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)) \land (r \in A \land (y \in Y \land z \in Z) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to r \in A$
18	16 17	jca	$⊢ ((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)) \land (r \in A \land (y \in Y \land z \in Z) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to (p \in A \land r \in A)$
19		simp22l	$⊢ ((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)) \land (r \in A \land (y \in Y \land z \in Z) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to x \in X$
20		simp32l	$⊢ ((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)) \land (r \in A \land (y \in Y \land z \in Z) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to y \in Y$
21		simp32r	$⊢ ((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)) \land (r \in A \land (y \in Y \land z \in Z) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to z \in Z$
22	19 20 21	3jca	$⊢ ((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)) \land (r \in A \land (y \in Y \land z \in Z) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to (x \in X \land y \in Y \land z \in Z)$
23		simp23	$⊢ ((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)) \land (r \in A \land (y \in Y \land z \in Z) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to p \underset{˙}{\leq} (x \underset{˙}{\lor} r)$
24		simp33	$⊢ ((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)) \land (r \in A \land (y \in Y \land z \in Z) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to r \underset{˙}{\leq} (y \underset{˙}{\lor} z)$
25	23 24	jca	$⊢ ((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)) \land (r \in A \land (y \in Y \land z \in Z) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))$
26	1 2 3 4	paddasslem14	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)$
27	14 15 18 22 25 26	syl32anc	$⊢ ((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)) \land (r \in A \land (y \in Y \land z \in Z) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)$
28	27	3expia	$⊢ ((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 ((r \in A \land (y \in Y \land z \in Z) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z))$
29	28	3expd	$⊢ ((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 (r \in A \to ((y \in Y \land z \in Z) \to (r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z))))$
30	29	imp	$⊢ (((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))) \land r \in A) \to ((y \in Y \land z \in Z) \to (r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)))$
31	30	rexlimdvv	$⊢ (((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))) \land r \in A) \to (\exists y \in Y \exists z \in Z r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z))$
32	31	expimpd	$⊢ ((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 ((r \in A \land \exists y \in Y \exists z \in Z r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z))$
33	13 32	mpd	$⊢ ((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)$

Metamath Proof Explorer

Theorem paddasslem15

Proof