Metamath Proof Explorer

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}}_{ℋ}$
3oa.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
3oa.3 ${⊢}{C}\in {\mathbf{C}}_{ℋ}$
3oa.4 ${⊢}{R}=\perp \left({B}\right)\cap \left({B}{\vee }_{ℋ}{A}\right)$
3oa.5 ${⊢}{S}=\perp \left({C}\right)\cap \left({C}{\vee }_{ℋ}{A}\right)$
Assertion 3oalem6 ${⊢}{B}{+}_{ℋ}\left({R}\cap \left({S}{+}_{ℋ}\left(\left({B}{+}_{ℋ}{C}\right)\cap \left({R}{+}_{ℋ}{S}\right)\right)\right)\right)\subseteq {B}{\vee }_{ℋ}\left({R}\cap \left({S}{\vee }_{ℋ}\left(\left({B}{\vee }_{ℋ}{C}\right)\cap \left({R}{\vee }_{ℋ}{S}\right)\right)\right)\right)$

Proof

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