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 ⊢ 𝐴 ∈ Sℋ
5oalem5.2 ⊢ 𝐵 ∈ Sℋ
5oalem5.3 ⊢ 𝐶 ∈ Sℋ
5oalem5.4 ⊢ 𝐷 ∈ Sℋ
5oalem5.5 ⊢ 𝐹 ∈ Sℋ
5oalem5.6 ⊢ 𝐺 ∈ Sℋ
5oalem5.7 ⊢ 𝑅 ∈ Sℋ
5oalem5.8 ⊢ 𝑆 ∈ Sℋ
Assertion 5oalem6 ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) → ℎ ∈ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 5oalem5.1 ⊢ 𝐴 ∈ Sℋ
2 5oalem5.2 ⊢ 𝐵 ∈ Sℋ
3 5oalem5.3 ⊢ 𝐶 ∈ Sℋ
4 5oalem5.4 ⊢ 𝐷 ∈ Sℋ
5 5oalem5.5 ⊢ 𝐹 ∈ Sℋ
6 5oalem5.6 ⊢ 𝐺 ∈ Sℋ
7 5oalem5.7 ⊢ 𝑅 ∈ Sℋ
8 5oalem5.8 ⊢ 𝑆 ∈ Sℋ
9 an4 ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ↔ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( ℎ = ( 𝑥 +ℎ 𝑦 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) )
10 an4 ⊢ ( ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ↔ ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ∧ ( ℎ = ( 𝑓 +ℎ 𝑔 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) )
11 eqeq1 ⊢ ( ℎ = ( 𝑥 +ℎ 𝑦 ) → ( ℎ = ( 𝑣 +ℎ 𝑢 ) ↔ ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ) )
12 11 biimpcd ⊢ ( ℎ = ( 𝑣 +ℎ 𝑢 ) → ( ℎ = ( 𝑥 +ℎ 𝑦 ) → ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ) )
13 eqeq1 ⊢ ( ℎ = ( 𝑧 +ℎ 𝑤 ) → ( ℎ = ( 𝑣 +ℎ 𝑢 ) ↔ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) )
14 13 biimpcd ⊢ ( ℎ = ( 𝑣 +ℎ 𝑢 ) → ( ℎ = ( 𝑧 +ℎ 𝑤 ) → ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) )
15 12 14 anim12d ⊢ ( ℎ = ( 𝑣 +ℎ 𝑢 ) → ( ( ℎ = ( 𝑥 +ℎ 𝑦 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) → ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) ) )
16 eqeq1 ⊢ ( ℎ = ( 𝑓 +ℎ 𝑔 ) → ( ℎ = ( 𝑣 +ℎ 𝑢 ) ↔ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) )
17 16 biimpcd ⊢ ( ℎ = ( 𝑣 +ℎ 𝑢 ) → ( ℎ = ( 𝑓 +ℎ 𝑔 ) → ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) )
18 15 17 anim12d ⊢ ( ℎ = ( 𝑣 +ℎ 𝑢 ) → ( ( ( ℎ = ( 𝑥 +ℎ 𝑦 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) → ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) ) )
19 18 expdcom ⊢ ( ( ℎ = ( 𝑥 +ℎ 𝑦 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) → ( ℎ = ( 𝑓 +ℎ 𝑔 ) → ( ℎ = ( 𝑣 +ℎ 𝑢 ) → ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) ) ) )
20 19 imp32 ⊢ ( ( ( ℎ = ( 𝑥 +ℎ 𝑦 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ∧ ( ℎ = ( 𝑓 +ℎ 𝑔 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) → ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) )
21 20 anim2i ⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ) ∧ ( ( ℎ = ( 𝑥 +ℎ 𝑦 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ∧ ( ℎ = ( 𝑓 +ℎ 𝑔 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) → ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ) ∧ ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) ) )
22 21 an4s ⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( ℎ = ( 𝑥 +ℎ 𝑦 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ∧ ( ℎ = ( 𝑓 +ℎ 𝑔 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) → ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ) ∧ ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) ) )
23 9 10 22 syl2anb ⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) → ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ) ∧ ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) ) )
24 1 2 3 4 5 6 7 8 5oalem5 ⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ) ) ∧ ( ( ( 𝑥 +ℎ 𝑦 ) = ( 𝑣 +ℎ 𝑢 ) ∧ ( 𝑧 +ℎ 𝑤 ) = ( 𝑣 +ℎ 𝑢 ) ) ∧ ( 𝑓 +ℎ 𝑔 ) = ( 𝑣 +ℎ 𝑢 ) ) ) → ( 𝑥 −ℎ 𝑧 ) ∈ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) )
25 23 24 syl ⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) → ( 𝑥 −ℎ 𝑧 ) ∈ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) )
26 1 3 shscli ⊢ ( 𝐴 +ℋ 𝐶 ) ∈ Sℋ
27 2 4 shscli ⊢ ( 𝐵 +ℋ 𝐷 ) ∈ Sℋ
28 26 27 shincli ⊢ ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∈ Sℋ
29 1 7 shscli ⊢ ( 𝐴 +ℋ 𝑅 ) ∈ Sℋ
30 2 8 shscli ⊢ ( 𝐵 +ℋ 𝑆 ) ∈ Sℋ
31 29 30 shincli ⊢ ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) ∈ Sℋ
32 3 7 shscli ⊢ ( 𝐶 +ℋ 𝑅 ) ∈ Sℋ
33 4 8 shscli ⊢ ( 𝐷 +ℋ 𝑆 ) ∈ Sℋ
34 32 33 shincli ⊢ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ∈ Sℋ
35 31 34 shscli ⊢ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ∈ Sℋ
36 28 35 shincli ⊢ ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∈ Sℋ
37 1 5 shscli ⊢ ( 𝐴 +ℋ 𝐹 ) ∈ Sℋ
38 2 6 shscli ⊢ ( 𝐵 +ℋ 𝐺 ) ∈ Sℋ
39 37 38 shincli ⊢ ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∈ Sℋ
40 5 7 shscli ⊢ ( 𝐹 +ℋ 𝑅 ) ∈ Sℋ
41 6 8 shscli ⊢ ( 𝐺 +ℋ 𝑆 ) ∈ Sℋ
42 40 41 shincli ⊢ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ∈ Sℋ
43 31 42 shscli ⊢ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ∈ Sℋ
44 39 43 shincli ⊢ ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ∈ Sℋ
45 3 5 shscli ⊢ ( 𝐶 +ℋ 𝐹 ) ∈ Sℋ
46 4 6 shscli ⊢ ( 𝐷 +ℋ 𝐺 ) ∈ Sℋ
47 45 46 shincli ⊢ ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∈ Sℋ
48 34 42 shscli ⊢ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ∈ Sℋ
49 47 48 shincli ⊢ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ∈ Sℋ
50 44 49 shscli ⊢ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ∈ Sℋ
51 36 50 shincli ⊢ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ∈ Sℋ
52 1 2 3 51 5oalem1 ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ ( 𝑥 −ℎ 𝑧 ) ∈ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) → ℎ ∈ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) ) )
53 52 expr ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ 𝑧 ∈ 𝐶 ) → ( ( 𝑥 −ℎ 𝑧 ) ∈ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) → ℎ ∈ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) ) ) )
54 53 adantrr ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ) → ( ( 𝑥 −ℎ 𝑧 ) ∈ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) → ℎ ∈ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) ) ) )
55 54 adantrr ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) → ( ( 𝑥 −ℎ 𝑧 ) ∈ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) → ℎ ∈ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) ) ) )
56 55 adantr ⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) → ( ( 𝑥 −ℎ 𝑧 ) ∈ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) → ℎ ∈ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) ) ) )
57 25 56 mpd ⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ℎ = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷 ) ∧ ℎ = ( 𝑧 +ℎ 𝑤 ) ) ) ∧ ( ( ( 𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺 ) ∧ ℎ = ( 𝑓 +ℎ 𝑔 ) ) ∧ ( ( 𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆 ) ∧ ℎ = ( 𝑣 +ℎ 𝑢 ) ) ) ) → ℎ ∈ ( 𝐵 +ℋ ( 𝐴 ∩ ( 𝐶 +ℋ ( ( ( ( 𝐴 +ℋ 𝐶 ) ∩ ( 𝐵 +ℋ 𝐷 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) ) ) ∩ ( ( ( ( 𝐴 +ℋ 𝐹 ) ∩ ( 𝐵 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐴 +ℋ 𝑅 ) ∩ ( 𝐵 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) +ℋ ( ( ( 𝐶 +ℋ 𝐹 ) ∩ ( 𝐷 +ℋ 𝐺 ) ) ∩ ( ( ( 𝐶 +ℋ 𝑅 ) ∩ ( 𝐷 +ℋ 𝑆 ) ) +ℋ ( ( 𝐹 +ℋ 𝑅 ) ∩ ( 𝐺 +ℋ 𝑆 ) ) ) ) ) ) ) ) ) )