Theorem cmbr

Description: Binary relation expressing A commutes with B . Definition of commutes in Kalmbach p. 20. (Contributed by NM, 14-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	cmbr	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{𝐶}_{\mathscr{H}}B\leftrightarrow A=\left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap \perp \left(B\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$$⊢x=A\to \left(x\in {\mathbf{C}}_{\mathscr{H}}\leftrightarrow A\in {\mathbf{C}}_{\mathscr{H}}\right)$$
2	1	anbi1d	$$⊢x=A\to \left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\leftrightarrow \left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\right)$$
3		id	$$⊢x=A\to x=A$$
4		ineq1	$$⊢x=A\to x\cap y=A\cap y$$
5		ineq1	$$⊢x=A\to x\cap \perp \left(y\right)=A\cap \perp \left(y\right)$$
6	4 5	oveq12d	$$⊢x=A\to \left(x\cap y\right){\vee }_{\mathscr{H}}\left(x\cap \perp \left(y\right)\right)=\left(A\cap y\right){\vee }_{\mathscr{H}}\left(A\cap \perp \left(y\right)\right)$$
7	3 6	eqeq12d	$$⊢x=A\to \left(x=\left(x\cap y\right){\vee }_{\mathscr{H}}\left(x\cap \perp \left(y\right)\right)\leftrightarrow A=\left(A\cap y\right){\vee }_{\mathscr{H}}\left(A\cap \perp \left(y\right)\right)\right)$$
8	2 7	anbi12d	$$⊢x=A\to \left(\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge x=\left(x\cap y\right){\vee }_{\mathscr{H}}\left(x\cap \perp \left(y\right)\right)\right)\leftrightarrow \left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge A=\left(A\cap y\right){\vee }_{\mathscr{H}}\left(A\cap \perp \left(y\right)\right)\right)\right)$$
9		eleq1	$$⊢y=B\to \left(y\in {\mathbf{C}}_{\mathscr{H}}\leftrightarrow B\in {\mathbf{C}}_{\mathscr{H}}\right)$$
10	9	anbi2d	$$⊢y=B\to \left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\leftrightarrow \left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\right)$$
11		ineq2	$$⊢y=B\to A\cap y=A\cap B$$
12		fveq2	$$⊢y=B\to \perp \left(y\right)=\perp \left(B\right)$$
13	12	ineq2d	$$⊢y=B\to A\cap \perp \left(y\right)=A\cap \perp \left(B\right)$$
14	11 13	oveq12d	$$⊢y=B\to \left(A\cap y\right){\vee }_{\mathscr{H}}\left(A\cap \perp \left(y\right)\right)=\left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap \perp \left(B\right)\right)$$
15	14	eqeq2d	$$⊢y=B\to \left(A=\left(A\cap y\right){\vee }_{\mathscr{H}}\left(A\cap \perp \left(y\right)\right)\leftrightarrow A=\left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap \perp \left(B\right)\right)\right)$$
16	10 15	anbi12d	$$⊢y=B\to \left(\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge A=\left(A\cap y\right){\vee }_{\mathscr{H}}\left(A\cap \perp \left(y\right)\right)\right)\leftrightarrow \left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge A=\left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap \perp \left(B\right)\right)\right)\right)$$
17		df-cm	$$⊢{𝐶}_{\mathscr{H}}=\left\{⟨x,y⟩|\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge x=\left(x\cap y\right){\vee }_{\mathscr{H}}\left(x\cap \perp \left(y\right)\right)\right)\right\}$$
18	8 16 17	brabg	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{𝐶}_{\mathscr{H}}B\leftrightarrow \left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge A=\left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap \perp \left(B\right)\right)\right)\right)$$
19	18	bianabs	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{𝐶}_{\mathscr{H}}B\leftrightarrow A=\left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap \perp \left(B\right)\right)\right)$$