paddasslem13

Description: Lemma for paddass . The case when r .<_ ( x .\/ y ) . (Unlike the proof in Maeda and Maeda, we don't need x =/= y .) (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	paddasslem13	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \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		simpl1l	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to K \in HL$
6		simpl21	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to X \subseteq A$
7		simpl22	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to Y \subseteq A$
8	3 4	paddssat	$⊢ (K \in HL \land X \subseteq A \land Y \subseteq A) \to X \underset{˙}{+} Y \subseteq A$
9	5 6 7 8	syl3anc	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to X \underset{˙}{+} Y \subseteq A$
10		simpl23	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to Z \subseteq A$
11	3 4	sspadd1	$⊢ (K \in HL \land X \underset{˙}{+} Y \subseteq A \land Z \subseteq A) \to X \underset{˙}{+} Y \subseteq (X \underset{˙}{+} Y) \underset{˙}{+} Z$
12	5 9 10 11	syl3anc	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to X \underset{˙}{+} Y \subseteq (X \underset{˙}{+} Y) \underset{˙}{+} Z$
13	5	hllatd	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to K \in Lat$
14		simprll	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to x \in X$
15		simprlr	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to y \in Y$
16		simpl3l	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to p \in A$
17		eqid	$⊢ {Base}_{K} = {Base}_{K}$
18	17 3	atbase	$⊢ p \in A \to p \in {Base}_{K}$
19	16 18	syl	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to p \in {Base}_{K}$
20	6 14	sseldd	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to x \in A$
21	17 3	atbase	$⊢ x \in A \to x \in {Base}_{K}$
22	20 21	syl	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to x \in {Base}_{K}$
23		simpl3r	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to r \in A$
24	17 3	atbase	$⊢ r \in A \to r \in {Base}_{K}$
25	23 24	syl	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to r \in {Base}_{K}$
26	17 2	latjcl	$⊢ (K \in Lat \land x \in {Base}_{K} \land r \in {Base}_{K}) \to x \underset{˙}{\lor} r \in {Base}_{K}$
27	13 22 25 26	syl3anc	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to x \underset{˙}{\lor} r \in {Base}_{K}$
28	7 15	sseldd	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to y \in A$
29	17 3	atbase	$⊢ y \in A \to y \in {Base}_{K}$
30	28 29	syl	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to y \in {Base}_{K}$
31	17 2	latjcl	$⊢ (K \in Lat \land x \in {Base}_{K} \land y \in {Base}_{K}) \to x \underset{˙}{\lor} y \in {Base}_{K}$
32	13 22 30 31	syl3anc	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to x \underset{˙}{\lor} y \in {Base}_{K}$
33		simprrr	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to p \underset{˙}{\leq} (x \underset{˙}{\lor} r)$
34	17 1 2	latlej1	$⊢ (K \in Lat \land x \in {Base}_{K} \land y \in {Base}_{K}) \to x \underset{˙}{\leq} (x \underset{˙}{\lor} y)$
35	13 22 30 34	syl3anc	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to x \underset{˙}{\leq} (x \underset{˙}{\lor} y)$
36		simprrl	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to r \underset{˙}{\leq} (x \underset{˙}{\lor} y)$
37	17 1 2	latjle12	$⊢ (K \in Lat \land (x \in {Base}_{K} \land r \in {Base}_{K} \land x \underset{˙}{\lor} y \in {Base}_{K})) \to ((x \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \leftrightarrow (x \underset{˙}{\lor} r) \underset{˙}{\leq} (x \underset{˙}{\lor} y))$
38	13 22 25 32 37	syl13anc	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to ((x \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \leftrightarrow (x \underset{˙}{\lor} r) \underset{˙}{\leq} (x \underset{˙}{\lor} y))$
39	35 36 38	mpbi2and	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to (x \underset{˙}{\lor} r) \underset{˙}{\leq} (x \underset{˙}{\lor} y)$
40	17 1 13 19 27 32 33 39	lattrd	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to p \underset{˙}{\leq} (x \underset{˙}{\lor} y)$
41	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 (p \in A \land p \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \to p \in (X \underset{˙}{+} Y)$
42	13 6 7 14 15 16 40 41	syl322anc	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to p \in (X \underset{˙}{+} Y)$
43	12 42	sseldd	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)$

Metamath Proof Explorer

Theorem paddasslem13

Proof