# Metamath Proof Explorer

## 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}}_{ℋ}$
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 3oalem5 ${⊢}\left({B}{+}_{ℋ}{R}\right)\cap \left({C}{+}_{ℋ}{S}\right)=\left({B}{\vee }_{ℋ}{R}\right)\cap \left({C}{\vee }_{ℋ}{S}\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 4 3oalem4 ${⊢}{R}\subseteq \perp \left({B}\right)$
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 2 osumi ${⊢}{R}\subseteq \perp \left({B}\right)\to {R}{+}_{ℋ}{B}={R}{\vee }_{ℋ}{B}$
12 6 11 ax-mp ${⊢}{R}{+}_{ℋ}{B}={R}{\vee }_{ℋ}{B}$
13 2 chshii ${⊢}{B}\in {\mathbf{S}}_{ℋ}$
14 10 chshii ${⊢}{R}\in {\mathbf{S}}_{ℋ}$
15 13 14 shscomi ${⊢}{B}{+}_{ℋ}{R}={R}{+}_{ℋ}{B}$
16 2 10 chjcomi ${⊢}{B}{\vee }_{ℋ}{R}={R}{\vee }_{ℋ}{B}$
17 12 15 16 3eqtr4i ${⊢}{B}{+}_{ℋ}{R}={B}{\vee }_{ℋ}{R}$
18 5 3oalem4 ${⊢}{S}\subseteq \perp \left({C}\right)$
19 3 choccli ${⊢}\perp \left({C}\right)\in {\mathbf{C}}_{ℋ}$
20 3 1 chjcli ${⊢}{C}{\vee }_{ℋ}{A}\in {\mathbf{C}}_{ℋ}$
21 19 20 chincli ${⊢}\perp \left({C}\right)\cap \left({C}{\vee }_{ℋ}{A}\right)\in {\mathbf{C}}_{ℋ}$
22 5 21 eqeltri ${⊢}{S}\in {\mathbf{C}}_{ℋ}$
23 22 3 osumi ${⊢}{S}\subseteq \perp \left({C}\right)\to {S}{+}_{ℋ}{C}={S}{\vee }_{ℋ}{C}$
24 18 23 ax-mp ${⊢}{S}{+}_{ℋ}{C}={S}{\vee }_{ℋ}{C}$
25 3 chshii ${⊢}{C}\in {\mathbf{S}}_{ℋ}$
26 22 chshii ${⊢}{S}\in {\mathbf{S}}_{ℋ}$
27 25 26 shscomi ${⊢}{C}{+}_{ℋ}{S}={S}{+}_{ℋ}{C}$
28 3 22 chjcomi ${⊢}{C}{\vee }_{ℋ}{S}={S}{\vee }_{ℋ}{C}$
29 24 27 28 3eqtr4i ${⊢}{C}{+}_{ℋ}{S}={C}{\vee }_{ℋ}{S}$
30 17 29 ineq12i ${⊢}\left({B}{+}_{ℋ}{R}\right)\cap \left({C}{+}_{ℋ}{S}\right)=\left({B}{\vee }_{ℋ}{R}\right)\cap \left({C}{\vee }_{ℋ}{S}\right)$