Theorem hhssnv 31352

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

Hypotheses

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

Assertion

Ref	Expression
hhssnv	⊢ 𝑊 ∈ NrmCVec

Proof of Theorem hhssnv

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hhssnv.2	. . . . 5 ⊢ 𝐻 ∈ Sℋ
2	1	hhssabloi 31350	. . . 4 ⊢ ( +ℎ ↾ (𝐻 × 𝐻)) ∈ AbelOp
3		ablogrpo 30635	. . . 4 ⊢ (( +ℎ ↾ (𝐻 × 𝐻)) ∈ AbelOp → ( +ℎ ↾ (𝐻 × 𝐻)) ∈ GrpOp)
4	2, 3	ax-mp 5	. . 3 ⊢ ( +ℎ ↾ (𝐻 × 𝐻)) ∈ GrpOp
5	1	shssii 31301	. . . . . 6 ⊢ 𝐻 ⊆ ℋ
6		xpss12 5647	. . . . . 6 ⊢ ((𝐻 ⊆ ℋ ∧ 𝐻 ⊆ ℋ) → (𝐻 × 𝐻) ⊆ ( ℋ × ℋ))
7	5, 5, 6	mp2an 693	. . . . 5 ⊢ (𝐻 × 𝐻) ⊆ ( ℋ × ℋ)
8		ax-hfvadd 31088	. . . . . 6 ⊢ +ℎ :( ℋ × ℋ)⟶ ℋ
9	8	fdmi 6681	. . . . 5 ⊢ dom +ℎ = ( ℋ × ℋ)
10	7, 9	sseqtrri 3985	. . . 4 ⊢ (𝐻 × 𝐻) ⊆ dom +ℎ
11		ssdmres 5980	. . . 4 ⊢ ((𝐻 × 𝐻) ⊆ dom +ℎ ↔ dom ( +ℎ ↾ (𝐻 × 𝐻)) = (𝐻 × 𝐻))
12	10, 11	mpbi 230	. . 3 ⊢ dom ( +ℎ ↾ (𝐻 × 𝐻)) = (𝐻 × 𝐻)
13	4, 12	grporn 30609	. 2 ⊢ 𝐻 = ran ( +ℎ ↾ (𝐻 × 𝐻))
14		sh0 31304	. . . . . 6 ⊢ (𝐻 ∈ Sℋ → 0ℎ ∈ 𝐻)
15	1, 14	ax-mp 5	. . . . 5 ⊢ 0ℎ ∈ 𝐻
16		ovres 7534	. . . . 5 ⊢ ((0ℎ ∈ 𝐻 ∧ 0ℎ ∈ 𝐻) → (0ℎ( +ℎ ↾ (𝐻 × 𝐻))0ℎ) = (0ℎ +ℎ 0ℎ))
17	15, 15, 16	mp2an 693	. . . 4 ⊢ (0ℎ( +ℎ ↾ (𝐻 × 𝐻))0ℎ) = (0ℎ +ℎ 0ℎ)
18		ax-hv0cl 31091	. . . . 5 ⊢ 0ℎ ∈ ℋ
19	18	hvaddlidi 31117	. . . 4 ⊢ (0ℎ +ℎ 0ℎ) = 0ℎ
20	17, 19	eqtri 2760	. . 3 ⊢ (0ℎ( +ℎ ↾ (𝐻 × 𝐻))0ℎ) = 0ℎ
21		eqid 2737	. . . . 5 ⊢ (GId‘( +ℎ ↾ (𝐻 × 𝐻))) = (GId‘( +ℎ ↾ (𝐻 × 𝐻)))
22	13, 21	grpoid 30608	. . . 4 ⊢ ((( +ℎ ↾ (𝐻 × 𝐻)) ∈ GrpOp ∧ 0ℎ ∈ 𝐻) → (0ℎ = (GId‘( +ℎ ↾ (𝐻 × 𝐻))) ↔ (0ℎ( +ℎ ↾ (𝐻 × 𝐻))0ℎ) = 0ℎ))
23	4, 15, 22	mp2an 693	. . 3 ⊢ (0ℎ = (GId‘( +ℎ ↾ (𝐻 × 𝐻))) ↔ (0ℎ( +ℎ ↾ (𝐻 × 𝐻))0ℎ) = 0ℎ)
24	20, 23	mpbir 231	. 2 ⊢ 0ℎ = (GId‘( +ℎ ↾ (𝐻 × 𝐻)))
25		ax-hfvmul 31093	. . . . . 6 ⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ
26		ffn 6670	. . . . . 6 ⊢ ( ·ℎ :(ℂ × ℋ)⟶ ℋ → ·ℎ Fn (ℂ × ℋ))
27	25, 26	ax-mp 5	. . . . 5 ⊢ ·ℎ Fn (ℂ × ℋ)
28		ssid 3958	. . . . . 6 ⊢ ℂ ⊆ ℂ
29		xpss12 5647	. . . . . 6 ⊢ ((ℂ ⊆ ℂ ∧ 𝐻 ⊆ ℋ) → (ℂ × 𝐻) ⊆ (ℂ × ℋ))
30	28, 5, 29	mp2an 693	. . . . 5 ⊢ (ℂ × 𝐻) ⊆ (ℂ × ℋ)
31		fnssres 6623	. . . . 5 ⊢ (( ·ℎ Fn (ℂ × ℋ) ∧ (ℂ × 𝐻) ⊆ (ℂ × ℋ)) → ( ·ℎ ↾ (ℂ × 𝐻)) Fn (ℂ × 𝐻))
32	27, 30, 31	mp2an 693	. . . 4 ⊢ ( ·ℎ ↾ (ℂ × 𝐻)) Fn (ℂ × 𝐻)
33		ovelrn 7544	. . . . . . 7 ⊢ (( ·ℎ ↾ (ℂ × 𝐻)) Fn (ℂ × 𝐻) → (𝑧 ∈ ran ( ·ℎ ↾ (ℂ × 𝐻)) ↔ ∃𝑥 ∈ ℂ ∃𝑦 ∈ 𝐻 𝑧 = (𝑥( ·ℎ ↾ (ℂ × 𝐻))𝑦)))
34	32, 33	ax-mp 5	. . . . . 6 ⊢ (𝑧 ∈ ran ( ·ℎ ↾ (ℂ × 𝐻)) ↔ ∃𝑥 ∈ ℂ ∃𝑦 ∈ 𝐻 𝑧 = (𝑥( ·ℎ ↾ (ℂ × 𝐻))𝑦))
35		ovres 7534	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑥( ·ℎ ↾ (ℂ × 𝐻))𝑦) = (𝑥 ·ℎ 𝑦))
36		shmulcl 31306	. . . . . . . . . 10 ⊢ ((𝐻 ∈ Sℋ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑥 ·ℎ 𝑦) ∈ 𝐻)
37	1, 36	mp3an1 1451	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑥 ·ℎ 𝑦) ∈ 𝐻)
38	35, 37	eqeltrd 2837	. . . . . . . 8 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑥( ·ℎ ↾ (ℂ × 𝐻))𝑦) ∈ 𝐻)
39		eleq1 2825	. . . . . . . 8 ⊢ (𝑧 = (𝑥( ·ℎ ↾ (ℂ × 𝐻))𝑦) → (𝑧 ∈ 𝐻 ↔ (𝑥( ·ℎ ↾ (ℂ × 𝐻))𝑦) ∈ 𝐻))
40	38, 39	syl5ibrcom 247	. . . . . . 7 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑧 = (𝑥( ·ℎ ↾ (ℂ × 𝐻))𝑦) → 𝑧 ∈ 𝐻))
41	40	rexlimivv 3180	. . . . . 6 ⊢ (∃𝑥 ∈ ℂ ∃𝑦 ∈ 𝐻 𝑧 = (𝑥( ·ℎ ↾ (ℂ × 𝐻))𝑦) → 𝑧 ∈ 𝐻)
42	34, 41	sylbi 217	. . . . 5 ⊢ (𝑧 ∈ ran ( ·ℎ ↾ (ℂ × 𝐻)) → 𝑧 ∈ 𝐻)
43	42	ssriv 3939	. . . 4 ⊢ ran ( ·ℎ ↾ (ℂ × 𝐻)) ⊆ 𝐻
44		df-f 6504	. . . 4 ⊢ (( ·ℎ ↾ (ℂ × 𝐻)):(ℂ × 𝐻)⟶𝐻 ↔ (( ·ℎ ↾ (ℂ × 𝐻)) Fn (ℂ × 𝐻) ∧ ran ( ·ℎ ↾ (ℂ × 𝐻)) ⊆ 𝐻))
45	32, 43, 44	mpbir2an 712	. . 3 ⊢ ( ·ℎ ↾ (ℂ × 𝐻)):(ℂ × 𝐻)⟶𝐻
46		ax-1cn 11096	. . . . 5 ⊢ 1 ∈ ℂ
47		ovres 7534	. . . . 5 ⊢ ((1 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (1( ·ℎ ↾ (ℂ × 𝐻))𝑥) = (1 ·ℎ 𝑥))
48	46, 47	mpan 691	. . . 4 ⊢ (𝑥 ∈ 𝐻 → (1( ·ℎ ↾ (ℂ × 𝐻))𝑥) = (1 ·ℎ 𝑥))
49	1	sheli 31302	. . . . 5 ⊢ (𝑥 ∈ 𝐻 → 𝑥 ∈ ℋ)
50		ax-hvmulid 31094	. . . . 5 ⊢ (𝑥 ∈ ℋ → (1 ·ℎ 𝑥) = 𝑥)
51	49, 50	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐻 → (1 ·ℎ 𝑥) = 𝑥)
52	48, 51	eqtrd 2772	. . 3 ⊢ (𝑥 ∈ 𝐻 → (1( ·ℎ ↾ (ℂ × 𝐻))𝑥) = 𝑥)
53		id 22	. . . . 5 ⊢ (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
54	1	sheli 31302	. . . . 5 ⊢ (𝑧 ∈ 𝐻 → 𝑧 ∈ ℋ)
55		ax-hvdistr1 31096	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦 ·ℎ (𝑥 +ℎ 𝑧)) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑦 ·ℎ 𝑧)))
56	53, 49, 54, 55	syl3an 1161	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦 ·ℎ (𝑥 +ℎ 𝑧)) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑦 ·ℎ 𝑧)))
57		ovres 7534	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑧) = (𝑥 +ℎ 𝑧))
58	57	3adant1 1131	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑧) = (𝑥 +ℎ 𝑧))
59	58	oveq2d 7384	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·ℎ ↾ (ℂ × 𝐻))(𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑧)) = (𝑦( ·ℎ ↾ (ℂ × 𝐻))(𝑥 +ℎ 𝑧)))
60		shaddcl 31305	. . . . . . . 8 ⊢ ((𝐻 ∈ Sℋ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥 +ℎ 𝑧) ∈ 𝐻)
61	1, 60	mp3an1 1451	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥 +ℎ 𝑧) ∈ 𝐻)
62		ovres 7534	. . . . . . 7 ⊢ ((𝑦 ∈ ℂ ∧ (𝑥 +ℎ 𝑧) ∈ 𝐻) → (𝑦( ·ℎ ↾ (ℂ × 𝐻))(𝑥 +ℎ 𝑧)) = (𝑦 ·ℎ (𝑥 +ℎ 𝑧)))
63	61, 62	sylan2 594	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ (𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻)) → (𝑦( ·ℎ ↾ (ℂ × 𝐻))(𝑥 +ℎ 𝑧)) = (𝑦 ·ℎ (𝑥 +ℎ 𝑧)))
64	63	3impb 1115	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·ℎ ↾ (ℂ × 𝐻))(𝑥 +ℎ 𝑧)) = (𝑦 ·ℎ (𝑥 +ℎ 𝑧)))
65	59, 64	eqtrd 2772	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·ℎ ↾ (ℂ × 𝐻))(𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑧)) = (𝑦 ·ℎ (𝑥 +ℎ 𝑧)))
66		ovres 7534	. . . . . . 7 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·ℎ ↾ (ℂ × 𝐻))𝑥) = (𝑦 ·ℎ 𝑥))
67	66	3adant3 1133	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·ℎ ↾ (ℂ × 𝐻))𝑥) = (𝑦 ·ℎ 𝑥))
68		ovres 7534	. . . . . . 7 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝐻) → (𝑦( ·ℎ ↾ (ℂ × 𝐻))𝑧) = (𝑦 ·ℎ 𝑧))
69	68	3adant2 1132	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·ℎ ↾ (ℂ × 𝐻))𝑧) = (𝑦 ·ℎ 𝑧))
70	67, 69	oveq12d 7386	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → ((𝑦( ·ℎ ↾ (ℂ × 𝐻))𝑥)( +ℎ ↾ (𝐻 × 𝐻))(𝑦( ·ℎ ↾ (ℂ × 𝐻))𝑧)) = ((𝑦 ·ℎ 𝑥)( +ℎ ↾ (𝐻 × 𝐻))(𝑦 ·ℎ 𝑧)))
71		shmulcl 31306	. . . . . . . 8 ⊢ ((𝐻 ∈ Sℋ ∧ 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦 ·ℎ 𝑥) ∈ 𝐻)
72	1, 71	mp3an1 1451	. . . . . . 7 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦 ·ℎ 𝑥) ∈ 𝐻)
73	72	3adant3 1133	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦 ·ℎ 𝑥) ∈ 𝐻)
74		shmulcl 31306	. . . . . . . 8 ⊢ ((𝐻 ∈ Sℋ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝐻) → (𝑦 ·ℎ 𝑧) ∈ 𝐻)
75	1, 74	mp3an1 1451	. . . . . . 7 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝐻) → (𝑦 ·ℎ 𝑧) ∈ 𝐻)
76	75	3adant2 1132	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦 ·ℎ 𝑧) ∈ 𝐻)
77	73, 76	ovresd 7535	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → ((𝑦 ·ℎ 𝑥)( +ℎ ↾ (𝐻 × 𝐻))(𝑦 ·ℎ 𝑧)) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑦 ·ℎ 𝑧)))
78	70, 77	eqtrd 2772	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → ((𝑦( ·ℎ ↾ (ℂ × 𝐻))𝑥)( +ℎ ↾ (𝐻 × 𝐻))(𝑦( ·ℎ ↾ (ℂ × 𝐻))𝑧)) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑦 ·ℎ 𝑧)))
79	56, 65, 78	3eqtr4d 2782	. . 3 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·ℎ ↾ (ℂ × 𝐻))(𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑧)) = ((𝑦( ·ℎ ↾ (ℂ × 𝐻))𝑥)( +ℎ ↾ (𝐻 × 𝐻))(𝑦( ·ℎ ↾ (ℂ × 𝐻))𝑧)))
80		ax-hvdistr2 31097	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℋ) → ((𝑦 + 𝑧) ·ℎ 𝑥) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑧 ·ℎ 𝑥)))
81	49, 80	syl3an3 1166	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 + 𝑧) ·ℎ 𝑥) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑧 ·ℎ 𝑥)))
82		addcl 11120	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑦 + 𝑧) ∈ ℂ)
83		ovres 7534	. . . . 5 ⊢ (((𝑦 + 𝑧) ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 + 𝑧)( ·ℎ ↾ (ℂ × 𝐻))𝑥) = ((𝑦 + 𝑧) ·ℎ 𝑥))
84	82, 83	stoic3 1778	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 + 𝑧)( ·ℎ ↾ (ℂ × 𝐻))𝑥) = ((𝑦 + 𝑧) ·ℎ 𝑥))
85	66	3adant2 1132	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·ℎ ↾ (ℂ × 𝐻))𝑥) = (𝑦 ·ℎ 𝑥))
86		ovres 7534	. . . . . . 7 ⊢ ((𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧( ·ℎ ↾ (ℂ × 𝐻))𝑥) = (𝑧 ·ℎ 𝑥))
87	86	3adant1 1131	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧( ·ℎ ↾ (ℂ × 𝐻))𝑥) = (𝑧 ·ℎ 𝑥))
88	85, 87	oveq12d 7386	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦( ·ℎ ↾ (ℂ × 𝐻))𝑥)( +ℎ ↾ (𝐻 × 𝐻))(𝑧( ·ℎ ↾ (ℂ × 𝐻))𝑥)) = ((𝑦 ·ℎ 𝑥)( +ℎ ↾ (𝐻 × 𝐻))(𝑧 ·ℎ 𝑥)))
89	72	3adant2 1132	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦 ·ℎ 𝑥) ∈ 𝐻)
90		shmulcl 31306	. . . . . . . 8 ⊢ ((𝐻 ∈ Sℋ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧 ·ℎ 𝑥) ∈ 𝐻)
91	1, 90	mp3an1 1451	. . . . . . 7 ⊢ ((𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧 ·ℎ 𝑥) ∈ 𝐻)
92	91	3adant1 1131	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧 ·ℎ 𝑥) ∈ 𝐻)
93	89, 92	ovresd 7535	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 ·ℎ 𝑥)( +ℎ ↾ (𝐻 × 𝐻))(𝑧 ·ℎ 𝑥)) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑧 ·ℎ 𝑥)))
94	88, 93	eqtrd 2772	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦( ·ℎ ↾ (ℂ × 𝐻))𝑥)( +ℎ ↾ (𝐻 × 𝐻))(𝑧( ·ℎ ↾ (ℂ × 𝐻))𝑥)) = ((𝑦 ·ℎ 𝑥) +ℎ (𝑧 ·ℎ 𝑥)))
95	81, 84, 94	3eqtr4d 2782	. . 3 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 + 𝑧)( ·ℎ ↾ (ℂ × 𝐻))𝑥) = ((𝑦( ·ℎ ↾ (ℂ × 𝐻))𝑥)( +ℎ ↾ (𝐻 × 𝐻))(𝑧( ·ℎ ↾ (ℂ × 𝐻))𝑥)))
96		ax-hvmulass 31095	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℋ) → ((𝑦 · 𝑧) ·ℎ 𝑥) = (𝑦 ·ℎ (𝑧 ·ℎ 𝑥)))
97	49, 96	syl3an3 1166	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 · 𝑧) ·ℎ 𝑥) = (𝑦 ·ℎ (𝑧 ·ℎ 𝑥)))
98		mulcl 11122	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑦 · 𝑧) ∈ ℂ)
99		ovres 7534	. . . . 5 ⊢ (((𝑦 · 𝑧) ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 · 𝑧)( ·ℎ ↾ (ℂ × 𝐻))𝑥) = ((𝑦 · 𝑧) ·ℎ 𝑥))
100	98, 99	stoic3 1778	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 · 𝑧)( ·ℎ ↾ (ℂ × 𝐻))𝑥) = ((𝑦 · 𝑧) ·ℎ 𝑥))
101	87	oveq2d 7384	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·ℎ ↾ (ℂ × 𝐻))(𝑧( ·ℎ ↾ (ℂ × 𝐻))𝑥)) = (𝑦( ·ℎ ↾ (ℂ × 𝐻))(𝑧 ·ℎ 𝑥)))
102		ovres 7534	. . . . . . 7 ⊢ ((𝑦 ∈ ℂ ∧ (𝑧 ·ℎ 𝑥) ∈ 𝐻) → (𝑦( ·ℎ ↾ (ℂ × 𝐻))(𝑧 ·ℎ 𝑥)) = (𝑦 ·ℎ (𝑧 ·ℎ 𝑥)))
103	91, 102	sylan2 594	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ (𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻)) → (𝑦( ·ℎ ↾ (ℂ × 𝐻))(𝑧 ·ℎ 𝑥)) = (𝑦 ·ℎ (𝑧 ·ℎ 𝑥)))
104	103	3impb 1115	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·ℎ ↾ (ℂ × 𝐻))(𝑧 ·ℎ 𝑥)) = (𝑦 ·ℎ (𝑧 ·ℎ 𝑥)))
105	101, 104	eqtrd 2772	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·ℎ ↾ (ℂ × 𝐻))(𝑧( ·ℎ ↾ (ℂ × 𝐻))𝑥)) = (𝑦 ·ℎ (𝑧 ·ℎ 𝑥)))
106	97, 100, 105	3eqtr4d 2782	. . 3 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 · 𝑧)( ·ℎ ↾ (ℂ × 𝐻))𝑥) = (𝑦( ·ℎ ↾ (ℂ × 𝐻))(𝑧( ·ℎ ↾ (ℂ × 𝐻))𝑥)))
107		eqid 2737	. . 3 ⊢ ⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩ = ⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩
108	2, 12, 45, 52, 79, 95, 106, 107	isvciOLD 30668	. 2 ⊢ ⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩ ∈ CVecOLD
109		normf 31211	. . 3 ⊢ normℎ: ℋ⟶ℝ
110		fssres 6708	. . 3 ⊢ ((normℎ: ℋ⟶ℝ ∧ 𝐻 ⊆ ℋ) → (normℎ ↾ 𝐻):𝐻⟶ℝ)
111	109, 5, 110	mp2an 693	. 2 ⊢ (normℎ ↾ 𝐻):𝐻⟶ℝ
112		fvres 6861	. . . . 5 ⊢ (𝑥 ∈ 𝐻 → ((normℎ ↾ 𝐻)‘𝑥) = (normℎ‘𝑥))
113	112	eqeq1d 2739	. . . 4 ⊢ (𝑥 ∈ 𝐻 → (((normℎ ↾ 𝐻)‘𝑥) = 0 ↔ (normℎ‘𝑥) = 0))
114		norm-i 31217	. . . . 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 31228	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℋ) → (normℎ‘(𝑦 ·ℎ 𝑥)) = ((abs‘𝑦) · (normℎ‘𝑥)))
119	49, 118	sylan2 594	. . 3 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (normℎ‘(𝑦 ·ℎ 𝑥)) = ((abs‘𝑦) · (normℎ‘𝑥)))
120	66	fveq2d 6846	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((normℎ ↾ 𝐻)‘(𝑦( ·ℎ ↾ (ℂ × 𝐻))𝑥)) = ((normℎ ↾ 𝐻)‘(𝑦 ·ℎ 𝑥)))
121		fvres 6861	. . . . 5 ⊢ ((𝑦 ·ℎ 𝑥) ∈ 𝐻 → ((normℎ ↾ 𝐻)‘(𝑦 ·ℎ 𝑥)) = (normℎ‘(𝑦 ·ℎ 𝑥)))
122	72, 121	syl 17	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((normℎ ↾ 𝐻)‘(𝑦 ·ℎ 𝑥)) = (normℎ‘(𝑦 ·ℎ 𝑥)))
123	120, 122	eqtrd 2772	. . 3 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((normℎ ↾ 𝐻)‘(𝑦( ·ℎ ↾ (ℂ × 𝐻))𝑥)) = (normℎ‘(𝑦 ·ℎ 𝑥)))
124	112	adantl 481	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((normℎ ↾ 𝐻)‘𝑥) = (normℎ‘𝑥))
125	124	oveq2d 7384	. . 3 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((abs‘𝑦) · ((normℎ ↾ 𝐻)‘𝑥)) = ((abs‘𝑦) · (normℎ‘𝑥)))
126	119, 123, 125	3eqtr4d 2782	. 2 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((normℎ ↾ 𝐻)‘(𝑦( ·ℎ ↾ (ℂ × 𝐻))𝑥)) = ((abs‘𝑦) · ((normℎ ↾ 𝐻)‘𝑥)))
127	1	sheli 31302	. . . 4 ⊢ (𝑦 ∈ 𝐻 → 𝑦 ∈ ℋ)
128		norm-ii 31226	. . . 4 ⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (normℎ‘(𝑥 +ℎ 𝑦)) ≤ ((normℎ‘𝑥) + (normℎ‘𝑦)))
129	49, 127, 128	syl2an 597	. . 3 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (normℎ‘(𝑥 +ℎ 𝑦)) ≤ ((normℎ‘𝑥) + (normℎ‘𝑦)))
130		ovres 7534	. . . . 5 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑦) = (𝑥 +ℎ 𝑦))
131	130	fveq2d 6846	. . . 4 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → ((normℎ ↾ 𝐻)‘(𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑦)) = ((normℎ ↾ 𝐻)‘(𝑥 +ℎ 𝑦)))
132		shaddcl 31305	. . . . . 6 ⊢ ((𝐻 ∈ Sℋ ∧ 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (𝑥 +ℎ 𝑦) ∈ 𝐻)
133	1, 132	mp3an1 1451	. . . . 5 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (𝑥 +ℎ 𝑦) ∈ 𝐻)
134		fvres 6861	. . . . 5 ⊢ ((𝑥 +ℎ 𝑦) ∈ 𝐻 → ((normℎ ↾ 𝐻)‘(𝑥 +ℎ 𝑦)) = (normℎ‘(𝑥 +ℎ 𝑦)))
135	133, 134	syl 17	. . . 4 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → ((normℎ ↾ 𝐻)‘(𝑥 +ℎ 𝑦)) = (normℎ‘(𝑥 +ℎ 𝑦)))
136	131, 135	eqtrd 2772	. . 3 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → ((normℎ ↾ 𝐻)‘(𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑦)) = (normℎ‘(𝑥 +ℎ 𝑦)))
137		fvres 6861	. . . 4 ⊢ (𝑦 ∈ 𝐻 → ((normℎ ↾ 𝐻)‘𝑦) = (normℎ‘𝑦))
138	112, 137	oveqan12d 7387	. . 3 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (((normℎ ↾ 𝐻)‘𝑥) + ((normℎ ↾ 𝐻)‘𝑦)) = ((normℎ‘𝑥) + (normℎ‘𝑦)))
139	129, 136, 138	3brtr4d 5132	. 2 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → ((normℎ ↾ 𝐻)‘(𝑥( +ℎ ↾ (𝐻 × 𝐻))𝑦)) ≤ (((normℎ ↾ 𝐻)‘𝑥) + ((normℎ ↾ 𝐻)‘𝑦)))
140		hhssnvt.1	. 2 ⊢ 𝑊 = ⟨⟨( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))⟩, (normℎ ↾ 𝐻)⟩
141	13, 24, 108, 111, 117, 126, 139, 140	isnvi 30701	1 ⊢ 𝑊 ∈ NrmCVec

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∃wrex 3062   ⊆ wss 3903  ⟨cop 4588   class class class wbr 5100   × cxp 5630  dom cdm 5632  ran crn 5633   ↾ cres 5634   Fn wfn 6495  ⟶wf 6496  ‘cfv 6500  (class class class)co 7368  ℂcc 11036  ℝcr 11037  0cc0 11038  1c1 11039   + caddc 11041   · cmul 11043   ≤ cle 11179  abscabs 15169  GrpOpcgr 30577  GIdcgi 30578  AbelOpcablo 30632  NrmCVeccnv 30672   ℋchba 31007   +_ℎ cva 31008   ·_ℎ csm 31009  norm_ℎcno 31011  0_ℎc0v 31012   S_ℋ csh 31016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-pre-sup 11116  ax-hilex 31087  ax-hfvadd 31088  ax-hvcom 31089  ax-hvass 31090  ax-hv0cl 31091  ax-hvaddid 31092  ax-hfvmul 31093  ax-hvmulid 31094  ax-hvmulass 31095  ax-hvdistr1 31096  ax-hvdistr2 31097  ax-hvmul0 31098  ax-hfi 31167  ax-his1 31170  ax-his2 31171  ax-his3 31172  ax-his4 31173

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-om 7819  df-1st 7943  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-sup 9357  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-div 11807  df-nn 12158  df-2 12220  df-3 12221  df-4 12222  df-n0 12414  df-z 12501  df-uz 12764  df-rp 12918  df-seq 13937  df-exp 13997  df-cj 15034  df-re 15035  df-im 15036  df-sqrt 15170  df-abs 15171  df-grpo 30581  df-gid 30582  df-ginv 30583  df-ablo 30633  df-vc 30647  df-nv 30680  df-va 30683  df-ba 30684  df-sm 30685  df-0v 30686  df-nmcv 30688  df-hnorm 31056  df-hba 31057  df-hvsub 31059  df-sh 31295

This theorem is referenced by:  hhssnvt  31353  hhssvsf  31361  hhssims  31362  hhssmet  31364  hhssmetdval  31365  hhssbnOLD  31367