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

Theorem mayete3i 31653
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 3962 . . . . . . . 8 (𝑥 ∈ (𝑋𝑌) ↔ (𝑥𝑋𝑥𝑌))
2 mayete3.a . . . . . . . . . . . . 13 𝐴C
3 mayete3.c . . . . . . . . . . . . 13 𝐶C
42, 3chjcli 31382 . . . . . . . . . . . 12 (𝐴 𝐶) ∈ C
5 mayete3.f . . . . . . . . . . . 12 𝐹C
64, 5chjcli 31382 . . . . . . . . . . 11 ((𝐴 𝐶) ∨ 𝐹) ∈ C
76cheli 31157 . . . . . . . . . 10 (𝑥 ∈ ((𝐴 𝐶) ∨ 𝐹) → 𝑥 ∈ ℋ)
8 mayete3.x . . . . . . . . . 10 𝑋 = ((𝐴 𝐶) ∨ 𝐹)
97, 8eleq2s 2843 . . . . . . . . 9 (𝑥𝑋𝑥 ∈ ℋ)
109adantr 479 . . . . . . . 8 ((𝑥𝑋𝑥𝑌) → 𝑥 ∈ ℋ)
111, 10sylbi 216 . . . . . . 7 (𝑥 ∈ (𝑋𝑌) → 𝑥 ∈ ℋ)
12 ax-hvmulid 30931 . . . . . . . 8 (𝑥 ∈ ℋ → (1 · 𝑥) = 𝑥)
13 2cn 12334 . . . . . . . . . . 11 2 ∈ ℂ
14 2ne0 12363 . . . . . . . . . . 11 2 ≠ 0
15 recid2 11934 . . . . . . . . . . 11 ((2 ∈ ℂ ∧ 2 ≠ 0) → ((1 / 2) · 2) = 1)
1613, 14, 15mp2an 690 . . . . . . . . . 10 ((1 / 2) · 2) = 1
1716oveq1i 7433 . . . . . . . . 9 (((1 / 2) · 2) · 𝑥) = (1 · 𝑥)
18 halfcn 12474 . . . . . . . . . 10 (1 / 2) ∈ ℂ
19 ax-hvmulass 30932 . . . . . . . . . 10 (((1 / 2) ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑥 ∈ ℋ) → (((1 / 2) · 2) · 𝑥) = ((1 / 2) · (2 · 𝑥)))
2018, 13, 19mp3an12 1447 . . . . . . . . 9 (𝑥 ∈ ℋ → (((1 / 2) · 2) · 𝑥) = ((1 / 2) · (2 · 𝑥)))
2117, 20eqtr3id 2779 . . . . . . . 8 (𝑥 ∈ ℋ → (1 · 𝑥) = ((1 / 2) · (2 · 𝑥)))
2212, 21eqtr3d 2767 . . . . . . 7 (𝑥 ∈ ℋ → 𝑥 = ((1 / 2) · (2 · 𝑥)))
2311, 22syl 17 . . . . . 6 (𝑥 ∈ (𝑋𝑌) → 𝑥 = ((1 / 2) · (2 · 𝑥)))
24 hv2times 30986 . . . . . . . . . . . . . 14 (𝑥 ∈ ℋ → (2 · 𝑥) = (𝑥 + 𝑥))
2524oveq1d 7438 . . . . . . . . . . . . 13 (𝑥 ∈ ℋ → ((2 · 𝑥) + 𝑥) = ((𝑥 + 𝑥) + 𝑥))
2611, 25syl 17 . . . . . . . . . . . 12 (𝑥 ∈ (𝑋𝑌) → ((2 · 𝑥) + 𝑥) = ((𝑥 + 𝑥) + 𝑥))
27 inss2 4230 . . . . . . . . . . . . . 14 (𝑋𝑌) ⊆ 𝑌
2827sseli 3974 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑋𝑌) → 𝑥𝑌)
29 mayete3.y . . . . . . . . . . . . . . 15 𝑌 = (((𝐴 𝐵) ∩ (𝐶 𝐷)) ∩ (𝐹 𝐺))
3029elin2 4197 . . . . . . . . . . . . . 14 (𝑥𝑌 ↔ (𝑥 ∈ ((𝐴 𝐵) ∩ (𝐶 𝐷)) ∧ 𝑥 ∈ (𝐹 𝐺)))
31 elin 3962 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((𝐴 𝐵) ∩ (𝐶 𝐷)) ↔ (𝑥 ∈ (𝐴 𝐵) ∧ 𝑥 ∈ (𝐶 𝐷)))
32 mayete3.ab . . . . . . . . . . . . . . . . . . 19 𝐴 ⊆ (⊥‘𝐵)
33 mayete3.b . . . . . . . . . . . . . . . . . . . 20 𝐵C
342, 33pjdsi 31637 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (𝐴 𝐵) ∧ 𝐴 ⊆ (⊥‘𝐵)) → 𝑥 = (((proj𝐴)‘𝑥) + ((proj𝐵)‘𝑥)))
3532, 34mpan2 689 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴 𝐵) → 𝑥 = (((proj𝐴)‘𝑥) + ((proj𝐵)‘𝑥)))
36 mayete3.cd . . . . . . . . . . . . . . . . . . 19 𝐶 ⊆ (⊥‘𝐷)
37 mayete3.d . . . . . . . . . . . . . . . . . . . 20 𝐷C
383, 37pjdsi 31637 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (𝐶 𝐷) ∧ 𝐶 ⊆ (⊥‘𝐷)) → 𝑥 = (((proj𝐶)‘𝑥) + ((proj𝐷)‘𝑥)))
3936, 38mpan2 689 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐶 𝐷) → 𝑥 = (((proj𝐶)‘𝑥) + ((proj𝐷)‘𝑥)))
4035, 39oveqan12d 7442 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (𝐴 𝐵) ∧ 𝑥 ∈ (𝐶 𝐷)) → (𝑥 + 𝑥) = ((((proj𝐴)‘𝑥) + ((proj𝐵)‘𝑥)) + (((proj𝐶)‘𝑥) + ((proj𝐷)‘𝑥))))
4131, 40sylbi 216 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((𝐴 𝐵) ∩ (𝐶 𝐷)) → (𝑥 + 𝑥) = ((((proj𝐴)‘𝑥) + ((proj𝐵)‘𝑥)) + (((proj𝐶)‘𝑥) + ((proj𝐷)‘𝑥))))
42 inss1 4229 . . . . . . . . . . . . . . . . . 18 ((𝐴 𝐵) ∩ (𝐶 𝐷)) ⊆ (𝐴 𝐵)
4342sseli 3974 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((𝐴 𝐵) ∩ (𝐶 𝐷)) → 𝑥 ∈ (𝐴 𝐵))
442, 33chjcli 31382 . . . . . . . . . . . . . . . . . 18 (𝐴 𝐵) ∈ C
4544cheli 31157 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴 𝐵) → 𝑥 ∈ ℋ)
462pjhcli 31343 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℋ → ((proj𝐴)‘𝑥) ∈ ℋ)
4733pjhcli 31343 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℋ → ((proj𝐵)‘𝑥) ∈ ℋ)
483pjhcli 31343 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℋ → ((proj𝐶)‘𝑥) ∈ ℋ)
4937pjhcli 31343 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℋ → ((proj𝐷)‘𝑥) ∈ ℋ)
50 hvadd4 30961 . . . . . . . . . . . . . . . . . 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 2765 . . . . . . . . . . . . . . 15 (𝑥 ∈ ((𝐴 𝐵) ∩ (𝐶 𝐷)) → (𝑥 + 𝑥) = ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + (((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥))))
54 mayete3.fg . . . . . . . . . . . . . . . 16 𝐹 ⊆ (⊥‘𝐺)
55 mayete3.g . . . . . . . . . . . . . . . . 17 𝐺C
565, 55pjdsi 31637 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (𝐹 𝐺) ∧ 𝐹 ⊆ (⊥‘𝐺)) → 𝑥 = (((proj𝐹)‘𝑥) + ((proj𝐺)‘𝑥)))
5754, 56mpan2 689 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐹 𝐺) → 𝑥 = (((proj𝐹)‘𝑥) + ((proj𝐺)‘𝑥)))
5853, 57oveqan12d 7442 . . . . . . . . . . . . . 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 30937 . . . . . . . . . . . . . . 15 ((((proj𝐴)‘𝑥) ∈ ℋ ∧ ((proj𝐶)‘𝑥) ∈ ℋ) → (((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) ∈ ℋ)
6246, 48, 61syl2anc 582 . . . . . . . . . . . . . 14 (𝑥 ∈ ℋ → (((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) ∈ ℋ)
63 hvaddcl 30937 . . . . . . . . . . . . . . 15 ((((proj𝐵)‘𝑥) ∈ ℋ ∧ ((proj𝐷)‘𝑥) ∈ ℋ) → (((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) ∈ ℋ)
6447, 49, 63syl2anc 582 . . . . . . . . . . . . . 14 (𝑥 ∈ ℋ → (((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) ∈ ℋ)
655pjhcli 31343 . . . . . . . . . . . . . 14 (𝑥 ∈ ℋ → ((proj𝐹)‘𝑥) ∈ ℋ)
6655pjhcli 31343 . . . . . . . . . . . . . 14 (𝑥 ∈ ℋ → ((proj𝐺)‘𝑥) ∈ ℋ)
67 hvadd4 30961 . . . . . . . . . . . . . 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 2769 . . . . . . . . . . 11 (𝑥 ∈ (𝑋𝑌) → ((2 · 𝑥) + 𝑥) = (((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)) + ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥))))
71 inss1 4229 . . . . . . . . . . . . . 14 (𝑋𝑌) ⊆ 𝑋
7271sseli 3974 . . . . . . . . . . . . 13 (𝑥 ∈ (𝑋𝑌) → 𝑥𝑋)
7372, 8eleqtrdi 2835 . . . . . . . . . . . 12 (𝑥 ∈ (𝑋𝑌) → 𝑥 ∈ ((𝐴 𝐶) ∨ 𝐹))
74 mayete3.ac . . . . . . . . . . . 12 𝐴 ⊆ (⊥‘𝐶)
75 mayete3.af . . . . . . . . . . . . 13 𝐴 ⊆ (⊥‘𝐹)
76 mayete3.cf . . . . . . . . . . . . 13 𝐶 ⊆ (⊥‘𝐹)
772, 3, 5pjds3i 31638 . . . . . . . . . . . . 13 (((𝑥 ∈ ((𝐴 𝐶) ∨ 𝐹) ∧ 𝐴 ⊆ (⊥‘𝐶)) ∧ (𝐴 ⊆ (⊥‘𝐹) ∧ 𝐶 ⊆ (⊥‘𝐹))) → 𝑥 = ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)))
7875, 76, 77mpanr12 703 . . . . . . . . . . . 12 ((𝑥 ∈ ((𝐴 𝐶) ∨ 𝐹) ∧ 𝐴 ⊆ (⊥‘𝐶)) → 𝑥 = ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)))
7973, 74, 78sylancl 584 . . . . . . . . . . 11 (𝑥 ∈ (𝑋𝑌) → 𝑥 = ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)))
8070, 79oveq12d 7441 . . . . . . . . . 10 (𝑥 ∈ (𝑋𝑌) → (((2 · 𝑥) + 𝑥) − 𝑥) = ((((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)) + ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥))) − ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥))))
81 hvmulcl 30938 . . . . . . . . . . . . 13 ((2 ∈ ℂ ∧ 𝑥 ∈ ℋ) → (2 · 𝑥) ∈ ℋ)
8213, 81mpan 688 . . . . . . . . . . . 12 (𝑥 ∈ ℋ → (2 · 𝑥) ∈ ℋ)
83 hvpncan 30964 . . . . . . . . . . . 12 (((2 · 𝑥) ∈ ℋ ∧ 𝑥 ∈ ℋ) → (((2 · 𝑥) + 𝑥) − 𝑥) = (2 · 𝑥))
8482, 83mpancom 686 . . . . . . . . . . 11 (𝑥 ∈ ℋ → (((2 · 𝑥) + 𝑥) − 𝑥) = (2 · 𝑥))
8511, 84syl 17 . . . . . . . . . 10 (𝑥 ∈ (𝑋𝑌) → (((2 · 𝑥) + 𝑥) − 𝑥) = (2 · 𝑥))
8680, 85eqtr3d 2767 . . . . . . . . 9 (𝑥 ∈ (𝑋𝑌) → ((((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)) + ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥))) − ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥))) = (2 · 𝑥))
87 hvaddcl 30937 . . . . . . . . . . . 12 (((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) ∈ ℋ ∧ ((proj𝐹)‘𝑥) ∈ ℋ) → ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)) ∈ ℋ)
8862, 65, 87syl2anc 582 . . . . . . . . . . 11 (𝑥 ∈ ℋ → ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)) ∈ ℋ)
89 hvaddcl 30937 . . . . . . . . . . . 12 (((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) ∈ ℋ ∧ ((proj𝐺)‘𝑥) ∈ ℋ) → ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥)) ∈ ℋ)
9064, 66, 89syl2anc 582 . . . . . . . . . . 11 (𝑥 ∈ ℋ → ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥)) ∈ ℋ)
91 hvpncan2 30965 . . . . . . . . . . 11 ((((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)) ∈ ℋ ∧ ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥)) ∈ ℋ) → ((((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥)) + ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥))) − ((((proj𝐴)‘𝑥) + ((proj𝐶)‘𝑥)) + ((proj𝐹)‘𝑥))) = ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥)))
9288, 90, 91syl2anc 582 . . . . . . . . . 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 2767 . . . . . . . 8 (𝑥 ∈ (𝑋𝑌) → (2 · 𝑥) = ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥)))
9533pjcli 31342 . . . . . . . . . . 11 (𝑥 ∈ ℋ → ((proj𝐵)‘𝑥) ∈ 𝐵)
9637pjcli 31342 . . . . . . . . . . 11 (𝑥 ∈ ℋ → ((proj𝐷)‘𝑥) ∈ 𝐷)
9733chshii 31152 . . . . . . . . . . . 12 𝐵S
9837chshii 31152 . . . . . . . . . . . 12 𝐷S
9997, 98shsvai 31289 . . . . . . . . . . 11 ((((proj𝐵)‘𝑥) ∈ 𝐵 ∧ ((proj𝐷)‘𝑥) ∈ 𝐷) → (((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) ∈ (𝐵 + 𝐷))
10095, 96, 99syl2anc 582 . . . . . . . . . 10 (𝑥 ∈ ℋ → (((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) ∈ (𝐵 + 𝐷))
10155pjcli 31342 . . . . . . . . . 10 (𝑥 ∈ ℋ → ((proj𝐺)‘𝑥) ∈ 𝐺)
10297, 98shscli 31242 . . . . . . . . . . 11 (𝐵 + 𝐷) ∈ S
10355chshii 31152 . . . . . . . . . . 11 𝐺S
104102, 103shsvai 31289 . . . . . . . . . 10 (((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) ∈ (𝐵 + 𝐷) ∧ ((proj𝐺)‘𝑥) ∈ 𝐺) → ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥)) ∈ ((𝐵 + 𝐷) + 𝐺))
105100, 101, 104syl2anc 582 . . . . . . . . 9 (𝑥 ∈ ℋ → ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥)) ∈ ((𝐵 + 𝐷) + 𝐺))
10611, 105syl 17 . . . . . . . 8 (𝑥 ∈ (𝑋𝑌) → ((((proj𝐵)‘𝑥) + ((proj𝐷)‘𝑥)) + ((proj𝐺)‘𝑥)) ∈ ((𝐵 + 𝐷) + 𝐺))
10794, 106eqeltrd 2825 . . . . . . 7 (𝑥 ∈ (𝑋𝑌) → (2 · 𝑥) ∈ ((𝐵 + 𝐷) + 𝐺))
108102, 103shscli 31242 . . . . . . . 8 ((𝐵 + 𝐷) + 𝐺) ∈ S
109 shmulcl 31143 . . . . . . . 8 ((((𝐵 + 𝐷) + 𝐺) ∈ S ∧ (1 / 2) ∈ ℂ ∧ (2 · 𝑥) ∈ ((𝐵 + 𝐷) + 𝐺)) → ((1 / 2) · (2 · 𝑥)) ∈ ((𝐵 + 𝐷) + 𝐺))
110108, 18, 109mp3an12 1447 . . . . . . 7 ((2 · 𝑥) ∈ ((𝐵 + 𝐷) + 𝐺) → ((1 / 2) · (2 · 𝑥)) ∈ ((𝐵 + 𝐷) + 𝐺))
111107, 110syl 17 . . . . . 6 (𝑥 ∈ (𝑋𝑌) → ((1 / 2) · (2 · 𝑥)) ∈ ((𝐵 + 𝐷) + 𝐺))
11223, 111eqeltrd 2825 . . . . 5 (𝑥 ∈ (𝑋𝑌) → 𝑥 ∈ ((𝐵 + 𝐷) + 𝐺))
113112ssriv 3982 . . . 4 (𝑋𝑌) ⊆ ((𝐵 + 𝐷) + 𝐺)
11433, 37chsleji 31383 . . . . 5 (𝐵 + 𝐷) ⊆ (𝐵 𝐷)
11533, 37chjcli 31382 . . . . . . 7 (𝐵 𝐷) ∈ C
116115chshii 31152 . . . . . 6 (𝐵 𝐷) ∈ S
117102, 116, 103shlessi 31302 . . . . 5 ((𝐵 + 𝐷) ⊆ (𝐵 𝐷) → ((𝐵 + 𝐷) + 𝐺) ⊆ ((𝐵 𝐷) + 𝐺))
118114, 117ax-mp 5 . . . 4 ((𝐵 + 𝐷) + 𝐺) ⊆ ((𝐵 𝐷) + 𝐺)
119113, 118sstri 3988 . . 3 (𝑋𝑌) ⊆ ((𝐵 𝐷) + 𝐺)
120115, 55chsleji 31383 . . 3 ((𝐵 𝐷) + 𝐺) ⊆ ((𝐵 𝐷) ∨ 𝐺)
121119, 120sstri 3988 . 2 (𝑋𝑌) ⊆ ((𝐵 𝐷) ∨ 𝐺)
122 mayete3.z . 2 𝑍 = ((𝐵 𝐷) ∨ 𝐺)
123121, 122sseqtrri 4016 1 (𝑋𝑌) ⊆ 𝑍
Colors of variables: wff setvar class
Syntax hints:  wa 394   = wceq 1533  wcel 2098  wne 2929  cin 3945  wss 3946  cfv 6553  (class class class)co 7423  cc 11152  0cc0 11154  1c1 11155   · cmul 11159   / cdiv 11917  2c2 12314  chba 30844   + cva 30845   · csm 30846   cmv 30850   S csh 30853   C cch 30854  cort 30855   + cph 30856   chj 30858  projcpjh 30862
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5368  ax-pr 5432  ax-un 7745  ax-inf2 9680  ax-cc 10474  ax-cnex 11210  ax-resscn 11211  ax-1cn 11212  ax-icn 11213  ax-addcl 11214  ax-addrcl 11215  ax-mulcl 11216  ax-mulrcl 11217  ax-mulcom 11218  ax-addass 11219  ax-mulass 11220  ax-distr 11221  ax-i2m1 11222  ax-1ne0 11223  ax-1rid 11224  ax-rnegex 11225  ax-rrecex 11226  ax-cnre 11227  ax-pre-lttri 11228  ax-pre-lttrn 11229  ax-pre-ltadd 11230  ax-pre-mulgt0 11231  ax-pre-sup 11232  ax-addf 11233  ax-mulf 11234  ax-hilex 30924  ax-hfvadd 30925  ax-hvcom 30926  ax-hvass 30927  ax-hv0cl 30928  ax-hvaddid 30929  ax-hfvmul 30930  ax-hvmulid 30931  ax-hvmulass 30932  ax-hvdistr1 30933  ax-hvdistr2 30934  ax-hvmul0 30935  ax-hfi 31004  ax-his1 31007  ax-his2 31008  ax-his3 31009  ax-his4 31010  ax-hcompl 31127
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-iin 5003  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5579  df-eprel 5585  df-po 5593  df-so 5594  df-fr 5636  df-se 5637  df-we 5638  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-pred 6311  df-ord 6378  df-on 6379  df-lim 6380  df-suc 6381  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-isom 6562  df-riota 7379  df-ov 7426  df-oprab 7427  df-mpo 7428  df-of 7689  df-om 7876  df-1st 8002  df-2nd 8003  df-supp 8174  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-1o 8495  df-2o 8496  df-oadd 8499  df-omul 8500  df-er 8733  df-map 8856  df-pm 8857  df-ixp 8926  df-en 8974  df-dom 8975  df-sdom 8976  df-fin 8977  df-fsupp 9402  df-fi 9450  df-sup 9481  df-inf 9482  df-oi 9549  df-card 9978  df-acn 9981  df-pnf 11296  df-mnf 11297  df-xr 11298  df-ltxr 11299  df-le 11300  df-sub 11492  df-neg 11493  df-div 11918  df-nn 12260  df-2 12322  df-3 12323  df-4 12324  df-5 12325  df-6 12326  df-7 12327  df-8 12328  df-9 12329  df-n0 12520  df-z 12606  df-dec 12725  df-uz 12870  df-q 12980  df-rp 13024  df-xneg 13141  df-xadd 13142  df-xmul 13143  df-ioo 13377  df-ico 13379  df-icc 13380  df-fz 13534  df-fzo 13677  df-fl 13807  df-seq 14017  df-exp 14077  df-hash 14343  df-cj 15099  df-re 15100  df-im 15101  df-sqrt 15235  df-abs 15236  df-clim 15485  df-rlim 15486  df-sum 15686  df-struct 17144  df-sets 17161  df-slot 17179  df-ndx 17191  df-base 17209  df-ress 17238  df-plusg 17274  df-mulr 17275  df-starv 17276  df-sca 17277  df-vsca 17278  df-ip 17279  df-tset 17280  df-ple 17281  df-ds 17283  df-unif 17284  df-hom 17285  df-cco 17286  df-rest 17432  df-topn 17433  df-0g 17451  df-gsum 17452  df-topgen 17453  df-pt 17454  df-prds 17457  df-xrs 17512  df-qtop 17517  df-imas 17518  df-xps 17520  df-mre 17594  df-mrc 17595  df-acs 17597  df-mgm 18628  df-sgrp 18707  df-mnd 18723  df-submnd 18769  df-mulg 19057  df-cntz 19306  df-cmn 19775  df-psmet 21327  df-xmet 21328  df-met 21329  df-bl 21330  df-mopn 21331  df-fbas 21332  df-fg 21333  df-cnfld 21336  df-top 22879  df-topon 22896  df-topsp 22918  df-bases 22932  df-cld 23006  df-ntr 23007  df-cls 23008  df-nei 23085  df-cn 23214  df-cnp 23215  df-lm 23216  df-haus 23302  df-tx 23549  df-hmeo 23742  df-fil 23833  df-fm 23925  df-flim 23926  df-flf 23927  df-xms 24309  df-ms 24310  df-tms 24311  df-cfil 25266  df-cau 25267  df-cmet 25268  df-grpo 30418  df-gid 30419  df-ginv 30420  df-gdiv 30421  df-ablo 30470  df-vc 30484  df-nv 30517  df-va 30520  df-ba 30521  df-sm 30522  df-0v 30523  df-vs 30524  df-nmcv 30525  df-ims 30526  df-dip 30626  df-ssp 30647  df-ph 30738  df-cbn 30788  df-hnorm 30893  df-hba 30894  df-hvsub 30896  df-hlim 30897  df-hcau 30898  df-sh 31132  df-ch 31146  df-oc 31177  df-ch0 31178  df-shs 31233  df-chj 31235  df-pjh 31320
This theorem is referenced by:  mayetes3i  31654
  Copyright terms: Public domain W3C validator