dalem24

Description: Lemma for dath . Show that auxiliary atom G is outside of plane Y . (Contributed by NM, 2-Aug-2012)

	Ref	Expression
Hypotheses	dalem.ph	$⊢ φ \leftrightarrow (((K \in HL \land C \in {Base}_{K}) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (Y \in O \land Z \in O) \land ((\neg C \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg C \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg C \underset{˙}{\leq} (R \underset{˙}{\lor} P)) \land (\neg C \underset{˙}{\leq} (S \underset{˙}{\lor} T) \land \neg C \underset{˙}{\leq} (T \underset{˙}{\lor} U) \land \neg C \underset{˙}{\leq} (U \underset{˙}{\lor} S)) \land (C \underset{˙}{\leq} (P \underset{˙}{\lor} S) \land C \underset{˙}{\leq} (Q \underset{˙}{\lor} T) \land C \underset{˙}{\leq} (R \underset{˙}{\lor} U))))$
	dalem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dalem.j	$⊢ \underset{˙}{\lor} = join (K)$
	dalem.a	$⊢ A = Atoms (K)$
	dalem.ps	$⊢ ψ \leftrightarrow ((c \in A \land d \in A) \land \neg c \underset{˙}{\leq} Y \land (d \neq c \land \neg d \underset{˙}{\leq} Y \land C \underset{˙}{\leq} (c \underset{˙}{\lor} d)))$
	dalem23.m	$⊢ \underset{˙}{\land} = meet (K)$
	dalem23.o	$⊢ O = LPlanes (K)$
	dalem23.y	$⊢ Y = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R$
	dalem23.z	$⊢ Z = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$
	dalem23.g	$⊢ G = (c \underset{˙}{\lor} P) \underset{˙}{\land} (d \underset{˙}{\lor} S)$
Assertion	dalem24	$⊢ (φ \land Y = Z \land ψ) \to \neg G \underset{˙}{\leq} Y$

Proof

Step	Hyp	Ref	Expression
1		dalem.ph	$⊢ φ \leftrightarrow (((K \in HL \land C \in {Base}_{K}) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (Y \in O \land Z \in O) \land ((\neg C \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg C \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg C \underset{˙}{\leq} (R \underset{˙}{\lor} P)) \land (\neg C \underset{˙}{\leq} (S \underset{˙}{\lor} T) \land \neg C \underset{˙}{\leq} (T \underset{˙}{\lor} U) \land \neg C \underset{˙}{\leq} (U \underset{˙}{\lor} S)) \land (C \underset{˙}{\leq} (P \underset{˙}{\lor} S) \land C \underset{˙}{\leq} (Q \underset{˙}{\lor} T) \land C \underset{˙}{\leq} (R \underset{˙}{\lor} U))))$
2		dalem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dalem.j	$⊢ \underset{˙}{\lor} = join (K)$
4		dalem.a	$⊢ A = Atoms (K)$
5		dalem.ps	$⊢ ψ \leftrightarrow ((c \in A \land d \in A) \land \neg c \underset{˙}{\leq} Y \land (d \neq c \land \neg d \underset{˙}{\leq} Y \land C \underset{˙}{\leq} (c \underset{˙}{\lor} d)))$
6		dalem23.m	$⊢ \underset{˙}{\land} = meet (K)$
7		dalem23.o	$⊢ O = LPlanes (K)$
8		dalem23.y	$⊢ Y = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R$
9		dalem23.z	$⊢ Z = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$
10		dalem23.g	$⊢ G = (c \underset{˙}{\lor} P) \underset{˙}{\land} (d \underset{˙}{\lor} S)$
11	10	oveq1i	$⊢ G \underset{˙}{\land} Y = ((c \underset{˙}{\lor} P) \underset{˙}{\land} (d \underset{˙}{\lor} S)) \underset{˙}{\land} Y$
12	1	dalemkehl	$⊢ φ \to K \in HL$
13		hlol	$⊢ K \in HL \to K \in OL$
14	12 13	syl	$⊢ φ \to K \in OL$
15	14	3ad2ant1	$⊢ (φ \land Y = Z \land ψ) \to K \in OL$
16	12	3ad2ant1	$⊢ (φ \land Y = Z \land ψ) \to K \in HL$
17	5	dalemccea	$⊢ ψ \to c \in A$
18	17	3ad2ant3	$⊢ (φ \land Y = Z \land ψ) \to c \in A$
19	1	dalempea	$⊢ φ \to P \in A$
20	19	3ad2ant1	$⊢ (φ \land Y = Z \land ψ) \to P \in A$
21		eqid	$⊢ {Base}_{K} = {Base}_{K}$
22	21 3 4	hlatjcl	$⊢ (K \in HL \land c \in A \land P \in A) \to c \underset{˙}{\lor} P \in {Base}_{K}$
23	16 18 20 22	syl3anc	$⊢ (φ \land Y = Z \land ψ) \to c \underset{˙}{\lor} P \in {Base}_{K}$
24	5	dalemddea	$⊢ ψ \to d \in A$
25	24	3ad2ant3	$⊢ (φ \land Y = Z \land ψ) \to d \in A$
26	1	dalemsea	$⊢ φ \to S \in A$
27	26	3ad2ant1	$⊢ (φ \land Y = Z \land ψ) \to S \in A$
28	21 3 4	hlatjcl	$⊢ (K \in HL \land d \in A \land S \in A) \to d \underset{˙}{\lor} S \in {Base}_{K}$
29	16 25 27 28	syl3anc	$⊢ (φ \land Y = Z \land ψ) \to d \underset{˙}{\lor} S \in {Base}_{K}$
30	1 7	dalemyeb	$⊢ φ \to Y \in {Base}_{K}$
31	30	3ad2ant1	$⊢ (φ \land Y = Z \land ψ) \to Y \in {Base}_{K}$
32	21 6	latmmdir	$⊢ (K \in OL \land (c \underset{˙}{\lor} P \in {Base}_{K} \land d \underset{˙}{\lor} S \in {Base}_{K} \land Y \in {Base}_{K})) \to ((c \underset{˙}{\lor} P) \underset{˙}{\land} (d \underset{˙}{\lor} S)) \underset{˙}{\land} Y = ((c \underset{˙}{\lor} P) \underset{˙}{\land} Y) \underset{˙}{\land} ((d \underset{˙}{\lor} S) \underset{˙}{\land} Y)$
33	15 23 29 31 32	syl13anc	$⊢ (φ \land Y = Z \land ψ) \to ((c \underset{˙}{\lor} P) \underset{˙}{\land} (d \underset{˙}{\lor} S)) \underset{˙}{\land} Y = ((c \underset{˙}{\lor} P) \underset{˙}{\land} Y) \underset{˙}{\land} ((d \underset{˙}{\lor} S) \underset{˙}{\land} Y)$
34	11 33	eqtrid	$⊢ (φ \land Y = Z \land ψ) \to G \underset{˙}{\land} Y = ((c \underset{˙}{\lor} P) \underset{˙}{\land} Y) \underset{˙}{\land} ((d \underset{˙}{\lor} S) \underset{˙}{\land} Y)$
35	3 4	hlatjcom	$⊢ (K \in HL \land c \in A \land P \in A) \to c \underset{˙}{\lor} P = P \underset{˙}{\lor} c$
36	16 18 20 35	syl3anc	$⊢ (φ \land Y = Z \land ψ) \to c \underset{˙}{\lor} P = P \underset{˙}{\lor} c$
37	36	oveq1d	$⊢ (φ \land Y = Z \land ψ) \to (c \underset{˙}{\lor} P) \underset{˙}{\land} Y = (P \underset{˙}{\lor} c) \underset{˙}{\land} Y$
38	1 2 3 4 7 8	dalemply	$⊢ φ \to P \underset{˙}{\leq} Y$
39	38	3ad2ant1	$⊢ (φ \land Y = Z \land ψ) \to P \underset{˙}{\leq} Y$
40	5	dalem-ccly	$⊢ ψ \to \neg c \underset{˙}{\leq} Y$
41	40	3ad2ant3	$⊢ (φ \land Y = Z \land ψ) \to \neg c \underset{˙}{\leq} Y$
42	21 2 3 6 4	2atjm	$⊢ (K \in HL \land (P \in A \land c \in A \land Y \in {Base}_{K}) \land (P \underset{˙}{\leq} Y \land \neg c \underset{˙}{\leq} Y)) \to (P \underset{˙}{\lor} c) \underset{˙}{\land} Y = P$
43	16 20 18 31 39 41 42	syl132anc	$⊢ (φ \land Y = Z \land ψ) \to (P \underset{˙}{\lor} c) \underset{˙}{\land} Y = P$
44	37 43	eqtrd	$⊢ (φ \land Y = Z \land ψ) \to (c \underset{˙}{\lor} P) \underset{˙}{\land} Y = P$
45	3 4	hlatjcom	$⊢ (K \in HL \land d \in A \land S \in A) \to d \underset{˙}{\lor} S = S \underset{˙}{\lor} d$
46	16 25 27 45	syl3anc	$⊢ (φ \land Y = Z \land ψ) \to d \underset{˙}{\lor} S = S \underset{˙}{\lor} d$
47	46	oveq1d	$⊢ (φ \land Y = Z \land ψ) \to (d \underset{˙}{\lor} S) \underset{˙}{\land} Y = (S \underset{˙}{\lor} d) \underset{˙}{\land} Y$
48	1 2 3 4 9	dalemsly	$⊢ (φ \land Y = Z) \to S \underset{˙}{\leq} Y$
49	48	3adant3	$⊢ (φ \land Y = Z \land ψ) \to S \underset{˙}{\leq} Y$
50	5	dalem-ddly	$⊢ ψ \to \neg d \underset{˙}{\leq} Y$
51	50	3ad2ant3	$⊢ (φ \land Y = Z \land ψ) \to \neg d \underset{˙}{\leq} Y$
52	21 2 3 6 4	2atjm	$⊢ (K \in HL \land (S \in A \land d \in A \land Y \in {Base}_{K}) \land (S \underset{˙}{\leq} Y \land \neg d \underset{˙}{\leq} Y)) \to (S \underset{˙}{\lor} d) \underset{˙}{\land} Y = S$
53	16 27 25 31 49 51 52	syl132anc	$⊢ (φ \land Y = Z \land ψ) \to (S \underset{˙}{\lor} d) \underset{˙}{\land} Y = S$
54	47 53	eqtrd	$⊢ (φ \land Y = Z \land ψ) \to (d \underset{˙}{\lor} S) \underset{˙}{\land} Y = S$
55	44 54	oveq12d	$⊢ (φ \land Y = Z \land ψ) \to ((c \underset{˙}{\lor} P) \underset{˙}{\land} Y) \underset{˙}{\land} ((d \underset{˙}{\lor} S) \underset{˙}{\land} Y) = P \underset{˙}{\land} S$
56	1 2 3 4 7 8	dalempnes	$⊢ φ \to P \neq S$
57		hlatl	$⊢ K \in HL \to K \in AtLat$
58	12 57	syl	$⊢ φ \to K \in AtLat$
59		eqid	$⊢ 0. (K) = 0. (K)$
60	6 59 4	atnem0	$⊢ (K \in AtLat \land P \in A \land S \in A) \to (P \neq S \leftrightarrow P \underset{˙}{\land} S = 0. (K))$
61	58 19 26 60	syl3anc	$⊢ φ \to (P \neq S \leftrightarrow P \underset{˙}{\land} S = 0. (K))$
62	56 61	mpbid	$⊢ φ \to P \underset{˙}{\land} S = 0. (K)$
63	62	3ad2ant1	$⊢ (φ \land Y = Z \land ψ) \to P \underset{˙}{\land} S = 0. (K)$
64	34 55 63	3eqtrd	$⊢ (φ \land Y = Z \land ψ) \to G \underset{˙}{\land} Y = 0. (K)$
65	58	3ad2ant1	$⊢ (φ \land Y = Z \land ψ) \to K \in AtLat$
66	1 2 3 4 5 6 7 8 9 10	dalem23	$⊢ (φ \land Y = Z \land ψ) \to G \in A$
67	21 2 6 59 4	atnle	$⊢ (K \in AtLat \land G \in A \land Y \in {Base}_{K}) \to (\neg G \underset{˙}{\leq} Y \leftrightarrow G \underset{˙}{\land} Y = 0. (K))$
68	65 66 31 67	syl3anc	$⊢ (φ \land Y = Z \land ψ) \to (\neg G \underset{˙}{\leq} Y \leftrightarrow G \underset{˙}{\land} Y = 0. (K))$
69	64 68	mpbird	$⊢ (φ \land Y = Z \land ψ) \to \neg G \underset{˙}{\leq} Y$

Metamath Proof Explorer

Theorem dalem24

Proof