Theorem dalem25

Description: Lemma for dath . Show that the dummy center of perspectivity c is different from auxiliary atom G . (Contributed by NM, 3-Aug-2012)

	Ref	Expression
Hypotheses	dalem.ph	$$⊢\phi \leftrightarrow \left(\left(\left(K\in \mathrm{HL}\wedge C\in {\mathrm{Base}}_K\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(Y\in O\wedge Z\in O\right)\wedge \left(\left(\neg C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }P\right)\right)\wedge \left(\neg C\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg C\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg C\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\wedge \left(C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)\wedge C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }T\right)\wedge C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\right)\right)$$
	dalem.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dalem.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dalem.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dalem.ps	$$⊢\psi \leftrightarrow \left(\left(c\in A\wedge d\in A\right)\wedge \neg c\underset{\dot{}}{\le }Y\wedge \left(d\ne c\wedge \neg d\underset{\dot{}}{\le }Y\wedge C\underset{\dot{}}{\le }\left(c\underset{\dot{}}{\vee }d\right)\right)\right)$$
	dalem23.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	dalem23.o	$$⊢O=\mathrm{LPlanes}\left(K\right)$$
	dalem23.y	$$⊢Y=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R$$
	dalem23.z	$$⊢Z=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U$$
	dalem23.g	$$⊢G=\left(c\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(d\underset{\dot{}}{\vee }S\right)$$
Assertion	dalem25	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to c\ne G$$

Proof

Step	Hyp	Ref	Expression
1		dalem.ph	$$⊢\phi \leftrightarrow \left(\left(\left(K\in \mathrm{HL}\wedge C\in {\mathrm{Base}}_K\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(Y\in O\wedge Z\in O\right)\wedge \left(\left(\neg C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }P\right)\right)\wedge \left(\neg C\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg C\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg C\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\wedge \left(C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)\wedge C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }T\right)\wedge C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\right)\right)$$
2		dalem.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		dalem.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		dalem.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		dalem.ps	$$⊢\psi \leftrightarrow \left(\left(c\in A\wedge d\in A\right)\wedge \neg c\underset{\dot{}}{\le }Y\wedge \left(d\ne c\wedge \neg d\underset{\dot{}}{\le }Y\wedge C\underset{\dot{}}{\le }\left(c\underset{\dot{}}{\vee }d\right)\right)\right)$$
6		dalem23.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
7		dalem23.o	$$⊢O=\mathrm{LPlanes}\left(K\right)$$
8		dalem23.y	$$⊢Y=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R$$
9		dalem23.z	$$⊢Z=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U$$
10		dalem23.g	$$⊢G=\left(c\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(d\underset{\dot{}}{\vee }S\right)$$
11	1 2 3 4	dalemcnes	$$⊢\phi \to C\ne S$$
12	11	3ad2ant1	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to C\ne S$$
13	5	dalemclccjdd	$$⊢\psi \to C\underset{\dot{}}{\le }\left(c\underset{\dot{}}{\vee }d\right)$$
14	13	3ad2ant3	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to C\underset{\dot{}}{\le }\left(c\underset{\dot{}}{\vee }d\right)$$
15	14	adantr	$$⊢\left(\left(\phi \wedge Y=Z\wedge \psi \right)\wedge c=G\right)\to C\underset{\dot{}}{\le }\left(c\underset{\dot{}}{\vee }d\right)$$
16		simpr	$$⊢\left(\left(\phi \wedge Y=Z\wedge \psi \right)\wedge c=G\right)\to c=G$$
17	1	dalemkelat	$$⊢\phi \to K\in \mathrm{Lat}$$
18	17	3ad2ant1	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to K\in \mathrm{Lat}$$
19	1	dalemkehl	$$⊢\phi \to K\in \mathrm{HL}$$
20	19	3ad2ant1	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to K\in \mathrm{HL}$$
21	5	dalemccea	$$⊢\psi \to c\in A$$
22	21	3ad2ant3	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to c\in A$$
23	1	dalempea	$$⊢\phi \to P\in A$$
24	23	3ad2ant1	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to P\in A$$
25		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
26	25 3 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge c\in A\wedge P\in A\right)\to c\underset{\dot{}}{\vee }P\in {\mathrm{Base}}_K$$
27	20 22 24 26	syl3anc	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to c\underset{\dot{}}{\vee }P\in {\mathrm{Base}}_K$$
28	5	dalemddea	$$⊢\psi \to d\in A$$
29	28	3ad2ant3	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to d\in A$$
30	1	dalemsea	$$⊢\phi \to S\in A$$
31	30	3ad2ant1	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to S\in A$$
32	25 3 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge d\in A\wedge S\in A\right)\to d\underset{\dot{}}{\vee }S\in {\mathrm{Base}}_K$$
33	20 29 31 32	syl3anc	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to d\underset{\dot{}}{\vee }S\in {\mathrm{Base}}_K$$
34	25 2 6	latmle2	$$⊢\left(K\in \mathrm{Lat}\wedge c\underset{\dot{}}{\vee }P\in {\mathrm{Base}}_K\wedge d\underset{\dot{}}{\vee }S\in {\mathrm{Base}}_K\right)\to \left(\left(c\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(d\underset{\dot{}}{\vee }S\right)\right)\underset{\dot{}}{\le }\left(d\underset{\dot{}}{\vee }S\right)$$
35	18 27 33 34	syl3anc	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to \left(\left(c\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(d\underset{\dot{}}{\vee }S\right)\right)\underset{\dot{}}{\le }\left(d\underset{\dot{}}{\vee }S\right)$$
36	10 35	eqbrtrid	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to G\underset{\dot{}}{\le }\left(d\underset{\dot{}}{\vee }S\right)$$
37	3 4	hlatjcom	$$⊢\left(K\in \mathrm{HL}\wedge d\in A\wedge S\in A\right)\to d\underset{\dot{}}{\vee }S=S\underset{\dot{}}{\vee }d$$
38	20 29 31 37	syl3anc	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to d\underset{\dot{}}{\vee }S=S\underset{\dot{}}{\vee }d$$
39	36 38	breqtrd	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to G\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)$$
40	39	adantr	$$⊢\left(\left(\phi \wedge Y=Z\wedge \psi \right)\wedge c=G\right)\to G\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)$$
41	16 40	eqbrtrd	$$⊢\left(\left(\phi \wedge Y=Z\wedge \psi \right)\wedge c=G\right)\to c\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)$$
42	2 3 4	hlatlej2	$$⊢\left(K\in \mathrm{HL}\wedge S\in A\wedge d\in A\right)\to d\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)$$
43	20 31 29 42	syl3anc	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to d\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)$$
44	43	adantr	$$⊢\left(\left(\phi \wedge Y=Z\wedge \psi \right)\wedge c=G\right)\to d\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)$$
45	5 4	dalemcceb	$$⊢\psi \to c\in {\mathrm{Base}}_K$$
46	45	3ad2ant3	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to c\in {\mathrm{Base}}_K$$
47	25 4	atbase	$$⊢d\in A\to d\in {\mathrm{Base}}_K$$
48	28 47	syl	$$⊢\psi \to d\in {\mathrm{Base}}_K$$
49	48	3ad2ant3	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to d\in {\mathrm{Base}}_K$$
50	25 3 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge S\in A\wedge d\in A\right)\to S\underset{\dot{}}{\vee }d\in {\mathrm{Base}}_K$$
51	20 31 29 50	syl3anc	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to S\underset{\dot{}}{\vee }d\in {\mathrm{Base}}_K$$
52	25 2 3	latjle12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(c\in {\mathrm{Base}}_K\wedge d\in {\mathrm{Base}}_K\wedge S\underset{\dot{}}{\vee }d\in {\mathrm{Base}}_K\right)\right)\to \left(\left(c\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)\wedge d\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)\right)\leftrightarrow \left(c\underset{\dot{}}{\vee }d\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)\right)$$
53	18 46 49 51 52	syl13anc	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to \left(\left(c\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)\wedge d\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)\right)\leftrightarrow \left(c\underset{\dot{}}{\vee }d\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)\right)$$
54	53	adantr	$$⊢\left(\left(\phi \wedge Y=Z\wedge \psi \right)\wedge c=G\right)\to \left(\left(c\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)\wedge d\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)\right)\leftrightarrow \left(c\underset{\dot{}}{\vee }d\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)\right)$$
55	41 44 54	mpbi2and	$$⊢\left(\left(\phi \wedge Y=Z\wedge \psi \right)\wedge c=G\right)\to \left(c\underset{\dot{}}{\vee }d\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)$$
56	1 4	dalemceb	$$⊢\phi \to C\in {\mathrm{Base}}_K$$
57	56	3ad2ant1	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to C\in {\mathrm{Base}}_K$$
58	25 3 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge c\in A\wedge d\in A\right)\to c\underset{\dot{}}{\vee }d\in {\mathrm{Base}}_K$$
59	20 22 29 58	syl3anc	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to c\underset{\dot{}}{\vee }d\in {\mathrm{Base}}_K$$
60	25 2	lattr	$$⊢\left(K\in \mathrm{Lat}\wedge \left(C\in {\mathrm{Base}}_K\wedge c\underset{\dot{}}{\vee }d\in {\mathrm{Base}}_K\wedge S\underset{\dot{}}{\vee }d\in {\mathrm{Base}}_K\right)\right)\to \left(\left(C\underset{\dot{}}{\le }\left(c\underset{\dot{}}{\vee }d\right)\wedge \left(c\underset{\dot{}}{\vee }d\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)\right)\to C\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)\right)$$
61	18 57 59 51 60	syl13anc	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to \left(\left(C\underset{\dot{}}{\le }\left(c\underset{\dot{}}{\vee }d\right)\wedge \left(c\underset{\dot{}}{\vee }d\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)\right)\to C\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)\right)$$
62	61	adantr	$$⊢\left(\left(\phi \wedge Y=Z\wedge \psi \right)\wedge c=G\right)\to \left(\left(C\underset{\dot{}}{\le }\left(c\underset{\dot{}}{\vee }d\right)\wedge \left(c\underset{\dot{}}{\vee }d\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)\right)\to C\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)\right)$$
63	15 55 62	mp2and	$$⊢\left(\left(\phi \wedge Y=Z\wedge \psi \right)\wedge c=G\right)\to C\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)$$
64	1 7	dalemyeb	$$⊢\phi \to Y\in {\mathrm{Base}}_K$$
65	64	3ad2ant1	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to Y\in {\mathrm{Base}}_K$$
66	25 2 6	latmlem1	$$⊢\left(K\in \mathrm{Lat}\wedge \left(C\in {\mathrm{Base}}_K\wedge S\underset{\dot{}}{\vee }d\in {\mathrm{Base}}_K\wedge Y\in {\mathrm{Base}}_K\right)\right)\to \left(C\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)\to \left(C\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }d\right)\underset{\dot{}}{\wedge }Y\right)\right)$$
67	18 57 51 65 66	syl13anc	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to \left(C\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)\to \left(C\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }d\right)\underset{\dot{}}{\wedge }Y\right)\right)$$
68	67	adantr	$$⊢\left(\left(\phi \wedge Y=Z\wedge \psi \right)\wedge c=G\right)\to \left(C\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }d\right)\to \left(C\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }d\right)\underset{\dot{}}{\wedge }Y\right)\right)$$
69	63 68	mpd	$$⊢\left(\left(\phi \wedge Y=Z\wedge \psi \right)\wedge c=G\right)\to \left(C\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }d\right)\underset{\dot{}}{\wedge }Y\right)$$
70	1 2 3 4 7 8 9	dalem17	$$⊢\left(\phi \wedge Y=Z\right)\to C\underset{\dot{}}{\le }Y$$
71	70	3adant3	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to C\underset{\dot{}}{\le }Y$$
72	25 2 6	latleeqm1	$$⊢\left(K\in \mathrm{Lat}\wedge C\in {\mathrm{Base}}_K\wedge Y\in {\mathrm{Base}}_K\right)\to \left(C\underset{\dot{}}{\le }Y\leftrightarrow C\underset{\dot{}}{\wedge }Y=C\right)$$
73	18 57 65 72	syl3anc	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to \left(C\underset{\dot{}}{\le }Y\leftrightarrow C\underset{\dot{}}{\wedge }Y=C\right)$$
74	71 73	mpbid	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to C\underset{\dot{}}{\wedge }Y=C$$
75	74	adantr	$$⊢\left(\left(\phi \wedge Y=Z\wedge \psi \right)\wedge c=G\right)\to C\underset{\dot{}}{\wedge }Y=C$$
76	1 2 3 4 9	dalemsly	$$⊢\left(\phi \wedge Y=Z\right)\to S\underset{\dot{}}{\le }Y$$
77	76	3adant3	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to S\underset{\dot{}}{\le }Y$$
78	5	dalem-ddly	$$⊢\psi \to \neg d\underset{\dot{}}{\le }Y$$
79	78	3ad2ant3	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to \neg d\underset{\dot{}}{\le }Y$$
80	25 2 3 6 4	2atjm	$$⊢\left(K\in \mathrm{HL}\wedge \left(S\in A\wedge d\in A\wedge Y\in {\mathrm{Base}}_K\right)\wedge \left(S\underset{\dot{}}{\le }Y\wedge \neg d\underset{\dot{}}{\le }Y\right)\right)\to \left(S\underset{\dot{}}{\vee }d\right)\underset{\dot{}}{\wedge }Y=S$$
81	20 31 29 65 77 79 80	syl132anc	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to \left(S\underset{\dot{}}{\vee }d\right)\underset{\dot{}}{\wedge }Y=S$$
82	81	adantr	$$⊢\left(\left(\phi \wedge Y=Z\wedge \psi \right)\wedge c=G\right)\to \left(S\underset{\dot{}}{\vee }d\right)\underset{\dot{}}{\wedge }Y=S$$
83	69 75 82	3brtr3d	$$⊢\left(\left(\phi \wedge Y=Z\wedge \psi \right)\wedge c=G\right)\to C\underset{\dot{}}{\le }S$$
84		hlatl	$$⊢K\in \mathrm{HL}\to K\in \mathrm{AtLat}$$
85	19 84	syl	$$⊢\phi \to K\in \mathrm{AtLat}$$
86	1 2 3 4 7 8	dalemcea	$$⊢\phi \to C\in A$$
87	2 4	atcmp	$$⊢\left(K\in \mathrm{AtLat}\wedge C\in A\wedge S\in A\right)\to \left(C\underset{\dot{}}{\le }S\leftrightarrow C=S\right)$$
88	85 86 30 87	syl3anc	$$⊢\phi \to \left(C\underset{\dot{}}{\le }S\leftrightarrow C=S\right)$$
89	88	3ad2ant1	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to \left(C\underset{\dot{}}{\le }S\leftrightarrow C=S\right)$$
90	89	adantr	$$⊢\left(\left(\phi \wedge Y=Z\wedge \psi \right)\wedge c=G\right)\to \left(C\underset{\dot{}}{\le }S\leftrightarrow C=S\right)$$
91	83 90	mpbid	$$⊢\left(\left(\phi \wedge Y=Z\wedge \psi \right)\wedge c=G\right)\to C=S$$
92	91	ex	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to \left(c=G\to C=S\right)$$
93	92	necon3d	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to \left(C\ne S\to c\ne G\right)$$
94	12 93	mpd	$$⊢\left(\phi \wedge Y=Z\wedge \psi \right)\to c\ne G$$