Step | Hyp | Ref
| Expression |
1 | | shscl.1 |
. . . 4
⊢ 𝐴 ∈
Sℋ |
2 | | shscl.2 |
. . . 4
⊢ 𝐵 ∈
Sℋ |
3 | | shsss 29260 |
. . . 4
⊢ ((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
→ (𝐴
+ℋ 𝐵)
⊆ ℋ) |
4 | 1, 2, 3 | mp2an 692 |
. . 3
⊢ (𝐴 +ℋ 𝐵) ⊆
ℋ |
5 | | sh0 29163 |
. . . . . 6
⊢ (𝐴 ∈
Sℋ → 0ℎ ∈ 𝐴) |
6 | 1, 5 | ax-mp 5 |
. . . . 5
⊢
0ℎ ∈ 𝐴 |
7 | | sh0 29163 |
. . . . . 6
⊢ (𝐵 ∈
Sℋ → 0ℎ ∈ 𝐵) |
8 | 2, 7 | ax-mp 5 |
. . . . 5
⊢
0ℎ ∈ 𝐵 |
9 | | ax-hv0cl 28950 |
. . . . . . 7
⊢
0ℎ ∈ ℋ |
10 | 9 | hvaddid2i 28976 |
. . . . . 6
⊢
(0ℎ +ℎ 0ℎ) =
0ℎ |
11 | 10 | eqcomi 2748 |
. . . . 5
⊢
0ℎ = (0ℎ +ℎ
0ℎ) |
12 | | rspceov 7229 |
. . . . 5
⊢
((0ℎ ∈ 𝐴 ∧ 0ℎ ∈ 𝐵 ∧ 0ℎ =
(0ℎ +ℎ 0ℎ)) →
∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 0ℎ = (𝑥 +ℎ 𝑦)) |
13 | 6, 8, 11, 12 | mp3an 1462 |
. . . 4
⊢
∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 0ℎ = (𝑥 +ℎ 𝑦) |
14 | 1, 2 | shseli 29263 |
. . . 4
⊢
(0ℎ ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 0ℎ = (𝑥 +ℎ 𝑦)) |
15 | 13, 14 | mpbir 234 |
. . 3
⊢
0ℎ ∈ (𝐴 +ℋ 𝐵) |
16 | 4, 15 | pm3.2i 474 |
. 2
⊢ ((𝐴 +ℋ 𝐵) ⊆ ℋ ∧
0ℎ ∈ (𝐴 +ℋ 𝐵)) |
17 | 1, 2 | shseli 29263 |
. . . . . 6
⊢ (𝑥 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤)) |
18 | 1, 2 | shseli 29263 |
. . . . . 6
⊢ (𝑦 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑣 ∈ 𝐴 ∃𝑢 ∈ 𝐵 𝑦 = (𝑣 +ℎ 𝑢)) |
19 | | shaddcl 29164 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈
Sℋ ∧ 𝑧 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → (𝑧 +ℎ 𝑣) ∈ 𝐴) |
20 | 1, 19 | mp3an1 1449 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → (𝑧 +ℎ 𝑣) ∈ 𝐴) |
21 | 20 | ad2ant2r 747 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ (𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵)) → (𝑧 +ℎ 𝑣) ∈ 𝐴) |
22 | 21 | ad2ant2r 747 |
. . . . . . . . . . . . 13
⊢ ((((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑥 = (𝑧 +ℎ 𝑤)) ∧ ((𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ 𝑦 = (𝑣 +ℎ 𝑢))) → (𝑧 +ℎ 𝑣) ∈ 𝐴) |
23 | | shaddcl 29164 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈
Sℋ ∧ 𝑤 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵) → (𝑤 +ℎ 𝑢) ∈ 𝐵) |
24 | 2, 23 | mp3an1 1449 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵) → (𝑤 +ℎ 𝑢) ∈ 𝐵) |
25 | 24 | ad2ant2l 746 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ (𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵)) → (𝑤 +ℎ 𝑢) ∈ 𝐵) |
26 | 25 | ad2ant2r 747 |
. . . . . . . . . . . . 13
⊢ ((((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑥 = (𝑧 +ℎ 𝑤)) ∧ ((𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ 𝑦 = (𝑣 +ℎ 𝑢))) → (𝑤 +ℎ 𝑢) ∈ 𝐵) |
27 | | oveq12 7191 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = (𝑧 +ℎ 𝑤) ∧ 𝑦 = (𝑣 +ℎ 𝑢)) → (𝑥 +ℎ 𝑦) = ((𝑧 +ℎ 𝑤) +ℎ (𝑣 +ℎ 𝑢))) |
28 | 27 | ad2ant2l 746 |
. . . . . . . . . . . . . 14
⊢ ((((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑥 = (𝑧 +ℎ 𝑤)) ∧ ((𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ 𝑦 = (𝑣 +ℎ 𝑢))) → (𝑥 +ℎ 𝑦) = ((𝑧 +ℎ 𝑤) +ℎ (𝑣 +ℎ 𝑢))) |
29 | 1 | sheli 29161 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ 𝐴 → 𝑧 ∈ ℋ) |
30 | 1 | sheli 29161 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∈ 𝐴 → 𝑣 ∈ ℋ) |
31 | 29, 30 | anim12i 616 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → (𝑧 ∈ ℋ ∧ 𝑣 ∈ ℋ)) |
32 | 2 | sheli 29161 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ 𝐵 → 𝑤 ∈ ℋ) |
33 | 2 | sheli 29161 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ 𝐵 → 𝑢 ∈ ℋ) |
34 | 32, 33 | anim12i 616 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵) → (𝑤 ∈ ℋ ∧ 𝑢 ∈ ℋ)) |
35 | | hvadd4 28983 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑧 ∈ ℋ ∧ 𝑣 ∈ ℋ) ∧ (𝑤 ∈ ℋ ∧ 𝑢 ∈ ℋ)) → ((𝑧 +ℎ 𝑣) +ℎ (𝑤 +ℎ 𝑢)) = ((𝑧 +ℎ 𝑤) +ℎ (𝑣 +ℎ 𝑢))) |
36 | 31, 34, 35 | syl2an 599 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑧 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (𝑤 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)) → ((𝑧 +ℎ 𝑣) +ℎ (𝑤 +ℎ 𝑢)) = ((𝑧 +ℎ 𝑤) +ℎ (𝑣 +ℎ 𝑢))) |
37 | 36 | an4s 660 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ (𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵)) → ((𝑧 +ℎ 𝑣) +ℎ (𝑤 +ℎ 𝑢)) = ((𝑧 +ℎ 𝑤) +ℎ (𝑣 +ℎ 𝑢))) |
38 | 37 | ad2ant2r 747 |
. . . . . . . . . . . . . 14
⊢ ((((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑥 = (𝑧 +ℎ 𝑤)) ∧ ((𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ 𝑦 = (𝑣 +ℎ 𝑢))) → ((𝑧 +ℎ 𝑣) +ℎ (𝑤 +ℎ 𝑢)) = ((𝑧 +ℎ 𝑤) +ℎ (𝑣 +ℎ 𝑢))) |
39 | 28, 38 | eqtr4d 2777 |
. . . . . . . . . . . . 13
⊢ ((((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑥 = (𝑧 +ℎ 𝑤)) ∧ ((𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ 𝑦 = (𝑣 +ℎ 𝑢))) → (𝑥 +ℎ 𝑦) = ((𝑧 +ℎ 𝑣) +ℎ (𝑤 +ℎ 𝑢))) |
40 | | rspceov 7229 |
. . . . . . . . . . . . 13
⊢ (((𝑧 +ℎ 𝑣) ∈ 𝐴 ∧ (𝑤 +ℎ 𝑢) ∈ 𝐵 ∧ (𝑥 +ℎ 𝑦) = ((𝑧 +ℎ 𝑣) +ℎ (𝑤 +ℎ 𝑢))) → ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑥 +ℎ 𝑦) = (𝑓 +ℎ 𝑔)) |
41 | 22, 26, 39, 40 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ ((((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑥 = (𝑧 +ℎ 𝑤)) ∧ ((𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ 𝑦 = (𝑣 +ℎ 𝑢))) → ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑥 +ℎ 𝑦) = (𝑓 +ℎ 𝑔)) |
42 | 41 | ancoms 462 |
. . . . . . . . . . 11
⊢ ((((𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ 𝑦 = (𝑣 +ℎ 𝑢)) ∧ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑥 = (𝑧 +ℎ 𝑤))) → ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑥 +ℎ 𝑦) = (𝑓 +ℎ 𝑔)) |
43 | 42 | exp43 440 |
. . . . . . . . . 10
⊢ ((𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) → (𝑦 = (𝑣 +ℎ 𝑢) → ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → (𝑥 = (𝑧 +ℎ 𝑤) → ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑥 +ℎ 𝑦) = (𝑓 +ℎ 𝑔))))) |
44 | 43 | rexlimivv 3203 |
. . . . . . . . 9
⊢
(∃𝑣 ∈
𝐴 ∃𝑢 ∈ 𝐵 𝑦 = (𝑣 +ℎ 𝑢) → ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → (𝑥 = (𝑧 +ℎ 𝑤) → ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑥 +ℎ 𝑦) = (𝑓 +ℎ 𝑔)))) |
45 | 44 | com3l 89 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → (𝑥 = (𝑧 +ℎ 𝑤) → (∃𝑣 ∈ 𝐴 ∃𝑢 ∈ 𝐵 𝑦 = (𝑣 +ℎ 𝑢) → ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑥 +ℎ 𝑦) = (𝑓 +ℎ 𝑔)))) |
46 | 45 | rexlimivv 3203 |
. . . . . . 7
⊢
(∃𝑧 ∈
𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤) → (∃𝑣 ∈ 𝐴 ∃𝑢 ∈ 𝐵 𝑦 = (𝑣 +ℎ 𝑢) → ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑥 +ℎ 𝑦) = (𝑓 +ℎ 𝑔))) |
47 | 46 | imp 410 |
. . . . . 6
⊢
((∃𝑧 ∈
𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤) ∧ ∃𝑣 ∈ 𝐴 ∃𝑢 ∈ 𝐵 𝑦 = (𝑣 +ℎ 𝑢)) → ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑥 +ℎ 𝑦) = (𝑓 +ℎ 𝑔)) |
48 | 17, 18, 47 | syl2anb 601 |
. . . . 5
⊢ ((𝑥 ∈ (𝐴 +ℋ 𝐵) ∧ 𝑦 ∈ (𝐴 +ℋ 𝐵)) → ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑥 +ℎ 𝑦) = (𝑓 +ℎ 𝑔)) |
49 | 1, 2 | shseli 29263 |
. . . . 5
⊢ ((𝑥 +ℎ 𝑦) ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑥 +ℎ 𝑦) = (𝑓 +ℎ 𝑔)) |
50 | 48, 49 | sylibr 237 |
. . . 4
⊢ ((𝑥 ∈ (𝐴 +ℋ 𝐵) ∧ 𝑦 ∈ (𝐴 +ℋ 𝐵)) → (𝑥 +ℎ 𝑦) ∈ (𝐴 +ℋ 𝐵)) |
51 | 50 | rgen2 3116 |
. . 3
⊢
∀𝑥 ∈
(𝐴 +ℋ
𝐵)∀𝑦 ∈ (𝐴 +ℋ 𝐵)(𝑥 +ℎ 𝑦) ∈ (𝐴 +ℋ 𝐵) |
52 | | shmulcl 29165 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
Sℋ ∧ 𝑥 ∈ ℂ ∧ 𝑣 ∈ 𝐴) → (𝑥 ·ℎ 𝑣) ∈ 𝐴) |
53 | 1, 52 | mp3an1 1449 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ 𝑣 ∈ 𝐴) → (𝑥 ·ℎ 𝑣) ∈ 𝐴) |
54 | 53 | adantrr 717 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ (𝑣 ∈ 𝐴 ∧ (𝑢 ∈ 𝐵 ∧ 𝑦 = (𝑣 +ℎ 𝑢)))) → (𝑥 ·ℎ 𝑣) ∈ 𝐴) |
55 | | shmulcl 29165 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈
Sℋ ∧ 𝑥 ∈ ℂ ∧ 𝑢 ∈ 𝐵) → (𝑥 ·ℎ 𝑢) ∈ 𝐵) |
56 | 2, 55 | mp3an1 1449 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧ 𝑢 ∈ 𝐵) → (𝑥 ·ℎ 𝑢) ∈ 𝐵) |
57 | 56 | adantrr 717 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ (𝑢 ∈ 𝐵 ∧ 𝑦 = (𝑣 +ℎ 𝑢))) → (𝑥 ·ℎ 𝑢) ∈ 𝐵) |
58 | 57 | adantrl 716 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ (𝑣 ∈ 𝐴 ∧ (𝑢 ∈ 𝐵 ∧ 𝑦 = (𝑣 +ℎ 𝑢)))) → (𝑥 ·ℎ 𝑢) ∈ 𝐵) |
59 | | oveq2 7190 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑣 +ℎ 𝑢) → (𝑥 ·ℎ 𝑦) = (𝑥 ·ℎ (𝑣 +ℎ 𝑢))) |
60 | 59 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝐵 ∧ 𝑦 = (𝑣 +ℎ 𝑢)) → (𝑥 ·ℎ 𝑦) = (𝑥 ·ℎ (𝑣 +ℎ 𝑢))) |
61 | 60 | ad2antll 729 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ (𝑣 ∈ 𝐴 ∧ (𝑢 ∈ 𝐵 ∧ 𝑦 = (𝑣 +ℎ 𝑢)))) → (𝑥 ·ℎ 𝑦) = (𝑥 ·ℎ (𝑣 +ℎ 𝑢))) |
62 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → 𝑥 ∈
ℂ) |
63 | | ax-hvdistr1 28955 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ 𝑣 ∈ ℋ ∧ 𝑢 ∈ ℋ) → (𝑥
·ℎ (𝑣 +ℎ 𝑢)) = ((𝑥 ·ℎ 𝑣) +ℎ (𝑥
·ℎ 𝑢))) |
64 | 62, 30, 33, 63 | syl3an 1161 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ 𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) → (𝑥 ·ℎ (𝑣 +ℎ 𝑢)) = ((𝑥 ·ℎ 𝑣) +ℎ (𝑥
·ℎ 𝑢))) |
65 | 64 | 3expb 1121 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧ (𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵)) → (𝑥 ·ℎ (𝑣 +ℎ 𝑢)) = ((𝑥 ·ℎ 𝑣) +ℎ (𝑥
·ℎ 𝑢))) |
66 | 65 | adantrrr 725 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ (𝑣 ∈ 𝐴 ∧ (𝑢 ∈ 𝐵 ∧ 𝑦 = (𝑣 +ℎ 𝑢)))) → (𝑥 ·ℎ (𝑣 +ℎ 𝑢)) = ((𝑥 ·ℎ 𝑣) +ℎ (𝑥
·ℎ 𝑢))) |
67 | 61, 66 | eqtrd 2774 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ (𝑣 ∈ 𝐴 ∧ (𝑢 ∈ 𝐵 ∧ 𝑦 = (𝑣 +ℎ 𝑢)))) → (𝑥 ·ℎ 𝑦) = ((𝑥 ·ℎ 𝑣) +ℎ (𝑥
·ℎ 𝑢))) |
68 | | rspceov 7229 |
. . . . . . . . . . . 12
⊢ (((𝑥
·ℎ 𝑣) ∈ 𝐴 ∧ (𝑥 ·ℎ 𝑢) ∈ 𝐵 ∧ (𝑥 ·ℎ 𝑦) = ((𝑥 ·ℎ 𝑣) +ℎ (𝑥
·ℎ 𝑢))) → ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑥 ·ℎ 𝑦) = (𝑓 +ℎ 𝑔)) |
69 | 54, 58, 67, 68 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ (𝑣 ∈ 𝐴 ∧ (𝑢 ∈ 𝐵 ∧ 𝑦 = (𝑣 +ℎ 𝑢)))) → ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑥 ·ℎ 𝑦) = (𝑓 +ℎ 𝑔)) |
70 | 69 | ancoms 462 |
. . . . . . . . . 10
⊢ (((𝑣 ∈ 𝐴 ∧ (𝑢 ∈ 𝐵 ∧ 𝑦 = (𝑣 +ℎ 𝑢))) ∧ 𝑥 ∈ ℂ) → ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑥 ·ℎ 𝑦) = (𝑓 +ℎ 𝑔)) |
71 | 70 | exp42 439 |
. . . . . . . . 9
⊢ (𝑣 ∈ 𝐴 → (𝑢 ∈ 𝐵 → (𝑦 = (𝑣 +ℎ 𝑢) → (𝑥 ∈ ℂ → ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑥 ·ℎ 𝑦) = (𝑓 +ℎ 𝑔))))) |
72 | 71 | imp 410 |
. . . . . . . 8
⊢ ((𝑣 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) → (𝑦 = (𝑣 +ℎ 𝑢) → (𝑥 ∈ ℂ → ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑥 ·ℎ 𝑦) = (𝑓 +ℎ 𝑔)))) |
73 | 72 | rexlimivv 3203 |
. . . . . . 7
⊢
(∃𝑣 ∈
𝐴 ∃𝑢 ∈ 𝐵 𝑦 = (𝑣 +ℎ 𝑢) → (𝑥 ∈ ℂ → ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑥 ·ℎ 𝑦) = (𝑓 +ℎ 𝑔))) |
74 | 73 | impcom 411 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧
∃𝑣 ∈ 𝐴 ∃𝑢 ∈ 𝐵 𝑦 = (𝑣 +ℎ 𝑢)) → ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑥 ·ℎ 𝑦) = (𝑓 +ℎ 𝑔)) |
75 | 18, 74 | sylan2b 597 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ (𝐴 +ℋ 𝐵)) → ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑥 ·ℎ 𝑦) = (𝑓 +ℎ 𝑔)) |
76 | 1, 2 | shseli 29263 |
. . . . 5
⊢ ((𝑥
·ℎ 𝑦) ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑥 ·ℎ 𝑦) = (𝑓 +ℎ 𝑔)) |
77 | 75, 76 | sylibr 237 |
. . . 4
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ (𝐴 +ℋ 𝐵)) → (𝑥 ·ℎ 𝑦) ∈ (𝐴 +ℋ 𝐵)) |
78 | 77 | rgen2 3116 |
. . 3
⊢
∀𝑥 ∈
ℂ ∀𝑦 ∈
(𝐴 +ℋ
𝐵)(𝑥 ·ℎ 𝑦) ∈ (𝐴 +ℋ 𝐵) |
79 | 51, 78 | pm3.2i 474 |
. 2
⊢
(∀𝑥 ∈
(𝐴 +ℋ
𝐵)∀𝑦 ∈ (𝐴 +ℋ 𝐵)(𝑥 +ℎ 𝑦) ∈ (𝐴 +ℋ 𝐵) ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ (𝐴 +ℋ 𝐵)(𝑥 ·ℎ 𝑦) ∈ (𝐴 +ℋ 𝐵)) |
80 | | issh2 29156 |
. 2
⊢ ((𝐴 +ℋ 𝐵) ∈
Sℋ ↔ (((𝐴 +ℋ 𝐵) ⊆ ℋ ∧ 0ℎ
∈ (𝐴
+ℋ 𝐵))
∧ (∀𝑥 ∈
(𝐴 +ℋ
𝐵)∀𝑦 ∈ (𝐴 +ℋ 𝐵)(𝑥 +ℎ 𝑦) ∈ (𝐴 +ℋ 𝐵) ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ (𝐴 +ℋ 𝐵)(𝑥 ·ℎ 𝑦) ∈ (𝐴 +ℋ 𝐵)))) |
81 | 16, 79, 80 | mpbir2an 711 |
1
⊢ (𝐴 +ℋ 𝐵) ∈
Sℋ |