hhssnv - Hilbert Space Explorer

	Hilbert Space Explorer		< Previous Next > Nearby theorems
Mirrors > Home > HSE Home > Th. List > hhssnv		Structured version Visualization version GIF version

Theorem hhssnv 30206

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 30204	. . . 4 ⊢ ( +_ℎ ↾ (𝐻 × 𝐻)) ∈ AbelOp
3		ablogrpo 29489	. . . 4 ⊢ (( +_ℎ ↾ (𝐻 × 𝐻)) ∈ AbelOp → ( +_ℎ ↾ (𝐻 × 𝐻)) ∈ GrpOp)
4	2, 3	ax-mp 5	. . 3 ⊢ ( +_ℎ ↾ (𝐻 × 𝐻)) ∈ GrpOp
5	1	shssii 30155	. . . . . 6 ⊢ 𝐻 ⊆ ℋ
6		xpss12 5648	. . . . . 6 ⊢ ((𝐻 ⊆ ℋ ∧ 𝐻 ⊆ ℋ) → (𝐻 × 𝐻) ⊆ ( ℋ × ℋ))
7	5, 5, 6	mp2an 690	. . . . 5 ⊢ (𝐻 × 𝐻) ⊆ ( ℋ × ℋ)
8		ax-hfvadd 29942	. . . . . 6 ⊢ +_ℎ :( ℋ × ℋ)⟶ ℋ
9	8	fdmi 6680	. . . . 5 ⊢ dom +_ℎ = ( ℋ × ℋ)
10	7, 9	sseqtrri 3981	. . . 4 ⊢ (𝐻 × 𝐻) ⊆ dom +_ℎ
11		ssdmres 5960	. . . 4 ⊢ ((𝐻 × 𝐻) ⊆ dom +_ℎ ↔ dom ( +_ℎ ↾ (𝐻 × 𝐻)) = (𝐻 × 𝐻))
12	10, 11	mpbi 229	. . 3 ⊢ dom ( +_ℎ ↾ (𝐻 × 𝐻)) = (𝐻 × 𝐻)
13	4, 12	grporn 29463	. 2 ⊢ 𝐻 = ran ( +_ℎ ↾ (𝐻 × 𝐻))
14		sh0 30158	. . . . . 6 ⊢ (𝐻 ∈ S_ℋ → 0_ℎ ∈ 𝐻)
15	1, 14	ax-mp 5	. . . . 5 ⊢ 0_ℎ ∈ 𝐻
16		ovres 7520	. . . . 5 ⊢ ((0_ℎ ∈ 𝐻 ∧ 0_ℎ ∈ 𝐻) → (0_ℎ( +_ℎ ↾ (𝐻 × 𝐻))0_ℎ) = (0_ℎ +_ℎ 0_ℎ))
17	15, 15, 16	mp2an 690	. . . 4 ⊢ (0_ℎ( +_ℎ ↾ (𝐻 × 𝐻))0_ℎ) = (0_ℎ +_ℎ 0_ℎ)
18		ax-hv0cl 29945	. . . . 5 ⊢ 0_ℎ ∈ ℋ
19	18	hvaddid2i 29971	. . . 4 ⊢ (0_ℎ +_ℎ 0_ℎ) = 0_ℎ
20	17, 19	eqtri 2764	. . 3 ⊢ (0_ℎ( +_ℎ ↾ (𝐻 × 𝐻))0_ℎ) = 0_ℎ
21		eqid 2736	. . . . 5 ⊢ (GId‘( +_ℎ ↾ (𝐻 × 𝐻))) = (GId‘( +_ℎ ↾ (𝐻 × 𝐻)))
22	13, 21	grpoid 29462	. . . 4 ⊢ ((( +_ℎ ↾ (𝐻 × 𝐻)) ∈ GrpOp ∧ 0_ℎ ∈ 𝐻) → (0_ℎ = (GId‘( +_ℎ ↾ (𝐻 × 𝐻))) ↔ (0_ℎ( +_ℎ ↾ (𝐻 × 𝐻))0_ℎ) = 0_ℎ))
23	4, 15, 22	mp2an 690	. . 3 ⊢ (0_ℎ = (GId‘( +_ℎ ↾ (𝐻 × 𝐻))) ↔ (0_ℎ( +_ℎ ↾ (𝐻 × 𝐻))0_ℎ) = 0_ℎ)
24	20, 23	mpbir 230	. 2 ⊢ 0_ℎ = (GId‘( +_ℎ ↾ (𝐻 × 𝐻)))
25		ax-hfvmul 29947	. . . . . 6 ⊢ ·_ℎ :(ℂ × ℋ)⟶ ℋ
26		ffn 6668	. . . . . 6 ⊢ ( ·_ℎ :(ℂ × ℋ)⟶ ℋ → ·_ℎ Fn (ℂ × ℋ))
27	25, 26	ax-mp 5	. . . . 5 ⊢ ·_ℎ Fn (ℂ × ℋ)
28		ssid 3966	. . . . . 6 ⊢ ℂ ⊆ ℂ
29		xpss12 5648	. . . . . 6 ⊢ ((ℂ ⊆ ℂ ∧ 𝐻 ⊆ ℋ) → (ℂ × 𝐻) ⊆ (ℂ × ℋ))
30	28, 5, 29	mp2an 690	. . . . 5 ⊢ (ℂ × 𝐻) ⊆ (ℂ × ℋ)
31		fnssres 6624	. . . . 5 ⊢ (( ·_ℎ Fn (ℂ × ℋ) ∧ (ℂ × 𝐻) ⊆ (ℂ × ℋ)) → ( ·_ℎ ↾ (ℂ × 𝐻)) Fn (ℂ × 𝐻))
32	27, 30, 31	mp2an 690	. . . 4 ⊢ ( ·_ℎ ↾ (ℂ × 𝐻)) Fn (ℂ × 𝐻)
33		ovelrn 7530	. . . . . . 7 ⊢ (( ·_ℎ ↾ (ℂ × 𝐻)) Fn (ℂ × 𝐻) → (𝑧 ∈ ran ( ·_ℎ ↾ (ℂ × 𝐻)) ↔ ∃𝑥 ∈ ℂ ∃𝑦 ∈ 𝐻 𝑧 = (𝑥( ·_ℎ ↾ (ℂ × 𝐻))𝑦)))
34	32, 33	ax-mp 5	. . . . . 6 ⊢ (𝑧 ∈ ran ( ·_ℎ ↾ (ℂ × 𝐻)) ↔ ∃𝑥 ∈ ℂ ∃𝑦 ∈ 𝐻 𝑧 = (𝑥( ·_ℎ ↾ (ℂ × 𝐻))𝑦))
35		ovres 7520	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑥( ·_ℎ ↾ (ℂ × 𝐻))𝑦) = (𝑥 ·_ℎ 𝑦))
36		shmulcl 30160	. . . . . . . . . 10 ⊢ ((𝐻 ∈ S_ℋ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑥 ·_ℎ 𝑦) ∈ 𝐻)
37	1, 36	mp3an1 1448	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑥 ·_ℎ 𝑦) ∈ 𝐻)
38	35, 37	eqeltrd 2838	. . . . . . . 8 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑥( ·_ℎ ↾ (ℂ × 𝐻))𝑦) ∈ 𝐻)
39		eleq1 2825	. . . . . . . 8 ⊢ (𝑧 = (𝑥( ·_ℎ ↾ (ℂ × 𝐻))𝑦) → (𝑧 ∈ 𝐻 ↔ (𝑥( ·_ℎ ↾ (ℂ × 𝐻))𝑦) ∈ 𝐻))
40	38, 39	syl5ibrcom 246	. . . . . . 7 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑧 = (𝑥( ·_ℎ ↾ (ℂ × 𝐻))𝑦) → 𝑧 ∈ 𝐻))
41	40	rexlimivv 3196	. . . . . 6 ⊢ (∃𝑥 ∈ ℂ ∃𝑦 ∈ 𝐻 𝑧 = (𝑥( ·_ℎ ↾ (ℂ × 𝐻))𝑦) → 𝑧 ∈ 𝐻)
42	34, 41	sylbi 216	. . . . 5 ⊢ (𝑧 ∈ ran ( ·_ℎ ↾ (ℂ × 𝐻)) → 𝑧 ∈ 𝐻)
43	42	ssriv 3948	. . . 4 ⊢ ran ( ·_ℎ ↾ (ℂ × 𝐻)) ⊆ 𝐻
44		df-f 6500	. . . 4 ⊢ (( ·_ℎ ↾ (ℂ × 𝐻)):(ℂ × 𝐻)⟶𝐻 ↔ (( ·_ℎ ↾ (ℂ × 𝐻)) Fn (ℂ × 𝐻) ∧ ran ( ·_ℎ ↾ (ℂ × 𝐻)) ⊆ 𝐻))
45	32, 43, 44	mpbir2an 709	. . 3 ⊢ ( ·_ℎ ↾ (ℂ × 𝐻)):(ℂ × 𝐻)⟶𝐻
46		ax-1cn 11109	. . . . 5 ⊢ 1 ∈ ℂ
47		ovres 7520	. . . . 5 ⊢ ((1 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (1( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = (1 ·_ℎ 𝑥))
48	46, 47	mpan 688	. . . 4 ⊢ (𝑥 ∈ 𝐻 → (1( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = (1 ·_ℎ 𝑥))
49	1	sheli 30156	. . . . 5 ⊢ (𝑥 ∈ 𝐻 → 𝑥 ∈ ℋ)
50		ax-hvmulid 29948	. . . . 5 ⊢ (𝑥 ∈ ℋ → (1 ·_ℎ 𝑥) = 𝑥)
51	49, 50	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐻 → (1 ·_ℎ 𝑥) = 𝑥)
52	48, 51	eqtrd 2776	. . 3 ⊢ (𝑥 ∈ 𝐻 → (1( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = 𝑥)
53		id 22	. . . . 5 ⊢ (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
54	1	sheli 30156	. . . . 5 ⊢ (𝑧 ∈ 𝐻 → 𝑧 ∈ ℋ)
55		ax-hvdistr1 29950	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦 ·_ℎ (𝑥 +_ℎ 𝑧)) = ((𝑦 ·_ℎ 𝑥) +_ℎ (𝑦 ·_ℎ 𝑧)))
56	53, 49, 54, 55	syl3an 1160	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦 ·_ℎ (𝑥 +_ℎ 𝑧)) = ((𝑦 ·_ℎ 𝑥) +_ℎ (𝑦 ·_ℎ 𝑧)))
57		ovres 7520	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥( +_ℎ ↾ (𝐻 × 𝐻))𝑧) = (𝑥 +_ℎ 𝑧))
58	57	3adant1 1130	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥( +_ℎ ↾ (𝐻 × 𝐻))𝑧) = (𝑥 +_ℎ 𝑧))
59	58	oveq2d 7373	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑥( +_ℎ ↾ (𝐻 × 𝐻))𝑧)) = (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑥 +_ℎ 𝑧)))
60		shaddcl 30159	. . . . . . . 8 ⊢ ((𝐻 ∈ S_ℋ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥 +_ℎ 𝑧) ∈ 𝐻)
61	1, 60	mp3an1 1448	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥 +_ℎ 𝑧) ∈ 𝐻)
62		ovres 7520	. . . . . . 7 ⊢ ((𝑦 ∈ ℂ ∧ (𝑥 +_ℎ 𝑧) ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑥 +_ℎ 𝑧)) = (𝑦 ·_ℎ (𝑥 +_ℎ 𝑧)))
63	61, 62	sylan2 593	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ (𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻)) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑥 +_ℎ 𝑧)) = (𝑦 ·_ℎ (𝑥 +_ℎ 𝑧)))
64	63	3impb 1115	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑥 +_ℎ 𝑧)) = (𝑦 ·_ℎ (𝑥 +_ℎ 𝑧)))
65	59, 64	eqtrd 2776	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑥( +_ℎ ↾ (𝐻 × 𝐻))𝑧)) = (𝑦 ·_ℎ (𝑥 +_ℎ 𝑧)))
66		ovres 7520	. . . . . . 7 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = (𝑦 ·_ℎ 𝑥))
67	66	3adant3 1132	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = (𝑦 ·_ℎ 𝑥))
68		ovres 7520	. . . . . . 7 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑧) = (𝑦 ·_ℎ 𝑧))
69	68	3adant2 1131	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑧) = (𝑦 ·_ℎ 𝑧))
70	67, 69	oveq12d 7375	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → ((𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥)( +_ℎ ↾ (𝐻 × 𝐻))(𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑧)) = ((𝑦 ·_ℎ 𝑥)( +_ℎ ↾ (𝐻 × 𝐻))(𝑦 ·_ℎ 𝑧)))
71		shmulcl 30160	. . . . . . . 8 ⊢ ((𝐻 ∈ S_ℋ ∧ 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦 ·_ℎ 𝑥) ∈ 𝐻)
72	1, 71	mp3an1 1448	. . . . . . 7 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦 ·_ℎ 𝑥) ∈ 𝐻)
73	72	3adant3 1132	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦 ·_ℎ 𝑥) ∈ 𝐻)
74		shmulcl 30160	. . . . . . . 8 ⊢ ((𝐻 ∈ S_ℋ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝐻) → (𝑦 ·_ℎ 𝑧) ∈ 𝐻)
75	1, 74	mp3an1 1448	. . . . . . 7 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝐻) → (𝑦 ·_ℎ 𝑧) ∈ 𝐻)
76	75	3adant2 1131	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦 ·_ℎ 𝑧) ∈ 𝐻)
77	73, 76	ovresd 7521	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → ((𝑦 ·_ℎ 𝑥)( +_ℎ ↾ (𝐻 × 𝐻))(𝑦 ·_ℎ 𝑧)) = ((𝑦 ·_ℎ 𝑥) +_ℎ (𝑦 ·_ℎ 𝑧)))
78	70, 77	eqtrd 2776	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → ((𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥)( +_ℎ ↾ (𝐻 × 𝐻))(𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑧)) = ((𝑦 ·_ℎ 𝑥) +_ℎ (𝑦 ·_ℎ 𝑧)))
79	56, 65, 78	3eqtr4d 2786	. . 3 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑥( +_ℎ ↾ (𝐻 × 𝐻))𝑧)) = ((𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥)( +_ℎ ↾ (𝐻 × 𝐻))(𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑧)))
80		ax-hvdistr2 29951	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℋ) → ((𝑦 + 𝑧) ·_ℎ 𝑥) = ((𝑦 ·_ℎ 𝑥) +_ℎ (𝑧 ·_ℎ 𝑥)))
81	49, 80	syl3an3 1165	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 + 𝑧) ·_ℎ 𝑥) = ((𝑦 ·_ℎ 𝑥) +_ℎ (𝑧 ·_ℎ 𝑥)))
82		addcl 11133	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑦 + 𝑧) ∈ ℂ)
83		ovres 7520	. . . . 5 ⊢ (((𝑦 + 𝑧) ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 + 𝑧)( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = ((𝑦 + 𝑧) ·_ℎ 𝑥))
84	82, 83	stoic3 1778	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 + 𝑧)( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = ((𝑦 + 𝑧) ·_ℎ 𝑥))
85	66	3adant2 1131	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = (𝑦 ·_ℎ 𝑥))
86		ovres 7520	. . . . . . 7 ⊢ ((𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = (𝑧 ·_ℎ 𝑥))
87	86	3adant1 1130	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = (𝑧 ·_ℎ 𝑥))
88	85, 87	oveq12d 7375	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥)( +_ℎ ↾ (𝐻 × 𝐻))(𝑧( ·_ℎ ↾ (ℂ × 𝐻))𝑥)) = ((𝑦 ·_ℎ 𝑥)( +_ℎ ↾ (𝐻 × 𝐻))(𝑧 ·_ℎ 𝑥)))
89	72	3adant2 1131	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦 ·_ℎ 𝑥) ∈ 𝐻)
90		shmulcl 30160	. . . . . . . 8 ⊢ ((𝐻 ∈ S_ℋ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧 ·_ℎ 𝑥) ∈ 𝐻)
91	1, 90	mp3an1 1448	. . . . . . 7 ⊢ ((𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧 ·_ℎ 𝑥) ∈ 𝐻)
92	91	3adant1 1130	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧 ·_ℎ 𝑥) ∈ 𝐻)
93	89, 92	ovresd 7521	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 ·_ℎ 𝑥)( +_ℎ ↾ (𝐻 × 𝐻))(𝑧 ·_ℎ 𝑥)) = ((𝑦 ·_ℎ 𝑥) +_ℎ (𝑧 ·_ℎ 𝑥)))
94	88, 93	eqtrd 2776	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥)( +_ℎ ↾ (𝐻 × 𝐻))(𝑧( ·_ℎ ↾ (ℂ × 𝐻))𝑥)) = ((𝑦 ·_ℎ 𝑥) +_ℎ (𝑧 ·_ℎ 𝑥)))
95	81, 84, 94	3eqtr4d 2786	. . 3 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 + 𝑧)( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = ((𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥)( +_ℎ ↾ (𝐻 × 𝐻))(𝑧( ·_ℎ ↾ (ℂ × 𝐻))𝑥)))
96		ax-hvmulass 29949	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℋ) → ((𝑦 · 𝑧) ·_ℎ 𝑥) = (𝑦 ·_ℎ (𝑧 ·_ℎ 𝑥)))
97	49, 96	syl3an3 1165	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 · 𝑧) ·_ℎ 𝑥) = (𝑦 ·_ℎ (𝑧 ·_ℎ 𝑥)))
98		mulcl 11135	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑦 · 𝑧) ∈ ℂ)
99		ovres 7520	. . . . 5 ⊢ (((𝑦 · 𝑧) ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 · 𝑧)( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = ((𝑦 · 𝑧) ·_ℎ 𝑥))
100	98, 99	stoic3 1778	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 · 𝑧)( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = ((𝑦 · 𝑧) ·_ℎ 𝑥))
101	87	oveq2d 7373	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑧( ·_ℎ ↾ (ℂ × 𝐻))𝑥)) = (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑧 ·_ℎ 𝑥)))
102		ovres 7520	. . . . . . 7 ⊢ ((𝑦 ∈ ℂ ∧ (𝑧 ·_ℎ 𝑥) ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑧 ·_ℎ 𝑥)) = (𝑦 ·_ℎ (𝑧 ·_ℎ 𝑥)))
103	91, 102	sylan2 593	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ (𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻)) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑧 ·_ℎ 𝑥)) = (𝑦 ·_ℎ (𝑧 ·_ℎ 𝑥)))
104	103	3impb 1115	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑧 ·_ℎ 𝑥)) = (𝑦 ·_ℎ (𝑧 ·_ℎ 𝑥)))
105	101, 104	eqtrd 2776	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑧( ·_ℎ ↾ (ℂ × 𝐻))𝑥)) = (𝑦 ·_ℎ (𝑧 ·_ℎ 𝑥)))
106	97, 100, 105	3eqtr4d 2786	. . 3 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 · 𝑧)( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑧( ·_ℎ ↾ (ℂ × 𝐻))𝑥)))
107		eqid 2736	. . 3 ⊢ ⟨( +_ℎ ↾ (𝐻 × 𝐻)), ( ·_ℎ ↾ (ℂ × 𝐻))⟩ = ⟨( +_ℎ ↾ (𝐻 × 𝐻)), ( ·_ℎ ↾ (ℂ × 𝐻))⟩
108	2, 12, 45, 52, 79, 95, 106, 107	isvciOLD 29522	. 2 ⊢ ⟨( +_ℎ ↾ (𝐻 × 𝐻)), ( ·_ℎ ↾ (ℂ × 𝐻))⟩ ∈ CVec_OLD
109		normf 30065	. . 3 ⊢ norm_ℎ: ℋ⟶ℝ
110		fssres 6708	. . 3 ⊢ ((norm_ℎ: ℋ⟶ℝ ∧ 𝐻 ⊆ ℋ) → (norm_ℎ ↾ 𝐻):𝐻⟶ℝ)
111	109, 5, 110	mp2an 690	. 2 ⊢ (norm_ℎ ↾ 𝐻):𝐻⟶ℝ
112		fvres 6861	. . . . 5 ⊢ (𝑥 ∈ 𝐻 → ((norm_ℎ ↾ 𝐻)‘𝑥) = (norm_ℎ‘𝑥))
113	112	eqeq1d 2738	. . . 4 ⊢ (𝑥 ∈ 𝐻 → (((norm_ℎ ↾ 𝐻)‘𝑥) = 0 ↔ (norm_ℎ‘𝑥) = 0))
114		norm-i 30071	. . . . 5 ⊢ (𝑥 ∈ ℋ → ((norm_ℎ‘𝑥) = 0 ↔ 𝑥 = 0_ℎ))
115	49, 114	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐻 → ((norm_ℎ‘𝑥) = 0 ↔ 𝑥 = 0_ℎ))
116	113, 115	bitrd 278	. . 3 ⊢ (𝑥 ∈ 𝐻 → (((norm_ℎ ↾ 𝐻)‘𝑥) = 0 ↔ 𝑥 = 0_ℎ))
117	116	biimpa 477	. 2 ⊢ ((𝑥 ∈ 𝐻 ∧ ((norm_ℎ ↾ 𝐻)‘𝑥) = 0) → 𝑥 = 0_ℎ)
118		norm-iii 30082	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℋ) → (norm_ℎ‘(𝑦 ·_ℎ 𝑥)) = ((abs‘𝑦) · (norm_ℎ‘𝑥)))
119	49, 118	sylan2 593	. . 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 2776	. . 3 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((norm_ℎ ↾ 𝐻)‘(𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥)) = (norm_ℎ‘(𝑦 ·_ℎ 𝑥)))
124	112	adantl 482	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((norm_ℎ ↾ 𝐻)‘𝑥) = (norm_ℎ‘𝑥))
125	124	oveq2d 7373	. . 3 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((abs‘𝑦) · ((norm_ℎ ↾ 𝐻)‘𝑥)) = ((abs‘𝑦) · (norm_ℎ‘𝑥)))
126	119, 123, 125	3eqtr4d 2786	. 2 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((norm_ℎ ↾ 𝐻)‘(𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥)) = ((abs‘𝑦) · ((norm_ℎ ↾ 𝐻)‘𝑥)))
127	1	sheli 30156	. . . 4 ⊢ (𝑦 ∈ 𝐻 → 𝑦 ∈ ℋ)
128		norm-ii 30080	. . . 4 ⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (norm_ℎ‘(𝑥 +_ℎ 𝑦)) ≤ ((norm_ℎ‘𝑥) + (norm_ℎ‘𝑦)))
129	49, 127, 128	syl2an 596	. . 3 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (norm_ℎ‘(𝑥 +_ℎ 𝑦)) ≤ ((norm_ℎ‘𝑥) + (norm_ℎ‘𝑦)))
130		ovres 7520	. . . . 5 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (𝑥( +_ℎ ↾ (𝐻 × 𝐻))𝑦) = (𝑥 +_ℎ 𝑦))
131	130	fveq2d 6846	. . . 4 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → ((norm_ℎ ↾ 𝐻)‘(𝑥( +_ℎ ↾ (𝐻 × 𝐻))𝑦)) = ((norm_ℎ ↾ 𝐻)‘(𝑥 +_ℎ 𝑦)))
132		shaddcl 30159	. . . . . 6 ⊢ ((𝐻 ∈ S_ℋ ∧ 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (𝑥 +_ℎ 𝑦) ∈ 𝐻)
133	1, 132	mp3an1 1448	. . . . 5 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (𝑥 +_ℎ 𝑦) ∈ 𝐻)
134		fvres 6861	. . . . 5 ⊢ ((𝑥 +_ℎ 𝑦) ∈ 𝐻 → ((norm_ℎ ↾ 𝐻)‘(𝑥 +_ℎ 𝑦)) = (norm_ℎ‘(𝑥 +_ℎ 𝑦)))
135	133, 134	syl 17	. . . 4 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → ((norm_ℎ ↾ 𝐻)‘(𝑥 +_ℎ 𝑦)) = (norm_ℎ‘(𝑥 +_ℎ 𝑦)))
136	131, 135	eqtrd 2776	. . 3 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → ((norm_ℎ ↾ 𝐻)‘(𝑥( +_ℎ ↾ (𝐻 × 𝐻))𝑦)) = (norm_ℎ‘(𝑥 +_ℎ 𝑦)))
137		fvres 6861	. . . 4 ⊢ (𝑦 ∈ 𝐻 → ((norm_ℎ ↾ 𝐻)‘𝑦) = (norm_ℎ‘𝑦))
138	112, 137	oveqan12d 7376	. . 3 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (((norm_ℎ ↾ 𝐻)‘𝑥) + ((norm_ℎ ↾ 𝐻)‘𝑦)) = ((norm_ℎ‘𝑥) + (norm_ℎ‘𝑦)))
139	129, 136, 138	3brtr4d 5137	. 2 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → ((norm_ℎ ↾ 𝐻)‘(𝑥( +_ℎ ↾ (𝐻 × 𝐻))𝑦)) ≤ (((norm_ℎ ↾ 𝐻)‘𝑥) + ((norm_ℎ ↾ 𝐻)‘𝑦)))
140		hhssnvt.1	. 2 ⊢ 𝑊 = ⟨⟨( +_ℎ ↾ (𝐻 × 𝐻)), ( ·_ℎ ↾ (ℂ × 𝐻))⟩, (norm_ℎ ↾ 𝐻)⟩
141	13, 24, 108, 111, 117, 126, 139, 140	isnvi 29555	1 ⊢ 𝑊 ∈ NrmCVec

Colors of variables: wff setvar class

Syntax hints: ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ∃wrex 3073 ⊆ wss 3910 ⟨cop 4592 class class class wbr 5105 × cxp 5631 dom cdm 5633 ran crn 5634 ↾ cres 5635 Fn wfn 6491 ⟶wf 6492 ‘cfv 6496 (class class class)co 7357 ℂcc 11049 ℝcr 11050 0cc0 11051 1c1 11052 + caddc 11054 · cmul 11056 ≤ cle 11190 abscabs 15119 GrpOpcgr 29431 GIdcgi 29432 AbelOpcablo 29486 NrmCVeccnv 29526 ℋchba 29861 +_ℎ cva 29862 ·_ℎ csm 29863 norm_ℎcno 29865 0_ℎc0v 29866 S_ℋ csh 29870

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128 ax-pre-sup 11129 ax-hilex 29941 ax-hfvadd 29942 ax-hvcom 29943 ax-hvass 29944 ax-hv0cl 29945 ax-hvaddid 29946 ax-hfvmul 29947 ax-hvmulid 29948 ax-hvmulass 29949 ax-hvdistr1 29950 ax-hvdistr2 29951 ax-hvmul0 29952 ax-hfi 30021 ax-his1 30024 ax-his2 30025 ax-his3 30026 ax-his4 30027

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-om 7803 df-1st 7921 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-er 8648 df-en 8884 df-dom 8885 df-sdom 8886 df-sup 9378 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-div 11813 df-nn 12154 df-2 12216 df-3 12217 df-4 12218 df-n0 12414 df-z 12500 df-uz 12764 df-rp 12916 df-seq 13907 df-exp 13968 df-cj 14984 df-re 14985 df-im 14986 df-sqrt 15120 df-abs 15121 df-grpo 29435 df-gid 29436 df-ginv 29437 df-ablo 29487 df-vc 29501 df-nv 29534 df-va 29537 df-ba 29538 df-sm 29539 df-0v 29540 df-nmcv 29542 df-hnorm 29910 df-hba 29911 df-hvsub 29913 df-sh 30149

This theorem is referenced by: hhssnvt 30207 hhssvsf 30215 hhssims 30216 hhssmet 30218 hhssmetdval 30219 hhssbnOLD 30221

W3C validator