Theorem isltrn2N

Description: The predicate "is a lattice translation". Version of isltrn that considers only different p and q . TODO: Can this eliminate some separate proofs for the p = q case? (Contributed by NM, 22-Apr-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ltrnset.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	ltrnset.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	ltrnset.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	ltrnset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	ltrnset.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	ltrnset.d	$$⊢D=\mathrm{LDil}\left(K\right)\left(W\right)$$
	ltrnset.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
Assertion	isltrn2N	$$⊢\left(K\in B\wedge W\in H\right)\to \left(F\in T\leftrightarrow \left(F\in D\wedge \forall p\in A\forall q\in A\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\wedge p\ne q\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)$$

Proof

Step	Hyp	Ref	Expression
1		ltrnset.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		ltrnset.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		ltrnset.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		ltrnset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		ltrnset.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
6		ltrnset.d	$$⊢D=\mathrm{LDil}\left(K\right)\left(W\right)$$
7		ltrnset.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
8	1 2 3 4 5 6 7	isltrn	$$⊢\left(K\in B\wedge W\in H\right)\to \left(F\in T\leftrightarrow \left(F\in D\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)$$
9		3simpa	$$⊢\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\wedge p\ne q\right)\to \left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)$$
10	9	imim1i	$$⊢\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\wedge p\ne q\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)$$
11		3anass	$$⊢\left(p\ne q\wedge \neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\leftrightarrow \left(p\ne q\wedge \left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\right)$$
12		3anrot	$$⊢\left(p\ne q\wedge \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\wedge p\ne q\right)$$
13		df-ne	$$⊢p\ne q\leftrightarrow \neg p=q$$
14	13	anbi1i	$$⊢\left(p\ne q\wedge \left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\right)\leftrightarrow \left(\neg p=q\wedge \left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\right)$$
15	11 12 14	3bitr3i	$$⊢\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\wedge p\ne q\right)\leftrightarrow \left(\neg p=q\wedge \left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\right)\right)$$
16	15	imbi1i	$$⊢\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\wedge p\ne q\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=q\wedge \left(\neg p\underset{\dot{}}{\le }W\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\right)$$
17		impexp	$$⊢\left(\left(\neg p=q\wedge \left(\neg p\underset{\dot{}}{\le }W\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\right)\leftrightarrow \left(\neg p=q\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)$$
18	16 17	bitri	$$⊢\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\wedge p\ne q\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(\neg p=q\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)$$
19		id	$$⊢p=q\to p=q$$
20		fveq2	$$⊢p=q\to F\left(p\right)=F\left(q\right)$$
21	19 20	oveq12d	$$⊢p=q\to p\underset{\dot{}}{\vee }F\left(p\right)=q\underset{\dot{}}{\vee }F\left(q\right)$$
22	21	oveq1d	$$⊢p=q\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$$
23	22	a1d	$$⊢p=q\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)$$
24		pm2.61	$$⊢\left(p=q\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)\to \left(\left(\neg p=q\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)\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)$$
25	23 24	ax-mp	$$⊢\left(\neg p=q\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)\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)$$
26	18 25	sylbi	$$⊢\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\wedge p\ne q\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)$$
27	10 26	impbii	$$⊢\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\wedge p\ne q\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)$$
28	27	2ralbii	$$⊢\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)\leftrightarrow \forall p\in A\forall q\in A\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\wedge p\ne q\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)$$
29	28	anbi2i	$$⊢\left(F\in D\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)\leftrightarrow \left(F\in D\wedge \forall p\in A\forall q\in A\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\wedge p\ne q\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)$$
30	8 29	syl6bb	$$⊢\left(K\in B\wedge W\in H\right)\to \left(F\in T\leftrightarrow \left(F\in D\wedge \forall p\in A\forall q\in A\left(\left(\neg p\underset{\dot{}}{\le }W\wedge \neg q\underset{\dot{}}{\le }W\wedge p\ne q\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)$$