Theorem trlset

Description: The set of traces of lattice translations for a fiducial co-atom W . (Contributed by NM, 20-May-2012)

	Ref	Expression
Hypotheses	trlset.b	$$⊢B={\mathrm{Base}}_K$$
	trlset.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	trlset.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	trlset.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	trlset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	trlset.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	trlset.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	trlset.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
Assertion	trlset	$$⊢\left(K\in C\wedge W\in H\right)\to R=\left(f\in T⟼\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }W\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		trlset.b	$$⊢B={\mathrm{Base}}_K$$
2		trlset.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		trlset.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		trlset.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
5		trlset.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
6		trlset.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
7		trlset.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
8		trlset.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
9	1 2 3 4 5 6	trlfset	$$⊢K\in C\to \mathrm{trL}\left(K\right)=\left(w\in H⟼\left(f\in \mathrm{LTrn}\left(K\right)\left(w\right)⟼\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }w\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }w\right)\right)\right)\right)$$
10	9	fveq1d	$$⊢K\in C\to \mathrm{trL}\left(K\right)\left(W\right)=\left(w\in H⟼\left(f\in \mathrm{LTrn}\left(K\right)\left(w\right)⟼\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }w\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }w\right)\right)\right)\right)\left(W\right)$$
11	8 10	syl5eq	$$⊢K\in C\to R=\left(w\in H⟼\left(f\in \mathrm{LTrn}\left(K\right)\left(w\right)⟼\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }w\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }w\right)\right)\right)\right)\left(W\right)$$
12		fveq2	$$⊢w=W\to \mathrm{LTrn}\left(K\right)\left(w\right)=\mathrm{LTrn}\left(K\right)\left(W\right)$$
13		breq2	$$⊢w=W\to \left(p\underset{\dot{}}{\le }w\leftrightarrow p\underset{\dot{}}{\le }W\right)$$
14	13	notbid	$$⊢w=W\to \left(\neg p\underset{\dot{}}{\le }w\leftrightarrow \neg p\underset{\dot{}}{\le }W\right)$$
15		oveq2	$$⊢w=W\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$$
16	15	eqeq2d	$$⊢w=W\to \left(x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }w\leftrightarrow x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }W\right)$$
17	14 16	imbi12d	$$⊢w=W\to \left(\left(\neg p\underset{\dot{}}{\le }w\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }w\right)\leftrightarrow \left(\neg p\underset{\dot{}}{\le }W\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }W\right)\right)$$
18	17	ralbidv	$$⊢w=W\to \left(\forall p\in A\left(\neg p\underset{\dot{}}{\le }w\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }w\right)\leftrightarrow \forall p\in A\left(\neg p\underset{\dot{}}{\le }W\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }W\right)\right)$$
19	18	riotabidv	$$⊢w=W\to \left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }w\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }w\right)\right)=\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }W\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }W\right)\right)$$
20	12 19	mpteq12dv	$$⊢w=W\to \left(f\in \mathrm{LTrn}\left(K\right)\left(w\right)⟼\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }w\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }w\right)\right)\right)=\left(f\in \mathrm{LTrn}\left(K\right)\left(W\right)⟼\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }W\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
21		eqid	$$⊢\left(w\in H⟼\left(f\in \mathrm{LTrn}\left(K\right)\left(w\right)⟼\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }w\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }w\right)\right)\right)\right)=\left(w\in H⟼\left(f\in \mathrm{LTrn}\left(K\right)\left(w\right)⟼\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }w\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }w\right)\right)\right)\right)$$
22		fvex	$$⊢\mathrm{LTrn}\left(K\right)\left(W\right)\in \mathrm{V}$$
23	22	mptex	$$⊢\left(f\in \mathrm{LTrn}\left(K\right)\left(W\right)⟼\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }W\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }W\right)\right)\right)\in \mathrm{V}$$
24	20 21 23	fvmpt	$$⊢W\in H\to \left(w\in H⟼\left(f\in \mathrm{LTrn}\left(K\right)\left(w\right)⟼\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }w\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }w\right)\right)\right)\right)\left(W\right)=\left(f\in \mathrm{LTrn}\left(K\right)\left(W\right)⟼\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }W\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
25	7	mpteq1i	$$⊢\left(f\in T⟼\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }W\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }W\right)\right)\right)=\left(f\in \mathrm{LTrn}\left(K\right)\left(W\right)⟼\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }W\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
26	24 25	eqtr4di	$$⊢W\in H\to \left(w\in H⟼\left(f\in \mathrm{LTrn}\left(K\right)\left(w\right)⟼\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }w\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }w\right)\right)\right)\right)\left(W\right)=\left(f\in T⟼\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }W\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
27	11 26	sylan9eq	$$⊢\left(K\in C\wedge W\in H\right)\to R=\left(f\in T⟼\left(\iota x\in B|\forall p\in A\left(\neg p\underset{\dot{}}{\le }W\to x=\left(p\underset{\dot{}}{\vee }f\left(p\right)\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$