Theorem 3oalem6

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	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)$$

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	2	chshii	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
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	chshii	$$⊢R\in {\mathbf{S}}_{\mathscr{H}}$$
12	3	choccli	$$⊢\perp \left(C\right)\in {\mathbf{C}}_{\mathscr{H}}$$
13	3 1	chjcli	$$⊢C{\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}$$
14	12 13	chincli	$$⊢\perp \left(C\right)\cap \left(C{\vee }_{\mathscr{H}}A\right)\in {\mathbf{C}}_{\mathscr{H}}$$
15	5 14	eqeltri	$$⊢S\in {\mathbf{C}}_{\mathscr{H}}$$
16	15	chshii	$$⊢S\in {\mathbf{S}}_{\mathscr{H}}$$
17	3	chshii	$$⊢C\in {\mathbf{S}}_{\mathscr{H}}$$
18	6 17	shscli	$$⊢B{+}_{\mathscr{H}}C\in {\mathbf{S}}_{\mathscr{H}}$$
19	11 16	shscli	$$⊢R{+}_{\mathscr{H}}S\in {\mathbf{S}}_{\mathscr{H}}$$
20	18 19	shincli	$$⊢\left(B{+}_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)\in {\mathbf{S}}_{\mathscr{H}}$$
21	16 20	shscli	$$⊢S{+}_{\mathscr{H}}\left(\left(B{+}_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)\right)\in {\mathbf{S}}_{\mathscr{H}}$$
22	11 21	shincli	$$⊢R\cap \left(S{+}_{\mathscr{H}}\left(\left(B{+}_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)\right)\right)\in {\mathbf{S}}_{\mathscr{H}}$$
23	6 22	shsleji	$$⊢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{+}_{\mathscr{H}}\left(\left(B{+}_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)\right)\right)\right)$$
24	16 20	shsleji	$$⊢S{+}_{\mathscr{H}}\left(\left(B{+}_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)\right)\subseteq S{\vee }_{\mathscr{H}}\left(\left(B{+}_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)\right)$$
25	2 3	chsleji	$$⊢B{+}_{\mathscr{H}}C\subseteq B{\vee }_{\mathscr{H}}C$$
26		ssrin	$$⊢B{+}_{\mathscr{H}}C\subseteq B{\vee }_{\mathscr{H}}C\to \left(B{+}_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)\subseteq \left(B{\vee }_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)$$
27	25 26	ax-mp	$$⊢\left(B{+}_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)\subseteq \left(B{\vee }_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)$$
28	10 15	chsleji	$$⊢R{+}_{\mathscr{H}}S\subseteq R{\vee }_{\mathscr{H}}S$$
29		sslin	$$⊢R{+}_{\mathscr{H}}S\subseteq R{\vee }_{\mathscr{H}}S\to \left(B{\vee }_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)\subseteq \left(B{\vee }_{\mathscr{H}}C\right)\cap \left(R{\vee }_{\mathscr{H}}S\right)$$
30	28 29	ax-mp	$$⊢\left(B{\vee }_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)\subseteq \left(B{\vee }_{\mathscr{H}}C\right)\cap \left(R{\vee }_{\mathscr{H}}S\right)$$
31	27 30	sstri	$$⊢\left(B{+}_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)\subseteq \left(B{\vee }_{\mathscr{H}}C\right)\cap \left(R{\vee }_{\mathscr{H}}S\right)$$
32	2 3	chjcli	$$⊢B{\vee }_{\mathscr{H}}C\in {\mathbf{C}}_{\mathscr{H}}$$
33	10 15	chjcli	$$⊢R{\vee }_{\mathscr{H}}S\in {\mathbf{C}}_{\mathscr{H}}$$
34	32 33	chincli	$$⊢\left(B{\vee }_{\mathscr{H}}C\right)\cap \left(R{\vee }_{\mathscr{H}}S\right)\in {\mathbf{C}}_{\mathscr{H}}$$
35	34	chshii	$$⊢\left(B{\vee }_{\mathscr{H}}C\right)\cap \left(R{\vee }_{\mathscr{H}}S\right)\in {\mathbf{S}}_{\mathscr{H}}$$
36	20 35 16	shlej2i	$$⊢\left(B{+}_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)\subseteq \left(B{\vee }_{\mathscr{H}}C\right)\cap \left(R{\vee }_{\mathscr{H}}S\right)\to S{\vee }_{\mathscr{H}}\left(\left(B{+}_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)\right)\subseteq S{\vee }_{\mathscr{H}}\left(\left(B{\vee }_{\mathscr{H}}C\right)\cap \left(R{\vee }_{\mathscr{H}}S\right)\right)$$
37	31 36	ax-mp	$$⊢S{\vee }_{\mathscr{H}}\left(\left(B{+}_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)\right)\subseteq S{\vee }_{\mathscr{H}}\left(\left(B{\vee }_{\mathscr{H}}C\right)\cap \left(R{\vee }_{\mathscr{H}}S\right)\right)$$
38	24 37	sstri	$$⊢S{+}_{\mathscr{H}}\left(\left(B{+}_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)\right)\subseteq S{\vee }_{\mathscr{H}}\left(\left(B{\vee }_{\mathscr{H}}C\right)\cap \left(R{\vee }_{\mathscr{H}}S\right)\right)$$
39		sslin	$$⊢S{+}_{\mathscr{H}}\left(\left(B{+}_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)\right)\subseteq S{\vee }_{\mathscr{H}}\left(\left(B{\vee }_{\mathscr{H}}C\right)\cap \left(R{\vee }_{\mathscr{H}}S\right)\right)\to R\cap \left(S{+}_{\mathscr{H}}\left(\left(B{+}_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)\right)\right)\subseteq 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)$$
40	38 39	ax-mp	$$⊢R\cap \left(S{+}_{\mathscr{H}}\left(\left(B{+}_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)\right)\right)\subseteq 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)$$
41	15 34	chjcli	$$⊢S{\vee }_{\mathscr{H}}\left(\left(B{\vee }_{\mathscr{H}}C\right)\cap \left(R{\vee }_{\mathscr{H}}S\right)\right)\in {\mathbf{C}}_{\mathscr{H}}$$
42	10 41	chincli	$$⊢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)\in {\mathbf{C}}_{\mathscr{H}}$$
43	42	chshii	$$⊢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)\in {\mathbf{S}}_{\mathscr{H}}$$
44	22 43 6	shlej2i	$$⊢R\cap \left(S{+}_{\mathscr{H}}\left(\left(B{+}_{\mathscr{H}}C\right)\cap \left(R{+}_{\mathscr{H}}S\right)\right)\right)\subseteq 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)\to B{\vee }_{\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)$$
45	40 44	ax-mp	$$⊢B{\vee }_{\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)$$
46	23 45	sstri	$$⊢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)$$