Theorem cmtfvalN

Description: Value of commutes relation. (Contributed by NM, 6-Nov-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cmtfval.b	$$⊢B={\mathrm{Base}}_K$$
	cmtfval.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cmtfval.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	cmtfval.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
	cmtfval.c	$$⊢C=\mathrm{cm}\left(K\right)$$
Assertion	cmtfvalN	$$⊢K\in A\to C=\left\{⟨x,y⟩|\left(x\in B\wedge y\in B\wedge x=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(y\right)\right)\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		cmtfval.b	$$⊢B={\mathrm{Base}}_K$$
2		cmtfval.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		cmtfval.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		cmtfval.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
5		cmtfval.c	$$⊢C=\mathrm{cm}\left(K\right)$$
6		elex	$$⊢K\in A\to K\in \mathrm{V}$$
7		fveq2	$$⊢p=K\to {\mathrm{Base}}_p={\mathrm{Base}}_K$$
8	7 1	eqtr4di	$$⊢p=K\to {\mathrm{Base}}_p=B$$
9	8	eleq2d	$$⊢p=K\to \left(x\in {\mathrm{Base}}_p\leftrightarrow x\in B\right)$$
10	8	eleq2d	$$⊢p=K\to \left(y\in {\mathrm{Base}}_p\leftrightarrow y\in B\right)$$
11		fveq2	$$⊢p=K\to \mathrm{join}\left(p\right)=\mathrm{join}\left(K\right)$$
12	11 2	eqtr4di	$$⊢p=K\to \mathrm{join}\left(p\right)=\underset{\dot{}}{\vee }$$
13		fveq2	$$⊢p=K\to \mathrm{meet}\left(p\right)=\mathrm{meet}\left(K\right)$$
14	13 3	eqtr4di	$$⊢p=K\to \mathrm{meet}\left(p\right)=\underset{\dot{}}{\wedge }$$
15	14	oveqd	$$⊢p=K\to x\mathrm{meet}\left(p\right)y=x\underset{\dot{}}{\wedge }y$$
16		eqidd	$$⊢p=K\to x=x$$
17		fveq2	$$⊢p=K\to \mathrm{oc}\left(p\right)=\mathrm{oc}\left(K\right)$$
18	17 4	eqtr4di	$$⊢p=K\to \mathrm{oc}\left(p\right)=\underset{\dot{}}{\perp }$$
19	18	fveq1d	$$⊢p=K\to \mathrm{oc}\left(p\right)\left(y\right)=\underset{\dot{}}{\perp }\left(y\right)$$
20	14 16 19	oveq123d	$$⊢p=K\to x\mathrm{meet}\left(p\right)\mathrm{oc}\left(p\right)\left(y\right)=x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(y\right)$$
21	12 15 20	oveq123d	$$⊢p=K\to \left(x\mathrm{meet}\left(p\right)y\right)\mathrm{join}\left(p\right)\left(x\mathrm{meet}\left(p\right)\mathrm{oc}\left(p\right)\left(y\right)\right)=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(y\right)\right)$$
22	21	eqeq2d	$$⊢p=K\to \left(x=\left(x\mathrm{meet}\left(p\right)y\right)\mathrm{join}\left(p\right)\left(x\mathrm{meet}\left(p\right)\mathrm{oc}\left(p\right)\left(y\right)\right)\leftrightarrow x=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(y\right)\right)\right)$$
23	9 10 22	3anbi123d	$$⊢p=K\to \left(\left(x\in {\mathrm{Base}}_p\wedge y\in {\mathrm{Base}}_p\wedge x=\left(x\mathrm{meet}\left(p\right)y\right)\mathrm{join}\left(p\right)\left(x\mathrm{meet}\left(p\right)\mathrm{oc}\left(p\right)\left(y\right)\right)\right)\leftrightarrow \left(x\in B\wedge y\in B\wedge x=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(y\right)\right)\right)\right)$$
24	23	opabbidv	$$⊢p=K\to \left\{⟨x,y⟩|\left(x\in {\mathrm{Base}}_p\wedge y\in {\mathrm{Base}}_p\wedge x=\left(x\mathrm{meet}\left(p\right)y\right)\mathrm{join}\left(p\right)\left(x\mathrm{meet}\left(p\right)\mathrm{oc}\left(p\right)\left(y\right)\right)\right)\right\}=\left\{⟨x,y⟩|\left(x\in B\wedge y\in B\wedge x=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(y\right)\right)\right)\right\}$$
25		df-cmtN	$$⊢\mathrm{cm}=\left(p\in \mathrm{V}⟼\left\{⟨x,y⟩|\left(x\in {\mathrm{Base}}_p\wedge y\in {\mathrm{Base}}_p\wedge x=\left(x\mathrm{meet}\left(p\right)y\right)\mathrm{join}\left(p\right)\left(x\mathrm{meet}\left(p\right)\mathrm{oc}\left(p\right)\left(y\right)\right)\right)\right\}\right)$$
26		df-3an	$$⊢\left(x\in B\wedge y\in B\wedge x=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(y\right)\right)\right)\leftrightarrow \left(\left(x\in B\wedge y\in B\right)\wedge x=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(y\right)\right)\right)$$
27	26	opabbii	$$⊢\left\{⟨x,y⟩|\left(x\in B\wedge y\in B\wedge x=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(y\right)\right)\right)\right\}=\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge x=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(y\right)\right)\right)\right\}$$
28	1	fvexi	$$⊢B\in \mathrm{V}$$
29	28 28	xpex	$$⊢B\times B\in \mathrm{V}$$
30		opabssxp	$$⊢\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge x=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(y\right)\right)\right)\right\}\subseteq B\times B$$
31	29 30	ssexi	$$⊢\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge x=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(y\right)\right)\right)\right\}\in \mathrm{V}$$
32	27 31	eqeltri	$$⊢\left\{⟨x,y⟩|\left(x\in B\wedge y\in B\wedge x=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(y\right)\right)\right)\right\}\in \mathrm{V}$$
33	24 25 32	fvmpt	$$⊢K\in \mathrm{V}\to \mathrm{cm}\left(K\right)=\left\{⟨x,y⟩|\left(x\in B\wedge y\in B\wedge x=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(y\right)\right)\right)\right\}$$
34	5 33	syl5eq	$$⊢K\in \mathrm{V}\to C=\left\{⟨x,y⟩|\left(x\in B\wedge y\in B\wedge x=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(y\right)\right)\right)\right\}$$
35	6 34	syl	$$⊢K\in A\to C=\left\{⟨x,y⟩|\left(x\in B\wedge y\in B\wedge x=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(y\right)\right)\right)\right\}$$