# Metamath Proof Explorer

## Theorem 5oalem4

Description: Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000) (New usage is discouraged.)

Ref Expression
Hypotheses 5oalem3.1 ${⊢}{A}\in {\mathbf{S}}_{ℋ}$
5oalem3.2 ${⊢}{B}\in {\mathbf{S}}_{ℋ}$
5oalem3.3 ${⊢}{C}\in {\mathbf{S}}_{ℋ}$
5oalem3.4 ${⊢}{D}\in {\mathbf{S}}_{ℋ}$
5oalem3.5 ${⊢}{F}\in {\mathbf{S}}_{ℋ}$
5oalem3.6 ${⊢}{G}\in {\mathbf{S}}_{ℋ}$
Assertion 5oalem4 ${⊢}\left(\left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge \left({z}\in {C}\wedge {w}\in {D}\right)\right)\wedge \left({f}\in {F}\wedge {g}\in {G}\right)\right)\wedge \left({x}{+}_{ℎ}{y}={f}{+}_{ℎ}{g}\wedge {z}{+}_{ℎ}{w}={f}{+}_{ℎ}{g}\right)\right)\to {x}{-}_{ℎ}{z}\in \left(\left(\left({A}{+}_{ℋ}{C}\right)\cap \left({B}{+}_{ℋ}{D}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{F}\right)\cap \left({B}{+}_{ℋ}{G}\right)\right){+}_{ℋ}\left(\left({C}{+}_{ℋ}{F}\right)\cap \left({D}{+}_{ℋ}{G}\right)\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 5oalem3.1 ${⊢}{A}\in {\mathbf{S}}_{ℋ}$
2 5oalem3.2 ${⊢}{B}\in {\mathbf{S}}_{ℋ}$
3 5oalem3.3 ${⊢}{C}\in {\mathbf{S}}_{ℋ}$
4 5oalem3.4 ${⊢}{D}\in {\mathbf{S}}_{ℋ}$
5 5oalem3.5 ${⊢}{F}\in {\mathbf{S}}_{ℋ}$
6 5oalem3.6 ${⊢}{G}\in {\mathbf{S}}_{ℋ}$
7 eqtr3 ${⊢}\left({x}{+}_{ℎ}{y}={f}{+}_{ℎ}{g}\wedge {z}{+}_{ℎ}{w}={f}{+}_{ℎ}{g}\right)\to {x}{+}_{ℎ}{y}={z}{+}_{ℎ}{w}$
8 1 2 3 4 5oalem2 ${⊢}\left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge \left({z}\in {C}\wedge {w}\in {D}\right)\right)\wedge {x}{+}_{ℎ}{y}={z}{+}_{ℎ}{w}\right)\to {x}{-}_{ℎ}{z}\in \left(\left({A}{+}_{ℋ}{C}\right)\cap \left({B}{+}_{ℋ}{D}\right)\right)$
9 7 8 sylan2 ${⊢}\left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge \left({z}\in {C}\wedge {w}\in {D}\right)\right)\wedge \left({x}{+}_{ℎ}{y}={f}{+}_{ℎ}{g}\wedge {z}{+}_{ℎ}{w}={f}{+}_{ℎ}{g}\right)\right)\to {x}{-}_{ℎ}{z}\in \left(\left({A}{+}_{ℋ}{C}\right)\cap \left({B}{+}_{ℋ}{D}\right)\right)$
10 9 adantlr ${⊢}\left(\left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge \left({z}\in {C}\wedge {w}\in {D}\right)\right)\wedge \left({f}\in {F}\wedge {g}\in {G}\right)\right)\wedge \left({x}{+}_{ℎ}{y}={f}{+}_{ℎ}{g}\wedge {z}{+}_{ℎ}{w}={f}{+}_{ℎ}{g}\right)\right)\to {x}{-}_{ℎ}{z}\in \left(\left({A}{+}_{ℋ}{C}\right)\cap \left({B}{+}_{ℋ}{D}\right)\right)$
11 1 2 3 4 5 6 5oalem3 ${⊢}\left(\left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge \left({z}\in {C}\wedge {w}\in {D}\right)\right)\wedge \left({f}\in {F}\wedge {g}\in {G}\right)\right)\wedge \left({x}{+}_{ℎ}{y}={f}{+}_{ℎ}{g}\wedge {z}{+}_{ℎ}{w}={f}{+}_{ℎ}{g}\right)\right)\to {x}{-}_{ℎ}{z}\in \left(\left(\left({A}{+}_{ℋ}{F}\right)\cap \left({B}{+}_{ℋ}{G}\right)\right){+}_{ℋ}\left(\left({C}{+}_{ℋ}{F}\right)\cap \left({D}{+}_{ℋ}{G}\right)\right)\right)$
12 10 11 elind ${⊢}\left(\left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge \left({z}\in {C}\wedge {w}\in {D}\right)\right)\wedge \left({f}\in {F}\wedge {g}\in {G}\right)\right)\wedge \left({x}{+}_{ℎ}{y}={f}{+}_{ℎ}{g}\wedge {z}{+}_{ℎ}{w}={f}{+}_{ℎ}{g}\right)\right)\to {x}{-}_{ℎ}{z}\in \left(\left(\left({A}{+}_{ℋ}{C}\right)\cap \left({B}{+}_{ℋ}{D}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{F}\right)\cap \left({B}{+}_{ℋ}{G}\right)\right){+}_{ℋ}\left(\left({C}{+}_{ℋ}{F}\right)\cap \left({D}{+}_{ℋ}{G}\right)\right)\right)\right)$