paddasslem12

Description: Lemma for paddass . The case when 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	paddasslem12	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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)$

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 x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 K \in HL$
6		simpl21	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 X \subseteq A$
7		simpl22	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 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 x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 X \underset{˙}{+} Y \subseteq A$
10		simpl23	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 Z \subseteq A$
11	5 9 10	3jca	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 (K \in HL \land X \underset{˙}{+} Y \subseteq A \land Z \subseteq A)$
12	3 4	sspadd2	$⊢ (K \in HL \land Y \subseteq A \land X \subseteq A) \to Y \subseteq X \underset{˙}{+} Y$
13	5 7 6 12	syl3anc	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 Y \subseteq X \underset{˙}{+} Y$
14	3 4	paddss1	$⊢ (K \in HL \land X \underset{˙}{+} Y \subseteq A \land Z \subseteq A) \to (Y \subseteq X \underset{˙}{+} Y \to Y \underset{˙}{+} Z \subseteq (X \underset{˙}{+} Y) \underset{˙}{+} Z)$
15	11 13 14	sylc	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 Y \underset{˙}{+} Z \subseteq (X \underset{˙}{+} Y) \underset{˙}{+} Z$
16	5	hllatd	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 K \in Lat$
17		simprll	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 y \in Y$
18		simprlr	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 z \in Z$
19		simpl3l	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 A$
20		eqid	$⊢ {Base}_{K} = {Base}_{K}$
21	20 3	atbase	$⊢ p \in A \to p \in {Base}_{K}$
22	19 21	syl	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 {Base}_{K}$
23	7 17	sseldd	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 y \in A$
24	20 3	atbase	$⊢ y \in A \to y \in {Base}_{K}$
25	23 24	syl	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 y \in {Base}_{K}$
26		simpl3r	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 r \in A$
27	20 3	atbase	$⊢ r \in A \to r \in {Base}_{K}$
28	26 27	syl	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 r \in {Base}_{K}$
29	20 2	latjcl	$⊢ (K \in Lat \land y \in {Base}_{K} \land r \in {Base}_{K}) \to y \underset{˙}{\lor} r \in {Base}_{K}$
30	16 25 28 29	syl3anc	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 y \underset{˙}{\lor} r \in {Base}_{K}$
31	10 18	sseldd	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 z \in A$
32	20 3	atbase	$⊢ z \in A \to z \in {Base}_{K}$
33	31 32	syl	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 z \in {Base}_{K}$
34	20 2	latjcl	$⊢ (K \in Lat \land y \in {Base}_{K} \land z \in {Base}_{K}) \to y \underset{˙}{\lor} z \in {Base}_{K}$
35	16 25 33 34	syl3anc	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 y \underset{˙}{\lor} z \in {Base}_{K}$
36		simpl1r	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 x = y$
37		simprrl	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 \underset{˙}{\leq} (x \underset{˙}{\lor} r)$
38		oveq1	$⊢ x = y \to x \underset{˙}{\lor} r = y \underset{˙}{\lor} r$
39	38	breq2d	$⊢ x = y \to (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \leftrightarrow p \underset{˙}{\leq} (y \underset{˙}{\lor} r))$
40	39	biimpa	$⊢ (x = y \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)) \to p \underset{˙}{\leq} (y \underset{˙}{\lor} r)$
41	36 37 40	syl2anc	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 \underset{˙}{\leq} (y \underset{˙}{\lor} r)$
42	20 1 2	latlej1	$⊢ (K \in Lat \land y \in {Base}_{K} \land z \in {Base}_{K}) \to y \underset{˙}{\leq} (y \underset{˙}{\lor} z)$
43	16 25 33 42	syl3anc	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 y \underset{˙}{\leq} (y \underset{˙}{\lor} z)$
44		simprrr	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 r \underset{˙}{\leq} (y \underset{˙}{\lor} z)$
45	20 1 2	latjle12	$⊢ (K \in Lat \land (y \in {Base}_{K} \land r \in {Base}_{K} \land y \underset{˙}{\lor} z \in {Base}_{K})) \to ((y \underset{˙}{\leq} (y \underset{˙}{\lor} z) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \leftrightarrow (y \underset{˙}{\lor} r) \underset{˙}{\leq} (y \underset{˙}{\lor} z))$
46	16 25 28 35 45	syl13anc	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 ((y \underset{˙}{\leq} (y \underset{˙}{\lor} z) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \leftrightarrow (y \underset{˙}{\lor} r) \underset{˙}{\leq} (y \underset{˙}{\lor} z))$
47	43 44 46	mpbi2and	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 (y \underset{˙}{\lor} r) \underset{˙}{\leq} (y \underset{˙}{\lor} z)$
48	20 1 16 22 30 35 41 47	lattrd	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 \underset{˙}{\leq} (y \underset{˙}{\lor} z)$
49	1 2 3 4	elpaddri	$⊢ ((K \in Lat \land Y \subseteq A \land Z \subseteq A) \land (y \in Y \land z \in Z) \land (p \in A \land p \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to p \in (Y \underset{˙}{+} Z)$
50	16 7 10 17 18 19 48 49	syl322anc	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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 (Y \underset{˙}{+} Z)$
51	15 50	sseldd	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \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)$

Metamath Proof Explorer

Theorem paddasslem12

Proof