Theorem ltrnu

Description: Uniqueness property of a lattice translation value for atoms not under the fiducial co-atom W . Similar to definition of translation in Crawley p. 111. (Contributed by NM, 20-May-2012)

	Ref	Expression
Hypotheses	ltrnu.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	ltrnu.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	ltrnu.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	ltrnu.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	ltrnu.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	ltrnu.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
Assertion	ltrnu	$$⊢\left(\left(\left(K\in V\wedge W\in H\right)\wedge F\in T\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to \left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\wedge }W=\left(Q\underset{\dot{}}{\vee }F\left(Q\right)\right)\underset{\dot{}}{\wedge }W$$

Proof

Step	Hyp	Ref	Expression
1		ltrnu.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		ltrnu.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		ltrnu.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		ltrnu.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		ltrnu.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
6		ltrnu.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
7		an4	$$⊢\left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\leftrightarrow \left(\left(P\in A\wedge Q\in A\right)\wedge \left(\neg P\underset{\dot{}}{\le }W\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)$$
8		simpr	$$⊢\left(\left(\left(K\in V\wedge W\in H\right)\wedge F\in T\right)\wedge \left(P\in A\wedge Q\in A\right)\right)\to \left(P\in A\wedge Q\in A\right)$$
9		simplr	$$⊢\left(\left(\left(K\in V\wedge W\in H\right)\wedge F\in T\right)\wedge \left(P\in A\wedge Q\in A\right)\right)\to F\in T$$
10		eqid	$$⊢\mathrm{LDil}\left(K\right)\left(W\right)=\mathrm{LDil}\left(K\right)\left(W\right)$$
11	1 2 3 4 5 10 6	isltrn	$$⊢\left(K\in V\wedge W\in H\right)\to \left(F\in T\leftrightarrow \left(F\in \mathrm{LDil}\left(K\right)\left(W\right)\wedge \forall p\in A\forall q\in A\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\to \left(p\underset{\dot{}}{\vee }F\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }F\left(q\right)\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
12	11	ad2antrr	$$⊢\left(\left(\left(K\in V\wedge W\in H\right)\wedge F\in T\right)\wedge \left(P\in A\wedge Q\in A\right)\right)\to \left(F\in T\leftrightarrow \left(F\in \mathrm{LDil}\left(K\right)\left(W\right)\wedge \forall p\in A\forall q\in A\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\to \left(p\underset{\dot{}}{\vee }F\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }F\left(q\right)\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
13		simpr	$$⊢\left(F\in \mathrm{LDil}\left(K\right)\left(W\right)\wedge \forall p\in A\forall q\in A\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\to \left(p\underset{\dot{}}{\vee }F\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }F\left(q\right)\right)\underset{\dot{}}{\wedge }W\right)\right)\to \forall p\in A\forall q\in A\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\to \left(p\underset{\dot{}}{\vee }F\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }F\left(q\right)\right)\underset{\dot{}}{\wedge }W\right)$$
14	12 13	syl6bi	$$⊢\left(\left(\left(K\in V\wedge W\in H\right)\wedge F\in T\right)\wedge \left(P\in A\wedge Q\in A\right)\right)\to \left(F\in T\to \forall p\in A\forall q\in A\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\to \left(p\underset{\dot{}}{\vee }F\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }F\left(q\right)\right)\underset{\dot{}}{\wedge }W\right)\right)$$
15	9 14	mpd	$$⊢\left(\left(\left(K\in V\wedge W\in H\right)\wedge F\in T\right)\wedge \left(P\in A\wedge Q\in A\right)\right)\to \forall p\in A\forall q\in A\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\to \left(p\underset{\dot{}}{\vee }F\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }F\left(q\right)\right)\underset{\dot{}}{\wedge }W\right)$$
16		breq1	$$⊢p=P\to \left(p\underset{\dot{}}{\le }W\leftrightarrow P\underset{\dot{}}{\le }W\right)$$
17	16	notbid	$$⊢p=P\to \left(\neg p\underset{\dot{}}{\le }W\leftrightarrow \neg P\underset{\dot{}}{\le }W\right)$$
18	17	anbi1d	$$⊢p=P\to \left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\leftrightarrow \left(\neg P\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\right)$$
19		id	$$⊢p=P\to p=P$$
20		fveq2	$$⊢p=P\to F\left(p\right)=F\left(P\right)$$
21	19 20	oveq12d	$$⊢p=P\to p\underset{\dot{}}{\vee }F\left(p\right)=P\underset{\dot{}}{\vee }F\left(P\right)$$
22	21	oveq1d	$$⊢p=P\to \left(p\underset{\dot{}}{\vee }F\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\wedge }W$$
23	22	eqeq1d	$$⊢p=P\to \left(\left(p\underset{\dot{}}{\vee }F\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }F\left(q\right)\right)\underset{\dot{}}{\wedge }W\leftrightarrow \left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }F\left(q\right)\right)\underset{\dot{}}{\wedge }W\right)$$
24	18 23	imbi12d	$$⊢p=P\to \left(\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\to \left(p\underset{\dot{}}{\vee }F\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }F\left(q\right)\right)\underset{\dot{}}{\wedge }W\right)\leftrightarrow \left(\left(\neg P\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\to \left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }F\left(q\right)\right)\underset{\dot{}}{\wedge }W\right)\right)$$
25		breq1	$$⊢q=Q\to \left(q\underset{\dot{}}{\le }W\leftrightarrow Q\underset{\dot{}}{\le }W\right)$$
26	25	notbid	$$⊢q=Q\to \left(\neg q\underset{\dot{}}{\le }W\leftrightarrow \neg Q\underset{\dot{}}{\le }W\right)$$
27	26	anbi2d	$$⊢q=Q\to \left(\left(\neg P\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\leftrightarrow \left(\neg P\underset{\dot{}}{\le }W\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)$$
28		id	$$⊢q=Q\to q=Q$$
29		fveq2	$$⊢q=Q\to F\left(q\right)=F\left(Q\right)$$
30	28 29	oveq12d	$$⊢q=Q\to q\underset{\dot{}}{\vee }F\left(q\right)=Q\underset{\dot{}}{\vee }F\left(Q\right)$$
31	30	oveq1d	$$⊢q=Q\to \left(q\underset{\dot{}}{\vee }F\left(q\right)\right)\underset{\dot{}}{\wedge }W=\left(Q\underset{\dot{}}{\vee }F\left(Q\right)\right)\underset{\dot{}}{\wedge }W$$
32	31	eqeq2d	$$⊢q=Q\to \left(\left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }F\left(q\right)\right)\underset{\dot{}}{\wedge }W\leftrightarrow \left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\wedge }W=\left(Q\underset{\dot{}}{\vee }F\left(Q\right)\right)\underset{\dot{}}{\wedge }W\right)$$
33	27 32	imbi12d	$$⊢q=Q\to \left(\left(\left(\neg P\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\to \left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }F\left(q\right)\right)\underset{\dot{}}{\wedge }W\right)\leftrightarrow \left(\left(\neg P\underset{\dot{}}{\le }W\wedge \neg Q\underset{\dot{}}{\le }W\right)\to \left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\wedge }W=\left(Q\underset{\dot{}}{\vee }F\left(Q\right)\right)\underset{\dot{}}{\wedge }W\right)\right)$$
34	24 33	rspc2v	$$⊢\left(P\in A\wedge Q\in A\right)\to \left(\forall p\in A\forall q\in A\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\to \left(p\underset{\dot{}}{\vee }F\left(p\right)\right)\underset{\dot{}}{\wedge }W=\left(q\underset{\dot{}}{\vee }F\left(q\right)\right)\underset{\dot{}}{\wedge }W\right)\to \left(\left(\neg P\underset{\dot{}}{\le }W\wedge \neg Q\underset{\dot{}}{\le }W\right)\to \left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\wedge }W=\left(Q\underset{\dot{}}{\vee }F\left(Q\right)\right)\underset{\dot{}}{\wedge }W\right)\right)$$
35	8 15 34	sylc	$$⊢\left(\left(\left(K\in V\wedge W\in H\right)\wedge F\in T\right)\wedge \left(P\in A\wedge Q\in A\right)\right)\to \left(\left(\neg P\underset{\dot{}}{\le }W\wedge \neg Q\underset{\dot{}}{\le }W\right)\to \left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\wedge }W=\left(Q\underset{\dot{}}{\vee }F\left(Q\right)\right)\underset{\dot{}}{\wedge }W\right)$$
36	35	impr	$$⊢\left(\left(\left(K\in V\wedge W\in H\right)\wedge F\in T\right)\wedge \left(\left(P\in A\wedge Q\in A\right)\wedge \left(\neg P\underset{\dot{}}{\le }W\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\wedge }W=\left(Q\underset{\dot{}}{\vee }F\left(Q\right)\right)\underset{\dot{}}{\wedge }W$$
37	7 36	sylan2b	$$⊢\left(\left(\left(K\in V\wedge W\in H\right)\wedge F\in T\right)\wedge \left(\left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\right)\to \left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\wedge }W=\left(Q\underset{\dot{}}{\vee }F\left(Q\right)\right)\underset{\dot{}}{\wedge }W$$
38	37	3impb	$$⊢\left(\left(\left(K\in V\wedge W\in H\right)\wedge F\in T\right)\wedge \left(P\in A\wedge \neg P\underset{\dot{}}{\le }W\right)\wedge \left(Q\in A\wedge \neg Q\underset{\dot{}}{\le }W\right)\right)\to \left(P\underset{\dot{}}{\vee }F\left(P\right)\right)\underset{\dot{}}{\wedge }W=\left(Q\underset{\dot{}}{\vee }F\left(Q\right)\right)\underset{\dot{}}{\wedge }W$$