| Step | Hyp | Ref
| Expression |
| 1 | | hhssnv.2 |
. . . . 5
⊢ 𝐻 ∈
Sℋ |
| 2 | 1 | hhssabloi 31281 |
. . . 4
⊢ (
+ℎ ↾ (𝐻 × 𝐻)) ∈ AbelOp |
| 3 | | ablogrpo 30566 |
. . . 4
⊢ ((
+ℎ ↾ (𝐻 × 𝐻)) ∈ AbelOp → (
+ℎ ↾ (𝐻 × 𝐻)) ∈ GrpOp) |
| 4 | 2, 3 | ax-mp 5 |
. . 3
⊢ (
+ℎ ↾ (𝐻 × 𝐻)) ∈ GrpOp |
| 5 | 1 | shssii 31232 |
. . . . . 6
⊢ 𝐻 ⊆
ℋ |
| 6 | | xpss12 5700 |
. . . . . 6
⊢ ((𝐻 ⊆ ℋ ∧ 𝐻 ⊆ ℋ) → (𝐻 × 𝐻) ⊆ ( ℋ ×
ℋ)) |
| 7 | 5, 5, 6 | mp2an 692 |
. . . . 5
⊢ (𝐻 × 𝐻) ⊆ ( ℋ ×
ℋ) |
| 8 | | ax-hfvadd 31019 |
. . . . . 6
⊢
+ℎ :( ℋ × ℋ)⟶
ℋ |
| 9 | 8 | fdmi 6747 |
. . . . 5
⊢ dom
+ℎ = ( ℋ × ℋ) |
| 10 | 7, 9 | sseqtrri 4033 |
. . . 4
⊢ (𝐻 × 𝐻) ⊆ dom
+ℎ |
| 11 | | ssdmres 6031 |
. . . 4
⊢ ((𝐻 × 𝐻) ⊆ dom +ℎ ↔
dom ( +ℎ ↾ (𝐻 × 𝐻)) = (𝐻 × 𝐻)) |
| 12 | 10, 11 | mpbi 230 |
. . 3
⊢ dom (
+ℎ ↾ (𝐻 × 𝐻)) = (𝐻 × 𝐻) |
| 13 | 4, 12 | grporn 30540 |
. 2
⊢ 𝐻 = ran ( +ℎ
↾ (𝐻 × 𝐻)) |
| 14 | | sh0 31235 |
. . . . . 6
⊢ (𝐻 ∈
Sℋ → 0ℎ ∈ 𝐻) |
| 15 | 1, 14 | ax-mp 5 |
. . . . 5
⊢
0ℎ ∈ 𝐻 |
| 16 | | ovres 7599 |
. . . . 5
⊢
((0ℎ ∈ 𝐻 ∧ 0ℎ ∈ 𝐻) → (0ℎ(
+ℎ ↾ (𝐻 × 𝐻))0ℎ) =
(0ℎ +ℎ
0ℎ)) |
| 17 | 15, 15, 16 | mp2an 692 |
. . . 4
⊢
(0ℎ( +ℎ ↾ (𝐻 × 𝐻))0ℎ) =
(0ℎ +ℎ
0ℎ) |
| 18 | | ax-hv0cl 31022 |
. . . . 5
⊢
0ℎ ∈ ℋ |
| 19 | 18 | hvaddlidi 31048 |
. . . 4
⊢
(0ℎ +ℎ 0ℎ) =
0ℎ |
| 20 | 17, 19 | eqtri 2765 |
. . 3
⊢
(0ℎ( +ℎ ↾ (𝐻 × 𝐻))0ℎ) =
0ℎ |
| 21 | | eqid 2737 |
. . . . 5
⊢
(GId‘( +ℎ ↾ (𝐻 × 𝐻))) = (GId‘( +ℎ
↾ (𝐻 × 𝐻))) |
| 22 | 13, 21 | grpoid 30539 |
. . . 4
⊢ (((
+ℎ ↾ (𝐻 × 𝐻)) ∈ GrpOp ∧ 0ℎ
∈ 𝐻) →
(0ℎ = (GId‘( +ℎ ↾ (𝐻 × 𝐻))) ↔ (0ℎ(
+ℎ ↾ (𝐻 × 𝐻))0ℎ) =
0ℎ)) |
| 23 | 4, 15, 22 | mp2an 692 |
. . 3
⊢
(0ℎ = (GId‘( +ℎ ↾ (𝐻 × 𝐻))) ↔ (0ℎ(
+ℎ ↾ (𝐻 × 𝐻))0ℎ) =
0ℎ) |
| 24 | 20, 23 | mpbir 231 |
. 2
⊢
0ℎ = (GId‘( +ℎ ↾ (𝐻 × 𝐻))) |
| 25 | | ax-hfvmul 31024 |
. . . . . 6
⊢
·ℎ :(ℂ × ℋ)⟶
ℋ |
| 26 | | ffn 6736 |
. . . . . 6
⊢ (
·ℎ :(ℂ × ℋ)⟶ ℋ
→ ·ℎ Fn (ℂ ×
ℋ)) |
| 27 | 25, 26 | ax-mp 5 |
. . . . 5
⊢
·ℎ Fn (ℂ ×
ℋ) |
| 28 | | ssid 4006 |
. . . . . 6
⊢ ℂ
⊆ ℂ |
| 29 | | xpss12 5700 |
. . . . . 6
⊢ ((ℂ
⊆ ℂ ∧ 𝐻
⊆ ℋ) → (ℂ × 𝐻) ⊆ (ℂ ×
ℋ)) |
| 30 | 28, 5, 29 | mp2an 692 |
. . . . 5
⊢ (ℂ
× 𝐻) ⊆ (ℂ
× ℋ) |
| 31 | | fnssres 6691 |
. . . . 5
⊢ ((
·ℎ Fn (ℂ × ℋ) ∧ (ℂ
× 𝐻) ⊆ (ℂ
× ℋ)) → ( ·ℎ ↾ (ℂ
× 𝐻)) Fn (ℂ
× 𝐻)) |
| 32 | 27, 30, 31 | mp2an 692 |
. . . 4
⊢ (
·ℎ ↾ (ℂ × 𝐻)) Fn (ℂ × 𝐻) |
| 33 | | ovelrn 7609 |
. . . . . . 7
⊢ ((
·ℎ ↾ (ℂ × 𝐻)) Fn (ℂ × 𝐻) → (𝑧 ∈ ran (
·ℎ ↾ (ℂ × 𝐻)) ↔ ∃𝑥 ∈ ℂ ∃𝑦 ∈ 𝐻 𝑧 = (𝑥( ·ℎ ↾
(ℂ × 𝐻))𝑦))) |
| 34 | 32, 33 | ax-mp 5 |
. . . . . 6
⊢ (𝑧 ∈ ran (
·ℎ ↾ (ℂ × 𝐻)) ↔ ∃𝑥 ∈ ℂ ∃𝑦 ∈ 𝐻 𝑧 = (𝑥( ·ℎ ↾
(ℂ × 𝐻))𝑦)) |
| 35 | | ovres 7599 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑥( ·ℎ ↾
(ℂ × 𝐻))𝑦) = (𝑥 ·ℎ 𝑦)) |
| 36 | | shmulcl 31237 |
. . . . . . . . . 10
⊢ ((𝐻 ∈
Sℋ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑥 ·ℎ 𝑦) ∈ 𝐻) |
| 37 | 1, 36 | mp3an1 1450 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑥 ·ℎ 𝑦) ∈ 𝐻) |
| 38 | 35, 37 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑥( ·ℎ ↾
(ℂ × 𝐻))𝑦) ∈ 𝐻) |
| 39 | | eleq1 2829 |
. . . . . . . 8
⊢ (𝑧 = (𝑥( ·ℎ ↾
(ℂ × 𝐻))𝑦) → (𝑧 ∈ 𝐻 ↔ (𝑥( ·ℎ ↾
(ℂ × 𝐻))𝑦) ∈ 𝐻)) |
| 40 | 38, 39 | syl5ibrcom 247 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑧 = (𝑥( ·ℎ ↾
(ℂ × 𝐻))𝑦) → 𝑧 ∈ 𝐻)) |
| 41 | 40 | rexlimivv 3201 |
. . . . . 6
⊢
(∃𝑥 ∈
ℂ ∃𝑦 ∈
𝐻 𝑧 = (𝑥( ·ℎ ↾
(ℂ × 𝐻))𝑦) → 𝑧 ∈ 𝐻) |
| 42 | 34, 41 | sylbi 217 |
. . . . 5
⊢ (𝑧 ∈ ran (
·ℎ ↾ (ℂ × 𝐻)) → 𝑧 ∈ 𝐻) |
| 43 | 42 | ssriv 3987 |
. . . 4
⊢ ran (
·ℎ ↾ (ℂ × 𝐻)) ⊆ 𝐻 |
| 44 | | df-f 6565 |
. . . 4
⊢ ((
·ℎ ↾ (ℂ × 𝐻)):(ℂ × 𝐻)⟶𝐻 ↔ ((
·ℎ ↾ (ℂ × 𝐻)) Fn (ℂ × 𝐻) ∧ ran (
·ℎ ↾ (ℂ × 𝐻)) ⊆ 𝐻)) |
| 45 | 32, 43, 44 | mpbir2an 711 |
. . 3
⊢ (
·ℎ ↾ (ℂ × 𝐻)):(ℂ × 𝐻)⟶𝐻 |
| 46 | | ax-1cn 11213 |
. . . . 5
⊢ 1 ∈
ℂ |
| 47 | | ovres 7599 |
. . . . 5
⊢ ((1
∈ ℂ ∧ 𝑥
∈ 𝐻) → (1(
·ℎ ↾ (ℂ × 𝐻))𝑥) = (1 ·ℎ
𝑥)) |
| 48 | 46, 47 | mpan 690 |
. . . 4
⊢ (𝑥 ∈ 𝐻 → (1(
·ℎ ↾ (ℂ × 𝐻))𝑥) = (1 ·ℎ
𝑥)) |
| 49 | 1 | sheli 31233 |
. . . . 5
⊢ (𝑥 ∈ 𝐻 → 𝑥 ∈ ℋ) |
| 50 | | ax-hvmulid 31025 |
. . . . 5
⊢ (𝑥 ∈ ℋ → (1
·ℎ 𝑥) = 𝑥) |
| 51 | 49, 50 | syl 17 |
. . . 4
⊢ (𝑥 ∈ 𝐻 → (1
·ℎ 𝑥) = 𝑥) |
| 52 | 48, 51 | eqtrd 2777 |
. . 3
⊢ (𝑥 ∈ 𝐻 → (1(
·ℎ ↾ (ℂ × 𝐻))𝑥) = 𝑥) |
| 53 | | id 22 |
. . . . 5
⊢ (𝑦 ∈ ℂ → 𝑦 ∈
ℂ) |
| 54 | 1 | sheli 31233 |
. . . . 5
⊢ (𝑧 ∈ 𝐻 → 𝑧 ∈ ℋ) |
| 55 | | ax-hvdistr1 31027 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦
·ℎ (𝑥 +ℎ 𝑧)) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑦
·ℎ 𝑧))) |
| 56 | 53, 49, 54, 55 | syl3an 1161 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦 ·ℎ (𝑥 +ℎ 𝑧)) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑦
·ℎ 𝑧))) |
| 57 | | ovres 7599 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑧) = (𝑥 +ℎ 𝑧)) |
| 58 | 57 | 3adant1 1131 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑧) = (𝑥 +ℎ 𝑧)) |
| 59 | 58 | oveq2d 7447 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑥( +ℎ ↾
(𝐻 × 𝐻))𝑧)) = (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑥 +ℎ 𝑧))) |
| 60 | | shaddcl 31236 |
. . . . . . . 8
⊢ ((𝐻 ∈
Sℋ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥 +ℎ 𝑧) ∈ 𝐻) |
| 61 | 1, 60 | mp3an1 1450 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥 +ℎ 𝑧) ∈ 𝐻) |
| 62 | | ovres 7599 |
. . . . . . 7
⊢ ((𝑦 ∈ ℂ ∧ (𝑥 +ℎ 𝑧) ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑥 +ℎ 𝑧)) = (𝑦 ·ℎ (𝑥 +ℎ 𝑧))) |
| 63 | 61, 62 | sylan2 593 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ (𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻)) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑥 +ℎ 𝑧)) = (𝑦 ·ℎ (𝑥 +ℎ 𝑧))) |
| 64 | 63 | 3impb 1115 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑥 +ℎ 𝑧)) = (𝑦 ·ℎ (𝑥 +ℎ 𝑧))) |
| 65 | 59, 64 | eqtrd 2777 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑥( +ℎ ↾
(𝐻 × 𝐻))𝑧)) = (𝑦 ·ℎ (𝑥 +ℎ 𝑧))) |
| 66 | | ovres 7599 |
. . . . . . 7
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑥) = (𝑦 ·ℎ 𝑥)) |
| 67 | 66 | 3adant3 1133 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑥) = (𝑦 ·ℎ 𝑥)) |
| 68 | | ovres 7599 |
. . . . . . 7
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑧) = (𝑦 ·ℎ 𝑧)) |
| 69 | 68 | 3adant2 1132 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑧) = (𝑦 ·ℎ 𝑧)) |
| 70 | 67, 69 | oveq12d 7449 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → ((𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑥)( +ℎ ↾
(𝐻 × 𝐻))(𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑧)) = ((𝑦 ·ℎ 𝑥)( +ℎ ↾
(𝐻 × 𝐻))(𝑦 ·ℎ 𝑧))) |
| 71 | | shmulcl 31237 |
. . . . . . . 8
⊢ ((𝐻 ∈
Sℋ ∧ 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦 ·ℎ 𝑥) ∈ 𝐻) |
| 72 | 1, 71 | mp3an1 1450 |
. . . . . . 7
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦 ·ℎ 𝑥) ∈ 𝐻) |
| 73 | 72 | 3adant3 1133 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦 ·ℎ 𝑥) ∈ 𝐻) |
| 74 | | shmulcl 31237 |
. . . . . . . 8
⊢ ((𝐻 ∈
Sℋ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝐻) → (𝑦 ·ℎ 𝑧) ∈ 𝐻) |
| 75 | 1, 74 | mp3an1 1450 |
. . . . . . 7
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝐻) → (𝑦 ·ℎ 𝑧) ∈ 𝐻) |
| 76 | 75 | 3adant2 1132 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦 ·ℎ 𝑧) ∈ 𝐻) |
| 77 | 73, 76 | ovresd 7600 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → ((𝑦 ·ℎ 𝑥)( +ℎ ↾
(𝐻 × 𝐻))(𝑦 ·ℎ 𝑧)) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑦
·ℎ 𝑧))) |
| 78 | 70, 77 | eqtrd 2777 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → ((𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑥)( +ℎ ↾
(𝐻 × 𝐻))(𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑧)) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑦
·ℎ 𝑧))) |
| 79 | 56, 65, 78 | 3eqtr4d 2787 |
. . 3
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑥( +ℎ ↾
(𝐻 × 𝐻))𝑧)) = ((𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑥)( +ℎ ↾
(𝐻 × 𝐻))(𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑧))) |
| 80 | | ax-hvdistr2 31028 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℋ) → ((𝑦 + 𝑧) ·ℎ 𝑥) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑧
·ℎ 𝑥))) |
| 81 | 49, 80 | syl3an3 1166 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 + 𝑧) ·ℎ 𝑥) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑧
·ℎ 𝑥))) |
| 82 | | addcl 11237 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑦 + 𝑧) ∈ ℂ) |
| 83 | | ovres 7599 |
. . . . 5
⊢ (((𝑦 + 𝑧) ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 + 𝑧)( ·ℎ ↾
(ℂ × 𝐻))𝑥) = ((𝑦 + 𝑧) ·ℎ 𝑥)) |
| 84 | 82, 83 | stoic3 1776 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 + 𝑧)( ·ℎ ↾
(ℂ × 𝐻))𝑥) = ((𝑦 + 𝑧) ·ℎ 𝑥)) |
| 85 | 66 | 3adant2 1132 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑥) = (𝑦 ·ℎ 𝑥)) |
| 86 | | ovres 7599 |
. . . . . . 7
⊢ ((𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧( ·ℎ ↾
(ℂ × 𝐻))𝑥) = (𝑧 ·ℎ 𝑥)) |
| 87 | 86 | 3adant1 1131 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧( ·ℎ ↾
(ℂ × 𝐻))𝑥) = (𝑧 ·ℎ 𝑥)) |
| 88 | 85, 87 | oveq12d 7449 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑥)( +ℎ ↾
(𝐻 × 𝐻))(𝑧( ·ℎ ↾
(ℂ × 𝐻))𝑥)) = ((𝑦 ·ℎ 𝑥)( +ℎ ↾
(𝐻 × 𝐻))(𝑧 ·ℎ 𝑥))) |
| 89 | 72 | 3adant2 1132 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦 ·ℎ 𝑥) ∈ 𝐻) |
| 90 | | shmulcl 31237 |
. . . . . . . 8
⊢ ((𝐻 ∈
Sℋ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧 ·ℎ 𝑥) ∈ 𝐻) |
| 91 | 1, 90 | mp3an1 1450 |
. . . . . . 7
⊢ ((𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧 ·ℎ 𝑥) ∈ 𝐻) |
| 92 | 91 | 3adant1 1131 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧 ·ℎ 𝑥) ∈ 𝐻) |
| 93 | 89, 92 | ovresd 7600 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 ·ℎ 𝑥)( +ℎ ↾
(𝐻 × 𝐻))(𝑧 ·ℎ 𝑥)) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑧
·ℎ 𝑥))) |
| 94 | 88, 93 | eqtrd 2777 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑥)( +ℎ ↾
(𝐻 × 𝐻))(𝑧( ·ℎ ↾
(ℂ × 𝐻))𝑥)) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑧
·ℎ 𝑥))) |
| 95 | 81, 84, 94 | 3eqtr4d 2787 |
. . 3
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 + 𝑧)( ·ℎ ↾
(ℂ × 𝐻))𝑥) = ((𝑦( ·ℎ ↾
(ℂ × 𝐻))𝑥)( +ℎ ↾
(𝐻 × 𝐻))(𝑧( ·ℎ ↾
(ℂ × 𝐻))𝑥))) |
| 96 | | ax-hvmulass 31026 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℋ) → ((𝑦 · 𝑧) ·ℎ 𝑥) = (𝑦 ·ℎ (𝑧
·ℎ 𝑥))) |
| 97 | 49, 96 | syl3an3 1166 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 · 𝑧) ·ℎ 𝑥) = (𝑦 ·ℎ (𝑧
·ℎ 𝑥))) |
| 98 | | mulcl 11239 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑦 · 𝑧) ∈ ℂ) |
| 99 | | ovres 7599 |
. . . . 5
⊢ (((𝑦 · 𝑧) ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 · 𝑧)( ·ℎ ↾
(ℂ × 𝐻))𝑥) = ((𝑦 · 𝑧) ·ℎ 𝑥)) |
| 100 | 98, 99 | stoic3 1776 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 · 𝑧)( ·ℎ ↾
(ℂ × 𝐻))𝑥) = ((𝑦 · 𝑧) ·ℎ 𝑥)) |
| 101 | 87 | oveq2d 7447 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑧(
·ℎ ↾ (ℂ × 𝐻))𝑥)) = (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑧
·ℎ 𝑥))) |
| 102 | | ovres 7599 |
. . . . . . 7
⊢ ((𝑦 ∈ ℂ ∧ (𝑧
·ℎ 𝑥) ∈ 𝐻) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑧
·ℎ 𝑥)) = (𝑦 ·ℎ (𝑧
·ℎ 𝑥))) |
| 103 | 91, 102 | sylan2 593 |
. . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ (𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻)) → (𝑦( ·ℎ ↾
(ℂ × 𝐻))(𝑧
·ℎ 𝑥)) = (𝑦 ·ℎ (𝑧
·ℎ 𝑥))) |
| 104 | 103 | 3impb 1115 |
. . . . 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 30599 |
. 2
⊢ 〈(
+ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉 ∈
CVecOLD |
| 109 | | normf 31142 |
. . 3
⊢
normℎ: ℋ⟶ℝ |
| 110 | | fssres 6774 |
. . 3
⊢
((normℎ: ℋ⟶ℝ ∧ 𝐻 ⊆ ℋ) →
(normℎ ↾ 𝐻):𝐻⟶ℝ) |
| 111 | 109, 5, 110 | mp2an 692 |
. 2
⊢
(normℎ ↾ 𝐻):𝐻⟶ℝ |
| 112 | | fvres 6925 |
. . . . 5
⊢ (𝑥 ∈ 𝐻 → ((normℎ ↾
𝐻)‘𝑥) = (normℎ‘𝑥)) |
| 113 | 112 | eqeq1d 2739 |
. . . 4
⊢ (𝑥 ∈ 𝐻 → (((normℎ ↾
𝐻)‘𝑥) = 0 ↔
(normℎ‘𝑥) = 0)) |
| 114 | | norm-i 31148 |
. . . . 5
⊢ (𝑥 ∈ ℋ →
((normℎ‘𝑥) = 0 ↔ 𝑥 = 0ℎ)) |
| 115 | 49, 114 | syl 17 |
. . . 4
⊢ (𝑥 ∈ 𝐻 →
((normℎ‘𝑥) = 0 ↔ 𝑥 = 0ℎ)) |
| 116 | 113, 115 | bitrd 279 |
. . 3
⊢ (𝑥 ∈ 𝐻 → (((normℎ ↾
𝐻)‘𝑥) = 0 ↔ 𝑥 = 0ℎ)) |
| 117 | 116 | biimpa 476 |
. 2
⊢ ((𝑥 ∈ 𝐻 ∧ ((normℎ ↾
𝐻)‘𝑥) = 0) → 𝑥 = 0ℎ) |
| 118 | | norm-iii 31159 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℋ) →
(normℎ‘(𝑦 ·ℎ 𝑥)) = ((abs‘𝑦) ·
(normℎ‘𝑥))) |
| 119 | 49, 118 | sylan2 593 |
. . 3
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) →
(normℎ‘(𝑦 ·ℎ 𝑥)) = ((abs‘𝑦) ·
(normℎ‘𝑥))) |
| 120 | 66 | fveq2d 6910 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((normℎ ↾
𝐻)‘(𝑦(
·ℎ ↾ (ℂ × 𝐻))𝑥)) = ((normℎ ↾ 𝐻)‘(𝑦 ·ℎ 𝑥))) |
| 121 | | fvres 6925 |
. . . . 5
⊢ ((𝑦
·ℎ 𝑥) ∈ 𝐻 → ((normℎ ↾
𝐻)‘(𝑦
·ℎ 𝑥)) = (normℎ‘(𝑦
·ℎ 𝑥))) |
| 122 | 72, 121 | syl 17 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((normℎ ↾
𝐻)‘(𝑦
·ℎ 𝑥)) = (normℎ‘(𝑦
·ℎ 𝑥))) |
| 123 | 120, 122 | eqtrd 2777 |
. . 3
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((normℎ ↾
𝐻)‘(𝑦(
·ℎ ↾ (ℂ × 𝐻))𝑥)) = (normℎ‘(𝑦
·ℎ 𝑥))) |
| 124 | 112 | adantl 481 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((normℎ ↾
𝐻)‘𝑥) = (normℎ‘𝑥)) |
| 125 | 124 | oveq2d 7447 |
. . 3
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((abs‘𝑦) · ((normℎ ↾
𝐻)‘𝑥)) = ((abs‘𝑦) ·
(normℎ‘𝑥))) |
| 126 | 119, 123,
125 | 3eqtr4d 2787 |
. 2
⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((normℎ ↾
𝐻)‘(𝑦(
·ℎ ↾ (ℂ × 𝐻))𝑥)) = ((abs‘𝑦) · ((normℎ ↾
𝐻)‘𝑥))) |
| 127 | 1 | sheli 31233 |
. . . 4
⊢ (𝑦 ∈ 𝐻 → 𝑦 ∈ ℋ) |
| 128 | | norm-ii 31157 |
. . . 4
⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) →
(normℎ‘(𝑥 +ℎ 𝑦)) ≤ ((normℎ‘𝑥) +
(normℎ‘𝑦))) |
| 129 | 49, 127, 128 | syl2an 596 |
. . 3
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) →
(normℎ‘(𝑥 +ℎ 𝑦)) ≤ ((normℎ‘𝑥) +
(normℎ‘𝑦))) |
| 130 | | ovres 7599 |
. . . . 5
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑦) = (𝑥 +ℎ 𝑦)) |
| 131 | 130 | fveq2d 6910 |
. . . 4
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → ((normℎ ↾
𝐻)‘(𝑥( +ℎ ↾
(𝐻 × 𝐻))𝑦)) = ((normℎ ↾ 𝐻)‘(𝑥 +ℎ 𝑦))) |
| 132 | | shaddcl 31236 |
. . . . . 6
⊢ ((𝐻 ∈
Sℋ ∧ 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (𝑥 +ℎ 𝑦) ∈ 𝐻) |
| 133 | 1, 132 | mp3an1 1450 |
. . . . 5
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (𝑥 +ℎ 𝑦) ∈ 𝐻) |
| 134 | | fvres 6925 |
. . . . 5
⊢ ((𝑥 +ℎ 𝑦) ∈ 𝐻 → ((normℎ ↾
𝐻)‘(𝑥 +ℎ 𝑦)) =
(normℎ‘(𝑥 +ℎ 𝑦))) |
| 135 | 133, 134 | syl 17 |
. . . 4
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → ((normℎ ↾
𝐻)‘(𝑥 +ℎ 𝑦)) =
(normℎ‘(𝑥 +ℎ 𝑦))) |
| 136 | 131, 135 | eqtrd 2777 |
. . 3
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → ((normℎ ↾
𝐻)‘(𝑥( +ℎ ↾
(𝐻 × 𝐻))𝑦)) = (normℎ‘(𝑥 +ℎ 𝑦))) |
| 137 | | fvres 6925 |
. . . 4
⊢ (𝑦 ∈ 𝐻 → ((normℎ ↾
𝐻)‘𝑦) = (normℎ‘𝑦)) |
| 138 | 112, 137 | oveqan12d 7450 |
. . 3
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (((normℎ ↾
𝐻)‘𝑥) + ((normℎ ↾ 𝐻)‘𝑦)) = ((normℎ‘𝑥) +
(normℎ‘𝑦))) |
| 139 | 129, 136,
138 | 3brtr4d 5175 |
. 2
⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → ((normℎ ↾
𝐻)‘(𝑥( +ℎ ↾
(𝐻 × 𝐻))𝑦)) ≤ (((normℎ ↾
𝐻)‘𝑥) + ((normℎ ↾ 𝐻)‘𝑦))) |
| 140 | | hhssnvt.1 |
. 2
⊢ 𝑊 = 〈〈(
+ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ
↾ (ℂ × 𝐻))〉, (normℎ ↾
𝐻)〉 |
| 141 | 13, 24, 108, 111, 117, 126, 139, 140 | isnvi 30632 |
1
⊢ 𝑊 ∈ NrmCVec |