# Metamath Proof Explorer

## Theorem 5oalem6

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

Ref Expression
Hypotheses 5oalem5.1 ${⊢}{A}\in {\mathbf{S}}_{ℋ}$
5oalem5.2 ${⊢}{B}\in {\mathbf{S}}_{ℋ}$
5oalem5.3 ${⊢}{C}\in {\mathbf{S}}_{ℋ}$
5oalem5.4 ${⊢}{D}\in {\mathbf{S}}_{ℋ}$
5oalem5.5 ${⊢}{F}\in {\mathbf{S}}_{ℋ}$
5oalem5.6 ${⊢}{G}\in {\mathbf{S}}_{ℋ}$
5oalem5.7 ${⊢}{R}\in {\mathbf{S}}_{ℋ}$
5oalem5.8 ${⊢}{S}\in {\mathbf{S}}_{ℋ}$
Assertion 5oalem6 ${⊢}\left(\left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {h}={x}{+}_{ℎ}{y}\right)\wedge \left(\left({z}\in {C}\wedge {w}\in {D}\right)\wedge {h}={z}{+}_{ℎ}{w}\right)\right)\wedge \left(\left(\left({f}\in {F}\wedge {g}\in {G}\right)\wedge {h}={f}{+}_{ℎ}{g}\right)\wedge \left(\left({v}\in {R}\wedge {u}\in {S}\right)\wedge {h}={v}{+}_{ℎ}{u}\right)\right)\right)\to {h}\in \left({B}{+}_{ℋ}\left({A}\cap \left({C}{+}_{ℋ}\left(\left(\left(\left({A}{+}_{ℋ}{C}\right)\cap \left({B}{+}_{ℋ}{D}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right)\right)\right)\cap \left(\left(\left(\left({A}{+}_{ℋ}{F}\right)\cap \left({B}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right){+}_{ℋ}\left(\left(\left({C}{+}_{ℋ}{F}\right)\cap \left({D}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right)\right)\right)\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 5oalem5.1 ${⊢}{A}\in {\mathbf{S}}_{ℋ}$
2 5oalem5.2 ${⊢}{B}\in {\mathbf{S}}_{ℋ}$
3 5oalem5.3 ${⊢}{C}\in {\mathbf{S}}_{ℋ}$
4 5oalem5.4 ${⊢}{D}\in {\mathbf{S}}_{ℋ}$
5 5oalem5.5 ${⊢}{F}\in {\mathbf{S}}_{ℋ}$
6 5oalem5.6 ${⊢}{G}\in {\mathbf{S}}_{ℋ}$
7 5oalem5.7 ${⊢}{R}\in {\mathbf{S}}_{ℋ}$
8 5oalem5.8 ${⊢}{S}\in {\mathbf{S}}_{ℋ}$
9 an4 ${⊢}\left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {h}={x}{+}_{ℎ}{y}\right)\wedge \left(\left({z}\in {C}\wedge {w}\in {D}\right)\wedge {h}={z}{+}_{ℎ}{w}\right)\right)↔\left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge \left({z}\in {C}\wedge {w}\in {D}\right)\right)\wedge \left({h}={x}{+}_{ℎ}{y}\wedge {h}={z}{+}_{ℎ}{w}\right)\right)$
10 an4 ${⊢}\left(\left(\left({f}\in {F}\wedge {g}\in {G}\right)\wedge {h}={f}{+}_{ℎ}{g}\right)\wedge \left(\left({v}\in {R}\wedge {u}\in {S}\right)\wedge {h}={v}{+}_{ℎ}{u}\right)\right)↔\left(\left(\left({f}\in {F}\wedge {g}\in {G}\right)\wedge \left({v}\in {R}\wedge {u}\in {S}\right)\right)\wedge \left({h}={f}{+}_{ℎ}{g}\wedge {h}={v}{+}_{ℎ}{u}\right)\right)$
11 eqeq1 ${⊢}{h}={x}{+}_{ℎ}{y}\to \left({h}={v}{+}_{ℎ}{u}↔{x}{+}_{ℎ}{y}={v}{+}_{ℎ}{u}\right)$
12 11 biimpcd ${⊢}{h}={v}{+}_{ℎ}{u}\to \left({h}={x}{+}_{ℎ}{y}\to {x}{+}_{ℎ}{y}={v}{+}_{ℎ}{u}\right)$
13 eqeq1 ${⊢}{h}={z}{+}_{ℎ}{w}\to \left({h}={v}{+}_{ℎ}{u}↔{z}{+}_{ℎ}{w}={v}{+}_{ℎ}{u}\right)$
14 13 biimpcd ${⊢}{h}={v}{+}_{ℎ}{u}\to \left({h}={z}{+}_{ℎ}{w}\to {z}{+}_{ℎ}{w}={v}{+}_{ℎ}{u}\right)$
15 12 14 anim12d ${⊢}{h}={v}{+}_{ℎ}{u}\to \left(\left({h}={x}{+}_{ℎ}{y}\wedge {h}={z}{+}_{ℎ}{w}\right)\to \left({x}{+}_{ℎ}{y}={v}{+}_{ℎ}{u}\wedge {z}{+}_{ℎ}{w}={v}{+}_{ℎ}{u}\right)\right)$
16 eqeq1 ${⊢}{h}={f}{+}_{ℎ}{g}\to \left({h}={v}{+}_{ℎ}{u}↔{f}{+}_{ℎ}{g}={v}{+}_{ℎ}{u}\right)$
17 16 biimpcd ${⊢}{h}={v}{+}_{ℎ}{u}\to \left({h}={f}{+}_{ℎ}{g}\to {f}{+}_{ℎ}{g}={v}{+}_{ℎ}{u}\right)$
18 15 17 anim12d ${⊢}{h}={v}{+}_{ℎ}{u}\to \left(\left(\left({h}={x}{+}_{ℎ}{y}\wedge {h}={z}{+}_{ℎ}{w}\right)\wedge {h}={f}{+}_{ℎ}{g}\right)\to \left(\left({x}{+}_{ℎ}{y}={v}{+}_{ℎ}{u}\wedge {z}{+}_{ℎ}{w}={v}{+}_{ℎ}{u}\right)\wedge {f}{+}_{ℎ}{g}={v}{+}_{ℎ}{u}\right)\right)$
19 18 expdcom ${⊢}\left({h}={x}{+}_{ℎ}{y}\wedge {h}={z}{+}_{ℎ}{w}\right)\to \left({h}={f}{+}_{ℎ}{g}\to \left({h}={v}{+}_{ℎ}{u}\to \left(\left({x}{+}_{ℎ}{y}={v}{+}_{ℎ}{u}\wedge {z}{+}_{ℎ}{w}={v}{+}_{ℎ}{u}\right)\wedge {f}{+}_{ℎ}{g}={v}{+}_{ℎ}{u}\right)\right)\right)$
20 19 imp32 ${⊢}\left(\left({h}={x}{+}_{ℎ}{y}\wedge {h}={z}{+}_{ℎ}{w}\right)\wedge \left({h}={f}{+}_{ℎ}{g}\wedge {h}={v}{+}_{ℎ}{u}\right)\right)\to \left(\left({x}{+}_{ℎ}{y}={v}{+}_{ℎ}{u}\wedge {z}{+}_{ℎ}{w}={v}{+}_{ℎ}{u}\right)\wedge {f}{+}_{ℎ}{g}={v}{+}_{ℎ}{u}\right)$
21 20 anim2i ${⊢}\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(\left({f}\in {F}\wedge {g}\in {G}\right)\wedge \left({v}\in {R}\wedge {u}\in {S}\right)\right)\right)\wedge \left(\left({h}={x}{+}_{ℎ}{y}\wedge {h}={z}{+}_{ℎ}{w}\right)\wedge \left({h}={f}{+}_{ℎ}{g}\wedge {h}={v}{+}_{ℎ}{u}\right)\right)\right)\to \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(\left({f}\in {F}\wedge {g}\in {G}\right)\wedge \left({v}\in {R}\wedge {u}\in {S}\right)\right)\right)\wedge \left(\left({x}{+}_{ℎ}{y}={v}{+}_{ℎ}{u}\wedge {z}{+}_{ℎ}{w}={v}{+}_{ℎ}{u}\right)\wedge {f}{+}_{ℎ}{g}={v}{+}_{ℎ}{u}\right)\right)$
22 21 an4s ${⊢}\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({h}={x}{+}_{ℎ}{y}\wedge {h}={z}{+}_{ℎ}{w}\right)\right)\wedge \left(\left(\left({f}\in {F}\wedge {g}\in {G}\right)\wedge \left({v}\in {R}\wedge {u}\in {S}\right)\right)\wedge \left({h}={f}{+}_{ℎ}{g}\wedge {h}={v}{+}_{ℎ}{u}\right)\right)\right)\to \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(\left({f}\in {F}\wedge {g}\in {G}\right)\wedge \left({v}\in {R}\wedge {u}\in {S}\right)\right)\right)\wedge \left(\left({x}{+}_{ℎ}{y}={v}{+}_{ℎ}{u}\wedge {z}{+}_{ℎ}{w}={v}{+}_{ℎ}{u}\right)\wedge {f}{+}_{ℎ}{g}={v}{+}_{ℎ}{u}\right)\right)$
23 9 10 22 syl2anb ${⊢}\left(\left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {h}={x}{+}_{ℎ}{y}\right)\wedge \left(\left({z}\in {C}\wedge {w}\in {D}\right)\wedge {h}={z}{+}_{ℎ}{w}\right)\right)\wedge \left(\left(\left({f}\in {F}\wedge {g}\in {G}\right)\wedge {h}={f}{+}_{ℎ}{g}\right)\wedge \left(\left({v}\in {R}\wedge {u}\in {S}\right)\wedge {h}={v}{+}_{ℎ}{u}\right)\right)\right)\to \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(\left({f}\in {F}\wedge {g}\in {G}\right)\wedge \left({v}\in {R}\wedge {u}\in {S}\right)\right)\right)\wedge \left(\left({x}{+}_{ℎ}{y}={v}{+}_{ℎ}{u}\wedge {z}{+}_{ℎ}{w}={v}{+}_{ℎ}{u}\right)\wedge {f}{+}_{ℎ}{g}={v}{+}_{ℎ}{u}\right)\right)$
24 1 2 3 4 5 6 7 8 5oalem5 ${⊢}\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(\left({f}\in {F}\wedge {g}\in {G}\right)\wedge \left({v}\in {R}\wedge {u}\in {S}\right)\right)\right)\wedge \left(\left({x}{+}_{ℎ}{y}={v}{+}_{ℎ}{u}\wedge {z}{+}_{ℎ}{w}={v}{+}_{ℎ}{u}\right)\wedge {f}{+}_{ℎ}{g}={v}{+}_{ℎ}{u}\right)\right)\to {x}{-}_{ℎ}{z}\in \left(\left(\left(\left({A}{+}_{ℋ}{C}\right)\cap \left({B}{+}_{ℋ}{D}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right)\right)\right)\cap \left(\left(\left(\left({A}{+}_{ℋ}{F}\right)\cap \left({B}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right){+}_{ℋ}\left(\left(\left({C}{+}_{ℋ}{F}\right)\cap \left({D}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right)\right)\right)$
25 23 24 syl ${⊢}\left(\left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {h}={x}{+}_{ℎ}{y}\right)\wedge \left(\left({z}\in {C}\wedge {w}\in {D}\right)\wedge {h}={z}{+}_{ℎ}{w}\right)\right)\wedge \left(\left(\left({f}\in {F}\wedge {g}\in {G}\right)\wedge {h}={f}{+}_{ℎ}{g}\right)\wedge \left(\left({v}\in {R}\wedge {u}\in {S}\right)\wedge {h}={v}{+}_{ℎ}{u}\right)\right)\right)\to {x}{-}_{ℎ}{z}\in \left(\left(\left(\left({A}{+}_{ℋ}{C}\right)\cap \left({B}{+}_{ℋ}{D}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right)\right)\right)\cap \left(\left(\left(\left({A}{+}_{ℋ}{F}\right)\cap \left({B}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right){+}_{ℋ}\left(\left(\left({C}{+}_{ℋ}{F}\right)\cap \left({D}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right)\right)\right)$
26 1 3 shscli ${⊢}{A}{+}_{ℋ}{C}\in {\mathbf{S}}_{ℋ}$
27 2 4 shscli ${⊢}{B}{+}_{ℋ}{D}\in {\mathbf{S}}_{ℋ}$
28 26 27 shincli ${⊢}\left({A}{+}_{ℋ}{C}\right)\cap \left({B}{+}_{ℋ}{D}\right)\in {\mathbf{S}}_{ℋ}$
29 1 7 shscli ${⊢}{A}{+}_{ℋ}{R}\in {\mathbf{S}}_{ℋ}$
30 2 8 shscli ${⊢}{B}{+}_{ℋ}{S}\in {\mathbf{S}}_{ℋ}$
31 29 30 shincli ${⊢}\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\in {\mathbf{S}}_{ℋ}$
32 3 7 shscli ${⊢}{C}{+}_{ℋ}{R}\in {\mathbf{S}}_{ℋ}$
33 4 8 shscli ${⊢}{D}{+}_{ℋ}{S}\in {\mathbf{S}}_{ℋ}$
34 32 33 shincli ${⊢}\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\in {\mathbf{S}}_{ℋ}$
35 31 34 shscli ${⊢}\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right)\in {\mathbf{S}}_{ℋ}$
36 28 35 shincli ${⊢}\left(\left({A}{+}_{ℋ}{C}\right)\cap \left({B}{+}_{ℋ}{D}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right)\right)\in {\mathbf{S}}_{ℋ}$
37 1 5 shscli ${⊢}{A}{+}_{ℋ}{F}\in {\mathbf{S}}_{ℋ}$
38 2 6 shscli ${⊢}{B}{+}_{ℋ}{G}\in {\mathbf{S}}_{ℋ}$
39 37 38 shincli ${⊢}\left({A}{+}_{ℋ}{F}\right)\cap \left({B}{+}_{ℋ}{G}\right)\in {\mathbf{S}}_{ℋ}$
40 5 7 shscli ${⊢}{F}{+}_{ℋ}{R}\in {\mathbf{S}}_{ℋ}$
41 6 8 shscli ${⊢}{G}{+}_{ℋ}{S}\in {\mathbf{S}}_{ℋ}$
42 40 41 shincli ${⊢}\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\in {\mathbf{S}}_{ℋ}$
43 31 42 shscli ${⊢}\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\in {\mathbf{S}}_{ℋ}$
44 39 43 shincli ${⊢}\left(\left({A}{+}_{ℋ}{F}\right)\cap \left({B}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\in {\mathbf{S}}_{ℋ}$
45 3 5 shscli ${⊢}{C}{+}_{ℋ}{F}\in {\mathbf{S}}_{ℋ}$
46 4 6 shscli ${⊢}{D}{+}_{ℋ}{G}\in {\mathbf{S}}_{ℋ}$
47 45 46 shincli ${⊢}\left({C}{+}_{ℋ}{F}\right)\cap \left({D}{+}_{ℋ}{G}\right)\in {\mathbf{S}}_{ℋ}$
48 34 42 shscli ${⊢}\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\in {\mathbf{S}}_{ℋ}$
49 47 48 shincli ${⊢}\left(\left({C}{+}_{ℋ}{F}\right)\cap \left({D}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\in {\mathbf{S}}_{ℋ}$
50 44 49 shscli ${⊢}\left(\left(\left({A}{+}_{ℋ}{F}\right)\cap \left({B}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right){+}_{ℋ}\left(\left(\left({C}{+}_{ℋ}{F}\right)\cap \left({D}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right)\in {\mathbf{S}}_{ℋ}$
51 36 50 shincli ${⊢}\left(\left(\left({A}{+}_{ℋ}{C}\right)\cap \left({B}{+}_{ℋ}{D}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right)\right)\right)\cap \left(\left(\left(\left({A}{+}_{ℋ}{F}\right)\cap \left({B}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right){+}_{ℋ}\left(\left(\left({C}{+}_{ℋ}{F}\right)\cap \left({D}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right)\right)\in {\mathbf{S}}_{ℋ}$
52 1 2 3 51 5oalem1 ${⊢}\left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {h}={x}{+}_{ℎ}{y}\right)\wedge \left({z}\in {C}\wedge {x}{-}_{ℎ}{z}\in \left(\left(\left(\left({A}{+}_{ℋ}{C}\right)\cap \left({B}{+}_{ℋ}{D}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right)\right)\right)\cap \left(\left(\left(\left({A}{+}_{ℋ}{F}\right)\cap \left({B}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right){+}_{ℋ}\left(\left(\left({C}{+}_{ℋ}{F}\right)\cap \left({D}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right)\right)\right)\right)\right)\to {h}\in \left({B}{+}_{ℋ}\left({A}\cap \left({C}{+}_{ℋ}\left(\left(\left(\left({A}{+}_{ℋ}{C}\right)\cap \left({B}{+}_{ℋ}{D}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right)\right)\right)\cap \left(\left(\left(\left({A}{+}_{ℋ}{F}\right)\cap \left({B}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right){+}_{ℋ}\left(\left(\left({C}{+}_{ℋ}{F}\right)\cap \left({D}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right)\right)\right)\right)\right)\right)$
53 52 expr ${⊢}\left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {h}={x}{+}_{ℎ}{y}\right)\wedge {z}\in {C}\right)\to \left({x}{-}_{ℎ}{z}\in \left(\left(\left(\left({A}{+}_{ℋ}{C}\right)\cap \left({B}{+}_{ℋ}{D}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right)\right)\right)\cap \left(\left(\left(\left({A}{+}_{ℋ}{F}\right)\cap \left({B}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right){+}_{ℋ}\left(\left(\left({C}{+}_{ℋ}{F}\right)\cap \left({D}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right)\right)\right)\to {h}\in \left({B}{+}_{ℋ}\left({A}\cap \left({C}{+}_{ℋ}\left(\left(\left(\left({A}{+}_{ℋ}{C}\right)\cap \left({B}{+}_{ℋ}{D}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right)\right)\right)\cap \left(\left(\left(\left({A}{+}_{ℋ}{F}\right)\cap \left({B}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right){+}_{ℋ}\left(\left(\left({C}{+}_{ℋ}{F}\right)\cap \left({D}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$
54 53 adantrr ${⊢}\left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {h}={x}{+}_{ℎ}{y}\right)\wedge \left({z}\in {C}\wedge {w}\in {D}\right)\right)\to \left({x}{-}_{ℎ}{z}\in \left(\left(\left(\left({A}{+}_{ℋ}{C}\right)\cap \left({B}{+}_{ℋ}{D}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right)\right)\right)\cap \left(\left(\left(\left({A}{+}_{ℋ}{F}\right)\cap \left({B}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right){+}_{ℋ}\left(\left(\left({C}{+}_{ℋ}{F}\right)\cap \left({D}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right)\right)\right)\to {h}\in \left({B}{+}_{ℋ}\left({A}\cap \left({C}{+}_{ℋ}\left(\left(\left(\left({A}{+}_{ℋ}{C}\right)\cap \left({B}{+}_{ℋ}{D}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right)\right)\right)\cap \left(\left(\left(\left({A}{+}_{ℋ}{F}\right)\cap \left({B}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right){+}_{ℋ}\left(\left(\left({C}{+}_{ℋ}{F}\right)\cap \left({D}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$
55 54 adantrr ${⊢}\left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {h}={x}{+}_{ℎ}{y}\right)\wedge \left(\left({z}\in {C}\wedge {w}\in {D}\right)\wedge {h}={z}{+}_{ℎ}{w}\right)\right)\to \left({x}{-}_{ℎ}{z}\in \left(\left(\left(\left({A}{+}_{ℋ}{C}\right)\cap \left({B}{+}_{ℋ}{D}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right)\right)\right)\cap \left(\left(\left(\left({A}{+}_{ℋ}{F}\right)\cap \left({B}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right){+}_{ℋ}\left(\left(\left({C}{+}_{ℋ}{F}\right)\cap \left({D}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right)\right)\right)\to {h}\in \left({B}{+}_{ℋ}\left({A}\cap \left({C}{+}_{ℋ}\left(\left(\left(\left({A}{+}_{ℋ}{C}\right)\cap \left({B}{+}_{ℋ}{D}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right)\right)\right)\cap \left(\left(\left(\left({A}{+}_{ℋ}{F}\right)\cap \left({B}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right){+}_{ℋ}\left(\left(\left({C}{+}_{ℋ}{F}\right)\cap \left({D}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$
56 55 adantr ${⊢}\left(\left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {h}={x}{+}_{ℎ}{y}\right)\wedge \left(\left({z}\in {C}\wedge {w}\in {D}\right)\wedge {h}={z}{+}_{ℎ}{w}\right)\right)\wedge \left(\left(\left({f}\in {F}\wedge {g}\in {G}\right)\wedge {h}={f}{+}_{ℎ}{g}\right)\wedge \left(\left({v}\in {R}\wedge {u}\in {S}\right)\wedge {h}={v}{+}_{ℎ}{u}\right)\right)\right)\to \left({x}{-}_{ℎ}{z}\in \left(\left(\left(\left({A}{+}_{ℋ}{C}\right)\cap \left({B}{+}_{ℋ}{D}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right)\right)\right)\cap \left(\left(\left(\left({A}{+}_{ℋ}{F}\right)\cap \left({B}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right){+}_{ℋ}\left(\left(\left({C}{+}_{ℋ}{F}\right)\cap \left({D}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right)\right)\right)\to {h}\in \left({B}{+}_{ℋ}\left({A}\cap \left({C}{+}_{ℋ}\left(\left(\left(\left({A}{+}_{ℋ}{C}\right)\cap \left({B}{+}_{ℋ}{D}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right)\right)\right)\cap \left(\left(\left(\left({A}{+}_{ℋ}{F}\right)\cap \left({B}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right){+}_{ℋ}\left(\left(\left({C}{+}_{ℋ}{F}\right)\cap \left({D}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$
57 25 56 mpd ${⊢}\left(\left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {h}={x}{+}_{ℎ}{y}\right)\wedge \left(\left({z}\in {C}\wedge {w}\in {D}\right)\wedge {h}={z}{+}_{ℎ}{w}\right)\right)\wedge \left(\left(\left({f}\in {F}\wedge {g}\in {G}\right)\wedge {h}={f}{+}_{ℎ}{g}\right)\wedge \left(\left({v}\in {R}\wedge {u}\in {S}\right)\wedge {h}={v}{+}_{ℎ}{u}\right)\right)\right)\to {h}\in \left({B}{+}_{ℋ}\left({A}\cap \left({C}{+}_{ℋ}\left(\left(\left(\left({A}{+}_{ℋ}{C}\right)\cap \left({B}{+}_{ℋ}{D}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right)\right)\right)\cap \left(\left(\left(\left({A}{+}_{ℋ}{F}\right)\cap \left({B}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({A}{+}_{ℋ}{R}\right)\cap \left({B}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right){+}_{ℋ}\left(\left(\left({C}{+}_{ℋ}{F}\right)\cap \left({D}{+}_{ℋ}{G}\right)\right)\cap \left(\left(\left({C}{+}_{ℋ}{R}\right)\cap \left({D}{+}_{ℋ}{S}\right)\right){+}_{ℋ}\left(\left({F}{+}_{ℋ}{R}\right)\cap \left({G}{+}_{ℋ}{S}\right)\right)\right)\right)\right)\right)\right)\right)\right)$