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 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