Theorem cdlemkuu

Description: Convert between function and operation forms of Y . TODO: Use operation form everywhere. (Contributed by NM, 6-Jul-2013)

	Ref	Expression
Hypotheses	cdlemk3.b	$$⊢B={\mathrm{Base}}_K$$
	cdlemk3.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cdlemk3.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cdlemk3.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	cdlemk3.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	cdlemk3.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	cdlemk3.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	cdlemk3.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
	cdlemk3.s	$$⊢S=\left(f\in T⟼\left(\iota i\in T|i\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(f\right)\right)\underset{\dot{}}{\wedge }\left(N\left(P\right)\underset{\dot{}}{\vee }R\left(f\circ F^{-1}\right)\right)\right)\right)$$
	cdlemk3.u1	$$⊢Y=\left(d\in T,e\in T⟼\left(\iota j\in T|j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(e\right)\right)\underset{\dot{}}{\wedge }\left(S\left(d\right)\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ d^{-1}\right)\right)\right)\right)$$
	cdlemk3.o2	$$⊢Q=S\left(D\right)$$
	cdlemk3.u2	$$⊢Z=\left(e\in T⟼\left(\iota j\in T|j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(e\right)\right)\underset{\dot{}}{\wedge }\left(Q\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ D^{-1}\right)\right)\right)\right)$$
Assertion	cdlemkuu	$$⊢\left(D\in T\wedge G\in T\right)\to DYG=Z\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		cdlemk3.b	$$⊢B={\mathrm{Base}}_K$$
2		cdlemk3.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		cdlemk3.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		cdlemk3.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
5		cdlemk3.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
6		cdlemk3.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
7		cdlemk3.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
8		cdlemk3.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
9		cdlemk3.s	$$⊢S=\left(f\in T⟼\left(\iota i\in T|i\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(f\right)\right)\underset{\dot{}}{\wedge }\left(N\left(P\right)\underset{\dot{}}{\vee }R\left(f\circ F^{-1}\right)\right)\right)\right)$$
10		cdlemk3.u1	$$⊢Y=\left(d\in T,e\in T⟼\left(\iota j\in T|j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(e\right)\right)\underset{\dot{}}{\wedge }\left(S\left(d\right)\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ d^{-1}\right)\right)\right)\right)$$
11		cdlemk3.o2	$$⊢Q=S\left(D\right)$$
12		cdlemk3.u2	$$⊢Z=\left(e\in T⟼\left(\iota j\in T|j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(e\right)\right)\underset{\dot{}}{\wedge }\left(Q\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ D^{-1}\right)\right)\right)\right)$$
13		fveq2	$$⊢d=D\to S\left(d\right)=S\left(D\right)$$
14	13 11	eqtr4di	$$⊢d=D\to S\left(d\right)=Q$$
15	14	fveq1d	$$⊢d=D\to S\left(d\right)\left(P\right)=Q\left(P\right)$$
16		cnveq	$$⊢d=D\to d^{-1}=D^{-1}$$
17	16	coeq2d	$$⊢d=D\to e\circ d^{-1}=e\circ D^{-1}$$
18	17	fveq2d	$$⊢d=D\to R\left(e\circ d^{-1}\right)=R\left(e\circ D^{-1}\right)$$
19	15 18	oveq12d	$$⊢d=D\to S\left(d\right)\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ d^{-1}\right)=Q\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ D^{-1}\right)$$
20	19	oveq2d	$$⊢d=D\to \left(P\underset{\dot{}}{\vee }R\left(e\right)\right)\underset{\dot{}}{\wedge }\left(S\left(d\right)\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ d^{-1}\right)\right)=\left(P\underset{\dot{}}{\vee }R\left(e\right)\right)\underset{\dot{}}{\wedge }\left(Q\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ D^{-1}\right)\right)$$
21	20	eqeq2d	$$⊢d=D\to \left(j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(e\right)\right)\underset{\dot{}}{\wedge }\left(S\left(d\right)\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ d^{-1}\right)\right)\leftrightarrow j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(e\right)\right)\underset{\dot{}}{\wedge }\left(Q\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ D^{-1}\right)\right)\right)$$
22	21	riotabidv	$$⊢d=D\to \left(\iota j\in T|j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(e\right)\right)\underset{\dot{}}{\wedge }\left(S\left(d\right)\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ d^{-1}\right)\right)\right)=\left(\iota j\in T|j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(e\right)\right)\underset{\dot{}}{\wedge }\left(Q\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ D^{-1}\right)\right)\right)$$
23		fveq2	$$⊢e=G\to R\left(e\right)=R\left(G\right)$$
24	23	oveq2d	$$⊢e=G\to P\underset{\dot{}}{\vee }R\left(e\right)=P\underset{\dot{}}{\vee }R\left(G\right)$$
25		coeq1	$$⊢e=G\to e\circ D^{-1}=G\circ D^{-1}$$
26	25	fveq2d	$$⊢e=G\to R\left(e\circ D^{-1}\right)=R\left(G\circ D^{-1}\right)$$
27	26	oveq2d	$$⊢e=G\to Q\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ D^{-1}\right)=Q\left(P\right)\underset{\dot{}}{\vee }R\left(G\circ D^{-1}\right)$$
28	24 27	oveq12d	$$⊢e=G\to \left(P\underset{\dot{}}{\vee }R\left(e\right)\right)\underset{\dot{}}{\wedge }\left(Q\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ D^{-1}\right)\right)=\left(P\underset{\dot{}}{\vee }R\left(G\right)\right)\underset{\dot{}}{\wedge }\left(Q\left(P\right)\underset{\dot{}}{\vee }R\left(G\circ D^{-1}\right)\right)$$
29	28	eqeq2d	$$⊢e=G\to \left(j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(e\right)\right)\underset{\dot{}}{\wedge }\left(Q\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ D^{-1}\right)\right)\leftrightarrow j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(G\right)\right)\underset{\dot{}}{\wedge }\left(Q\left(P\right)\underset{\dot{}}{\vee }R\left(G\circ D^{-1}\right)\right)\right)$$
30	29	riotabidv	$$⊢e=G\to \left(\iota j\in T|j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(e\right)\right)\underset{\dot{}}{\wedge }\left(Q\left(P\right)\underset{\dot{}}{\vee }R\left(e\circ D^{-1}\right)\right)\right)=\left(\iota j\in T|j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(G\right)\right)\underset{\dot{}}{\wedge }\left(Q\left(P\right)\underset{\dot{}}{\vee }R\left(G\circ D^{-1}\right)\right)\right)$$
31		riotaex	$$⊢\left(\iota j\in T|j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(G\right)\right)\underset{\dot{}}{\wedge }\left(Q\left(P\right)\underset{\dot{}}{\vee }R\left(G\circ D^{-1}\right)\right)\right)\in \mathrm{V}$$
32	22 30 10 31	ovmpo	$$⊢\left(D\in T\wedge G\in T\right)\to DYG=\left(\iota j\in T|j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(G\right)\right)\underset{\dot{}}{\wedge }\left(Q\left(P\right)\underset{\dot{}}{\vee }R\left(G\circ D^{-1}\right)\right)\right)$$
33	1 2 3 5 6 7 8 4 12	cdlemksv	$$⊢G\in T\to Z\left(G\right)=\left(\iota j\in T|j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(G\right)\right)\underset{\dot{}}{\wedge }\left(Q\left(P\right)\underset{\dot{}}{\vee }R\left(G\circ D^{-1}\right)\right)\right)$$
34	33	adantl	$$⊢\left(D\in T\wedge G\in T\right)\to Z\left(G\right)=\left(\iota j\in T|j\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(G\right)\right)\underset{\dot{}}{\wedge }\left(Q\left(P\right)\underset{\dot{}}{\vee }R\left(G\circ D^{-1}\right)\right)\right)$$
35	32 34	eqtr4d	$$⊢\left(D\in T\wedge G\in T\right)\to DYG=Z\left(G\right)$$