Theorem osumcor2i

Description: Corollary of osumi , showing it holds under the weaker hypothesis that A and B commute. (Contributed by NM, 6-Dec-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	osum.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	osum.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	osumcor2i	$$⊢A{𝐶}_{\mathscr{H}}B\to A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B$$

Proof

Step	Hyp	Ref	Expression
1		osum.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		osum.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3	1 2	cmcm2i	$$⊢A{𝐶}_{\mathscr{H}}B\leftrightarrow A{𝐶}_{\mathscr{H}}\perp \left(B\right)$$
4	2	choccli	$$⊢\perp \left(B\right)\in {\mathbf{C}}_{\mathscr{H}}$$
5	1 4	cmbr4i	$$⊢A{𝐶}_{\mathscr{H}}\perp \left(B\right)\leftrightarrow A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\subseteq \perp \left(B\right)$$
6	3 5	bitri	$$⊢A{𝐶}_{\mathscr{H}}B\leftrightarrow A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\subseteq \perp \left(B\right)$$
7	1	choccli	$$⊢\perp \left(A\right)\in {\mathbf{C}}_{\mathscr{H}}$$
8	7 4	chjcli	$$⊢\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\in {\mathbf{C}}_{\mathscr{H}}$$
9	1 8	chincli	$$⊢A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\in {\mathbf{C}}_{\mathscr{H}}$$
10	9 2	osumi	$$⊢A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\subseteq \perp \left(B\right)\to \left(A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\right){+}_{\mathscr{H}}B=\left(A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\right){\vee }_{\mathscr{H}}B$$
11	7 4	chjcomi	$$⊢\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)=\perp \left(B\right){\vee }_{\mathscr{H}}\perp \left(A\right)$$
12	11	ineq2i	$$⊢A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)=A\cap \left(\perp \left(B\right){\vee }_{\mathscr{H}}\perp \left(A\right)\right)$$
13	12	oveq1i	$$⊢\left(A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\right){\vee }_{\mathscr{H}}B=\left(A\cap \left(\perp \left(B\right){\vee }_{\mathscr{H}}\perp \left(A\right)\right)\right){\vee }_{\mathscr{H}}B$$
14	4 7	chjcli	$$⊢\perp \left(B\right){\vee }_{\mathscr{H}}\perp \left(A\right)\in {\mathbf{C}}_{\mathscr{H}}$$
15	1 14	chincli	$$⊢A\cap \left(\perp \left(B\right){\vee }_{\mathscr{H}}\perp \left(A\right)\right)\in {\mathbf{C}}_{\mathscr{H}}$$
16	15 2	chjcomi	$$⊢\left(A\cap \left(\perp \left(B\right){\vee }_{\mathscr{H}}\perp \left(A\right)\right)\right){\vee }_{\mathscr{H}}B=B{\vee }_{\mathscr{H}}\left(A\cap \left(\perp \left(B\right){\vee }_{\mathscr{H}}\perp \left(A\right)\right)\right)$$
17	13 16	eqtri	$$⊢\left(A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\right){\vee }_{\mathscr{H}}B=B{\vee }_{\mathscr{H}}\left(A\cap \left(\perp \left(B\right){\vee }_{\mathscr{H}}\perp \left(A\right)\right)\right)$$
18	2 1	pjoml4i	$$⊢B{\vee }_{\mathscr{H}}\left(A\cap \left(\perp \left(B\right){\vee }_{\mathscr{H}}\perp \left(A\right)\right)\right)=B{\vee }_{\mathscr{H}}A$$
19	2 1	chjcomi	$$⊢B{\vee }_{\mathscr{H}}A=A{\vee }_{\mathscr{H}}B$$
20	18 19	eqtri	$$⊢B{\vee }_{\mathscr{H}}\left(A\cap \left(\perp \left(B\right){\vee }_{\mathscr{H}}\perp \left(A\right)\right)\right)=A{\vee }_{\mathscr{H}}B$$
21	17 20	eqtri	$$⊢\left(A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\right){\vee }_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B$$
22	21	eqeq2i	$$⊢\left(A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\right){+}_{\mathscr{H}}B=\left(A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\right){\vee }_{\mathscr{H}}B\leftrightarrow \left(A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\right){+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B$$
23		inss1	$$⊢A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\subseteq A$$
24	9	chshii	$$⊢A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\in {\mathbf{S}}_{\mathscr{H}}$$
25	1	chshii	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
26	2	chshii	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
27	24 25 26	shlessi	$$⊢A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\subseteq A\to \left(A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\right){+}_{\mathscr{H}}B\subseteq A{+}_{\mathscr{H}}B$$
28	23 27	ax-mp	$$⊢\left(A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\right){+}_{\mathscr{H}}B\subseteq A{+}_{\mathscr{H}}B$$
29		sseq1	$$⊢\left(A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\right){+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\to \left(\left(A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\right){+}_{\mathscr{H}}B\subseteq A{+}_{\mathscr{H}}B\leftrightarrow A{\vee }_{\mathscr{H}}B\subseteq A{+}_{\mathscr{H}}B\right)$$
30	28 29	mpbii	$$⊢\left(A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\right){+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\to A{\vee }_{\mathscr{H}}B\subseteq A{+}_{\mathscr{H}}B$$
31	22 30	sylbi	$$⊢\left(A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\right){+}_{\mathscr{H}}B=\left(A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\right){\vee }_{\mathscr{H}}B\to A{\vee }_{\mathscr{H}}B\subseteq A{+}_{\mathscr{H}}B$$
32	10 31	syl	$$⊢A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}\perp \left(B\right)\right)\subseteq \perp \left(B\right)\to A{\vee }_{\mathscr{H}}B\subseteq A{+}_{\mathscr{H}}B$$
33	6 32	sylbi	$$⊢A{𝐶}_{\mathscr{H}}B\to A{\vee }_{\mathscr{H}}B\subseteq A{+}_{\mathscr{H}}B$$
34	1 2	chsleji	$$⊢A{+}_{\mathscr{H}}B\subseteq A{\vee }_{\mathscr{H}}B$$
35	33 34	jctil	$$⊢A{𝐶}_{\mathscr{H}}B\to \left(A{+}_{\mathscr{H}}B\subseteq A{\vee }_{\mathscr{H}}B\wedge A{\vee }_{\mathscr{H}}B\subseteq A{+}_{\mathscr{H}}B\right)$$
36		eqss	$$⊢A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\leftrightarrow \left(A{+}_{\mathscr{H}}B\subseteq A{\vee }_{\mathscr{H}}B\wedge A{\vee }_{\mathscr{H}}B\subseteq A{+}_{\mathscr{H}}B\right)$$
37	35 36	sylibr	$$⊢A{𝐶}_{\mathscr{H}}B\to A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B$$