Theorem cmtvalN

Description: Equivalence for commutes relation. Definition of commutes in Kalmbach p. 20. ( cmbr analog.) (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	cmtvalN	$$⊢\left(K\in A\wedge X\in B\wedge Y\in B\right)\to \left(XCY\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)$$

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	1 2 3 4 5	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\}$$
7		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)$$
8	7	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\}$$
9	6 8	eqtrdi	$$⊢K\in A\to C=\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\}$$
10	9	breqd	$$⊢K\in A\to \left(XCY\leftrightarrow X\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\}Y\right)$$
11	10	3ad2ant1	$$⊢\left(K\in A\wedge X\in B\wedge Y\in B\right)\to \left(XCY\leftrightarrow X\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\}Y\right)$$
12		df-br	$$⊢X\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\}Y\leftrightarrow ⟨X,Y⟩\in \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\}$$
13		id	$$⊢x=X\to x=X$$
14		oveq1	$$⊢x=X\to x\underset{\dot{}}{\wedge }y=X\underset{\dot{}}{\wedge }y$$
15		oveq1	$$⊢x=X\to x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(y\right)=X\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(y\right)$$
16	14 15	oveq12d	$$⊢x=X\to \left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\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)$$
17	13 16	eqeq12d	$$⊢x=X\to \left(x=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\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)$$
18		oveq2	$$⊢y=Y\to X\underset{\dot{}}{\wedge }y=X\underset{\dot{}}{\wedge }Y$$
19		fveq2	$$⊢y=Y\to \underset{\dot{}}{\perp }\left(y\right)=\underset{\dot{}}{\perp }\left(Y\right)$$
20	19	oveq2d	$$⊢y=Y\to X\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(y\right)=X\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(Y\right)$$
21	18 20	oveq12d	$$⊢y=Y\to \left(X\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\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	$$⊢y=Y\to \left(X=\left(X\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\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	17 22	opelopab2	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(⟨X,Y⟩\in \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\}\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)$$
24	12 23	bitrid	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(X\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\}Y\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)$$
25	24	3adant1	$$⊢\left(K\in A\wedge X\in B\wedge Y\in B\right)\to \left(X\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\}Y\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)$$
26	11 25	bitrd	$$⊢\left(K\in A\wedge X\in B\wedge Y\in B\right)\to \left(XCY\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)$$