Theorem diafval

Description: The partial isomorphism A for a lattice K . (Contributed by NM, 15-Oct-2013)

	Ref	Expression
Hypotheses	diaval.b	$$⊢B={\mathrm{Base}}_K$$
	diaval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	diaval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	diaval.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	diaval.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
	diaval.i	$$⊢I=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
Assertion	diafval	$$⊢\left(K\in V\wedge W\in H\right)\to I=\left(x\in \left\{y\in B|y\underset{\dot{}}{\le }W\right\}⟼\left\{f\in T|R\left(f\right)\underset{\dot{}}{\le }x\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		diaval.b	$$⊢B={\mathrm{Base}}_K$$
2		diaval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		diaval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		diaval.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
5		diaval.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
6		diaval.i	$$⊢I=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
7	1 2 3	diaffval	$$⊢K\in V\to \mathrm{DIsoA}\left(K\right)=\left(w\in H⟼\left(x\in \left\{y\in B|y\underset{\dot{}}{\le }w\right\}⟼\left\{f\in \mathrm{LTrn}\left(K\right)\left(w\right)|\mathrm{trL}\left(K\right)\left(w\right)\left(f\right)\underset{\dot{}}{\le }x\right\}\right)\right)$$
8	7	fveq1d	$$⊢K\in V\to \mathrm{DIsoA}\left(K\right)\left(W\right)=\left(w\in H⟼\left(x\in \left\{y\in B|y\underset{\dot{}}{\le }w\right\}⟼\left\{f\in \mathrm{LTrn}\left(K\right)\left(w\right)|\mathrm{trL}\left(K\right)\left(w\right)\left(f\right)\underset{\dot{}}{\le }x\right\}\right)\right)\left(W\right)$$
9	6 8	eqtrid	$$⊢K\in V\to I=\left(w\in H⟼\left(x\in \left\{y\in B|y\underset{\dot{}}{\le }w\right\}⟼\left\{f\in \mathrm{LTrn}\left(K\right)\left(w\right)|\mathrm{trL}\left(K\right)\left(w\right)\left(f\right)\underset{\dot{}}{\le }x\right\}\right)\right)\left(W\right)$$
10		breq2	$$⊢w=W\to \left(y\underset{\dot{}}{\le }w\leftrightarrow y\underset{\dot{}}{\le }W\right)$$
11	10	rabbidv	$$⊢w=W\to \left\{y\in B|y\underset{\dot{}}{\le }w\right\}=\left\{y\in B|y\underset{\dot{}}{\le }W\right\}$$
12		fveq2	$$⊢w=W\to \mathrm{LTrn}\left(K\right)\left(w\right)=\mathrm{LTrn}\left(K\right)\left(W\right)$$
13	12 4	eqtr4di	$$⊢w=W\to \mathrm{LTrn}\left(K\right)\left(w\right)=T$$
14		fveq2	$$⊢w=W\to \mathrm{trL}\left(K\right)\left(w\right)=\mathrm{trL}\left(K\right)\left(W\right)$$
15	14 5	eqtr4di	$$⊢w=W\to \mathrm{trL}\left(K\right)\left(w\right)=R$$
16	15	fveq1d	$$⊢w=W\to \mathrm{trL}\left(K\right)\left(w\right)\left(f\right)=R\left(f\right)$$
17	16	breq1d	$$⊢w=W\to \left(\mathrm{trL}\left(K\right)\left(w\right)\left(f\right)\underset{\dot{}}{\le }x\leftrightarrow R\left(f\right)\underset{\dot{}}{\le }x\right)$$
18	13 17	rabeqbidv	$$⊢w=W\to \left\{f\in \mathrm{LTrn}\left(K\right)\left(w\right)|\mathrm{trL}\left(K\right)\left(w\right)\left(f\right)\underset{\dot{}}{\le }x\right\}=\left\{f\in T|R\left(f\right)\underset{\dot{}}{\le }x\right\}$$
19	11 18	mpteq12dv	$$⊢w=W\to \left(x\in \left\{y\in B|y\underset{\dot{}}{\le }w\right\}⟼\left\{f\in \mathrm{LTrn}\left(K\right)\left(w\right)|\mathrm{trL}\left(K\right)\left(w\right)\left(f\right)\underset{\dot{}}{\le }x\right\}\right)=\left(x\in \left\{y\in B|y\underset{\dot{}}{\le }W\right\}⟼\left\{f\in T|R\left(f\right)\underset{\dot{}}{\le }x\right\}\right)$$
20		eqid	$$⊢\left(w\in H⟼\left(x\in \left\{y\in B|y\underset{\dot{}}{\le }w\right\}⟼\left\{f\in \mathrm{LTrn}\left(K\right)\left(w\right)|\mathrm{trL}\left(K\right)\left(w\right)\left(f\right)\underset{\dot{}}{\le }x\right\}\right)\right)=\left(w\in H⟼\left(x\in \left\{y\in B|y\underset{\dot{}}{\le }w\right\}⟼\left\{f\in \mathrm{LTrn}\left(K\right)\left(w\right)|\mathrm{trL}\left(K\right)\left(w\right)\left(f\right)\underset{\dot{}}{\le }x\right\}\right)\right)$$
21	1	fvexi	$$⊢B\in \mathrm{V}$$
22	21	mptrabex	$$⊢\left(x\in \left\{y\in B|y\underset{\dot{}}{\le }W\right\}⟼\left\{f\in T|R\left(f\right)\underset{\dot{}}{\le }x\right\}\right)\in \mathrm{V}$$
23	19 20 22	fvmpt	$$⊢W\in H\to \left(w\in H⟼\left(x\in \left\{y\in B|y\underset{\dot{}}{\le }w\right\}⟼\left\{f\in \mathrm{LTrn}\left(K\right)\left(w\right)|\mathrm{trL}\left(K\right)\left(w\right)\left(f\right)\underset{\dot{}}{\le }x\right\}\right)\right)\left(W\right)=\left(x\in \left\{y\in B|y\underset{\dot{}}{\le }W\right\}⟼\left\{f\in T|R\left(f\right)\underset{\dot{}}{\le }x\right\}\right)$$
24	9 23	sylan9eq	$$⊢\left(K\in V\wedge W\in H\right)\to I=\left(x\in \left\{y\in B|y\underset{\dot{}}{\le }W\right\}⟼\left\{f\in T|R\left(f\right)\underset{\dot{}}{\le }x\right\}\right)$$