Step | Hyp | Ref
| Expression |
1 | | ocval 28139 |
. . . 4
⊢ (𝐴 ⊆ ℋ →
(⊥‘𝐴) = {𝑥 ∈ ℋ ∣
∀𝑦 ∈ 𝐴 (𝑥 ·ih 𝑦) = 0}) |
2 | | ssrab2 3687 |
. . . 4
⊢ {𝑥 ∈ ℋ ∣
∀𝑦 ∈ 𝐴 (𝑥 ·ih 𝑦) = 0} ⊆
ℋ |
3 | 1, 2 | syl6eqss 3655 |
. . 3
⊢ (𝐴 ⊆ ℋ →
(⊥‘𝐴) ⊆
ℋ) |
4 | | ssel 3597 |
. . . . . . 7
⊢ (𝐴 ⊆ ℋ → (𝑦 ∈ 𝐴 → 𝑦 ∈ ℋ)) |
5 | | hi01 27953 |
. . . . . . 7
⊢ (𝑦 ∈ ℋ →
(0ℎ ·ih 𝑦) = 0) |
6 | 4, 5 | syl6 35 |
. . . . . 6
⊢ (𝐴 ⊆ ℋ → (𝑦 ∈ 𝐴 → (0ℎ
·ih 𝑦) = 0)) |
7 | 6 | ralrimiv 2965 |
. . . . 5
⊢ (𝐴 ⊆ ℋ →
∀𝑦 ∈ 𝐴 (0ℎ
·ih 𝑦) = 0) |
8 | | ax-hv0cl 27860 |
. . . . 5
⊢
0ℎ ∈ ℋ |
9 | 7, 8 | jctil 560 |
. . . 4
⊢ (𝐴 ⊆ ℋ →
(0ℎ ∈ ℋ ∧ ∀𝑦 ∈ 𝐴 (0ℎ
·ih 𝑦) = 0)) |
10 | | ocel 28140 |
. . . 4
⊢ (𝐴 ⊆ ℋ →
(0ℎ ∈ (⊥‘𝐴) ↔ (0ℎ ∈
ℋ ∧ ∀𝑦
∈ 𝐴
(0ℎ ·ih 𝑦) = 0))) |
11 | 9, 10 | mpbird 247 |
. . 3
⊢ (𝐴 ⊆ ℋ →
0ℎ ∈ (⊥‘𝐴)) |
12 | 3, 11 | jca 554 |
. 2
⊢ (𝐴 ⊆ ℋ →
((⊥‘𝐴) ⊆
ℋ ∧ 0ℎ ∈ (⊥‘𝐴))) |
13 | | ssel2 3598 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℋ ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℋ) |
14 | | ax-his2 27940 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑥 +ℎ 𝑦)
·ih 𝑧) = ((𝑥 ·ih 𝑧) + (𝑦 ·ih 𝑧))) |
15 | 14 | 3expa 1265 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → ((𝑥 +ℎ 𝑦)
·ih 𝑧) = ((𝑥 ·ih 𝑧) + (𝑦 ·ih 𝑧))) |
16 | | oveq12 6659 |
. . . . . . . . . . . . . 14
⊢ (((𝑥
·ih 𝑧) = 0 ∧ (𝑦 ·ih 𝑧) = 0) → ((𝑥
·ih 𝑧) + (𝑦 ·ih 𝑧)) = (0 + 0)) |
17 | | 00id 10211 |
. . . . . . . . . . . . . 14
⊢ (0 + 0) =
0 |
18 | 16, 17 | syl6eq 2672 |
. . . . . . . . . . . . 13
⊢ (((𝑥
·ih 𝑧) = 0 ∧ (𝑦 ·ih 𝑧) = 0) → ((𝑥
·ih 𝑧) + (𝑦 ·ih 𝑧)) = 0) |
19 | 15, 18 | sylan9eq 2676 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) ∧ ((𝑥
·ih 𝑧) = 0 ∧ (𝑦 ·ih 𝑧) = 0)) → ((𝑥 +ℎ 𝑦)
·ih 𝑧) = 0) |
20 | 19 | ex 450 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → (((𝑥
·ih 𝑧) = 0 ∧ (𝑦 ·ih 𝑧) = 0) → ((𝑥 +ℎ 𝑦)
·ih 𝑧) = 0)) |
21 | 20 | ancoms 469 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℋ ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) →
(((𝑥
·ih 𝑧) = 0 ∧ (𝑦 ·ih 𝑧) = 0) → ((𝑥 +ℎ 𝑦)
·ih 𝑧) = 0)) |
22 | 13, 21 | sylan 488 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℋ ∧ 𝑧 ∈ 𝐴) ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) → (((𝑥
·ih 𝑧) = 0 ∧ (𝑦 ·ih 𝑧) = 0) → ((𝑥 +ℎ 𝑦)
·ih 𝑧) = 0)) |
23 | 22 | an32s 846 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℋ ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ 𝐴) → (((𝑥 ·ih 𝑧) = 0 ∧ (𝑦 ·ih 𝑧) = 0) → ((𝑥 +ℎ 𝑦)
·ih 𝑧) = 0)) |
24 | 23 | ralimdva 2962 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℋ ∧ (𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ)) →
(∀𝑧 ∈ 𝐴 ((𝑥 ·ih 𝑧) = 0 ∧ (𝑦 ·ih 𝑧) = 0) → ∀𝑧 ∈ 𝐴 ((𝑥 +ℎ 𝑦) ·ih 𝑧) = 0)) |
25 | 24 | imdistanda 729 |
. . . . . 6
⊢ (𝐴 ⊆ ℋ → (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧
∀𝑧 ∈ 𝐴 ((𝑥 ·ih 𝑧) = 0 ∧ (𝑦 ·ih 𝑧) = 0)) → ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧
∀𝑧 ∈ 𝐴 ((𝑥 +ℎ 𝑦) ·ih 𝑧) = 0))) |
26 | | hvaddcl 27869 |
. . . . . . 7
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥 +ℎ 𝑦) ∈
ℋ) |
27 | 26 | anim1i 592 |
. . . . . 6
⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧
∀𝑧 ∈ 𝐴 ((𝑥 +ℎ 𝑦) ·ih 𝑧) = 0) → ((𝑥 +ℎ 𝑦) ∈ ℋ ∧
∀𝑧 ∈ 𝐴 ((𝑥 +ℎ 𝑦) ·ih 𝑧) = 0)) |
28 | 25, 27 | syl6 35 |
. . . . 5
⊢ (𝐴 ⊆ ℋ → (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧
∀𝑧 ∈ 𝐴 ((𝑥 ·ih 𝑧) = 0 ∧ (𝑦 ·ih 𝑧) = 0)) → ((𝑥 +ℎ 𝑦) ∈ ℋ ∧
∀𝑧 ∈ 𝐴 ((𝑥 +ℎ 𝑦) ·ih 𝑧) = 0))) |
29 | | ocel 28140 |
. . . . . . 7
⊢ (𝐴 ⊆ ℋ → (𝑥 ∈ (⊥‘𝐴) ↔ (𝑥 ∈ ℋ ∧ ∀𝑧 ∈ 𝐴 (𝑥 ·ih 𝑧) = 0))) |
30 | | ocel 28140 |
. . . . . . 7
⊢ (𝐴 ⊆ ℋ → (𝑦 ∈ (⊥‘𝐴) ↔ (𝑦 ∈ ℋ ∧ ∀𝑧 ∈ 𝐴 (𝑦 ·ih 𝑧) = 0))) |
31 | 29, 30 | anbi12d 747 |
. . . . . 6
⊢ (𝐴 ⊆ ℋ → ((𝑥 ∈ (⊥‘𝐴) ∧ 𝑦 ∈ (⊥‘𝐴)) ↔ ((𝑥 ∈ ℋ ∧ ∀𝑧 ∈ 𝐴 (𝑥 ·ih 𝑧) = 0) ∧ (𝑦 ∈ ℋ ∧ ∀𝑧 ∈ 𝐴 (𝑦 ·ih 𝑧) = 0)))) |
32 | | an4 865 |
. . . . . . 7
⊢ (((𝑥 ∈ ℋ ∧
∀𝑧 ∈ 𝐴 (𝑥 ·ih 𝑧) = 0) ∧ (𝑦 ∈ ℋ ∧ ∀𝑧 ∈ 𝐴 (𝑦 ·ih 𝑧) = 0)) ↔ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧
(∀𝑧 ∈ 𝐴 (𝑥 ·ih 𝑧) = 0 ∧ ∀𝑧 ∈ 𝐴 (𝑦 ·ih 𝑧) = 0))) |
33 | | r19.26 3064 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝐴 ((𝑥 ·ih 𝑧) = 0 ∧ (𝑦 ·ih 𝑧) = 0) ↔ (∀𝑧 ∈ 𝐴 (𝑥 ·ih 𝑧) = 0 ∧ ∀𝑧 ∈ 𝐴 (𝑦 ·ih 𝑧) = 0)) |
34 | 33 | anbi2i 730 |
. . . . . . 7
⊢ (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧
∀𝑧 ∈ 𝐴 ((𝑥 ·ih 𝑧) = 0 ∧ (𝑦 ·ih 𝑧) = 0)) ↔ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧
(∀𝑧 ∈ 𝐴 (𝑥 ·ih 𝑧) = 0 ∧ ∀𝑧 ∈ 𝐴 (𝑦 ·ih 𝑧) = 0))) |
35 | 32, 34 | bitr4i 267 |
. . . . . 6
⊢ (((𝑥 ∈ ℋ ∧
∀𝑧 ∈ 𝐴 (𝑥 ·ih 𝑧) = 0) ∧ (𝑦 ∈ ℋ ∧ ∀𝑧 ∈ 𝐴 (𝑦 ·ih 𝑧) = 0)) ↔ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧
∀𝑧 ∈ 𝐴 ((𝑥 ·ih 𝑧) = 0 ∧ (𝑦 ·ih 𝑧) = 0))) |
36 | 31, 35 | syl6bb 276 |
. . . . 5
⊢ (𝐴 ⊆ ℋ → ((𝑥 ∈ (⊥‘𝐴) ∧ 𝑦 ∈ (⊥‘𝐴)) ↔ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ ∀𝑧 ∈ 𝐴 ((𝑥 ·ih 𝑧) = 0 ∧ (𝑦 ·ih 𝑧) = 0)))) |
37 | | ocel 28140 |
. . . . 5
⊢ (𝐴 ⊆ ℋ → ((𝑥 +ℎ 𝑦) ∈ (⊥‘𝐴) ↔ ((𝑥 +ℎ 𝑦) ∈ ℋ ∧ ∀𝑧 ∈ 𝐴 ((𝑥 +ℎ 𝑦) ·ih 𝑧) = 0))) |
38 | 28, 36, 37 | 3imtr4d 283 |
. . . 4
⊢ (𝐴 ⊆ ℋ → ((𝑥 ∈ (⊥‘𝐴) ∧ 𝑦 ∈ (⊥‘𝐴)) → (𝑥 +ℎ 𝑦) ∈ (⊥‘𝐴))) |
39 | 38 | ralrimivv 2970 |
. . 3
⊢ (𝐴 ⊆ ℋ →
∀𝑥 ∈
(⊥‘𝐴)∀𝑦 ∈ (⊥‘𝐴)(𝑥 +ℎ 𝑦) ∈ (⊥‘𝐴)) |
40 | | mul01 10215 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℂ → (𝑥 · 0) =
0) |
41 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ ((𝑦
·ih 𝑧) = 0 → (𝑥 · (𝑦 ·ih 𝑧)) = (𝑥 · 0)) |
42 | 41 | eqeq1d 2624 |
. . . . . . . . . . . . 13
⊢ ((𝑦
·ih 𝑧) = 0 → ((𝑥 · (𝑦 ·ih 𝑧)) = 0 ↔ (𝑥 · 0) =
0)) |
43 | 40, 42 | syl5ibrcom 237 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℂ → ((𝑦
·ih 𝑧) = 0 → (𝑥 · (𝑦 ·ih 𝑧)) = 0)) |
44 | 43 | ad2antrl 764 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) → ((𝑦
·ih 𝑧) = 0 → (𝑥 · (𝑦 ·ih 𝑧)) = 0)) |
45 | | ax-his3 27941 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑥
·ℎ 𝑦) ·ih 𝑧) = (𝑥 · (𝑦 ·ih 𝑧))) |
46 | 45 | eqeq1d 2624 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (((𝑥
·ℎ 𝑦) ·ih 𝑧) = 0 ↔ (𝑥 · (𝑦 ·ih 𝑧)) = 0)) |
47 | 46 | 3expa 1265 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ 𝑧 ∈ ℋ) → (((𝑥
·ℎ 𝑦) ·ih 𝑧) = 0 ↔ (𝑥 · (𝑦 ·ih 𝑧)) = 0)) |
48 | 47 | ancoms 469 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) →
(((𝑥
·ℎ 𝑦) ·ih 𝑧) = 0 ↔ (𝑥 · (𝑦 ·ih 𝑧)) = 0)) |
49 | 44, 48 | sylibrd 249 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) → ((𝑦
·ih 𝑧) = 0 → ((𝑥 ·ℎ 𝑦)
·ih 𝑧) = 0)) |
50 | 13, 49 | sylan 488 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℋ ∧ 𝑧 ∈ 𝐴) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) → ((𝑦 ·ih 𝑧) = 0 → ((𝑥
·ℎ 𝑦) ·ih 𝑧) = 0)) |
51 | 50 | an32s 846 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) ∧ 𝑧 ∈ 𝐴) → ((𝑦 ·ih 𝑧) = 0 → ((𝑥
·ℎ 𝑦) ·ih 𝑧) = 0)) |
52 | 51 | ralimdva 2962 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℋ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ)) →
(∀𝑧 ∈ 𝐴 (𝑦 ·ih 𝑧) = 0 → ∀𝑧 ∈ 𝐴 ((𝑥 ·ℎ 𝑦)
·ih 𝑧) = 0)) |
53 | 52 | imdistanda 729 |
. . . . . 6
⊢ (𝐴 ⊆ ℋ → (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧
∀𝑧 ∈ 𝐴 (𝑦 ·ih 𝑧) = 0) → ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧
∀𝑧 ∈ 𝐴 ((𝑥 ·ℎ 𝑦)
·ih 𝑧) = 0))) |
54 | | hvmulcl 27870 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) → (𝑥
·ℎ 𝑦) ∈ ℋ) |
55 | 54 | anim1i 592 |
. . . . . 6
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧
∀𝑧 ∈ 𝐴 ((𝑥 ·ℎ 𝑦)
·ih 𝑧) = 0) → ((𝑥 ·ℎ 𝑦) ∈ ℋ ∧
∀𝑧 ∈ 𝐴 ((𝑥 ·ℎ 𝑦)
·ih 𝑧) = 0)) |
56 | 53, 55 | syl6 35 |
. . . . 5
⊢ (𝐴 ⊆ ℋ → (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧
∀𝑧 ∈ 𝐴 (𝑦 ·ih 𝑧) = 0) → ((𝑥
·ℎ 𝑦) ∈ ℋ ∧ ∀𝑧 ∈ 𝐴 ((𝑥 ·ℎ 𝑦)
·ih 𝑧) = 0))) |
57 | 30 | anbi2d 740 |
. . . . . 6
⊢ (𝐴 ⊆ ℋ → ((𝑥 ∈ ℂ ∧ 𝑦 ∈ (⊥‘𝐴)) ↔ (𝑥 ∈ ℂ ∧ (𝑦 ∈ ℋ ∧ ∀𝑧 ∈ 𝐴 (𝑦 ·ih 𝑧) = 0)))) |
58 | | anass 681 |
. . . . . 6
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧
∀𝑧 ∈ 𝐴 (𝑦 ·ih 𝑧) = 0) ↔ (𝑥 ∈ ℂ ∧ (𝑦 ∈ ℋ ∧
∀𝑧 ∈ 𝐴 (𝑦 ·ih 𝑧) = 0))) |
59 | 57, 58 | syl6bbr 278 |
. . . . 5
⊢ (𝐴 ⊆ ℋ → ((𝑥 ∈ ℂ ∧ 𝑦 ∈ (⊥‘𝐴)) ↔ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ) ∧ ∀𝑧 ∈ 𝐴 (𝑦 ·ih 𝑧) = 0))) |
60 | | ocel 28140 |
. . . . 5
⊢ (𝐴 ⊆ ℋ → ((𝑥
·ℎ 𝑦) ∈ (⊥‘𝐴) ↔ ((𝑥 ·ℎ 𝑦) ∈ ℋ ∧
∀𝑧 ∈ 𝐴 ((𝑥 ·ℎ 𝑦)
·ih 𝑧) = 0))) |
61 | 56, 59, 60 | 3imtr4d 283 |
. . . 4
⊢ (𝐴 ⊆ ℋ → ((𝑥 ∈ ℂ ∧ 𝑦 ∈ (⊥‘𝐴)) → (𝑥 ·ℎ 𝑦) ∈ (⊥‘𝐴))) |
62 | 61 | ralrimivv 2970 |
. . 3
⊢ (𝐴 ⊆ ℋ →
∀𝑥 ∈ ℂ
∀𝑦 ∈
(⊥‘𝐴)(𝑥
·ℎ 𝑦) ∈ (⊥‘𝐴)) |
63 | 39, 62 | jca 554 |
. 2
⊢ (𝐴 ⊆ ℋ →
(∀𝑥 ∈
(⊥‘𝐴)∀𝑦 ∈ (⊥‘𝐴)(𝑥 +ℎ 𝑦) ∈ (⊥‘𝐴) ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ (⊥‘𝐴)(𝑥 ·ℎ 𝑦) ∈ (⊥‘𝐴))) |
64 | | issh2 28066 |
. 2
⊢
((⊥‘𝐴)
∈ Sℋ ↔ (((⊥‘𝐴) ⊆ ℋ ∧
0ℎ ∈ (⊥‘𝐴)) ∧ (∀𝑥 ∈ (⊥‘𝐴)∀𝑦 ∈ (⊥‘𝐴)(𝑥 +ℎ 𝑦) ∈ (⊥‘𝐴) ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ (⊥‘𝐴)(𝑥 ·ℎ 𝑦) ∈ (⊥‘𝐴)))) |
65 | 12, 63, 64 | sylanbrc 698 |
1
⊢ (𝐴 ⊆ ℋ →
(⊥‘𝐴) ∈
Sℋ ) |