Metamath Proof Explorer

Theorem mayete3i

Description: Mayet's equation E_3. Part of Theorem 4.1 of Mayet3 p. 1223. (Contributed by NM, 22-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses mayete3.a ⊢ 𝐴 ∈ Cℋ
mayete3.b ⊢ 𝐵 ∈ Cℋ
mayete3.c ⊢ 𝐶 ∈ Cℋ
mayete3.d ⊢ 𝐷 ∈ Cℋ
mayete3.f ⊢ 𝐹 ∈ Cℋ
mayete3.g ⊢ 𝐺 ∈ Cℋ
mayete3.ac ⊢ 𝐴 ⊆ ( ⊥ ‘ 𝐶 )
mayete3.af ⊢ 𝐴 ⊆ ( ⊥ ‘ 𝐹 )
mayete3.cf ⊢ 𝐶 ⊆ ( ⊥ ‘ 𝐹 )
mayete3.ab ⊢ 𝐴 ⊆ ( ⊥ ‘ 𝐵 )
mayete3.cd ⊢ 𝐶 ⊆ ( ⊥ ‘ 𝐷 )
mayete3.fg ⊢ 𝐹 ⊆ ( ⊥ ‘ 𝐺 )
mayete3.x ⊢ 𝑋 = ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 )
mayete3.y ⊢ 𝑌 = ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ∩ ( 𝐹 ∨ℋ 𝐺 ) )
mayete3.z ⊢ 𝑍 = ( ( 𝐵 ∨ℋ 𝐷 ) ∨ℋ 𝐺 )
Assertion mayete3i ( 𝑋 ∩ 𝑌 ) ⊆ 𝑍

Proof

Step Hyp Ref Expression
1 mayete3.a ⊢ 𝐴 ∈ Cℋ
2 mayete3.b ⊢ 𝐵 ∈ Cℋ
3 mayete3.c ⊢ 𝐶 ∈ Cℋ
4 mayete3.d ⊢ 𝐷 ∈ Cℋ
5 mayete3.f ⊢ 𝐹 ∈ Cℋ
6 mayete3.g ⊢ 𝐺 ∈ Cℋ
7 mayete3.ac ⊢ 𝐴 ⊆ ( ⊥ ‘ 𝐶 )
8 mayete3.af ⊢ 𝐴 ⊆ ( ⊥ ‘ 𝐹 )
9 mayete3.cf ⊢ 𝐶 ⊆ ( ⊥ ‘ 𝐹 )
10 mayete3.ab ⊢ 𝐴 ⊆ ( ⊥ ‘ 𝐵 )
11 mayete3.cd ⊢ 𝐶 ⊆ ( ⊥ ‘ 𝐷 )
12 mayete3.fg ⊢ 𝐹 ⊆ ( ⊥ ‘ 𝐺 )
13 mayete3.x ⊢ 𝑋 = ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 )
14 mayete3.y ⊢ 𝑌 = ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ∩ ( 𝐹 ∨ℋ 𝐺 ) )
15 mayete3.z ⊢ 𝑍 = ( ( 𝐵 ∨ℋ 𝐷 ) ∨ℋ 𝐺 )
16 elin ⊢ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑌 ) )
17 1 3 chjcli ⊢ ( 𝐴 ∨ℋ 𝐶 ) ∈ Cℋ
18 17 5 chjcli ⊢ ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ∈ Cℋ
19 18 cheli ⊢ ( 𝑥 ∈ ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) → 𝑥 ∈ ℋ )
20 19 13 eleq2s ⊢ ( 𝑥 ∈ 𝑋 → 𝑥 ∈ ℋ )
21 20 adantr ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ ℋ )
22 16 21 sylbi ⊢ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) → 𝑥 ∈ ℋ )
23 ax-hvmulid ⊢ ( 𝑥 ∈ ℋ → ( 1 ·ℎ 𝑥 ) = 𝑥 )
24 2cn ⊢ 2 ∈ ℂ
25 2ne0 ⊢ 2 ≠ 0
26 recid2 ⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 1 / 2 ) · 2 ) = 1 )
27 24 25 26 mp2an ⊢ ( ( 1 / 2 ) · 2 ) = 1
28 27 oveq1i ⊢ ( ( ( 1 / 2 ) · 2 ) ·ℎ 𝑥 ) = ( 1 ·ℎ 𝑥 )
29 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
30 ax-hvmulass ⊢ ( ( ( 1 / 2 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( ( ( 1 / 2 ) · 2 ) ·ℎ 𝑥 ) = ( ( 1 / 2 ) ·ℎ ( 2 ·ℎ 𝑥 ) ) )
31 29 24 30 mp3an12 ⊢ ( 𝑥 ∈ ℋ → ( ( ( 1 / 2 ) · 2 ) ·ℎ 𝑥 ) = ( ( 1 / 2 ) ·ℎ ( 2 ·ℎ 𝑥 ) ) )
32 28 31 syl5eqr ⊢ ( 𝑥 ∈ ℋ → ( 1 ·ℎ 𝑥 ) = ( ( 1 / 2 ) ·ℎ ( 2 ·ℎ 𝑥 ) ) )
33 23 32 eqtr3d ⊢ ( 𝑥 ∈ ℋ → 𝑥 = ( ( 1 / 2 ) ·ℎ ( 2 ·ℎ 𝑥 ) ) )
34 22 33 syl ⊢ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) → 𝑥 = ( ( 1 / 2 ) ·ℎ ( 2 ·ℎ 𝑥 ) ) )
35 hv2times ⊢ ( 𝑥 ∈ ℋ → ( 2 ·ℎ 𝑥 ) = ( 𝑥 +ℎ 𝑥 ) )
36 35 oveq1d ⊢ ( 𝑥 ∈ ℋ → ( ( 2 ·ℎ 𝑥 ) +ℎ 𝑥 ) = ( ( 𝑥 +ℎ 𝑥 ) +ℎ 𝑥 ) )
37 22 36 syl ⊢ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) → ( ( 2 ·ℎ 𝑥 ) +ℎ 𝑥 ) = ( ( 𝑥 +ℎ 𝑥 ) +ℎ 𝑥 ) )
38 inss2 ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑌
39 38 sseli ⊢ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) → 𝑥 ∈ 𝑌 )
40 14 elin2 ⊢ ( 𝑥 ∈ 𝑌 ↔ ( 𝑥 ∈ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ∧ 𝑥 ∈ ( 𝐹 ∨ℋ 𝐺 ) ) )
41 elin ⊢ ( 𝑥 ∈ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ↔ ( 𝑥 ∈ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝑥 ∈ ( 𝐶 ∨ℋ 𝐷 ) ) )
42 1 2 pjdsi ⊢ ( ( 𝑥 ∈ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐴 ⊆ ( ⊥ ‘ 𝐵 ) ) → 𝑥 = ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) ) )
43 10 42 mpan2 ⊢ ( 𝑥 ∈ ( 𝐴 ∨ℋ 𝐵 ) → 𝑥 = ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) ) )
44 3 4 pjdsi ⊢ ( ( 𝑥 ∈ ( 𝐶 ∨ℋ 𝐷 ) ∧ 𝐶 ⊆ ( ⊥ ‘ 𝐷 ) ) → 𝑥 = ( ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) )
45 11 44 mpan2 ⊢ ( 𝑥 ∈ ( 𝐶 ∨ℋ 𝐷 ) → 𝑥 = ( ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) )
46 43 45 oveqan12d ⊢ ( ( 𝑥 ∈ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝑥 ∈ ( 𝐶 ∨ℋ 𝐷 ) ) → ( 𝑥 +ℎ 𝑥 ) = ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) ) +ℎ ( ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) ) )
47 41 46 sylbi ⊢ ( 𝑥 ∈ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) → ( 𝑥 +ℎ 𝑥 ) = ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) ) +ℎ ( ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) ) )
48 inss1 ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 )
49 48 sseli ⊢ ( 𝑥 ∈ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) → 𝑥 ∈ ( 𝐴 ∨ℋ 𝐵 ) )
50 1 2 chjcli ⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ
51 50 cheli ⊢ ( 𝑥 ∈ ( 𝐴 ∨ℋ 𝐵 ) → 𝑥 ∈ ℋ )
52 1 pjhcli ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) ∈ ℋ )
53 2 pjhcli ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) ∈ ℋ )
54 3 pjhcli ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ∈ ℋ )
55 4 pjhcli ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ∈ ℋ )
56 hvadd4 ⊢ ( ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) ∈ ℋ ∧ ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) ∈ ℋ ) ∧ ( ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ∈ ℋ ∧ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ∈ ℋ ) ) → ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) ) +ℎ ( ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) ) = ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) ) )
57 52 53 54 55 56 syl22anc ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) ) +ℎ ( ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) ) = ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) ) )
58 49 51 57 3syl ⊢ ( 𝑥 ∈ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) → ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) ) +ℎ ( ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) ) = ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) ) )
59 47 58 eqtrd ⊢ ( 𝑥 ∈ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) → ( 𝑥 +ℎ 𝑥 ) = ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) ) )
60 5 6 pjdsi ⊢ ( ( 𝑥 ∈ ( 𝐹 ∨ℋ 𝐺 ) ∧ 𝐹 ⊆ ( ⊥ ‘ 𝐺 ) ) → 𝑥 = ( ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) )
61 12 60 mpan2 ⊢ ( 𝑥 ∈ ( 𝐹 ∨ℋ 𝐺 ) → 𝑥 = ( ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) )
62 59 61 oveqan12d ⊢ ( ( 𝑥 ∈ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐶 ∨ℋ 𝐷 ) ) ∧ 𝑥 ∈ ( 𝐹 ∨ℋ 𝐺 ) ) → ( ( 𝑥 +ℎ 𝑥 ) +ℎ 𝑥 ) = ( ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) ) +ℎ ( ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ) )
63 40 62 sylbi ⊢ ( 𝑥 ∈ 𝑌 → ( ( 𝑥 +ℎ 𝑥 ) +ℎ 𝑥 ) = ( ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) ) +ℎ ( ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ) )
64 39 63 syl ⊢ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) → ( ( 𝑥 +ℎ 𝑥 ) +ℎ 𝑥 ) = ( ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) ) +ℎ ( ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ) )
65 hvaddcl ⊢ ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) ∈ ℋ ∧ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ∈ ℋ ) → ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) ∈ ℋ )
66 52 54 65 syl2anc ⊢ ( 𝑥 ∈ ℋ → ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) ∈ ℋ )
67 hvaddcl ⊢ ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) ∈ ℋ ∧ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ∈ ℋ ) → ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) ∈ ℋ )
68 53 55 67 syl2anc ⊢ ( 𝑥 ∈ ℋ → ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) ∈ ℋ )
69 5 pjhcli ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ∈ ℋ )
70 6 pjhcli ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℋ )
71 hvadd4 ⊢ ( ( ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) ∈ ℋ ∧ ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) ∈ ℋ ) ∧ ( ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ∈ ℋ ∧ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℋ ) ) → ( ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) ) +ℎ ( ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ) = ( ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ) +ℎ ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ) )
72 66 68 69 70 71 syl22anc ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) ) +ℎ ( ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ) = ( ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ) +ℎ ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ) )
73 22 72 syl ⊢ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) → ( ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) ) +ℎ ( ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ) = ( ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ) +ℎ ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ) )
74 37 64 73 3eqtrd ⊢ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) → ( ( 2 ·ℎ 𝑥 ) +ℎ 𝑥 ) = ( ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ) +ℎ ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ) )
75 inss1 ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑋
76 75 sseli ⊢ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) → 𝑥 ∈ 𝑋 )
77 76 13 eleqtrdi ⊢ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) → 𝑥 ∈ ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) )
78 1 3 5 pjds3i ⊢ ( ( ( 𝑥 ∈ ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ∧ 𝐴 ⊆ ( ⊥ ‘ 𝐶 ) ) ∧ ( 𝐴 ⊆ ( ⊥ ‘ 𝐹 ) ∧ 𝐶 ⊆ ( ⊥ ‘ 𝐹 ) ) ) → 𝑥 = ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ) )
79 8 9 78 mpanr12 ⊢ ( ( 𝑥 ∈ ( ( 𝐴 ∨ℋ 𝐶 ) ∨ℋ 𝐹 ) ∧ 𝐴 ⊆ ( ⊥ ‘ 𝐶 ) ) → 𝑥 = ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ) )
80 77 7 79 sylancl ⊢ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) → 𝑥 = ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ) )
81 74 80 oveq12d ⊢ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) → ( ( ( 2 ·ℎ 𝑥 ) +ℎ 𝑥 ) −ℎ 𝑥 ) = ( ( ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ) +ℎ ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ) −ℎ ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
82 hvmulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( 2 ·ℎ 𝑥 ) ∈ ℋ )
83 24 82 mpan ⊢ ( 𝑥 ∈ ℋ → ( 2 ·ℎ 𝑥 ) ∈ ℋ )
84 hvpncan ⊢ ( ( ( 2 ·ℎ 𝑥 ) ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( 2 ·ℎ 𝑥 ) +ℎ 𝑥 ) −ℎ 𝑥 ) = ( 2 ·ℎ 𝑥 ) )
85 83 84 mpancom ⊢ ( 𝑥 ∈ ℋ → ( ( ( 2 ·ℎ 𝑥 ) +ℎ 𝑥 ) −ℎ 𝑥 ) = ( 2 ·ℎ 𝑥 ) )
86 22 85 syl ⊢ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) → ( ( ( 2 ·ℎ 𝑥 ) +ℎ 𝑥 ) −ℎ 𝑥 ) = ( 2 ·ℎ 𝑥 ) )
87 81 86 eqtr3d ⊢ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) → ( ( ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ) +ℎ ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ) −ℎ ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ) ) = ( 2 ·ℎ 𝑥 ) )
88 hvaddcl ⊢ ( ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) ∈ ℋ ∧ ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ∈ ℋ ) → ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ) ∈ ℋ )
89 66 69 88 syl2anc ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ) ∈ ℋ )
90 hvaddcl ⊢ ( ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) ∈ ℋ ∧ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℋ ) → ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ∈ ℋ )
91 68 70 90 syl2anc ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ∈ ℋ )
92 hvpncan2 ⊢ ( ( ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ) ∈ ℋ ∧ ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ∈ ℋ ) → ( ( ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ) +ℎ ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ) −ℎ ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ) ) = ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) )
93 89 91 92 syl2anc ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ) +ℎ ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ) −ℎ ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ) ) = ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) )
94 22 93 syl ⊢ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) → ( ( ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ) +ℎ ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ) −ℎ ( ( ( ( projℎ ‘ 𝐴 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐶 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐹 ) ‘ 𝑥 ) ) ) = ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) )
95 87 94 eqtr3d ⊢ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) → ( 2 ·ℎ 𝑥 ) = ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) )
96 2 pjcli ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) ∈ 𝐵 )
97 4 pjcli ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ∈ 𝐷 )
98 2 chshii ⊢ 𝐵 ∈ Sℋ
99 4 chshii ⊢ 𝐷 ∈ Sℋ
100 98 99 shsvai ⊢ ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) ∈ 𝐵 ∧ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ∈ 𝐷 ) → ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) ∈ ( 𝐵 +ℋ 𝐷 ) )
101 96 97 100 syl2anc ⊢ ( 𝑥 ∈ ℋ → ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) ∈ ( 𝐵 +ℋ 𝐷 ) )
102 6 pjcli ⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐺 )
103 98 99 shscli ⊢ ( 𝐵 +ℋ 𝐷 ) ∈ Sℋ
104 6 chshii ⊢ 𝐺 ∈ Sℋ
105 103 104 shsvai ⊢ ( ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) ∈ ( 𝐵 +ℋ 𝐷 ) ∧ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐺 ) → ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ∈ ( ( 𝐵 +ℋ 𝐷 ) +ℋ 𝐺 ) )
106 101 102 105 syl2anc ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ∈ ( ( 𝐵 +ℋ 𝐷 ) +ℋ 𝐺 ) )
107 22 106 syl ⊢ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) → ( ( ( ( projℎ ‘ 𝐵 ) ‘ 𝑥 ) +ℎ ( ( projℎ ‘ 𝐷 ) ‘ 𝑥 ) ) +ℎ ( ( projℎ ‘ 𝐺 ) ‘ 𝑥 ) ) ∈ ( ( 𝐵 +ℋ 𝐷 ) +ℋ 𝐺 ) )
108 95 107 eqeltrd ⊢ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) → ( 2 ·ℎ 𝑥 ) ∈ ( ( 𝐵 +ℋ 𝐷 ) +ℋ 𝐺 ) )
109 103 104 shscli ⊢ ( ( 𝐵 +ℋ 𝐷 ) +ℋ 𝐺 ) ∈ Sℋ
110 shmulcl ⊢ ( ( ( ( 𝐵 +ℋ 𝐷 ) +ℋ 𝐺 ) ∈ Sℋ ∧ ( 1 / 2 ) ∈ ℂ ∧ ( 2 ·ℎ 𝑥 ) ∈ ( ( 𝐵 +ℋ 𝐷 ) +ℋ 𝐺 ) ) → ( ( 1 / 2 ) ·ℎ ( 2 ·ℎ 𝑥 ) ) ∈ ( ( 𝐵 +ℋ 𝐷 ) +ℋ 𝐺 ) )
111 109 29 110 mp3an12 ⊢ ( ( 2 ·ℎ 𝑥 ) ∈ ( ( 𝐵 +ℋ 𝐷 ) +ℋ 𝐺 ) → ( ( 1 / 2 ) ·ℎ ( 2 ·ℎ 𝑥 ) ) ∈ ( ( 𝐵 +ℋ 𝐷 ) +ℋ 𝐺 ) )
112 108 111 syl ⊢ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) → ( ( 1 / 2 ) ·ℎ ( 2 ·ℎ 𝑥 ) ) ∈ ( ( 𝐵 +ℋ 𝐷 ) +ℋ 𝐺 ) )
113 34 112 eqeltrd ⊢ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) → 𝑥 ∈ ( ( 𝐵 +ℋ 𝐷 ) +ℋ 𝐺 ) )
114 113 ssriv ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ ( ( 𝐵 +ℋ 𝐷 ) +ℋ 𝐺 )
115 2 4 chsleji ⊢ ( 𝐵 +ℋ 𝐷 ) ⊆ ( 𝐵 ∨ℋ 𝐷 )
116 2 4 chjcli ⊢ ( 𝐵 ∨ℋ 𝐷 ) ∈ Cℋ
117 116 chshii ⊢ ( 𝐵 ∨ℋ 𝐷 ) ∈ Sℋ
118 103 117 104 shlessi ⊢ ( ( 𝐵 +ℋ 𝐷 ) ⊆ ( 𝐵 ∨ℋ 𝐷 ) → ( ( 𝐵 +ℋ 𝐷 ) +ℋ 𝐺 ) ⊆ ( ( 𝐵 ∨ℋ 𝐷 ) +ℋ 𝐺 ) )
119 115 118 ax-mp ⊢ ( ( 𝐵 +ℋ 𝐷 ) +ℋ 𝐺 ) ⊆ ( ( 𝐵 ∨ℋ 𝐷 ) +ℋ 𝐺 )
120 114 119 sstri ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ ( ( 𝐵 ∨ℋ 𝐷 ) +ℋ 𝐺 )
121 116 6 chsleji ⊢ ( ( 𝐵 ∨ℋ 𝐷 ) +ℋ 𝐺 ) ⊆ ( ( 𝐵 ∨ℋ 𝐷 ) ∨ℋ 𝐺 )
122 120 121 sstri ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ ( ( 𝐵 ∨ℋ 𝐷 ) ∨ℋ 𝐺 )
123 122 15 sseqtrri ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑍