This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hhssnv

Description: Normed complex vector space property of a subspace. (Contributed by NM, 26-Mar-2008) (New usage is discouraged.)

Ref Expression
Hypotheses hhssnvt.1 ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
hhssnv.2 ⊢ 𝐻 ∈ Sℋ
Assertion hhssnv 𝑊 ∈ NrmCVec

Proof

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 hvaddlidi ⊢ ( 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