Theorem cdlemksv

Description: Part of proof of Lemma K of Crawley p. 118. Value of the sigma(p) function. (Contributed by NM, 26-Jun-2013)

	Ref	Expression
Hypotheses	cdlemk.b	$$⊢B={\mathrm{Base}}_K$$
	cdlemk.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cdlemk.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cdlemk.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	cdlemk.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	cdlemk.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	cdlemk.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
	cdlemk.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	cdlemk.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)$$
Assertion	cdlemksv	$$⊢G\in T\to S\left(G\right)=\left(\iota i\in T|i\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(G\right)\right)\underset{\dot{}}{\wedge }\left(N\left(P\right)\underset{\dot{}}{\vee }R\left(G\circ F^{-1}\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cdlemk.b	$$⊢B={\mathrm{Base}}_K$$
2		cdlemk.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		cdlemk.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		cdlemk.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		cdlemk.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
6		cdlemk.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
7		cdlemk.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
8		cdlemk.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
9		cdlemk.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		fveq2	$$⊢f=G\to R\left(f\right)=R\left(G\right)$$
11	10	oveq2d	$$⊢f=G\to P\underset{\dot{}}{\vee }R\left(f\right)=P\underset{\dot{}}{\vee }R\left(G\right)$$
12		coeq1	$$⊢f=G\to f\circ F^{-1}=G\circ F^{-1}$$
13	12	fveq2d	$$⊢f=G\to R\left(f\circ F^{-1}\right)=R\left(G\circ F^{-1}\right)$$
14	13	oveq2d	$$⊢f=G\to N\left(P\right)\underset{\dot{}}{\vee }R\left(f\circ F^{-1}\right)=N\left(P\right)\underset{\dot{}}{\vee }R\left(G\circ F^{-1}\right)$$
15	11 14	oveq12d	$$⊢f=G\to \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)=\left(P\underset{\dot{}}{\vee }R\left(G\right)\right)\underset{\dot{}}{\wedge }\left(N\left(P\right)\underset{\dot{}}{\vee }R\left(G\circ F^{-1}\right)\right)$$
16	15	eqeq2d	$$⊢f=G\to \left(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)\leftrightarrow i\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(G\right)\right)\underset{\dot{}}{\wedge }\left(N\left(P\right)\underset{\dot{}}{\vee }R\left(G\circ F^{-1}\right)\right)\right)$$
17	16	riotabidv	$$⊢f=G\to \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)=\left(\iota i\in T|i\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(G\right)\right)\underset{\dot{}}{\wedge }\left(N\left(P\right)\underset{\dot{}}{\vee }R\left(G\circ F^{-1}\right)\right)\right)$$
18		riotaex	$$⊢\left(\iota i\in T|i\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(G\right)\right)\underset{\dot{}}{\wedge }\left(N\left(P\right)\underset{\dot{}}{\vee }R\left(G\circ F^{-1}\right)\right)\right)\in \mathrm{V}$$
19	17 9 18	fvmpt	$$⊢G\in T\to S\left(G\right)=\left(\iota i\in T|i\left(P\right)=\left(P\underset{\dot{}}{\vee }R\left(G\right)\right)\underset{\dot{}}{\wedge }\left(N\left(P\right)\underset{\dot{}}{\vee }R\left(G\circ F^{-1}\right)\right)\right)$$