Step |
Hyp |
Ref |
Expression |
1 |
|
hhssnvt.1 |
⊢ 𝑊 = 〈 〈 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 〉 , ( normℎ ↾ 𝐻 ) 〉 |
2 |
|
hhssnv.2 |
⊢ 𝐻 ∈ Sℋ |
3 |
2
|
hhssabloi |
⊢ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ∈ AbelOp |
4 |
|
ablogrpo |
⊢ ( ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ∈ AbelOp → ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ∈ GrpOp ) |
5 |
3 4
|
ax-mp |
⊢ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ∈ GrpOp |
6 |
2
|
shssii |
⊢ 𝐻 ⊆ ℋ |
7 |
|
xpss12 |
⊢ ( ( 𝐻 ⊆ ℋ ∧ 𝐻 ⊆ ℋ ) → ( 𝐻 × 𝐻 ) ⊆ ( ℋ × ℋ ) ) |
8 |
6 6 7
|
mp2an |
⊢ ( 𝐻 × 𝐻 ) ⊆ ( ℋ × ℋ ) |
9 |
|
ax-hfvadd |
⊢ +ℎ : ( ℋ × ℋ ) ⟶ ℋ |
10 |
9
|
fdmi |
⊢ dom +ℎ = ( ℋ × ℋ ) |
11 |
8 10
|
sseqtrri |
⊢ ( 𝐻 × 𝐻 ) ⊆ dom +ℎ |
12 |
|
ssdmres |
⊢ ( ( 𝐻 × 𝐻 ) ⊆ dom +ℎ ↔ dom ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) = ( 𝐻 × 𝐻 ) ) |
13 |
11 12
|
mpbi |
⊢ dom ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) = ( 𝐻 × 𝐻 ) |
14 |
5 13
|
grporn |
⊢ 𝐻 = ran ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) |
15 |
|
sh0 |
⊢ ( 𝐻 ∈ Sℋ → 0ℎ ∈ 𝐻 ) |
16 |
2 15
|
ax-mp |
⊢ 0ℎ ∈ 𝐻 |
17 |
|
ovres |
⊢ ( ( 0ℎ ∈ 𝐻 ∧ 0ℎ ∈ 𝐻 ) → ( 0ℎ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 0ℎ ) = ( 0ℎ +ℎ 0ℎ ) ) |
18 |
16 16 17
|
mp2an |
⊢ ( 0ℎ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 0ℎ ) = ( 0ℎ +ℎ 0ℎ ) |
19 |
|
ax-hv0cl |
⊢ 0ℎ ∈ ℋ |
20 |
19
|
hvaddid2i |
⊢ ( 0ℎ +ℎ 0ℎ ) = 0ℎ |
21 |
18 20
|
eqtri |
⊢ ( 0ℎ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 0ℎ ) = 0ℎ |
22 |
|
eqid |
⊢ ( GId ‘ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ) = ( GId ‘ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ) |
23 |
14 22
|
grpoid |
⊢ ( ( ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ∈ GrpOp ∧ 0ℎ ∈ 𝐻 ) → ( 0ℎ = ( GId ‘ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ) ↔ ( 0ℎ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 0ℎ ) = 0ℎ ) ) |
24 |
5 16 23
|
mp2an |
⊢ ( 0ℎ = ( GId ‘ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ) ↔ ( 0ℎ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 0ℎ ) = 0ℎ ) |
25 |
21 24
|
mpbir |
⊢ 0ℎ = ( GId ‘ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ) |
26 |
|
ax-hfvmul |
⊢ ·ℎ : ( ℂ × ℋ ) ⟶ ℋ |
27 |
|
ffn |
⊢ ( ·ℎ : ( ℂ × ℋ ) ⟶ ℋ → ·ℎ Fn ( ℂ × ℋ ) ) |
28 |
26 27
|
ax-mp |
⊢ ·ℎ Fn ( ℂ × ℋ ) |
29 |
|
ssid |
⊢ ℂ ⊆ ℂ |
30 |
|
xpss12 |
⊢ ( ( ℂ ⊆ ℂ ∧ 𝐻 ⊆ ℋ ) → ( ℂ × 𝐻 ) ⊆ ( ℂ × ℋ ) ) |
31 |
29 6 30
|
mp2an |
⊢ ( ℂ × 𝐻 ) ⊆ ( ℂ × ℋ ) |
32 |
|
fnssres |
⊢ ( ( ·ℎ Fn ( ℂ × ℋ ) ∧ ( ℂ × 𝐻 ) ⊆ ( ℂ × ℋ ) ) → ( ·ℎ ↾ ( ℂ × 𝐻 ) ) Fn ( ℂ × 𝐻 ) ) |
33 |
28 31 32
|
mp2an |
⊢ ( ·ℎ ↾ ( ℂ × 𝐻 ) ) Fn ( ℂ × 𝐻 ) |
34 |
|
ovelrn |
⊢ ( ( ·ℎ ↾ ( ℂ × 𝐻 ) ) Fn ( ℂ × 𝐻 ) → ( 𝑧 ∈ ran ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ↔ ∃ 𝑥 ∈ ℂ ∃ 𝑦 ∈ 𝐻 𝑧 = ( 𝑥 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑦 ) ) ) |
35 |
33 34
|
ax-mp |
⊢ ( 𝑧 ∈ ran ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ↔ ∃ 𝑥 ∈ ℂ ∃ 𝑦 ∈ 𝐻 𝑧 = ( 𝑥 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑦 ) ) |
36 |
|
ovres |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑦 ) = ( 𝑥 ·ℎ 𝑦 ) ) |
37 |
|
shmulcl |
⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻 ) |
38 |
2 37
|
mp3an1 |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻 ) |
39 |
36 38
|
eqeltrd |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑦 ) ∈ 𝐻 ) |
40 |
|
eleq1 |
⊢ ( 𝑧 = ( 𝑥 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑦 ) → ( 𝑧 ∈ 𝐻 ↔ ( 𝑥 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑦 ) ∈ 𝐻 ) ) |
41 |
39 40
|
syl5ibrcom |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻 ) → ( 𝑧 = ( 𝑥 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑦 ) → 𝑧 ∈ 𝐻 ) ) |
42 |
41
|
rexlimivv |
⊢ ( ∃ 𝑥 ∈ ℂ ∃ 𝑦 ∈ 𝐻 𝑧 = ( 𝑥 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑦 ) → 𝑧 ∈ 𝐻 ) |
43 |
35 42
|
sylbi |
⊢ ( 𝑧 ∈ ran ( ·ℎ ↾ ( ℂ × 𝐻 ) ) → 𝑧 ∈ 𝐻 ) |
44 |
43
|
ssriv |
⊢ ran ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⊆ 𝐻 |
45 |
|
df-f |
⊢ ( ( ·ℎ ↾ ( ℂ × 𝐻 ) ) : ( ℂ × 𝐻 ) ⟶ 𝐻 ↔ ( ( ·ℎ ↾ ( ℂ × 𝐻 ) ) Fn ( ℂ × 𝐻 ) ∧ ran ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⊆ 𝐻 ) ) |
46 |
33 44 45
|
mpbir2an |
⊢ ( ·ℎ ↾ ( ℂ × 𝐻 ) ) : ( ℂ × 𝐻 ) ⟶ 𝐻 |
47 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
48 |
|
ovres |
⊢ ( ( 1 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( 1 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) = ( 1 ·ℎ 𝑥 ) ) |
49 |
47 48
|
mpan |
⊢ ( 𝑥 ∈ 𝐻 → ( 1 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) = ( 1 ·ℎ 𝑥 ) ) |
50 |
2
|
sheli |
⊢ ( 𝑥 ∈ 𝐻 → 𝑥 ∈ ℋ ) |
51 |
|
ax-hvmulid |
⊢ ( 𝑥 ∈ ℋ → ( 1 ·ℎ 𝑥 ) = 𝑥 ) |
52 |
50 51
|
syl |
⊢ ( 𝑥 ∈ 𝐻 → ( 1 ·ℎ 𝑥 ) = 𝑥 ) |
53 |
49 52
|
eqtrd |
⊢ ( 𝑥 ∈ 𝐻 → ( 1 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) = 𝑥 ) |
54 |
|
id |
⊢ ( 𝑦 ∈ ℂ → 𝑦 ∈ ℂ ) |
55 |
2
|
sheli |
⊢ ( 𝑧 ∈ 𝐻 → 𝑧 ∈ ℋ ) |
56 |
|
ax-hvdistr1 |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑦 ·ℎ ( 𝑥 +ℎ 𝑧 ) ) = ( ( 𝑦 ·ℎ 𝑥 ) +ℎ ( 𝑦 ·ℎ 𝑧 ) ) ) |
57 |
54 50 55 56
|
syl3an |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( 𝑦 ·ℎ ( 𝑥 +ℎ 𝑧 ) ) = ( ( 𝑦 ·ℎ 𝑥 ) +ℎ ( 𝑦 ·ℎ 𝑧 ) ) ) |
58 |
|
ovres |
⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑧 ) = ( 𝑥 +ℎ 𝑧 ) ) |
59 |
58
|
3adant1 |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑧 ) = ( 𝑥 +ℎ 𝑧 ) ) |
60 |
59
|
oveq2d |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑧 ) ) = ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ( 𝑥 +ℎ 𝑧 ) ) ) |
61 |
|
shaddcl |
⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( 𝑥 +ℎ 𝑧 ) ∈ 𝐻 ) |
62 |
2 61
|
mp3an1 |
⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( 𝑥 +ℎ 𝑧 ) ∈ 𝐻 ) |
63 |
|
ovres |
⊢ ( ( 𝑦 ∈ ℂ ∧ ( 𝑥 +ℎ 𝑧 ) ∈ 𝐻 ) → ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ( 𝑥 +ℎ 𝑧 ) ) = ( 𝑦 ·ℎ ( 𝑥 +ℎ 𝑧 ) ) ) |
64 |
62 63
|
sylan2 |
⊢ ( ( 𝑦 ∈ ℂ ∧ ( 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) ) → ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ( 𝑥 +ℎ 𝑧 ) ) = ( 𝑦 ·ℎ ( 𝑥 +ℎ 𝑧 ) ) ) |
65 |
64
|
3impb |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ( 𝑥 +ℎ 𝑧 ) ) = ( 𝑦 ·ℎ ( 𝑥 +ℎ 𝑧 ) ) ) |
66 |
60 65
|
eqtrd |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑧 ) ) = ( 𝑦 ·ℎ ( 𝑥 +ℎ 𝑧 ) ) ) |
67 |
|
ovres |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) ) |
68 |
67
|
3adant3 |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) ) |
69 |
|
ovres |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝐻 ) → ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑧 ) = ( 𝑦 ·ℎ 𝑧 ) ) |
70 |
69
|
3adant2 |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑧 ) = ( 𝑦 ·ℎ 𝑧 ) ) |
71 |
68 70
|
oveq12d |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑧 ) ) = ( ( 𝑦 ·ℎ 𝑥 ) ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ( 𝑦 ·ℎ 𝑧 ) ) ) |
72 |
|
shmulcl |
⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( 𝑦 ·ℎ 𝑥 ) ∈ 𝐻 ) |
73 |
2 72
|
mp3an1 |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( 𝑦 ·ℎ 𝑥 ) ∈ 𝐻 ) |
74 |
73
|
3adant3 |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( 𝑦 ·ℎ 𝑥 ) ∈ 𝐻 ) |
75 |
|
shmulcl |
⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝐻 ) → ( 𝑦 ·ℎ 𝑧 ) ∈ 𝐻 ) |
76 |
2 75
|
mp3an1 |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝐻 ) → ( 𝑦 ·ℎ 𝑧 ) ∈ 𝐻 ) |
77 |
76
|
3adant2 |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( 𝑦 ·ℎ 𝑧 ) ∈ 𝐻 ) |
78 |
74 77
|
ovresd |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( ( 𝑦 ·ℎ 𝑥 ) ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ( 𝑦 ·ℎ 𝑧 ) ) = ( ( 𝑦 ·ℎ 𝑥 ) +ℎ ( 𝑦 ·ℎ 𝑧 ) ) ) |
79 |
71 78
|
eqtrd |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑧 ) ) = ( ( 𝑦 ·ℎ 𝑥 ) +ℎ ( 𝑦 ·ℎ 𝑧 ) ) ) |
80 |
57 66 79
|
3eqtr4d |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻 ) → ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑧 ) ) = ( ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑧 ) ) ) |
81 |
|
ax-hvdistr2 |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑦 + 𝑧 ) ·ℎ 𝑥 ) = ( ( 𝑦 ·ℎ 𝑥 ) +ℎ ( 𝑧 ·ℎ 𝑥 ) ) ) |
82 |
50 81
|
syl3an3 |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( ( 𝑦 + 𝑧 ) ·ℎ 𝑥 ) = ( ( 𝑦 ·ℎ 𝑥 ) +ℎ ( 𝑧 ·ℎ 𝑥 ) ) ) |
83 |
|
addcl |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑦 + 𝑧 ) ∈ ℂ ) |
84 |
|
ovres |
⊢ ( ( ( 𝑦 + 𝑧 ) ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( ( 𝑦 + 𝑧 ) ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) = ( ( 𝑦 + 𝑧 ) ·ℎ 𝑥 ) ) |
85 |
83 84
|
stoic3 |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( ( 𝑦 + 𝑧 ) ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) = ( ( 𝑦 + 𝑧 ) ·ℎ 𝑥 ) ) |
86 |
67
|
3adant2 |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) = ( 𝑦 ·ℎ 𝑥 ) ) |
87 |
|
ovres |
⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( 𝑧 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) = ( 𝑧 ·ℎ 𝑥 ) ) |
88 |
87
|
3adant1 |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( 𝑧 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) = ( 𝑧 ·ℎ 𝑥 ) ) |
89 |
86 88
|
oveq12d |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ( 𝑧 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) ) = ( ( 𝑦 ·ℎ 𝑥 ) ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ( 𝑧 ·ℎ 𝑥 ) ) ) |
90 |
73
|
3adant2 |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( 𝑦 ·ℎ 𝑥 ) ∈ 𝐻 ) |
91 |
|
shmulcl |
⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( 𝑧 ·ℎ 𝑥 ) ∈ 𝐻 ) |
92 |
2 91
|
mp3an1 |
⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( 𝑧 ·ℎ 𝑥 ) ∈ 𝐻 ) |
93 |
92
|
3adant1 |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( 𝑧 ·ℎ 𝑥 ) ∈ 𝐻 ) |
94 |
90 93
|
ovresd |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( ( 𝑦 ·ℎ 𝑥 ) ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ( 𝑧 ·ℎ 𝑥 ) ) = ( ( 𝑦 ·ℎ 𝑥 ) +ℎ ( 𝑧 ·ℎ 𝑥 ) ) ) |
95 |
89 94
|
eqtrd |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ( 𝑧 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) ) = ( ( 𝑦 ·ℎ 𝑥 ) +ℎ ( 𝑧 ·ℎ 𝑥 ) ) ) |
96 |
82 85 95
|
3eqtr4d |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( ( 𝑦 + 𝑧 ) ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) = ( ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) ( 𝑧 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) ) ) |
97 |
|
ax-hvmulass |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑦 · 𝑧 ) ·ℎ 𝑥 ) = ( 𝑦 ·ℎ ( 𝑧 ·ℎ 𝑥 ) ) ) |
98 |
50 97
|
syl3an3 |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( ( 𝑦 · 𝑧 ) ·ℎ 𝑥 ) = ( 𝑦 ·ℎ ( 𝑧 ·ℎ 𝑥 ) ) ) |
99 |
|
mulcl |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑦 · 𝑧 ) ∈ ℂ ) |
100 |
|
ovres |
⊢ ( ( ( 𝑦 · 𝑧 ) ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( ( 𝑦 · 𝑧 ) ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) = ( ( 𝑦 · 𝑧 ) ·ℎ 𝑥 ) ) |
101 |
99 100
|
stoic3 |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( ( 𝑦 · 𝑧 ) ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) = ( ( 𝑦 · 𝑧 ) ·ℎ 𝑥 ) ) |
102 |
88
|
oveq2d |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ( 𝑧 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) ) = ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ( 𝑧 ·ℎ 𝑥 ) ) ) |
103 |
|
ovres |
⊢ ( ( 𝑦 ∈ ℂ ∧ ( 𝑧 ·ℎ 𝑥 ) ∈ 𝐻 ) → ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ( 𝑧 ·ℎ 𝑥 ) ) = ( 𝑦 ·ℎ ( 𝑧 ·ℎ 𝑥 ) ) ) |
104 |
92 103
|
sylan2 |
⊢ ( ( 𝑦 ∈ ℂ ∧ ( 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) ) → ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ( 𝑧 ·ℎ 𝑥 ) ) = ( 𝑦 ·ℎ ( 𝑧 ·ℎ 𝑥 ) ) ) |
105 |
104
|
3impb |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ( 𝑧 ·ℎ 𝑥 ) ) = ( 𝑦 ·ℎ ( 𝑧 ·ℎ 𝑥 ) ) ) |
106 |
102 105
|
eqtrd |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ( 𝑧 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) ) = ( 𝑦 ·ℎ ( 𝑧 ·ℎ 𝑥 ) ) ) |
107 |
98 101 106
|
3eqtr4d |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( ( 𝑦 · 𝑧 ) ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) = ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ( 𝑧 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) ) ) |
108 |
|
eqid |
⊢ 〈 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 〉 = 〈 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 〉 |
109 |
3 13 46 53 80 96 107 108
|
isvciOLD |
⊢ 〈 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 〉 ∈ CVecOLD |
110 |
|
normf |
⊢ normℎ : ℋ ⟶ ℝ |
111 |
|
fssres |
⊢ ( ( normℎ : ℋ ⟶ ℝ ∧ 𝐻 ⊆ ℋ ) → ( normℎ ↾ 𝐻 ) : 𝐻 ⟶ ℝ ) |
112 |
110 6 111
|
mp2an |
⊢ ( normℎ ↾ 𝐻 ) : 𝐻 ⟶ ℝ |
113 |
|
fvres |
⊢ ( 𝑥 ∈ 𝐻 → ( ( normℎ ↾ 𝐻 ) ‘ 𝑥 ) = ( normℎ ‘ 𝑥 ) ) |
114 |
113
|
eqeq1d |
⊢ ( 𝑥 ∈ 𝐻 → ( ( ( normℎ ↾ 𝐻 ) ‘ 𝑥 ) = 0 ↔ ( normℎ ‘ 𝑥 ) = 0 ) ) |
115 |
|
norm-i |
⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ 𝑥 ) = 0 ↔ 𝑥 = 0ℎ ) ) |
116 |
50 115
|
syl |
⊢ ( 𝑥 ∈ 𝐻 → ( ( normℎ ‘ 𝑥 ) = 0 ↔ 𝑥 = 0ℎ ) ) |
117 |
114 116
|
bitrd |
⊢ ( 𝑥 ∈ 𝐻 → ( ( ( normℎ ↾ 𝐻 ) ‘ 𝑥 ) = 0 ↔ 𝑥 = 0ℎ ) ) |
118 |
117
|
biimpa |
⊢ ( ( 𝑥 ∈ 𝐻 ∧ ( ( normℎ ↾ 𝐻 ) ‘ 𝑥 ) = 0 ) → 𝑥 = 0ℎ ) |
119 |
|
norm-iii |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( 𝑦 ·ℎ 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) |
120 |
50 119
|
sylan2 |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( normℎ ‘ ( 𝑦 ·ℎ 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) |
121 |
67
|
fveq2d |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( ( normℎ ↾ 𝐻 ) ‘ ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) ) = ( ( normℎ ↾ 𝐻 ) ‘ ( 𝑦 ·ℎ 𝑥 ) ) ) |
122 |
|
fvres |
⊢ ( ( 𝑦 ·ℎ 𝑥 ) ∈ 𝐻 → ( ( normℎ ↾ 𝐻 ) ‘ ( 𝑦 ·ℎ 𝑥 ) ) = ( normℎ ‘ ( 𝑦 ·ℎ 𝑥 ) ) ) |
123 |
73 122
|
syl |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( ( normℎ ↾ 𝐻 ) ‘ ( 𝑦 ·ℎ 𝑥 ) ) = ( normℎ ‘ ( 𝑦 ·ℎ 𝑥 ) ) ) |
124 |
121 123
|
eqtrd |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( ( normℎ ↾ 𝐻 ) ‘ ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) ) = ( normℎ ‘ ( 𝑦 ·ℎ 𝑥 ) ) ) |
125 |
113
|
adantl |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( ( normℎ ↾ 𝐻 ) ‘ 𝑥 ) = ( normℎ ‘ 𝑥 ) ) |
126 |
125
|
oveq2d |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( ( abs ‘ 𝑦 ) · ( ( normℎ ↾ 𝐻 ) ‘ 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) ) |
127 |
120 124 126
|
3eqtr4d |
⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ) → ( ( normℎ ↾ 𝐻 ) ‘ ( 𝑦 ( ·ℎ ↾ ( ℂ × 𝐻 ) ) 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( ( normℎ ↾ 𝐻 ) ‘ 𝑥 ) ) ) |
128 |
2
|
sheli |
⊢ ( 𝑦 ∈ 𝐻 → 𝑦 ∈ ℋ ) |
129 |
|
norm-ii |
⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ≤ ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ) |
130 |
50 128 129
|
syl2an |
⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ≤ ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ) |
131 |
|
ovres |
⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑦 ) = ( 𝑥 +ℎ 𝑦 ) ) |
132 |
131
|
fveq2d |
⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( ( normℎ ↾ 𝐻 ) ‘ ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑦 ) ) = ( ( normℎ ↾ 𝐻 ) ‘ ( 𝑥 +ℎ 𝑦 ) ) ) |
133 |
|
shaddcl |
⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻 ) |
134 |
2 133
|
mp3an1 |
⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻 ) |
135 |
|
fvres |
⊢ ( ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻 → ( ( normℎ ↾ 𝐻 ) ‘ ( 𝑥 +ℎ 𝑦 ) ) = ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) |
136 |
134 135
|
syl |
⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( ( normℎ ↾ 𝐻 ) ‘ ( 𝑥 +ℎ 𝑦 ) ) = ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) |
137 |
132 136
|
eqtrd |
⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( ( normℎ ↾ 𝐻 ) ‘ ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑦 ) ) = ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) |
138 |
|
fvres |
⊢ ( 𝑦 ∈ 𝐻 → ( ( normℎ ↾ 𝐻 ) ‘ 𝑦 ) = ( normℎ ‘ 𝑦 ) ) |
139 |
113 138
|
oveqan12d |
⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( ( ( normℎ ↾ 𝐻 ) ‘ 𝑥 ) + ( ( normℎ ↾ 𝐻 ) ‘ 𝑦 ) ) = ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ) |
140 |
130 137 139
|
3brtr4d |
⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( ( normℎ ↾ 𝐻 ) ‘ ( 𝑥 ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) 𝑦 ) ) ≤ ( ( ( normℎ ↾ 𝐻 ) ‘ 𝑥 ) + ( ( normℎ ↾ 𝐻 ) ‘ 𝑦 ) ) ) |
141 |
14 25 109 112 118 127 140 1
|
isnvi |
⊢ 𝑊 ∈ NrmCVec |