paddasslem8

	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	paddasslem8	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land s \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (s \underset{˙}{\lor} 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		simpl1	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land s \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (s \underset{˙}{\lor} z))) \to K \in HL$
6	5	hllatd	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land s \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (s \underset{˙}{\lor} z))) \to K \in Lat$
7		simpl21	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land s \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (s \underset{˙}{\lor} z))) \to X \subseteq A$
8		simpl22	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land s \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (s \underset{˙}{\lor} 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 (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land s \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (s \underset{˙}{\lor} z))) \to X \underset{˙}{+} Y \subseteq A$
11		simpl23	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land s \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (s \underset{˙}{\lor} z))) \to Z \subseteq A$
12		simpr11	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land s \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (s \underset{˙}{\lor} z))) \to x \in X$
13		simpr12	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land s \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (s \underset{˙}{\lor} z))) \to y \in Y$
14		simpl3r	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land s \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (s \underset{˙}{\lor} z))) \to s \in A$
15		simpr2	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land s \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (s \underset{˙}{\lor} z))) \to s \underset{˙}{\leq} (x \underset{˙}{\lor} y)$
16	1 2 3 4	elpaddri	$⊢ ((K \in Lat \land X \subseteq A \land Y \subseteq A) \land (x \in X \land y \in Y) \land (s \in A \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \to s \in (X \underset{˙}{+} Y)$
17	6 7 8 12 13 14 15 16	syl322anc	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land s \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (s \underset{˙}{\lor} z))) \to s \in (X \underset{˙}{+} Y)$
18		simpr13	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land s \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (s \underset{˙}{\lor} z))) \to z \in Z$
19		simpl3l	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land s \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (s \underset{˙}{\lor} z))) \to p \in A$
20		simpr3	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land s \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (s \underset{˙}{\lor} z))) \to p \underset{˙}{\leq} (s \underset{˙}{\lor} z)$
21	1 2 3 4	elpaddri	$⊢ ((K \in Lat \land X \underset{˙}{+} Y \subseteq A \land Z \subseteq A) \land (s \in (X \underset{˙}{+} Y) \land z \in Z) \land (p \in A \land p \underset{˙}{\leq} (s \underset{˙}{\lor} z))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)$
22	6 10 11 17 18 19 20 21	syl322anc	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land s \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (s \underset{˙}{\lor} z))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)$

Metamath Proof Explorer

Theorem paddasslem8

Proof