Theorem trlval

Description: The value of the trace of a lattice translation. (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	trlval	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge F\in T\right)\to R\left(F\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)$$

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 7 8	trlset	$$⊢\left(K\in V\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)$$
10	9	fveq1d	$$⊢\left(K\in V\wedge W\in H\right)\to R\left(F\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)\left(F\right)$$
11		fveq1	$$⊢f=F\to f\left(p\right)=F\left(p\right)$$
12	11	oveq2d	$$⊢f=F\to p\underset{\dot{}}{\vee }f\left(p\right)=p\underset{\dot{}}{\vee }F\left(p\right)$$
13	12	oveq1d	$$⊢f=F\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$$
14	13	eqeq2d	$$⊢f=F\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)$$
15	14	imbi2d	$$⊢f=F\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)$$
16	15	ralbidv	$$⊢f=F\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)$$
17	16	riotabidv	$$⊢f=F\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)$$
18		eqid	$$⊢\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 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)$$
19		riotaex	$$⊢\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)\in \mathrm{V}$$
20	17 18 19	fvmpt	$$⊢F\in T\to \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\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)$$
21	10 20	sylan9eq	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge F\in T\right)\to R\left(F\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)$$