HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  mayete3i Structured version   Visualization version   GIF version

Theorem mayete3i 30670
Description: Mayet's equation E3. Part of Theorem 4.1 of [Mayet3] p. 1223. (Contributed by NM, 22-Jun-2006.) (New usage is discouraged.)
Hypotheses
Ref Expression
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
Ref Expression
mayete3i (𝑋𝑌) ⊆ 𝑍

Proof of Theorem mayete3i
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elin 3926 . . . . . . . 8 (𝑥 ∈ (𝑋𝑌) ↔ (𝑥𝑋𝑥𝑌))
2 mayete3.a . . . . . . . . . . . . 13 𝐴C
3 mayete3.c . . . . . . . . . . . . 13 𝐶C
42, 3chjcli 30399 . . . . . . . . . . . 12 (𝐴 𝐶) ∈ C
5 mayete3.f . . . . . . . . . . . 12 𝐹C
64, 5chjcli 30399 . . . . . . . . . . 11 ((𝐴 𝐶) ∨ 𝐹) ∈ C
76cheli 30174 . . . . . . . . . 10 (𝑥 ∈ ((𝐴 𝐶) ∨ 𝐹) → 𝑥 ∈ ℋ)
8 mayete3.x . . . . . . . . . 10 𝑋 = ((𝐴 𝐶) ∨ 𝐹)
97, 8eleq2s 2856 . . . . . . . . 9 (𝑥𝑋𝑥 ∈ ℋ)
109adantr 481 . . . . . . . 8 ((𝑥𝑋𝑥𝑌) → 𝑥 ∈ ℋ)
111, 10sylbi 216 . . . . . . 7 (𝑥 ∈ (𝑋𝑌) → 𝑥 ∈ ℋ)
12 ax-hvmulid 29948 . . . . . . . 8 (𝑥 ∈ ℋ → (1 · 𝑥) = 𝑥)
13 2cn 12228 . . . . . . . . . . 11 2 ∈ ℂ
14 2ne0 12257 . . . . . . . . . . 11 2 ≠ 0
15 recid2 11828 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 2 ≠ 0) → ((1 / 2) · 2) = 1)
1613, 14, 15mp2an 690 . . . . . . . . . 10 ((1 / 2) · 2) = 1
1716oveq1i 7367 . . . . . . . . 9 (((1 / 2) · 2) · 𝑥) = (1 · 𝑥)
18 halfcn 12368 . . . . . . . . . 10 (1 / 2) ∈ ℂ
19 ax-hvmulass 29949 . . . . . . . . . 10 (((1 / 2) ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑥 ∈ ℋ) → (((1 / 2) · 2) · 𝑥) = ((1 / 2) · (2 · 𝑥)))
2018, 13, 19mp3an12 1451 . . . . . . . . 9 (𝑥 ∈ ℋ → (((1 / 2) · 2) · 𝑥) = ((1 / 2) · (2 · 𝑥)))
2117, 20eqtr3id 2790 . . . . . . . 8 (𝑥 ∈ ℋ → (1 · 𝑥) = ((1 / 2) · (2 · 𝑥)))
2212, 21eqtr3d 2778 . . . . . . 7 (𝑥 ∈ ℋ → 𝑥 = ((1 / 2) · (2 · 𝑥)))
2311, 22syl 17 . . . . . 6 (𝑥 ∈ (𝑋𝑌) → 𝑥 = ((1 / 2) · (2 · 𝑥)))
24 hv2times 30003 . . . . . . . . . . . . . 14 (𝑥 ∈ ℋ → (2 · 𝑥) = (𝑥 + 𝑥))
2524oveq1d 7372 . . . . . . . . . . . . 13 (𝑥 ∈ ℋ → ((2 · 𝑥) + 𝑥) = ((𝑥 + 𝑥) + 𝑥))
2611, 25syl 17 . . . . . . . . . . . 12 (𝑥 ∈ (𝑋𝑌) → ((2 · 𝑥) + 𝑥) = ((𝑥 + 𝑥) + 𝑥))
27 inss2 4189 . . . . . . . . . . . . . 14 (𝑋𝑌) ⊆ 𝑌
2827sseli 3940 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑋𝑌) → 𝑥𝑌)
29 mayete3.y . . . . . . . . . . . . . . 15 𝑌 = (((𝐴 𝐵) ∩ (𝐶 𝐷)) ∩ (𝐹 𝐺))
3029elin2 4157 . . . . . . . . . . . . . 14 (𝑥𝑌 ↔ (𝑥 ∈ ((𝐴 𝐵) ∩ (𝐶 𝐷)) ∧ 𝑥 ∈ (𝐹 𝐺)))
31 elin 3926 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((𝐴 𝐵) ∩ (𝐶 𝐷)) ↔ (𝑥 ∈ (𝐴 𝐵) ∧ 𝑥 ∈ (𝐶 𝐷)))
32 mayete3.ab . . . . . . . . . . . . . . . . . . 19 𝐴 ⊆ (⊥‘𝐵)
33 mayete3.b . . . . . . . . . . . . . . . . . . . 20 𝐵C
342, 33pjdsi 30654 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (𝐴 𝐵) ∧ 𝐴 ⊆ (⊥‘𝐵)) → 𝑥 = (((proj𝐴)‘𝑥) + ((proj𝐵)‘𝑥)))
3532, 34mpan2 689 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴 𝐵) → 𝑥 = (((proj𝐴)‘𝑥) + ((proj𝐵)‘𝑥)))
36 mayete3.cd . . . . . . . . . . . . . . . . . . 19 𝐶 ⊆ (⊥‘𝐷)
37 mayete3.d . . . . . . . . . . . . . . . . . . . 20 𝐷C
383, 37pjdsi 30654 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (𝐶 𝐷) ∧ 𝐶 ⊆ (⊥‘𝐷)) → 𝑥 = (((proj𝐶)‘𝑥) + ((proj𝐷)‘𝑥)))
3936, 38mpan2 689 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐶 𝐷) → 𝑥 = (((proj𝐶)‘𝑥) + ((proj𝐷)‘𝑥)))
4035, 39oveqan12d 7376 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (𝐴 𝐵) ∧ 𝑥 ∈ (𝐶 𝐷)) → (𝑥 + 𝑥) = ((((proj𝐴)‘𝑥) + ((proj𝐵)‘𝑥)) + (((proj𝐶)‘𝑥) + ((proj𝐷)‘𝑥))))
4131, 40sylbi 216 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((𝐴 𝐵) ∩ (𝐶 𝐷)) → (𝑥 + 𝑥) = ((((proj𝐴)‘𝑥) + ((proj𝐵)‘𝑥)) + (((proj𝐶)‘𝑥) + ((proj𝐷)‘𝑥))))
42 inss1 4188 . . . . . . . . . . . . . . . . . 18 ((𝐴 𝐵) ∩ (𝐶 𝐷)) ⊆ (𝐴 𝐵)
4342sseli 3940 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((𝐴 𝐵) ∩ (𝐶 𝐷)) → 𝑥 ∈ (𝐴 𝐵))
442, 33chjcli 30399 . . . . . . . . . . . . . . . . . 18 (𝐴 𝐵) ∈ C
4544cheli 30174 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴 𝐵) → 𝑥 ∈ ℋ)
462pjhcli 30360 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℋ → ((proj𝐴)‘𝑥) ∈ ℋ)
4733pjhcli 30360 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℋ → ((proj𝐵)‘𝑥) ∈ ℋ)
483pjhcli 30360 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℋ → ((proj𝐶)‘𝑥) ∈ ℋ)
4937pjhcli 30360 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℋ → ((proj𝐷)‘𝑥) ∈ ℋ)
50 hvadd4 29978 . . . . . . . . . . . . . . . . . 18 (((((proj𝐴)‘𝑥) ∈ ℋ ∧ ((proj𝐵)‘𝑥) ∈ ℋ) ∧ (((proj𝐶)‘𝑥) ∈ ℋ ∧ ((proj𝐷)‘𝑥) ∈ ℋ)) → ((((proj𝐴)‘𝑥) + ((proj𝐵)‘𝑥)) + (((proj𝐶)‘𝑥) + ((proj𝐷)‘𝑥))) = ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + (((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥))))
5146, 47, 48, 49, 50syl22anc 837 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℋ → ((((proj𝐴)‘𝑥) + ((proj𝐵)‘𝑥)) + (((proj𝐶)‘𝑥) + ((proj𝐷)‘𝑥))) = ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + (((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥))))
5243, 45, 513syl 18 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((𝐴 𝐵) ∩ (𝐶 𝐷)) → ((((proj𝐴)‘𝑥) + ((proj𝐵)‘𝑥)) + (((proj𝐶)‘𝑥) + ((proj𝐷)‘𝑥))) = ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + (((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥))))
5341, 52eqtrd 2776 . . . . . . . . . . . . . . 15 (𝑥 ∈ ((𝐴 𝐵) ∩ (𝐶 𝐷)) → (𝑥 + 𝑥) = ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + (((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥))))
54 mayete3.fg . . . . . . . . . . . . . . . 16 𝐹 ⊆ (⊥‘𝐺)
55 mayete3.g . . . . . . . . . . . . . . . . 17 𝐺C
565, 55pjdsi 30654 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (𝐹 𝐺) ∧ 𝐹 ⊆ (⊥‘𝐺)) → 𝑥 = (((proj𝐹)‘𝑥) + ((proj𝐺)‘𝑥)))
5754, 56mpan2 689 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐹 𝐺) → 𝑥 = (((proj𝐹)‘𝑥) + ((proj𝐺)‘𝑥)))
5853, 57oveqan12d 7376 . . . . . . . . . . . . . 14 ((𝑥 ∈ ((𝐴 𝐵) ∩ (𝐶 𝐷)) ∧ 𝑥 ∈ (𝐹 𝐺)) → ((𝑥 + 𝑥) + 𝑥) = (((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + (((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥))) + (((proj𝐹)‘𝑥) + ((proj𝐺)‘𝑥))))
5930, 58sylbi 216 . . . . . . . . . . . . 13 (𝑥𝑌 → ((𝑥 + 𝑥) + 𝑥) = (((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + (((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥))) + (((proj𝐹)‘𝑥) + ((proj𝐺)‘𝑥))))
6028, 59syl 17 . . . . . . . . . . . 12 (𝑥 ∈ (𝑋𝑌) → ((𝑥 + 𝑥) + 𝑥) = (((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + (((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥))) + (((proj𝐹)‘𝑥) + ((proj𝐺)‘𝑥))))
61 hvaddcl 29954 . . . . . . . . . . . . . . 15 ((((proj𝐴)‘𝑥) ∈ ℋ ∧ ((proj𝐶)‘𝑥) ∈ ℋ) → (((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) ∈ ℋ)
6246, 48, 61syl2anc 584 . . . . . . . . . . . . . 14 (𝑥 ∈ ℋ → (((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) ∈ ℋ)
63 hvaddcl 29954 . . . . . . . . . . . . . . 15 ((((proj𝐵)‘𝑥) ∈ ℋ ∧ ((proj𝐷)‘𝑥) ∈ ℋ) → (((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) ∈ ℋ)
6447, 49, 63syl2anc 584 . . . . . . . . . . . . . 14 (𝑥 ∈ ℋ → (((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) ∈ ℋ)
655pjhcli 30360 . . . . . . . . . . . . . 14 (𝑥 ∈ ℋ → ((proj𝐹)‘𝑥) ∈ ℋ)
6655pjhcli 30360 . . . . . . . . . . . . . 14 (𝑥 ∈ ℋ → ((proj𝐺)‘𝑥) ∈ ℋ)
67 hvadd4 29978 . . . . . . . . . . . . . 14 ((((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) ∈ ℋ ∧ (((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) ∈ ℋ) ∧ (((proj𝐹)‘𝑥) ∈ ℋ ∧ ((proj𝐺)‘𝑥) ∈ ℋ)) → (((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + (((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥))) + (((proj𝐹)‘𝑥) + ((proj𝐺)‘𝑥))) = (((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)) + ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥))))
6862, 64, 65, 66, 67syl22anc 837 . . . . . . . . . . . . 13 (𝑥 ∈ ℋ → (((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + (((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥))) + (((proj𝐹)‘𝑥) + ((proj𝐺)‘𝑥))) = (((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)) + ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥))))
6911, 68syl 17 . . . . . . . . . . . 12 (𝑥 ∈ (𝑋𝑌) → (((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + (((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥))) + (((proj𝐹)‘𝑥) + ((proj𝐺)‘𝑥))) = (((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)) + ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥))))
7026, 60, 693eqtrd 2780 . . . . . . . . . . 11 (𝑥 ∈ (𝑋𝑌) → ((2 · 𝑥) + 𝑥) = (((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)) + ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥))))
71 inss1 4188 . . . . . . . . . . . . . 14 (𝑋𝑌) ⊆ 𝑋
7271sseli 3940 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑋𝑌) → 𝑥𝑋)
7372, 8eleqtrdi 2848 . . . . . . . . . . . 12 (𝑥 ∈ (𝑋𝑌) → 𝑥 ∈ ((𝐴 𝐶) ∨ 𝐹))
74 mayete3.ac . . . . . . . . . . . 12 𝐴 ⊆ (⊥‘𝐶)
75 mayete3.af . . . . . . . . . . . . 13 𝐴 ⊆ (⊥‘𝐹)
76 mayete3.cf . . . . . . . . . . . . 13 𝐶 ⊆ (⊥‘𝐹)
772, 3, 5pjds3i 30655 . . . . . . . . . . . . 13 (((𝑥 ∈ ((𝐴 𝐶) ∨ 𝐹) ∧ 𝐴 ⊆ (⊥‘𝐶)) ∧ (𝐴 ⊆ (⊥‘𝐹) ∧ 𝐶 ⊆ (⊥‘𝐹))) → 𝑥 = ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)))
7875, 76, 77mpanr12 703 . . . . . . . . . . . 12 ((𝑥 ∈ ((𝐴 𝐶) ∨ 𝐹) ∧ 𝐴 ⊆ (⊥‘𝐶)) → 𝑥 = ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)))
7973, 74, 78sylancl 586 . . . . . . . . . . 11 (𝑥 ∈ (𝑋𝑌) → 𝑥 = ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)))
8070, 79oveq12d 7375 . . . . . . . . . 10 (𝑥 ∈ (𝑋𝑌) → (((2 · 𝑥) + 𝑥) − 𝑥) = ((((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)) + ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥))) − ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥))))
81 hvmulcl 29955 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ 𝑥 ∈ ℋ) → (2 · 𝑥) ∈ ℋ)
8213, 81mpan 688 . . . . . . . . . . . 12 (𝑥 ∈ ℋ → (2 · 𝑥) ∈ ℋ)
83 hvpncan 29981 . . . . . . . . . . . 12 (((2 · 𝑥) ∈ ℋ ∧ 𝑥 ∈ ℋ) → (((2 · 𝑥) + 𝑥) − 𝑥) = (2 · 𝑥))
8482, 83mpancom 686 . . . . . . . . . . 11 (𝑥 ∈ ℋ → (((2 · 𝑥) + 𝑥) − 𝑥) = (2 · 𝑥))
8511, 84syl 17 . . . . . . . . . 10 (𝑥 ∈ (𝑋𝑌) → (((2 · 𝑥) + 𝑥) − 𝑥) = (2 · 𝑥))
8680, 85eqtr3d 2778 . . . . . . . . 9 (𝑥 ∈ (𝑋𝑌) → ((((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)) + ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥))) − ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥))) = (2 · 𝑥))
87 hvaddcl 29954 . . . . . . . . . . . 12 (((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) ∈ ℋ ∧ ((proj𝐹)‘𝑥) ∈ ℋ) → ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)) ∈ ℋ)
8862, 65, 87syl2anc 584 . . . . . . . . . . 11 (𝑥 ∈ ℋ → ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)) ∈ ℋ)
89 hvaddcl 29954 . . . . . . . . . . . 12 (((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) ∈ ℋ ∧ ((proj𝐺)‘𝑥) ∈ ℋ) → ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥)) ∈ ℋ)
9064, 66, 89syl2anc 584 . . . . . . . . . . 11 (𝑥 ∈ ℋ → ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥)) ∈ ℋ)
91 hvpncan2 29982 . . . . . . . . . . 11 ((((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)) ∈ ℋ ∧ ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥)) ∈ ℋ) → ((((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)) + ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥))) − ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥))) = ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥)))
9288, 90, 91syl2anc 584 . . . . . . . . . 10 (𝑥 ∈ ℋ → ((((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)) + ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥))) − ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥))) = ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥)))
9311, 92syl 17 . . . . . . . . 9 (𝑥 ∈ (𝑋𝑌) → ((((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)) + ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥))) − ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥))) = ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥)))
9486, 93eqtr3d 2778 . . . . . . . 8 (𝑥 ∈ (𝑋𝑌) → (2 · 𝑥) = ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥)))
9533pjcli 30359 . . . . . . . . . . 11 (𝑥 ∈ ℋ → ((proj𝐵)‘𝑥) ∈ 𝐵)
9637pjcli 30359 . . . . . . . . . . 11 (𝑥 ∈ ℋ → ((proj𝐷)‘𝑥) ∈ 𝐷)
9733chshii 30169 . . . . . . . . . . . 12 𝐵S
9837chshii 30169 . . . . . . . . . . . 12 𝐷S
9997, 98shsvai 30306 . . . . . . . . . . 11 ((((proj𝐵)‘𝑥) ∈ 𝐵 ∧ ((proj𝐷)‘𝑥) ∈ 𝐷) → (((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) ∈ (𝐵 + 𝐷))
10095, 96, 99syl2anc 584 . . . . . . . . . 10 (𝑥 ∈ ℋ → (((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) ∈ (𝐵 + 𝐷))
10155pjcli 30359 . . . . . . . . . 10 (𝑥 ∈ ℋ → ((proj𝐺)‘𝑥) ∈ 𝐺)
10297, 98shscli 30259 . . . . . . . . . . 11 (𝐵 + 𝐷) ∈ S
10355chshii 30169 . . . . . . . . . . 11 𝐺S
104102, 103shsvai 30306 . . . . . . . . . 10 (((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) ∈ (𝐵 + 𝐷) ∧ ((proj𝐺)‘𝑥) ∈ 𝐺) → ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥)) ∈ ((𝐵 + 𝐷) + 𝐺))
105100, 101, 104syl2anc 584 . . . . . . . . 9 (𝑥 ∈ ℋ → ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥)) ∈ ((𝐵 + 𝐷) + 𝐺))
10611, 105syl 17 . . . . . . . 8 (𝑥 ∈ (𝑋𝑌) → ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥)) ∈ ((𝐵 + 𝐷) + 𝐺))
10794, 106eqeltrd 2838 . . . . . . 7 (𝑥 ∈ (𝑋𝑌) → (2 · 𝑥) ∈ ((𝐵 + 𝐷) + 𝐺))
108102, 103shscli 30259 . . . . . . . 8 ((𝐵 + 𝐷) + 𝐺) ∈ S
109 shmulcl 30160 . . . . . . . 8 ((((𝐵 + 𝐷) + 𝐺) ∈ S ∧ (1 / 2) ∈ ℂ ∧ (2 · 𝑥) ∈ ((𝐵 + 𝐷) + 𝐺)) → ((1 / 2) · (2 · 𝑥)) ∈ ((𝐵 + 𝐷) + 𝐺))
110108, 18, 109mp3an12 1451 . . . . . . 7 ((2 · 𝑥) ∈ ((𝐵 + 𝐷) + 𝐺) → ((1 / 2) · (2 · 𝑥)) ∈ ((𝐵 + 𝐷) + 𝐺))
111107, 110syl 17 . . . . . 6 (𝑥 ∈ (𝑋𝑌) → ((1 / 2) · (2 · 𝑥)) ∈ ((𝐵 + 𝐷) + 𝐺))
11223, 111eqeltrd 2838 . . . . 5 (𝑥 ∈ (𝑋𝑌) → 𝑥 ∈ ((𝐵 + 𝐷) + 𝐺))
113112ssriv 3948 . . . 4 (𝑋𝑌) ⊆ ((𝐵 + 𝐷) + 𝐺)
11433, 37chsleji 30400 . . . . 5 (𝐵 + 𝐷) ⊆ (𝐵 𝐷)
11533, 37chjcli 30399 . . . . . . 7 (𝐵 𝐷) ∈ C
116115chshii 30169 . . . . . 6 (𝐵 𝐷) ∈ S
117102, 116, 103shlessi 30319 . . . . 5 ((𝐵 + 𝐷) ⊆ (𝐵 𝐷) → ((𝐵 + 𝐷) + 𝐺) ⊆ ((𝐵 𝐷) + 𝐺))
118114, 117ax-mp 5 . . . 4 ((𝐵 + 𝐷) + 𝐺) ⊆ ((𝐵 𝐷) + 𝐺)
119113, 118sstri 3953 . . 3 (𝑋𝑌) ⊆ ((𝐵 𝐷) + 𝐺)
120115, 55chsleji 30400 . . 3 ((𝐵 𝐷) + 𝐺) ⊆ ((𝐵 𝐷) ∨ 𝐺)
121119, 120sstri 3953 . 2 (𝑋𝑌) ⊆ ((𝐵 𝐷) ∨ 𝐺)
122 mayete3.z . 2 𝑍 = ((𝐵 𝐷) ∨ 𝐺)
123121, 122sseqtrri 3981 1 (𝑋𝑌) ⊆ 𝑍
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1541  wcel 2106  wne 2943  cin 3909  wss 3910  cfv 6496  (class class class)co 7357  cc 11049  0cc0 11051  1c1 11052   · cmul 11056   / cdiv 11812  2c2 12208  chba 29861   + cva 29862   · csm 29863   cmv 29867   S csh 29870   C cch 29871  cort 29872   + cph 29873   chj 29875  projcpjh 29879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cc 10371  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131  ax-hilex 29941  ax-hfvadd 29942  ax-hvcom 29943  ax-hvass 29944  ax-hv0cl 29945  ax-hvaddid 29946  ax-hfvmul 29947  ax-hvmulid 29948  ax-hvmulass 29949  ax-hvdistr1 29950  ax-hvdistr2 29951  ax-hvmul0 29952  ax-hfi 30021  ax-his1 30024  ax-his2 30025  ax-his3 30026  ax-his4 30027  ax-hcompl 30144
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-oadd 8416  df-omul 8417  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-fi 9347  df-sup 9378  df-inf 9379  df-oi 9446  df-card 9875  df-acn 9878  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ioo 13268  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-fl 13697  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-clim 15370  df-rlim 15371  df-sum 15571  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-rest 17304  df-topn 17305  df-0g 17323  df-gsum 17324  df-topgen 17325  df-pt 17326  df-prds 17329  df-xrs 17384  df-qtop 17389  df-imas 17390  df-xps 17392  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-mulg 18873  df-cntz 19097  df-cmn 19564  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-fbas 20793  df-fg 20794  df-cnfld 20797  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-cld 22370  df-ntr 22371  df-cls 22372  df-nei 22449  df-cn 22578  df-cnp 22579  df-lm 22580  df-haus 22666  df-tx 22913  df-hmeo 23106  df-fil 23197  df-fm 23289  df-flim 23290  df-flf 23291  df-xms 23673  df-ms 23674  df-tms 23675  df-cfil 24619  df-cau 24620  df-cmet 24621  df-grpo 29435  df-gid 29436  df-ginv 29437  df-gdiv 29438  df-ablo 29487  df-vc 29501  df-nv 29534  df-va 29537  df-ba 29538  df-sm 29539  df-0v 29540  df-vs 29541  df-nmcv 29542  df-ims 29543  df-dip 29643  df-ssp 29664  df-ph 29755  df-cbn 29805  df-hnorm 29910  df-hba 29911  df-hvsub 29913  df-hlim 29914  df-hcau 29915  df-sh 30149  df-ch 30163  df-oc 30194  df-ch0 30195  df-shs 30250  df-chj 30252  df-pjh 30337
This theorem is referenced by:  mayetes3i  30671
  Copyright terms: Public domain W3C validator