Theorem cmbr3i

Description: Alternate definition for the commutes relation. Lemma 3 of Kalmbach p. 23. (Contributed by NM, 6-Dec-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjoml2.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	pjoml2.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	cmbr3i	$$⊢A{𝐶}_{\mathscr{H}}B\leftrightarrow A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)=A\cap B$$

Proof

Step	Hyp	Ref	Expression
1		pjoml2.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjoml2.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3	1 2	cmcmi	$$⊢A{𝐶}_{\mathscr{H}}B\leftrightarrow B{𝐶}_{\mathscr{H}}A$$
4	2 1	cmbr2i	$$⊢B{𝐶}_{\mathscr{H}}A\leftrightarrow B=\left(B{\vee }_{\mathscr{H}}A\right)\cap \left(B{\vee }_{\mathscr{H}}\perp \left(A\right)\right)$$
5	3 4	bitri	$$⊢A{𝐶}_{\mathscr{H}}B\leftrightarrow B=\left(B{\vee }_{\mathscr{H}}A\right)\cap \left(B{\vee }_{\mathscr{H}}\perp \left(A\right)\right)$$
6		ineq2	$$⊢B=\left(B{\vee }_{\mathscr{H}}A\right)\cap \left(B{\vee }_{\mathscr{H}}\perp \left(A\right)\right)\to A\cap B=A\cap \left(\left(B{\vee }_{\mathscr{H}}A\right)\cap \left(B{\vee }_{\mathscr{H}}\perp \left(A\right)\right)\right)$$
7		inass	$$⊢\left(A\cap \left(B{\vee }_{\mathscr{H}}A\right)\right)\cap \left(B{\vee }_{\mathscr{H}}\perp \left(A\right)\right)=A\cap \left(\left(B{\vee }_{\mathscr{H}}A\right)\cap \left(B{\vee }_{\mathscr{H}}\perp \left(A\right)\right)\right)$$
8	2 1	chjcomi	$$⊢B{\vee }_{\mathscr{H}}A=A{\vee }_{\mathscr{H}}B$$
9	8	ineq2i	$$⊢A\cap \left(B{\vee }_{\mathscr{H}}A\right)=A\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
10	1 2	chabs2i	$$⊢A\cap \left(A{\vee }_{\mathscr{H}}B\right)=A$$
11	9 10	eqtri	$$⊢A\cap \left(B{\vee }_{\mathscr{H}}A\right)=A$$
12	1	choccli	$$⊢\perp \left(A\right)\in {\mathbf{C}}_{\mathscr{H}}$$
13	2 12	chjcomi	$$⊢B{\vee }_{\mathscr{H}}\perp \left(A\right)=\perp \left(A\right){\vee }_{\mathscr{H}}B$$
14	11 13	ineq12i	$$⊢\left(A\cap \left(B{\vee }_{\mathscr{H}}A\right)\right)\cap \left(B{\vee }_{\mathscr{H}}\perp \left(A\right)\right)=A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)$$
15	7 14	eqtr3i	$$⊢A\cap \left(\left(B{\vee }_{\mathscr{H}}A\right)\cap \left(B{\vee }_{\mathscr{H}}\perp \left(A\right)\right)\right)=A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)$$
16	6 15	eqtr2di	$$⊢B=\left(B{\vee }_{\mathscr{H}}A\right)\cap \left(B{\vee }_{\mathscr{H}}\perp \left(A\right)\right)\to A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)=A\cap B$$
17	5 16	sylbi	$$⊢A{𝐶}_{\mathscr{H}}B\to A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)=A\cap B$$
18		inss1	$$⊢A\cap \perp \left(B\right)\subseteq A$$
19	2	choccli	$$⊢\perp \left(B\right)\in {\mathbf{C}}_{\mathscr{H}}$$
20	1 19	chincli	$$⊢A\cap \perp \left(B\right)\in {\mathbf{C}}_{\mathscr{H}}$$
21	20 1	pjoml2i	$$⊢A\cap \perp \left(B\right)\subseteq A\to \left(A\cap \perp \left(B\right)\right){\vee }_{\mathscr{H}}\left(\perp \left(A\cap \perp \left(B\right)\right)\cap A\right)=A$$
22	18 21	ax-mp	$$⊢\left(A\cap \perp \left(B\right)\right){\vee }_{\mathscr{H}}\left(\perp \left(A\cap \perp \left(B\right)\right)\cap A\right)=A$$
23	20	choccli	$$⊢\perp \left(A\cap \perp \left(B\right)\right)\in {\mathbf{C}}_{\mathscr{H}}$$
24	23 1	chincli	$$⊢\perp \left(A\cap \perp \left(B\right)\right)\cap A\in {\mathbf{C}}_{\mathscr{H}}$$
25	20 24	chjcomi	$$⊢\left(A\cap \perp \left(B\right)\right){\vee }_{\mathscr{H}}\left(\perp \left(A\cap \perp \left(B\right)\right)\cap A\right)=\left(\perp \left(A\cap \perp \left(B\right)\right)\cap A\right){\vee }_{\mathscr{H}}\left(A\cap \perp \left(B\right)\right)$$
26	22 25	eqtr3i	$$⊢A=\left(\perp \left(A\cap \perp \left(B\right)\right)\cap A\right){\vee }_{\mathscr{H}}\left(A\cap \perp \left(B\right)\right)$$
27	1 2	chdmm3i	$$⊢\perp \left(A\cap \perp \left(B\right)\right)=\perp \left(A\right){\vee }_{\mathscr{H}}B$$
28	27	ineq2i	$$⊢A\cap \perp \left(A\cap \perp \left(B\right)\right)=A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)$$
29		incom	$$⊢A\cap \perp \left(A\cap \perp \left(B\right)\right)=\perp \left(A\cap \perp \left(B\right)\right)\cap A$$
30	28 29	eqtr3i	$$⊢A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)=\perp \left(A\cap \perp \left(B\right)\right)\cap A$$
31	30	eqeq1i	$$⊢A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)=A\cap B\leftrightarrow \perp \left(A\cap \perp \left(B\right)\right)\cap A=A\cap B$$
32		oveq1	$$⊢\perp \left(A\cap \perp \left(B\right)\right)\cap A=A\cap B\to \left(\perp \left(A\cap \perp \left(B\right)\right)\cap A\right){\vee }_{\mathscr{H}}\left(A\cap \perp \left(B\right)\right)=\left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap \perp \left(B\right)\right)$$
33	31 32	sylbi	$$⊢A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)=A\cap B\to \left(\perp \left(A\cap \perp \left(B\right)\right)\cap A\right){\vee }_{\mathscr{H}}\left(A\cap \perp \left(B\right)\right)=\left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap \perp \left(B\right)\right)$$
34	26 33	syl5eq	$$⊢A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)=A\cap B\to A=\left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap \perp \left(B\right)\right)$$
35	1 2	cmbri	$$⊢A{𝐶}_{\mathscr{H}}B\leftrightarrow A=\left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap \perp \left(B\right)\right)$$
36	34 35	sylibr	$$⊢A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)=A\cap B\to A{𝐶}_{\mathscr{H}}B$$
37	17 36	impbii	$$⊢A{𝐶}_{\mathscr{H}}B\leftrightarrow A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)=A\cap B$$