Theorem 3oalem5

Description: Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	3oa.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	3oa.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
	3oa.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
	3oa.4	$$⊢R=\perp \left(B\right)\cap \left(B{\vee }_{\mathscr{H}}A\right)$$
	3oa.5	$$⊢S=\perp \left(C\right)\cap \left(C{\vee }_{\mathscr{H}}A\right)$$
Assertion	3oalem5	$$⊢\left(B{+}_{\mathscr{H}}R\right)\cap \left(C{+}_{\mathscr{H}}S\right)=\left(B{\vee }_{\mathscr{H}}R\right)\cap \left(C{\vee }_{\mathscr{H}}S\right)$$

Proof

Step	Hyp	Ref	Expression
1		3oa.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		3oa.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		3oa.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
4		3oa.4	$$⊢R=\perp \left(B\right)\cap \left(B{\vee }_{\mathscr{H}}A\right)$$
5		3oa.5	$$⊢S=\perp \left(C\right)\cap \left(C{\vee }_{\mathscr{H}}A\right)$$
6	4	3oalem4	$$⊢R\subseteq \perp \left(B\right)$$
7	2	choccli	$$⊢\perp \left(B\right)\in {\mathbf{C}}_{\mathscr{H}}$$
8	2 1	chjcli	$$⊢B{\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}$$
9	7 8	chincli	$$⊢\perp \left(B\right)\cap \left(B{\vee }_{\mathscr{H}}A\right)\in {\mathbf{C}}_{\mathscr{H}}$$
10	4 9	eqeltri	$$⊢R\in {\mathbf{C}}_{\mathscr{H}}$$
11	10 2	osumi	$$⊢R\subseteq \perp \left(B\right)\to R{+}_{\mathscr{H}}B=R{\vee }_{\mathscr{H}}B$$
12	6 11	ax-mp	$$⊢R{+}_{\mathscr{H}}B=R{\vee }_{\mathscr{H}}B$$
13	2	chshii	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
14	10	chshii	$$⊢R\in {\mathbf{S}}_{\mathscr{H}}$$
15	13 14	shscomi	$$⊢B{+}_{\mathscr{H}}R=R{+}_{\mathscr{H}}B$$
16	2 10	chjcomi	$$⊢B{\vee }_{\mathscr{H}}R=R{\vee }_{\mathscr{H}}B$$
17	12 15 16	3eqtr4i	$$⊢B{+}_{\mathscr{H}}R=B{\vee }_{\mathscr{H}}R$$
18	5	3oalem4	$$⊢S\subseteq \perp \left(C\right)$$
19	3	choccli	$$⊢\perp \left(C\right)\in {\mathbf{C}}_{\mathscr{H}}$$
20	3 1	chjcli	$$⊢C{\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}$$
21	19 20	chincli	$$⊢\perp \left(C\right)\cap \left(C{\vee }_{\mathscr{H}}A\right)\in {\mathbf{C}}_{\mathscr{H}}$$
22	5 21	eqeltri	$$⊢S\in {\mathbf{C}}_{\mathscr{H}}$$
23	22 3	osumi	$$⊢S\subseteq \perp \left(C\right)\to S{+}_{\mathscr{H}}C=S{\vee }_{\mathscr{H}}C$$
24	18 23	ax-mp	$$⊢S{+}_{\mathscr{H}}C=S{\vee }_{\mathscr{H}}C$$
25	3	chshii	$$⊢C\in {\mathbf{S}}_{\mathscr{H}}$$
26	22	chshii	$$⊢S\in {\mathbf{S}}_{\mathscr{H}}$$
27	25 26	shscomi	$$⊢C{+}_{\mathscr{H}}S=S{+}_{\mathscr{H}}C$$
28	3 22	chjcomi	$$⊢C{\vee }_{\mathscr{H}}S=S{\vee }_{\mathscr{H}}C$$
29	24 27 28	3eqtr4i	$$⊢C{+}_{\mathscr{H}}S=C{\vee }_{\mathscr{H}}S$$
30	17 29	ineq12i	$$⊢\left(B{+}_{\mathscr{H}}R\right)\cap \left(C{+}_{\mathscr{H}}S\right)=\left(B{\vee }_{\mathscr{H}}R\right)\cap \left(C{\vee }_{\mathscr{H}}S\right)$$