Theorem 3oai

Description: 3OA (weak) orthoarguesian law. Equation IV of GodowskiGreechie p. 249. (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	3oai	$$⊢\left(B{\vee }_{\mathscr{H}}R\right)\cap \left(C{\vee }_{\mathscr{H}}S\right)\subseteq B{\vee }_{\mathscr{H}}\left(R\cap \left(S{\vee }_{\mathscr{H}}\left(\left(B{\vee }_{\mathscr{H}}C\right)\cap \left(R{\vee }_{\mathscr{H}}S\right)\right)\right)\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	1 2 3 4 5	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)$$
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	3	choccli	$$⊢\perp \left(C\right)\in {\mathbf{C}}_{\mathscr{H}}$$
12	3 1	chjcli	$$⊢C{\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}$$
13	11 12	chincli	$$⊢\perp \left(C\right)\cap \left(C{\vee }_{\mathscr{H}}A\right)\in {\mathbf{C}}_{\mathscr{H}}$$
14	5 13	eqeltri	$$⊢S\in {\mathbf{C}}_{\mathscr{H}}$$
15	2 3 10 14	3oalem3	$$⊢\left(B{+}_{\mathscr{H}}R\right)\cap \left(C{+}_{\mathscr{H}}S\right)\subseteq B{+}_{\mathscr{H}}\left(R\cap \left(S{+}_{\mathscr{H}}\left(\left(B{+}_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)\right)\right)\right)$$
16	1 2 3 4 5	3oalem6	$$⊢B{+}_{\mathscr{H}}\left(R\cap \left(S{+}_{\mathscr{H}}\left(\left(B{+}_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)\right)\right)\right)\subseteq B{\vee }_{\mathscr{H}}\left(R\cap \left(S{\vee }_{\mathscr{H}}\left(\left(B{\vee }_{\mathscr{H}}C\right)\cap \left(R{\vee }_{\mathscr{H}}S\right)\right)\right)\right)$$
17	15 16	sstri	$$⊢\left(B{+}_{\mathscr{H}}R\right)\cap \left(C{+}_{\mathscr{H}}S\right)\subseteq B{\vee }_{\mathscr{H}}\left(R\cap \left(S{\vee }_{\mathscr{H}}\left(\left(B{\vee }_{\mathscr{H}}C\right)\cap \left(R{\vee }_{\mathscr{H}}S\right)\right)\right)\right)$$
18	6 17	eqsstrri	$$⊢\left(B{\vee }_{\mathscr{H}}R\right)\cap \left(C{\vee }_{\mathscr{H}}S\right)\subseteq B{\vee }_{\mathscr{H}}\left(R\cap \left(S{\vee }_{\mathscr{H}}\left(\left(B{\vee }_{\mathscr{H}}C\right)\cap \left(R{\vee }_{\mathscr{H}}S\right)\right)\right)\right)$$