Step | Hyp | Ref
| Expression |
1 | | hhssnv.2 |
. . . . 5
⊢ 𝐻 ∈
Sℋ |
2 | 1 | hhssabloi 29343 |
. . . 4
⊢ (
+ℎ ↾ (𝐻 × 𝐻)) ∈ AbelOp |
3 | | ablogrpo 28628 |
. . . 4
⊢ ((
+ℎ ↾ (𝐻 × 𝐻)) ∈ AbelOp → (
+ℎ ↾ (𝐻 × 𝐻)) ∈ GrpOp) |
4 | 2, 3 | ax-mp 5 |
. . 3
⊢ (
+ℎ ↾ (𝐻 × 𝐻)) ∈ GrpOp |
5 | 1 | shssii 29294 |
. . . . . 6
⊢ 𝐻 ⊆
ℋ |
6 | | xpss12 5566 |
. . . . . 6
⊢ ((𝐻 ⊆ ℋ ∧ 𝐻 ⊆ ℋ) → (𝐻 × 𝐻) ⊆ ( ℋ ×
ℋ)) |
7 | 5, 5, 6 | mp2an 692 |
. . . . 5
⊢ (𝐻 × 𝐻) ⊆ ( ℋ ×
ℋ) |
8 | | ax-hfvadd 29081 |
. . . . . 6
⊢
+ℎ :( ℋ × ℋ)⟶
ℋ |
9 | 8 | fdmi 6557 |
. . . . 5
⊢ dom
+ℎ = ( ℋ × ℋ) |
10 | 7, 9 | sseqtrri 3938 |
. . . 4
⊢ (𝐻 × 𝐻) ⊆ dom
+ℎ |
11 | | ssdmres 5874 |
. . . 4
⊢ ((𝐻 × 𝐻) ⊆ dom +ℎ ↔
dom ( +ℎ ↾ (𝐻 × 𝐻)) = (𝐻 × 𝐻)) |
12 | 10, 11 | mpbi 233 |
. . 3
⊢ dom (
+ℎ ↾ (𝐻 × 𝐻)) = (𝐻 × 𝐻) |
13 | 4, 12 | grporn 28602 |
. 2
⊢ 𝐻 = ran ( +ℎ
↾ (𝐻 × 𝐻)) |
14 | | sh0 29297 |
. . . . . 6
⊢ (𝐻 ∈
Sℋ → 0ℎ ∈ 𝐻) |
15 | 1, 14 | ax-mp 5 |
. . . . 5
⊢
0ℎ ∈ 𝐻 |
16 | | ovres 7374 |
. . . . 5
⊢
((0ℎ ∈ 𝐻 ∧ 0ℎ ∈ 𝐻) → (0ℎ(
+ℎ ↾ (𝐻 × 𝐻))0ℎ) =
(0ℎ +ℎ
0ℎ)) |
17 | 15, 15, 16 | mp2an 692 |
. . . 4
⊢
(0ℎ( +ℎ ↾ (𝐻 × 𝐻))0ℎ) =
(0ℎ +ℎ
0ℎ) |
18 | | ax-hv0cl 29084 |
. . . . 5
⊢
0ℎ ∈ ℋ |
19 | 18 | hvaddid2i 29110 |
. . . 4
⊢
(0ℎ +ℎ 0ℎ) =
0ℎ |
20 | 17, 19 | eqtri 2765 |
. . 3
⊢
(0ℎ( +ℎ ↾ (𝐻 × 𝐻))0ℎ) =
0ℎ |
21 | | eqid 2737 |
. . . . 5
⊢
(GId‘( +ℎ ↾ (𝐻 × 𝐻))) = (GId‘( +ℎ
↾ (𝐻 × 𝐻))) |
22 | 13, 21 | grpoid 28601 |
. . . 4
⊢ (((
+ℎ ↾ (𝐻 × 𝐻)) ∈ GrpOp ∧ 0ℎ
∈ 𝐻) →
(0ℎ = (GId‘( +ℎ ↾ (𝐻 × 𝐻))) ↔ (0ℎ(
+ℎ ↾ (𝐻 × 𝐻))0ℎ) =
0ℎ)) |
23 | 4, 15, 22 | mp2an 692 |
. . 3
⊢
(0ℎ = (GId‘( +ℎ ↾ (𝐻 × 𝐻))) ↔ (0ℎ(
+ℎ ↾ (𝐻 × 𝐻))0ℎ) =
0ℎ) |
24 | 20, 23 | mpbir 234 |
. 2
⊢
0ℎ = (GId‘( +ℎ ↾ (𝐻 × 𝐻))) |
25 | | ax-hfvmul 29086 |
. . . . . 6
⊢
·ℎ :(ℂ × ℋ)⟶
ℋ |
26 | | ffn 6545 |
. . . . . 6
⊢ (
·ℎ :(ℂ × ℋ)⟶ ℋ
→ ·ℎ Fn (ℂ ×
ℋ)) |
27 | 25, 26 | ax-mp 5 |
. . . . 5
⊢
·ℎ Fn (ℂ ×
ℋ) |
28 | | ssid 3923 |
. . . . . 6
⊢ ℂ
⊆ ℂ |
29 | | xpss12 5566 |
. . . . . 6
⊢ ((ℂ
⊆ ℂ ∧ 𝐻
⊆ ℋ) → (ℂ × 𝐻) ⊆ (ℂ ×
ℋ)) |
30 | 28, 5, 29 | mp2an 692 |
. . . . 5
⊢ (ℂ
× 𝐻) ⊆ (ℂ
× ℋ) |
31 | | fnssres 6500 |
. . . . 5
⊢ ((
·ℎ Fn (ℂ × ℋ) ∧ (ℂ
× 𝐻) ⊆ (ℂ
× ℋ)) → ( ·ℎ ↾ (ℂ
× 𝐻)) Fn (ℂ
× 𝐻)) |
32 | 27, 30, 31 | mp2an 692 |
. . . 4
⊢ (
·ℎ ↾ (ℂ × 𝐻)) Fn (ℂ × 𝐻) |
33 | | ovelrn 7384 |
. . . . . . 7
⊢ ((
·ℎ ↾ (ℂ × 𝐻)) Fn (ℂ × 𝐻) → (𝑧 ∈ ran (
·ℎ ↾ (ℂ × 𝐻)) ↔ ∃𝑥 ∈ ℂ ∃𝑦 ∈ 𝐻 𝑧 = (𝑥( ·ℎ ↾
(ℂ × 𝐻))𝑦))) |
34 | 32, 33 | ax-mp 5 |
. . . . . 6
⊢ (𝑧 ∈ ran (
·ℎ ↾ (ℂ × 𝐻)) ↔ ∃𝑥 ∈ ℂ ∃𝑦 ∈ 𝐻 𝑧 = (𝑥( ·ℎ ↾
(ℂ × 𝐻))𝑦)) |
35 | | ovres 7374 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑥( ·ℎ ↾
(ℂ × 𝐻))𝑦) = (𝑥 ·ℎ 𝑦)) |
36 | | shmulcl 29299 |
. . . . . . . . . 10
⊢ ((𝐻 ∈
Sℋ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑥 ·ℎ 𝑦) ∈ 𝐻) |
37 | 1, 36 | mp3an1 1450 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑥 ·ℎ 𝑦) ∈ 𝐻) |
38 | 35, 37 | eqeltrd 2838 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑥( ·ℎ ↾
(ℂ × 𝐻))𝑦) ∈ 𝐻) |
39 | | eleq1 2825 |
. . . . . . . 8
⊢ (𝑧 = (𝑥( ·ℎ ↾
(ℂ × 𝐻))𝑦) → (𝑧 ∈ 𝐻 ↔ (𝑥( ·ℎ ↾
(ℂ × 𝐻))𝑦) ∈ 𝐻)) |
40 | 38, 39 | syl5ibrcom 250 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑧 = (𝑥( ·ℎ ↾
(ℂ × 𝐻))𝑦) → 𝑧 ∈ 𝐻)) |
41 | 40 | rexlimivv 3211 |
. . . . . 6
⊢
(∃𝑥 ∈
ℂ ∃𝑦 ∈
𝐻 𝑧 = (𝑥( ·ℎ ↾
(ℂ × 𝐻))𝑦) → 𝑧 ∈ 𝐻) |
42 | 34, 41 | sylbi 220 |
. . . . 5
⊢ (𝑧 ∈ ran (
·ℎ ↾ (ℂ × 𝐻)) → 𝑧 ∈ 𝐻) |
43 | 42 | ssriv 3905 |
. . . 4
⊢ ran (
·ℎ ↾ (ℂ × 𝐻)) ⊆ 𝐻 |
44 | | df-f 6384 |
. . . 4
⊢ ((
·ℎ ↾ (ℂ × 𝐻)):(ℂ × 𝐻)⟶𝐻 ↔ ((
·ℎ ↾ (ℂ × 𝐻)) Fn (ℂ × 𝐻) ∧ ran (
·ℎ ↾ (ℂ × 𝐻)) ⊆ 𝐻)) |
45 | 32, 43, 44 | mpbir2an 711 |
. . 3
⊢ (
·ℎ ↾ (ℂ × 𝐻)):(ℂ × 𝐻)⟶𝐻 |
46 | | ax-1cn 10787 |
. . . . 5
⊢ 1 ∈
ℂ |
47 | | ovres 7374 |
. . . . 5
⊢ ((1
∈ ℂ ∧ 𝑥
∈ 𝐻) → (1(
·ℎ ↾ (ℂ × 𝐻))𝑥) = (1 ·ℎ
𝑥)) |
48 | 46, 47 | mpan 690 |
. . . 4
⊢ (𝑥 ∈ 𝐻 → (1(
·ℎ ↾ (ℂ × 𝐻))𝑥) = (1 ·ℎ
𝑥)) |
49 | 1 | sheli 29295 |
. . . . 5
⊢ (𝑥 ∈ 𝐻 → 𝑥 ∈ ℋ) |
50 | | ax-hvmulid 29087 |
. . . . 5
⊢ (𝑥 ∈ ℋ → (1
·ℎ 𝑥) = 𝑥) |
51 | 49, 50 | syl 17 |
. . . 4
⊢ (𝑥 ∈ 𝐻 → (1
·ℎ 𝑥) = 𝑥) |
52 | 48, 51 | eqtrd 2777 |
. . 3
⊢ (𝑥 ∈ 𝐻 → (1(
·ℎ ↾ (ℂ × 𝐻))𝑥) = 𝑥) |
53 | | id 22 |
. . . . 5
⊢ (𝑦 ∈ ℂ → 𝑦 ∈
ℂ) |
54 | 1 | sheli 29295 |
. . . . 5
⊢ (𝑧 ∈ 𝐻 → 𝑧 ∈ ℋ) |
55 | | ax-hvdistr1 29089 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦
·ℎ (𝑥 +ℎ 𝑧)) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑦
·ℎ 𝑧))) |
56 | 53, 49, 54, 55 | syl3an 1162 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦 ·ℎ (𝑥 +ℎ 𝑧)) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑦
·ℎ 𝑧))) |
57 | | ovres 7374 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑧) = (𝑥 +ℎ 𝑧)) |
58 | 57 | 3adant1 1132 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑧) = (𝑥 +ℎ 𝑧)) |
59 | 58 | oveq2d 7229 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑥( +ℎ ↾
(𝐻 × 𝐻))𝑧)) = (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑥 +ℎ 𝑧))) |
60 | | shaddcl 29298 |
. . . . . . . 8
⊢ ((𝐻 ∈
Sℋ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥 +ℎ 𝑧) ∈ 𝐻) |
61 | 1, 60 | mp3an1 1450 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥 +ℎ 𝑧) ∈ 𝐻) |
62 | | ovres 7374 |
. . . . . . 7
⊢ ((𝑦 ∈ ℂ ∧ (𝑥 +ℎ 𝑧) ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑥 +ℎ 𝑧)) = (𝑦 ·ℎ (𝑥 +ℎ 𝑧))) |
63 | 61, 62 | sylan2 596 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ (𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻)) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑥 +ℎ 𝑧)) = (𝑦 ·ℎ (𝑥 +ℎ 𝑧))) |
64 | 63 | 3impb 1117 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑥 +ℎ 𝑧)) = (𝑦 ·ℎ (𝑥 +ℎ 𝑧))) |
65 | 59, 64 | eqtrd 2777 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑥( +ℎ ↾
(𝐻 × 𝐻))𝑧)) = (𝑦 ·ℎ (𝑥 +ℎ 𝑧))) |
66 | | ovres 7374 |
. . . . . . 7
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑥) = (𝑦 ·ℎ 𝑥)) |
67 | 66 | 3adant3 1134 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑥) = (𝑦 ·ℎ 𝑥)) |
68 | | ovres 7374 |
. . . . . . 7
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑧) = (𝑦 ·ℎ 𝑧)) |
69 | 68 | 3adant2 1133 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑧) = (𝑦 ·ℎ 𝑧)) |
70 | 67, 69 | oveq12d 7231 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → ((𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑥)( +ℎ ↾
(𝐻 × 𝐻))(𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑧)) = ((𝑦 ·ℎ 𝑥)( +ℎ ↾
(𝐻 × 𝐻))(𝑦 ·ℎ 𝑧))) |
71 | | shmulcl 29299 |
. . . . . . . 8
⊢ ((𝐻 ∈
Sℋ ∧ 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦 ·ℎ 𝑥) ∈ 𝐻) |
72 | 1, 71 | mp3an1 1450 |
. . . . . . 7
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦 ·ℎ 𝑥) ∈ 𝐻) |
73 | 72 | 3adant3 1134 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦 ·ℎ 𝑥) ∈ 𝐻) |
74 | | shmulcl 29299 |
. . . . . . . 8
⊢ ((𝐻 ∈
Sℋ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝐻) → (𝑦 ·ℎ 𝑧) ∈ 𝐻) |
75 | 1, 74 | mp3an1 1450 |
. . . . . . 7
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝐻) → (𝑦 ·ℎ 𝑧) ∈ 𝐻) |
76 | 75 | 3adant2 1133 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦 ·ℎ 𝑧) ∈ 𝐻) |
77 | 73, 76 | ovresd 7375 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → ((𝑦 ·ℎ 𝑥)( +ℎ ↾
(𝐻 × 𝐻))(𝑦 ·ℎ 𝑧)) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑦
·ℎ 𝑧))) |
78 | 70, 77 | eqtrd 2777 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → ((𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑥)( +ℎ ↾
(𝐻 × 𝐻))(𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑧)) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑦
·ℎ 𝑧))) |
79 | 56, 65, 78 | 3eqtr4d 2787 |
. . 3
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑥( +ℎ ↾
(𝐻 × 𝐻))𝑧)) = ((𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑥)( +ℎ ↾
(𝐻 × 𝐻))(𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑧))) |
80 | | ax-hvdistr2 29090 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℋ) → ((𝑦 + 𝑧) ·ℎ 𝑥) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑧
·ℎ 𝑥))) |
81 | 49, 80 | syl3an3 1167 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 + 𝑧) ·ℎ 𝑥) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑧
·ℎ 𝑥))) |
82 | | addcl 10811 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑦 + 𝑧) ∈ ℂ) |
83 | | ovres 7374 |
. . . . 5
⊢ (((𝑦 + 𝑧) ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 + 𝑧)( ·ℎ ↾
(ℂ × 𝐻))𝑥) = ((𝑦 + 𝑧) ·ℎ 𝑥)) |
84 | 82, 83 | stoic3 1784 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 + 𝑧)( ·ℎ ↾
(ℂ × 𝐻))𝑥) = ((𝑦 + 𝑧) ·ℎ 𝑥)) |
85 | 66 | 3adant2 1133 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑥) = (𝑦 ·ℎ 𝑥)) |
86 | | ovres 7374 |
. . . . . . 7
⊢ ((𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧( ·ℎ ↾
(ℂ × 𝐻))𝑥) = (𝑧 ·ℎ 𝑥)) |
87 | 86 | 3adant1 1132 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧( ·ℎ ↾
(ℂ × 𝐻))𝑥) = (𝑧 ·ℎ 𝑥)) |
88 | 85, 87 | oveq12d 7231 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑥)( +ℎ ↾
(𝐻 × 𝐻))(𝑧( ·ℎ ↾
(ℂ × 𝐻))𝑥)) = ((𝑦 ·ℎ 𝑥)( +ℎ ↾
(𝐻 × 𝐻))(𝑧 ·ℎ 𝑥))) |
89 | 72 | 3adant2 1133 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦 ·ℎ 𝑥) ∈ 𝐻) |
90 | | shmulcl 29299 |
. . . . . . . 8
⊢ ((𝐻 ∈
Sℋ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧 ·ℎ 𝑥) ∈ 𝐻) |
91 | 1, 90 | mp3an1 1450 |
. . . . . . 7
⊢ ((𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧 ·ℎ 𝑥) ∈ 𝐻) |
92 | 91 | 3adant1 1132 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧 ·ℎ 𝑥) ∈ 𝐻) |
93 | 89, 92 | ovresd 7375 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 ·ℎ 𝑥)( +ℎ ↾
(𝐻 × 𝐻))(𝑧 ·ℎ 𝑥)) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑧
·ℎ 𝑥))) |
94 | 88, 93 | eqtrd 2777 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑥)( +ℎ ↾
(𝐻 × 𝐻))(𝑧( ·ℎ ↾
(ℂ × 𝐻))𝑥)) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑧
·ℎ 𝑥))) |
95 | 81, 84, 94 | 3eqtr4d 2787 |
. . 3
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 + 𝑧)( ·ℎ ↾
(ℂ × 𝐻))𝑥) = ((𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑥)( +ℎ ↾
(𝐻 × 𝐻))(𝑧( ·ℎ ↾
(ℂ × 𝐻))𝑥))) |
96 | | ax-hvmulass 29088 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℋ) → ((𝑦 · 𝑧) ·ℎ 𝑥) = (𝑦 ·ℎ (𝑧
·ℎ 𝑥))) |
97 | 49, 96 | syl3an3 1167 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 · 𝑧) ·ℎ 𝑥) = (𝑦 ·ℎ (𝑧
·ℎ 𝑥))) |
98 | | mulcl 10813 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑦 · 𝑧) ∈ ℂ) |
99 | | ovres 7374 |
. . . . 5
⊢ (((𝑦 · 𝑧) ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 · 𝑧)( ·ℎ ↾
(ℂ × 𝐻))𝑥) = ((𝑦 · 𝑧) ·ℎ 𝑥)) |
100 | 98, 99 | stoic3 1784 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 · 𝑧)( ·ℎ ↾
(ℂ × 𝐻))𝑥) = ((𝑦 · 𝑧) ·ℎ 𝑥)) |
101 | 87 | oveq2d 7229 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑧(
·ℎ ↾ (ℂ × 𝐻))𝑥)) = (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑧
·ℎ 𝑥))) |
102 | | ovres 7374 |
. . . . . . 7
⊢ ((𝑦 ∈ ℂ ∧ (𝑧
·ℎ 𝑥) ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑧
·ℎ 𝑥)) = (𝑦 ·ℎ (𝑧
·ℎ 𝑥))) |
103 | 91, 102 | sylan2 596 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ (𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻)) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑧
·ℎ 𝑥)) = (𝑦 ·ℎ (𝑧
·ℎ 𝑥))) |
104 | 103 | 3impb 1117 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑧
·ℎ 𝑥)) = (𝑦 ·ℎ (𝑧
·ℎ 𝑥))) |
105 | 101, 104 | eqtrd 2777 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑧(
·ℎ ↾ (ℂ × 𝐻))𝑥)) = (𝑦 ·ℎ (𝑧
·ℎ 𝑥))) |
106 | 97, 100, 105 | 3eqtr4d 2787 |
. . 3
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 · 𝑧)( ·ℎ ↾
(ℂ × 𝐻))𝑥) = (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑧(
·ℎ ↾ (ℂ × 𝐻))𝑥))) |
107 | | eqid 2737 |
. . 3
⊢ 〈(
+ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉 = 〈( +ℎ
↾ (𝐻 × 𝐻)), (
·ℎ ↾ (ℂ × 𝐻))〉 |
108 | 2, 12, 45, 52, 79, 95, 106, 107 | isvciOLD 28661 |
. 2
⊢ 〈(
+ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉 ∈
CVecOLD |
109 | | normf 29204 |
. . 3
⊢
normℎ: ℋ⟶ℝ |
110 | | fssres 6585 |
. . 3
⊢
((normℎ: ℋ⟶ℝ ∧ 𝐻 ⊆ ℋ) →
(normℎ ↾ 𝐻):𝐻⟶ℝ) |
111 | 109, 5, 110 | mp2an 692 |
. 2
⊢
(normℎ ↾ 𝐻):𝐻⟶ℝ |
112 | | fvres 6736 |
. . . . 5
⊢ (𝑥 ∈ 𝐻 → ((normℎ ↾
𝐻)‘𝑥) = (normℎ‘𝑥)) |
113 | 112 | eqeq1d 2739 |
. . . 4
⊢ (𝑥 ∈ 𝐻 → (((normℎ ↾
𝐻)‘𝑥) = 0 ↔
(normℎ‘𝑥) = 0)) |
114 | | norm-i 29210 |
. . . . 5
⊢ (𝑥 ∈ ℋ →
((normℎ‘𝑥) = 0 ↔ 𝑥 = 0ℎ)) |
115 | 49, 114 | syl 17 |
. . . 4
⊢ (𝑥 ∈ 𝐻 →
((normℎ‘𝑥) = 0 ↔ 𝑥 = 0ℎ)) |
116 | 113, 115 | bitrd 282 |
. . 3
⊢ (𝑥 ∈ 𝐻 → (((normℎ ↾
𝐻)‘𝑥) = 0 ↔ 𝑥 = 0ℎ)) |
117 | 116 | biimpa 480 |
. 2
⊢ ((𝑥 ∈ 𝐻 ∧ ((normℎ ↾
𝐻)‘𝑥) = 0) → 𝑥 = 0ℎ) |
118 | | norm-iii 29221 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℋ) →
(normℎ‘(𝑦 ·ℎ 𝑥)) = ((abs‘𝑦) ·
(normℎ‘𝑥))) |
119 | 49, 118 | sylan2 596 |
. . 3
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) →
(normℎ‘(𝑦 ·ℎ 𝑥)) = ((abs‘𝑦) ·
(normℎ‘𝑥))) |
120 | 66 | fveq2d 6721 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((normℎ ↾
𝐻)‘(𝑦(
·ℎ ↾ (ℂ × 𝐻))𝑥)) = ((normℎ ↾ 𝐻)‘(𝑦 ·ℎ 𝑥))) |
121 | | fvres 6736 |
. . . . 5
⊢ ((𝑦
·ℎ 𝑥) ∈ 𝐻 → ((normℎ ↾
𝐻)‘(𝑦
·ℎ 𝑥)) = (normℎ‘(𝑦
·ℎ 𝑥))) |
122 | 72, 121 | syl 17 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((normℎ ↾
𝐻)‘(𝑦
·ℎ 𝑥)) = (normℎ‘(𝑦
·ℎ 𝑥))) |
123 | 120, 122 | eqtrd 2777 |
. . 3
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((normℎ ↾
𝐻)‘(𝑦(
·ℎ ↾ (ℂ × 𝐻))𝑥)) = (normℎ‘(𝑦
·ℎ 𝑥))) |
124 | 112 | adantl 485 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((normℎ ↾
𝐻)‘𝑥) = (normℎ‘𝑥)) |
125 | 124 | oveq2d 7229 |
. . 3
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((abs‘𝑦) · ((normℎ ↾
𝐻)‘𝑥)) = ((abs‘𝑦) ·
(normℎ‘𝑥))) |
126 | 119, 123,
125 | 3eqtr4d 2787 |
. 2
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((normℎ ↾
𝐻)‘(𝑦(
·ℎ ↾ (ℂ × 𝐻))𝑥)) = ((abs‘𝑦) · ((normℎ ↾
𝐻)‘𝑥))) |
127 | 1 | sheli 29295 |
. . . 4
⊢ (𝑦 ∈ 𝐻 → 𝑦 ∈ ℋ) |
128 | | norm-ii 29219 |
. . . 4
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(normℎ‘(𝑥 +ℎ 𝑦)) ≤ ((normℎ‘𝑥) +
(normℎ‘𝑦))) |
129 | 49, 127, 128 | syl2an 599 |
. . 3
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) →
(normℎ‘(𝑥 +ℎ 𝑦)) ≤ ((normℎ‘𝑥) +
(normℎ‘𝑦))) |
130 | | ovres 7374 |
. . . . 5
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑦) = (𝑥 +ℎ 𝑦)) |
131 | 130 | fveq2d 6721 |
. . . 4
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → ((normℎ ↾
𝐻)‘(𝑥( +ℎ ↾
(𝐻 × 𝐻))𝑦)) = ((normℎ ↾ 𝐻)‘(𝑥 +ℎ 𝑦))) |
132 | | shaddcl 29298 |
. . . . . 6
⊢ ((𝐻 ∈
Sℋ ∧ 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (𝑥 +ℎ 𝑦) ∈ 𝐻) |
133 | 1, 132 | mp3an1 1450 |
. . . . 5
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (𝑥 +ℎ 𝑦) ∈ 𝐻) |
134 | | fvres 6736 |
. . . . 5
⊢ ((𝑥 +ℎ 𝑦) ∈ 𝐻 → ((normℎ ↾
𝐻)‘(𝑥 +ℎ 𝑦)) =
(normℎ‘(𝑥 +ℎ 𝑦))) |
135 | 133, 134 | syl 17 |
. . . 4
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → ((normℎ ↾
𝐻)‘(𝑥 +ℎ 𝑦)) =
(normℎ‘(𝑥 +ℎ 𝑦))) |
136 | 131, 135 | eqtrd 2777 |
. . 3
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → ((normℎ ↾
𝐻)‘(𝑥( +ℎ ↾
(𝐻 × 𝐻))𝑦)) = (normℎ‘(𝑥 +ℎ 𝑦))) |
137 | | fvres 6736 |
. . . 4
⊢ (𝑦 ∈ 𝐻 → ((normℎ ↾
𝐻)‘𝑦) = (normℎ‘𝑦)) |
138 | 112, 137 | oveqan12d 7232 |
. . 3
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (((normℎ ↾
𝐻)‘𝑥) + ((normℎ ↾ 𝐻)‘𝑦)) = ((normℎ‘𝑥) +
(normℎ‘𝑦))) |
139 | 129, 136,
138 | 3brtr4d 5085 |
. 2
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → ((normℎ ↾
𝐻)‘(𝑥( +ℎ ↾
(𝐻 × 𝐻))𝑦)) ≤ (((normℎ ↾
𝐻)‘𝑥) + ((normℎ ↾ 𝐻)‘𝑦))) |
140 | | hhssnvt.1 |
. 2
⊢ 𝑊 = 〈〈(
+ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉 |
141 | 13, 24, 108, 111, 117, 126, 139, 140 | isnvi 28694 |
1
⊢ 𝑊 ∈ NrmCVec |