Metamath Proof Explorer

Theorem 3oalem2

Description: Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses 3oalem1.1 ⊢ 𝐵 ∈ Cℋ
3oalem1.2 ⊢ 𝐶 ∈ Cℋ
3oalem1.3 ⊢ 𝑅 ∈ Cℋ
3oalem1.4 ⊢ 𝑆 ∈ Cℋ
Assertion 3oalem2 ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → 𝑣 ∈ ( 𝐵 +ℋ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 3oalem1.1 ⊢ 𝐵 ∈ Cℋ
2 3oalem1.2 ⊢ 𝐶 ∈ Cℋ
3 3oalem1.3 ⊢ 𝑅 ∈ Cℋ
4 3oalem1.4 ⊢ 𝑆 ∈ Cℋ
5 simplll ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → 𝑥 ∈ 𝐵 )
6 simpllr ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → 𝑦 ∈ 𝑅 )
7 1 2 3 4 3oalem1 ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑣 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) )
8 hvaddsub12 ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( 𝑦 +ℎ ( 𝑤 −ℎ 𝑤 ) ) = ( 𝑤 +ℎ ( 𝑦 −ℎ 𝑤 ) ) )
9 8 3anidm23 ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( 𝑦 +ℎ ( 𝑤 −ℎ 𝑤 ) ) = ( 𝑤 +ℎ ( 𝑦 −ℎ 𝑤 ) ) )
10 hvsubid ⊢ ( 𝑤 ∈ ℋ → ( 𝑤 −ℎ 𝑤 ) = 0ℎ )
11 10 oveq2d ⊢ ( 𝑤 ∈ ℋ → ( 𝑦 +ℎ ( 𝑤 −ℎ 𝑤 ) ) = ( 𝑦 +ℎ 0ℎ ) )
12 ax-hvaddid ⊢ ( 𝑦 ∈ ℋ → ( 𝑦 +ℎ 0ℎ ) = 𝑦 )
13 11 12 sylan9eqr ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( 𝑦 +ℎ ( 𝑤 −ℎ 𝑤 ) ) = 𝑦 )
14 9 13 eqtr3d ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( 𝑤 +ℎ ( 𝑦 −ℎ 𝑤 ) ) = 𝑦 )
15 14 ad2ant2l ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( 𝑤 +ℎ ( 𝑦 −ℎ 𝑤 ) ) = 𝑦 )
16 15 adantlr ⊢ ( ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑣 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( 𝑤 +ℎ ( 𝑦 −ℎ 𝑤 ) ) = 𝑦 )
17 7 16 syl ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → ( 𝑤 +ℎ ( 𝑦 −ℎ 𝑤 ) ) = 𝑦 )
18 simprlr ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → 𝑤 ∈ 𝑆 )
19 eqtr2 ⊢ ( ( 𝑣 = ( 𝑥 +ℎ 𝑦 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) → ( 𝑥 +ℎ 𝑦 ) = ( 𝑧 +ℎ 𝑤 ) )
20 19 oveq1d ⊢ ( ( 𝑣 = ( 𝑥 +ℎ 𝑦 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) → ( ( 𝑥 +ℎ 𝑦 ) −ℎ ( 𝑥 +ℎ 𝑤 ) ) = ( ( 𝑧 +ℎ 𝑤 ) −ℎ ( 𝑥 +ℎ 𝑤 ) ) )
21 20 ad2ant2l ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → ( ( 𝑥 +ℎ 𝑦 ) −ℎ ( 𝑥 +ℎ 𝑤 ) ) = ( ( 𝑧 +ℎ 𝑤 ) −ℎ ( 𝑥 +ℎ 𝑤 ) ) )
22 simpl ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → 𝑥 ∈ ℋ )
23 22 anim1i ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( 𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ ) )
24 hvsub4 ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑥 +ℎ 𝑦 ) −ℎ ( 𝑥 +ℎ 𝑤 ) ) = ( ( 𝑥 −ℎ 𝑥 ) +ℎ ( 𝑦 −ℎ 𝑤 ) ) )
25 23 24 syldan ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ( 𝑥 +ℎ 𝑦 ) −ℎ ( 𝑥 +ℎ 𝑤 ) ) = ( ( 𝑥 −ℎ 𝑥 ) +ℎ ( 𝑦 −ℎ 𝑤 ) ) )
26 hvsubid ⊢ ( 𝑥 ∈ ℋ → ( 𝑥 −ℎ 𝑥 ) = 0ℎ )
27 26 ad2antrr ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( 𝑥 −ℎ 𝑥 ) = 0ℎ )
28 27 oveq1d ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ( 𝑥 −ℎ 𝑥 ) +ℎ ( 𝑦 −ℎ 𝑤 ) ) = ( 0ℎ +ℎ ( 𝑦 −ℎ 𝑤 ) ) )
29 hvsubcl ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( 𝑦 −ℎ 𝑤 ) ∈ ℋ )
30 hvaddlid ⊢ ( ( 𝑦 −ℎ 𝑤 ) ∈ ℋ → ( 0ℎ +ℎ ( 𝑦 −ℎ 𝑤 ) ) = ( 𝑦 −ℎ 𝑤 ) )
31 29 30 syl ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( 0ℎ +ℎ ( 𝑦 −ℎ 𝑤 ) ) = ( 𝑦 −ℎ 𝑤 ) )
32 31 adantll ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( 0ℎ +ℎ ( 𝑦 −ℎ 𝑤 ) ) = ( 𝑦 −ℎ 𝑤 ) )
33 25 28 32 3eqtrd ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ( 𝑥 +ℎ 𝑦 ) −ℎ ( 𝑥 +ℎ 𝑤 ) ) = ( 𝑦 −ℎ 𝑤 ) )
34 33 ad2ant2rl ⊢ ( ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑣 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑥 +ℎ 𝑦 ) −ℎ ( 𝑥 +ℎ 𝑤 ) ) = ( 𝑦 −ℎ 𝑤 ) )
35 7 34 syl ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → ( ( 𝑥 +ℎ 𝑦 ) −ℎ ( 𝑥 +ℎ 𝑤 ) ) = ( 𝑦 −ℎ 𝑤 ) )
36 simpr ⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) )
37 simpr ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → 𝑤 ∈ ℋ )
38 37 anim2i ⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( 𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ ) )
39 hvsub4 ⊢ ( ( ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ∧ ( 𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑧 +ℎ 𝑤 ) −ℎ ( 𝑥 +ℎ 𝑤 ) ) = ( ( 𝑧 −ℎ 𝑥 ) +ℎ ( 𝑤 −ℎ 𝑤 ) ) )
40 36 38 39 syl2anc ⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑧 +ℎ 𝑤 ) −ℎ ( 𝑥 +ℎ 𝑤 ) ) = ( ( 𝑧 −ℎ 𝑥 ) +ℎ ( 𝑤 −ℎ 𝑤 ) ) )
41 10 ad2antll ⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( 𝑤 −ℎ 𝑤 ) = 0ℎ )
42 41 oveq2d ⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑧 −ℎ 𝑥 ) +ℎ ( 𝑤 −ℎ 𝑤 ) ) = ( ( 𝑧 −ℎ 𝑥 ) +ℎ 0ℎ ) )
43 hvsubcl ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑧 −ℎ 𝑥 ) ∈ ℋ )
44 ax-hvaddid ⊢ ( ( 𝑧 −ℎ 𝑥 ) ∈ ℋ → ( ( 𝑧 −ℎ 𝑥 ) +ℎ 0ℎ ) = ( 𝑧 −ℎ 𝑥 ) )
45 43 44 syl ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑧 −ℎ 𝑥 ) +ℎ 0ℎ ) = ( 𝑧 −ℎ 𝑥 ) )
46 45 ancoms ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑧 −ℎ 𝑥 ) +ℎ 0ℎ ) = ( 𝑧 −ℎ 𝑥 ) )
47 46 adantrr ⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑧 −ℎ 𝑥 ) +ℎ 0ℎ ) = ( 𝑧 −ℎ 𝑥 ) )
48 40 42 47 3eqtrd ⊢ ( ( 𝑥 ∈ ℋ ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑧 +ℎ 𝑤 ) −ℎ ( 𝑥 +ℎ 𝑤 ) ) = ( 𝑧 −ℎ 𝑥 ) )
49 48 adantlr ⊢ ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑧 +ℎ 𝑤 ) −ℎ ( 𝑥 +ℎ 𝑤 ) ) = ( 𝑧 −ℎ 𝑥 ) )
50 49 adantlr ⊢ ( ( ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑣 ∈ ℋ ) ∧ ( 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑧 +ℎ 𝑤 ) −ℎ ( 𝑥 +ℎ 𝑤 ) ) = ( 𝑧 −ℎ 𝑥 ) )
51 7 50 syl ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → ( ( 𝑧 +ℎ 𝑤 ) −ℎ ( 𝑥 +ℎ 𝑤 ) ) = ( 𝑧 −ℎ 𝑥 ) )
52 21 35 51 3eqtr3d ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → ( 𝑦 −ℎ 𝑤 ) = ( 𝑧 −ℎ 𝑥 ) )
53 simpll ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) → 𝑥 ∈ 𝐵 )
54 simpll ⊢ ( ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) → 𝑧 ∈ 𝐶 )
55 2 chshii ⊢ 𝐶 ∈ Sℋ
56 1 chshii ⊢ 𝐵 ∈ Sℋ
57 55 56 shsvsi ⊢ ( ( 𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑧 −ℎ 𝑥 ) ∈ ( 𝐶 +ℋ 𝐵 ) )
58 57 ancoms ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑧 −ℎ 𝑥 ) ∈ ( 𝐶 +ℋ 𝐵 ) )
59 56 55 shscomi ⊢ ( 𝐵 +ℋ 𝐶 ) = ( 𝐶 +ℋ 𝐵 )
60 58 59 eleqtrrdi ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑧 −ℎ 𝑥 ) ∈ ( 𝐵 +ℋ 𝐶 ) )
61 53 54 60 syl2an ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → ( 𝑧 −ℎ 𝑥 ) ∈ ( 𝐵 +ℋ 𝐶 ) )
62 52 61 eqeltrd ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → ( 𝑦 −ℎ 𝑤 ) ∈ ( 𝐵 +ℋ 𝐶 ) )
63 simplr ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) → 𝑦 ∈ 𝑅 )
64 simplr ⊢ ( ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) → 𝑤 ∈ 𝑆 )
65 3 chshii ⊢ 𝑅 ∈ Sℋ
66 4 chshii ⊢ 𝑆 ∈ Sℋ
67 65 66 shsvsi ⊢ ( ( 𝑦 ∈ 𝑅 ∧ 𝑤 ∈ 𝑆 ) → ( 𝑦 −ℎ 𝑤 ) ∈ ( 𝑅 +ℋ 𝑆 ) )
68 63 64 67 syl2an ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → ( 𝑦 −ℎ 𝑤 ) ∈ ( 𝑅 +ℋ 𝑆 ) )
69 62 68 elind ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → ( 𝑦 −ℎ 𝑤 ) ∈ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) )
70 56 55 shscli ⊢ ( 𝐵 +ℋ 𝐶 ) ∈ Sℋ
71 65 66 shscli ⊢ ( 𝑅 +ℋ 𝑆 ) ∈ Sℋ
72 70 71 shincli ⊢ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ∈ Sℋ
73 66 72 shsvai ⊢ ( ( 𝑤 ∈ 𝑆 ∧ ( 𝑦 −ℎ 𝑤 ) ∈ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) → ( 𝑤 +ℎ ( 𝑦 −ℎ 𝑤 ) ) ∈ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) )
74 18 69 73 syl2anc ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → ( 𝑤 +ℎ ( 𝑦 −ℎ 𝑤 ) ) ∈ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) )
75 17 74 eqeltrrd ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → 𝑦 ∈ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) )
76 6 75 elind ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → 𝑦 ∈ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) )
77 66 72 shscli ⊢ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ∈ Sℋ
78 65 77 shincli ⊢ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ∈ Sℋ
79 56 78 shsvai ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ) → ( 𝑥 +ℎ 𝑦 ) ∈ ( 𝐵 +ℋ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ) )
80 5 76 79 syl2anc ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → ( 𝑥 +ℎ 𝑦 ) ∈ ( 𝐵 +ℋ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ) )
81 eleq1 ⊢ ( 𝑣 = ( 𝑥 +ℎ 𝑦 ) → ( 𝑣 ∈ ( 𝐵 +ℋ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ) ↔ ( 𝑥 +ℎ 𝑦 ) ∈ ( 𝐵 +ℋ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ) ) )
82 81 ad2antlr ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → ( 𝑣 ∈ ( 𝐵 +ℋ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ) ↔ ( 𝑥 +ℎ 𝑦 ) ∈ ( 𝐵 +ℋ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ) ) )
83 80 82 mpbird ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅 ) ∧ 𝑣 = ( 𝑥 +ℎ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑣 = ( 𝑧 +ℎ 𝑤 ) ) ) → 𝑣 ∈ ( 𝐵 +ℋ ( 𝑅 ∩ ( 𝑆 +ℋ ( ( 𝐵 +ℋ 𝐶 ) ∩ ( 𝑅 +ℋ 𝑆 ) ) ) ) ) )