paddasslem5

Description: Lemma for paddass . Show s =/= z by contradiction. (Contributed by NM, 8-Jan-2012)

	Ref	Expression
Hypotheses	paddasslem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	paddasslem.j	$⊢ \underset{˙}{\lor} = join (K)$
	paddasslem.a	$⊢ A = Atoms (K)$
Assertion	paddasslem5	$⊢ ((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \to s \neq 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		breq1	$⊢ s = z \to (s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \leftrightarrow z \underset{˙}{\leq} (x \underset{˙}{\lor} y))$
5	4	biimpac	$⊢ (s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land s = z) \to z \underset{˙}{\leq} (x \underset{˙}{\lor} y)$
6		eqid	$⊢ {Base}_{K} = {Base}_{K}$
7		simpll1	$⊢ (((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to K \in HL$
8	7	hllatd	$⊢ (((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to K \in Lat$
9		simpll2	$⊢ (((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to r \in A$
10	6 3	atbase	$⊢ r \in A \to r \in {Base}_{K}$
11	9 10	syl	$⊢ (((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to r \in {Base}_{K}$
12		simp32	$⊢ (K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \to y \in A$
13	12	ad2antrr	$⊢ (((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to y \in A$
14	6 3	atbase	$⊢ y \in A \to y \in {Base}_{K}$
15	13 14	syl	$⊢ (((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to y \in {Base}_{K}$
16		simp33	$⊢ (K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \to z \in A$
17	16	ad2antrr	$⊢ (((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to z \in A$
18	6 3	atbase	$⊢ z \in A \to z \in {Base}_{K}$
19	17 18	syl	$⊢ (((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to z \in {Base}_{K}$
20	6 2	latjcl	$⊢ (K \in Lat \land y \in {Base}_{K} \land z \in {Base}_{K}) \to y \underset{˙}{\lor} z \in {Base}_{K}$
21	8 15 19 20	syl3anc	$⊢ (((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to y \underset{˙}{\lor} z \in {Base}_{K}$
22		simp31	$⊢ (K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \to x \in A$
23	22	ad2antrr	$⊢ (((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to x \in A$
24	6 3	atbase	$⊢ x \in A \to x \in {Base}_{K}$
25	23 24	syl	$⊢ (((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to x \in {Base}_{K}$
26	6 2	latjcl	$⊢ (K \in Lat \land x \in {Base}_{K} \land y \in {Base}_{K}) \to x \underset{˙}{\lor} y \in {Base}_{K}$
27	8 25 15 26	syl3anc	$⊢ (((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to x \underset{˙}{\lor} y \in {Base}_{K}$
28		simplr	$⊢ (((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to r \underset{˙}{\leq} (y \underset{˙}{\lor} z)$
29	1 2 3	hlatlej2	$⊢ (K \in HL \land x \in A \land y \in A) \to y \underset{˙}{\leq} (x \underset{˙}{\lor} y)$
30	7 23 13 29	syl3anc	$⊢ (((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to y \underset{˙}{\leq} (x \underset{˙}{\lor} y)$
31		simpr	$⊢ (((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to z \underset{˙}{\leq} (x \underset{˙}{\lor} y)$
32	6 1 2	latjle12	$⊢ (K \in Lat \land (y \in {Base}_{K} \land z \in {Base}_{K} \land x \underset{˙}{\lor} y \in {Base}_{K})) \to ((y \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \leftrightarrow (y \underset{˙}{\lor} z) \underset{˙}{\leq} (x \underset{˙}{\lor} y))$
33	32	biimpd	$⊢ (K \in Lat \land (y \in {Base}_{K} \land z \in {Base}_{K} \land x \underset{˙}{\lor} y \in {Base}_{K})) \to ((y \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to (y \underset{˙}{\lor} z) \underset{˙}{\leq} (x \underset{˙}{\lor} y))$
34	8 15 19 27 33	syl13anc	$⊢ (((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to ((y \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to (y \underset{˙}{\lor} z) \underset{˙}{\leq} (x \underset{˙}{\lor} y))$
35	30 31 34	mp2and	$⊢ (((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to (y \underset{˙}{\lor} z) \underset{˙}{\leq} (x \underset{˙}{\lor} y)$
36	6 1 8 11 21 27 28 35	lattrd	$⊢ (((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to r \underset{˙}{\leq} (x \underset{˙}{\lor} y)$
37	36	ex	$⊢ ((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \to (z \underset{˙}{\leq} (x \underset{˙}{\lor} y) \to r \underset{˙}{\leq} (x \underset{˙}{\lor} y))$
38	5 37	syl5	$⊢ ((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \to ((s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land s = z) \to r \underset{˙}{\leq} (x \underset{˙}{\lor} y))$
39	38	expdimp	$⊢ (((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to (s = z \to r \underset{˙}{\leq} (x \underset{˙}{\lor} y))$
40	39	necon3bd	$⊢ (((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \to (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \to s \neq z)$
41	40	exp31	$⊢ (K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \to (r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \to (s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \to (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \to s \neq z)))$
42	41	com23	$⊢ (K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \to (s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \to (r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \to (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \to s \neq z)))$
43	42	com24	$⊢ (K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \to (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \to (r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \to (s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \to s \neq z)))$
44	43	3imp2	$⊢ ((K \in HL \land r \in A \land (x \in A \land y \in A \land z \in A)) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \to s \neq z$

Metamath Proof Explorer

Theorem paddasslem5

Proof