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 31339

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 31337	. . . 4 ⊢ ( +_ℎ ↾ (𝐻 × 𝐻)) ∈ AbelOp
3		ablogrpo 30622	. . . 4 ⊢ (( +_ℎ ↾ (𝐻 × 𝐻)) ∈ AbelOp → ( +_ℎ ↾ (𝐻 × 𝐻)) ∈ GrpOp)
4	2, 3	ax-mp 5	. . 3 ⊢ ( +_ℎ ↾ (𝐻 × 𝐻)) ∈ GrpOp
5	1	shssii 31288	. . . . . 6 ⊢ 𝐻 ⊆ ℋ
6		xpss12 5639	. . . . . 6 ⊢ ((𝐻 ⊆ ℋ ∧ 𝐻 ⊆ ℋ) → (𝐻 × 𝐻) ⊆ ( ℋ × ℋ))
7	5, 5, 6	mp2an 692	. . . . 5 ⊢ (𝐻 × 𝐻) ⊆ ( ℋ × ℋ)
8		ax-hfvadd 31075	. . . . . 6 ⊢ +_ℎ :( ℋ × ℋ)⟶ ℋ
9	8	fdmi 6673	. . . . 5 ⊢ dom +_ℎ = ( ℋ × ℋ)
10	7, 9	sseqtrri 3983	. . . 4 ⊢ (𝐻 × 𝐻) ⊆ dom +_ℎ
11		ssdmres 5972	. . . 4 ⊢ ((𝐻 × 𝐻) ⊆ dom +_ℎ ↔ dom ( +_ℎ ↾ (𝐻 × 𝐻)) = (𝐻 × 𝐻))
12	10, 11	mpbi 230	. . 3 ⊢ dom ( +_ℎ ↾ (𝐻 × 𝐻)) = (𝐻 × 𝐻)
13	4, 12	grporn 30596	. 2 ⊢ 𝐻 = ran ( +_ℎ ↾ (𝐻 × 𝐻))
14		sh0 31291	. . . . . 6 ⊢ (𝐻 ∈ S_ℋ → 0_ℎ ∈ 𝐻)
15	1, 14	ax-mp 5	. . . . 5 ⊢ 0_ℎ ∈ 𝐻
16		ovres 7524	. . . . 5 ⊢ ((0_ℎ ∈ 𝐻 ∧ 0_ℎ ∈ 𝐻) → (0_ℎ( +_ℎ ↾ (𝐻 × 𝐻))0_ℎ) = (0_ℎ +_ℎ 0_ℎ))
17	15, 15, 16	mp2an 692	. . . 4 ⊢ (0_ℎ( +_ℎ ↾ (𝐻 × 𝐻))0_ℎ) = (0_ℎ +_ℎ 0_ℎ)
18		ax-hv0cl 31078	. . . . 5 ⊢ 0_ℎ ∈ ℋ
19	18	hvaddlidi 31104	. . . 4 ⊢ (0_ℎ +_ℎ 0_ℎ) = 0_ℎ
20	17, 19	eqtri 2759	. . 3 ⊢ (0_ℎ( +_ℎ ↾ (𝐻 × 𝐻))0_ℎ) = 0_ℎ
21		eqid 2736	. . . . 5 ⊢ (GId‘( +_ℎ ↾ (𝐻 × 𝐻))) = (GId‘( +_ℎ ↾ (𝐻 × 𝐻)))
22	13, 21	grpoid 30595	. . . 4 ⊢ ((( +_ℎ ↾ (𝐻 × 𝐻)) ∈ GrpOp ∧ 0_ℎ ∈ 𝐻) → (0_ℎ = (GId‘( +_ℎ ↾ (𝐻 × 𝐻))) ↔ (0_ℎ( +_ℎ ↾ (𝐻 × 𝐻))0_ℎ) = 0_ℎ))
23	4, 15, 22	mp2an 692	. . 3 ⊢ (0_ℎ = (GId‘( +_ℎ ↾ (𝐻 × 𝐻))) ↔ (0_ℎ( +_ℎ ↾ (𝐻 × 𝐻))0_ℎ) = 0_ℎ)
24	20, 23	mpbir 231	. 2 ⊢ 0_ℎ = (GId‘( +_ℎ ↾ (𝐻 × 𝐻)))
25		ax-hfvmul 31080	. . . . . 6 ⊢ ·_ℎ :(ℂ × ℋ)⟶ ℋ
26		ffn 6662	. . . . . 6 ⊢ ( ·_ℎ :(ℂ × ℋ)⟶ ℋ → ·_ℎ Fn (ℂ × ℋ))
27	25, 26	ax-mp 5	. . . . 5 ⊢ ·_ℎ Fn (ℂ × ℋ)
28		ssid 3956	. . . . . 6 ⊢ ℂ ⊆ ℂ
29		xpss12 5639	. . . . . 6 ⊢ ((ℂ ⊆ ℂ ∧ 𝐻 ⊆ ℋ) → (ℂ × 𝐻) ⊆ (ℂ × ℋ))
30	28, 5, 29	mp2an 692	. . . . 5 ⊢ (ℂ × 𝐻) ⊆ (ℂ × ℋ)
31		fnssres 6615	. . . . 5 ⊢ (( ·_ℎ Fn (ℂ × ℋ) ∧ (ℂ × 𝐻) ⊆ (ℂ × ℋ)) → ( ·_ℎ ↾ (ℂ × 𝐻)) Fn (ℂ × 𝐻))
32	27, 30, 31	mp2an 692	. . . 4 ⊢ ( ·_ℎ ↾ (ℂ × 𝐻)) Fn (ℂ × 𝐻)
33		ovelrn 7534	. . . . . . 7 ⊢ (( ·_ℎ ↾ (ℂ × 𝐻)) Fn (ℂ × 𝐻) → (𝑧 ∈ ran ( ·_ℎ ↾ (ℂ × 𝐻)) ↔ ∃𝑥 ∈ ℂ ∃𝑦 ∈ 𝐻 𝑧 = (𝑥( ·_ℎ ↾ (ℂ × 𝐻))𝑦)))
34	32, 33	ax-mp 5	. . . . . 6 ⊢ (𝑧 ∈ ran ( ·_ℎ ↾ (ℂ × 𝐻)) ↔ ∃𝑥 ∈ ℂ ∃𝑦 ∈ 𝐻 𝑧 = (𝑥( ·_ℎ ↾ (ℂ × 𝐻))𝑦))
35		ovres 7524	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑥( ·_ℎ ↾ (ℂ × 𝐻))𝑦) = (𝑥 ·_ℎ 𝑦))
36		shmulcl 31293	. . . . . . . . . 10 ⊢ ((𝐻 ∈ S_ℋ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑥 ·_ℎ 𝑦) ∈ 𝐻)
37	1, 36	mp3an1 1450	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑥 ·_ℎ 𝑦) ∈ 𝐻)
38	35, 37	eqeltrd 2836	. . . . . . . 8 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑥( ·_ℎ ↾ (ℂ × 𝐻))𝑦) ∈ 𝐻)
39		eleq1 2824	. . . . . . . 8 ⊢ (𝑧 = (𝑥( ·_ℎ ↾ (ℂ × 𝐻))𝑦) → (𝑧 ∈ 𝐻 ↔ (𝑥( ·_ℎ ↾ (ℂ × 𝐻))𝑦) ∈ 𝐻))
40	38, 39	syl5ibrcom 247	. . . . . . 7 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻) → (𝑧 = (𝑥( ·_ℎ ↾ (ℂ × 𝐻))𝑦) → 𝑧 ∈ 𝐻))
41	40	rexlimivv 3178	. . . . . 6 ⊢ (∃𝑥 ∈ ℂ ∃𝑦 ∈ 𝐻 𝑧 = (𝑥( ·_ℎ ↾ (ℂ × 𝐻))𝑦) → 𝑧 ∈ 𝐻)
42	34, 41	sylbi 217	. . . . 5 ⊢ (𝑧 ∈ ran ( ·_ℎ ↾ (ℂ × 𝐻)) → 𝑧 ∈ 𝐻)
43	42	ssriv 3937	. . . 4 ⊢ ran ( ·_ℎ ↾ (ℂ × 𝐻)) ⊆ 𝐻
44		df-f 6496	. . . 4 ⊢ (( ·_ℎ ↾ (ℂ × 𝐻)):(ℂ × 𝐻)⟶𝐻 ↔ (( ·_ℎ ↾ (ℂ × 𝐻)) Fn (ℂ × 𝐻) ∧ ran ( ·_ℎ ↾ (ℂ × 𝐻)) ⊆ 𝐻))
45	32, 43, 44	mpbir2an 711	. . 3 ⊢ ( ·_ℎ ↾ (ℂ × 𝐻)):(ℂ × 𝐻)⟶𝐻
46		ax-1cn 11084	. . . . 5 ⊢ 1 ∈ ℂ
47		ovres 7524	. . . . 5 ⊢ ((1 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (1( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = (1 ·_ℎ 𝑥))
48	46, 47	mpan 690	. . . 4 ⊢ (𝑥 ∈ 𝐻 → (1( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = (1 ·_ℎ 𝑥))
49	1	sheli 31289	. . . . 5 ⊢ (𝑥 ∈ 𝐻 → 𝑥 ∈ ℋ)
50		ax-hvmulid 31081	. . . . 5 ⊢ (𝑥 ∈ ℋ → (1 ·_ℎ 𝑥) = 𝑥)
51	49, 50	syl 17	. . . 4 ⊢ (𝑥 ∈ 𝐻 → (1 ·_ℎ 𝑥) = 𝑥)
52	48, 51	eqtrd 2771	. . 3 ⊢ (𝑥 ∈ 𝐻 → (1( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = 𝑥)
53		id 22	. . . . 5 ⊢ (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
54	1	sheli 31289	. . . . 5 ⊢ (𝑧 ∈ 𝐻 → 𝑧 ∈ ℋ)
55		ax-hvdistr1 31083	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦 ·_ℎ (𝑥 +_ℎ 𝑧)) = ((𝑦 ·_ℎ 𝑥) +_ℎ (𝑦 ·_ℎ 𝑧)))
56	53, 49, 54, 55	syl3an 1160	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦 ·_ℎ (𝑥 +_ℎ 𝑧)) = ((𝑦 ·_ℎ 𝑥) +_ℎ (𝑦 ·_ℎ 𝑧)))
57		ovres 7524	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥( +_ℎ ↾ (𝐻 × 𝐻))𝑧) = (𝑥 +_ℎ 𝑧))
58	57	3adant1 1130	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥( +_ℎ ↾ (𝐻 × 𝐻))𝑧) = (𝑥 +_ℎ 𝑧))
59	58	oveq2d 7374	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑥( +_ℎ ↾ (𝐻 × 𝐻))𝑧)) = (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑥 +_ℎ 𝑧)))
60		shaddcl 31292	. . . . . . . 8 ⊢ ((𝐻 ∈ S_ℋ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥 +_ℎ 𝑧) ∈ 𝐻)
61	1, 60	mp3an1 1450	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑥 +_ℎ 𝑧) ∈ 𝐻)
62		ovres 7524	. . . . . . 7 ⊢ ((𝑦 ∈ ℂ ∧ (𝑥 +_ℎ 𝑧) ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑥 +_ℎ 𝑧)) = (𝑦 ·_ℎ (𝑥 +_ℎ 𝑧)))
63	61, 62	sylan2 593	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ (𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻)) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑥 +_ℎ 𝑧)) = (𝑦 ·_ℎ (𝑥 +_ℎ 𝑧)))
64	63	3impb 1114	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑥 +_ℎ 𝑧)) = (𝑦 ·_ℎ (𝑥 +_ℎ 𝑧)))
65	59, 64	eqtrd 2771	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑥( +_ℎ ↾ (𝐻 × 𝐻))𝑧)) = (𝑦 ·_ℎ (𝑥 +_ℎ 𝑧)))
66		ovres 7524	. . . . . . 7 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = (𝑦 ·_ℎ 𝑥))
67	66	3adant3 1132	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = (𝑦 ·_ℎ 𝑥))
68		ovres 7524	. . . . . . 7 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑧) = (𝑦 ·_ℎ 𝑧))
69	68	3adant2 1131	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑧) = (𝑦 ·_ℎ 𝑧))
70	67, 69	oveq12d 7376	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → ((𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥)( +_ℎ ↾ (𝐻 × 𝐻))(𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑧)) = ((𝑦 ·_ℎ 𝑥)( +_ℎ ↾ (𝐻 × 𝐻))(𝑦 ·_ℎ 𝑧)))
71		shmulcl 31293	. . . . . . . 8 ⊢ ((𝐻 ∈ S_ℋ ∧ 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦 ·_ℎ 𝑥) ∈ 𝐻)
72	1, 71	mp3an1 1450	. . . . . . 7 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦 ·_ℎ 𝑥) ∈ 𝐻)
73	72	3adant3 1132	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦 ·_ℎ 𝑥) ∈ 𝐻)
74		shmulcl 31293	. . . . . . . 8 ⊢ ((𝐻 ∈ S_ℋ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝐻) → (𝑦 ·_ℎ 𝑧) ∈ 𝐻)
75	1, 74	mp3an1 1450	. . . . . . 7 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ 𝐻) → (𝑦 ·_ℎ 𝑧) ∈ 𝐻)
76	75	3adant2 1131	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦 ·_ℎ 𝑧) ∈ 𝐻)
77	73, 76	ovresd 7525	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → ((𝑦 ·_ℎ 𝑥)( +_ℎ ↾ (𝐻 × 𝐻))(𝑦 ·_ℎ 𝑧)) = ((𝑦 ·_ℎ 𝑥) +_ℎ (𝑦 ·_ℎ 𝑧)))
78	70, 77	eqtrd 2771	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → ((𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥)( +_ℎ ↾ (𝐻 × 𝐻))(𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑧)) = ((𝑦 ·_ℎ 𝑥) +_ℎ (𝑦 ·_ℎ 𝑧)))
79	56, 65, 78	3eqtr4d 2781	. . 3 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻 ∧ 𝑧 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑥( +_ℎ ↾ (𝐻 × 𝐻))𝑧)) = ((𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥)( +_ℎ ↾ (𝐻 × 𝐻))(𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑧)))
80		ax-hvdistr2 31084	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℋ) → ((𝑦 + 𝑧) ·_ℎ 𝑥) = ((𝑦 ·_ℎ 𝑥) +_ℎ (𝑧 ·_ℎ 𝑥)))
81	49, 80	syl3an3 1165	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 + 𝑧) ·_ℎ 𝑥) = ((𝑦 ·_ℎ 𝑥) +_ℎ (𝑧 ·_ℎ 𝑥)))
82		addcl 11108	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑦 + 𝑧) ∈ ℂ)
83		ovres 7524	. . . . 5 ⊢ (((𝑦 + 𝑧) ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 + 𝑧)( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = ((𝑦 + 𝑧) ·_ℎ 𝑥))
84	82, 83	stoic3 1777	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 + 𝑧)( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = ((𝑦 + 𝑧) ·_ℎ 𝑥))
85	66	3adant2 1131	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = (𝑦 ·_ℎ 𝑥))
86		ovres 7524	. . . . . . 7 ⊢ ((𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = (𝑧 ·_ℎ 𝑥))
87	86	3adant1 1130	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = (𝑧 ·_ℎ 𝑥))
88	85, 87	oveq12d 7376	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥)( +_ℎ ↾ (𝐻 × 𝐻))(𝑧( ·_ℎ ↾ (ℂ × 𝐻))𝑥)) = ((𝑦 ·_ℎ 𝑥)( +_ℎ ↾ (𝐻 × 𝐻))(𝑧 ·_ℎ 𝑥)))
89	72	3adant2 1131	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦 ·_ℎ 𝑥) ∈ 𝐻)
90		shmulcl 31293	. . . . . . . 8 ⊢ ((𝐻 ∈ S_ℋ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧 ·_ℎ 𝑥) ∈ 𝐻)
91	1, 90	mp3an1 1450	. . . . . . 7 ⊢ ((𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧 ·_ℎ 𝑥) ∈ 𝐻)
92	91	3adant1 1130	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑧 ·_ℎ 𝑥) ∈ 𝐻)
93	89, 92	ovresd 7525	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 ·_ℎ 𝑥)( +_ℎ ↾ (𝐻 × 𝐻))(𝑧 ·_ℎ 𝑥)) = ((𝑦 ·_ℎ 𝑥) +_ℎ (𝑧 ·_ℎ 𝑥)))
94	88, 93	eqtrd 2771	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥)( +_ℎ ↾ (𝐻 × 𝐻))(𝑧( ·_ℎ ↾ (ℂ × 𝐻))𝑥)) = ((𝑦 ·_ℎ 𝑥) +_ℎ (𝑧 ·_ℎ 𝑥)))
95	81, 84, 94	3eqtr4d 2781	. . 3 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 + 𝑧)( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = ((𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥)( +_ℎ ↾ (𝐻 × 𝐻))(𝑧( ·_ℎ ↾ (ℂ × 𝐻))𝑥)))
96		ax-hvmulass 31082	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℋ) → ((𝑦 · 𝑧) ·_ℎ 𝑥) = (𝑦 ·_ℎ (𝑧 ·_ℎ 𝑥)))
97	49, 96	syl3an3 1165	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 · 𝑧) ·_ℎ 𝑥) = (𝑦 ·_ℎ (𝑧 ·_ℎ 𝑥)))
98		mulcl 11110	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑦 · 𝑧) ∈ ℂ)
99		ovres 7524	. . . . 5 ⊢ (((𝑦 · 𝑧) ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 · 𝑧)( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = ((𝑦 · 𝑧) ·_ℎ 𝑥))
100	98, 99	stoic3 1777	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 · 𝑧)( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = ((𝑦 · 𝑧) ·_ℎ 𝑥))
101	87	oveq2d 7374	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑧( ·_ℎ ↾ (ℂ × 𝐻))𝑥)) = (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑧 ·_ℎ 𝑥)))
102		ovres 7524	. . . . . . 7 ⊢ ((𝑦 ∈ ℂ ∧ (𝑧 ·_ℎ 𝑥) ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑧 ·_ℎ 𝑥)) = (𝑦 ·_ℎ (𝑧 ·_ℎ 𝑥)))
103	91, 102	sylan2 593	. . . . . 6 ⊢ ((𝑦 ∈ ℂ ∧ (𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻)) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑧 ·_ℎ 𝑥)) = (𝑦 ·_ℎ (𝑧 ·_ℎ 𝑥)))
104	103	3impb 1114	. . . . 5 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑧 ·_ℎ 𝑥)) = (𝑦 ·_ℎ (𝑧 ·_ℎ 𝑥)))
105	101, 104	eqtrd 2771	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑧( ·_ℎ ↾ (ℂ × 𝐻))𝑥)) = (𝑦 ·_ℎ (𝑧 ·_ℎ 𝑥)))
106	97, 100, 105	3eqtr4d 2781	. . 3 ⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((𝑦 · 𝑧)( ·_ℎ ↾ (ℂ × 𝐻))𝑥) = (𝑦( ·_ℎ ↾ (ℂ × 𝐻))(𝑧( ·_ℎ ↾ (ℂ × 𝐻))𝑥)))
107		eqid 2736	. . 3 ⊢ ⟨( +_ℎ ↾ (𝐻 × 𝐻)), ( ·_ℎ ↾ (ℂ × 𝐻))⟩ = ⟨( +_ℎ ↾ (𝐻 × 𝐻)), ( ·_ℎ ↾ (ℂ × 𝐻))⟩
108	2, 12, 45, 52, 79, 95, 106, 107	isvciOLD 30655	. 2 ⊢ ⟨( +_ℎ ↾ (𝐻 × 𝐻)), ( ·_ℎ ↾ (ℂ × 𝐻))⟩ ∈ CVec_OLD
109		normf 31198	. . 3 ⊢ norm_ℎ: ℋ⟶ℝ
110		fssres 6700	. . 3 ⊢ ((norm_ℎ: ℋ⟶ℝ ∧ 𝐻 ⊆ ℋ) → (norm_ℎ ↾ 𝐻):𝐻⟶ℝ)
111	109, 5, 110	mp2an 692	. 2 ⊢ (norm_ℎ ↾ 𝐻):𝐻⟶ℝ
112		fvres 6853	. . . . 5 ⊢ (𝑥 ∈ 𝐻 → ((norm_ℎ ↾ 𝐻)‘𝑥) = (norm_ℎ‘𝑥))
113	112	eqeq1d 2738	. . . 4 ⊢ (𝑥 ∈ 𝐻 → (((norm_ℎ ↾ 𝐻)‘𝑥) = 0 ↔ (norm_ℎ‘𝑥) = 0))
114		norm-i 31204	. . . . 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 31215	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ ℋ) → (norm_ℎ‘(𝑦 ·_ℎ 𝑥)) = ((abs‘𝑦) · (norm_ℎ‘𝑥)))
119	49, 118	sylan2 593	. . 3 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → (norm_ℎ‘(𝑦 ·_ℎ 𝑥)) = ((abs‘𝑦) · (norm_ℎ‘𝑥)))
120	66	fveq2d 6838	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((norm_ℎ ↾ 𝐻)‘(𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥)) = ((norm_ℎ ↾ 𝐻)‘(𝑦 ·_ℎ 𝑥)))
121		fvres 6853	. . . . 5 ⊢ ((𝑦 ·_ℎ 𝑥) ∈ 𝐻 → ((norm_ℎ ↾ 𝐻)‘(𝑦 ·_ℎ 𝑥)) = (norm_ℎ‘(𝑦 ·_ℎ 𝑥)))
122	72, 121	syl 17	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((norm_ℎ ↾ 𝐻)‘(𝑦 ·_ℎ 𝑥)) = (norm_ℎ‘(𝑦 ·_ℎ 𝑥)))
123	120, 122	eqtrd 2771	. . 3 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((norm_ℎ ↾ 𝐻)‘(𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥)) = (norm_ℎ‘(𝑦 ·_ℎ 𝑥)))
124	112	adantl 481	. . . 4 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((norm_ℎ ↾ 𝐻)‘𝑥) = (norm_ℎ‘𝑥))
125	124	oveq2d 7374	. . 3 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((abs‘𝑦) · ((norm_ℎ ↾ 𝐻)‘𝑥)) = ((abs‘𝑦) · (norm_ℎ‘𝑥)))
126	119, 123, 125	3eqtr4d 2781	. 2 ⊢ ((𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝐻) → ((norm_ℎ ↾ 𝐻)‘(𝑦( ·_ℎ ↾ (ℂ × 𝐻))𝑥)) = ((abs‘𝑦) · ((norm_ℎ ↾ 𝐻)‘𝑥)))
127	1	sheli 31289	. . . 4 ⊢ (𝑦 ∈ 𝐻 → 𝑦 ∈ ℋ)
128		norm-ii 31213	. . . 4 ⊢ ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (norm_ℎ‘(𝑥 +_ℎ 𝑦)) ≤ ((norm_ℎ‘𝑥) + (norm_ℎ‘𝑦)))
129	49, 127, 128	syl2an 596	. . 3 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (norm_ℎ‘(𝑥 +_ℎ 𝑦)) ≤ ((norm_ℎ‘𝑥) + (norm_ℎ‘𝑦)))
130		ovres 7524	. . . . 5 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (𝑥( +_ℎ ↾ (𝐻 × 𝐻))𝑦) = (𝑥 +_ℎ 𝑦))
131	130	fveq2d 6838	. . . 4 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → ((norm_ℎ ↾ 𝐻)‘(𝑥( +_ℎ ↾ (𝐻 × 𝐻))𝑦)) = ((norm_ℎ ↾ 𝐻)‘(𝑥 +_ℎ 𝑦)))
132		shaddcl 31292	. . . . . 6 ⊢ ((𝐻 ∈ S_ℋ ∧ 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (𝑥 +_ℎ 𝑦) ∈ 𝐻)
133	1, 132	mp3an1 1450	. . . . 5 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (𝑥 +_ℎ 𝑦) ∈ 𝐻)
134		fvres 6853	. . . . 5 ⊢ ((𝑥 +_ℎ 𝑦) ∈ 𝐻 → ((norm_ℎ ↾ 𝐻)‘(𝑥 +_ℎ 𝑦)) = (norm_ℎ‘(𝑥 +_ℎ 𝑦)))
135	133, 134	syl 17	. . . 4 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → ((norm_ℎ ↾ 𝐻)‘(𝑥 +_ℎ 𝑦)) = (norm_ℎ‘(𝑥 +_ℎ 𝑦)))
136	131, 135	eqtrd 2771	. . 3 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → ((norm_ℎ ↾ 𝐻)‘(𝑥( +_ℎ ↾ (𝐻 × 𝐻))𝑦)) = (norm_ℎ‘(𝑥 +_ℎ 𝑦)))
137		fvres 6853	. . . 4 ⊢ (𝑦 ∈ 𝐻 → ((norm_ℎ ↾ 𝐻)‘𝑦) = (norm_ℎ‘𝑦))
138	112, 137	oveqan12d 7377	. . 3 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → (((norm_ℎ ↾ 𝐻)‘𝑥) + ((norm_ℎ ↾ 𝐻)‘𝑦)) = ((norm_ℎ‘𝑥) + (norm_ℎ‘𝑦)))
139	129, 136, 138	3brtr4d 5130	. 2 ⊢ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) → ((norm_ℎ ↾ 𝐻)‘(𝑥( +_ℎ ↾ (𝐻 × 𝐻))𝑦)) ≤ (((norm_ℎ ↾ 𝐻)‘𝑥) + ((norm_ℎ ↾ 𝐻)‘𝑦)))
140		hhssnvt.1	. 2 ⊢ 𝑊 = ⟨⟨( +_ℎ ↾ (𝐻 × 𝐻)), ( ·_ℎ ↾ (ℂ × 𝐻))⟩, (norm_ℎ ↾ 𝐻)⟩
141	13, 24, 108, 111, 117, 126, 139, 140	isnvi 30688	1 ⊢ 𝑊 ∈ NrmCVec

Colors of variables: wff setvar class

Syntax hints: ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ∃wrex 3060 ⊆ wss 3901 ⟨cop 4586 class class class wbr 5098 × cxp 5622 dom cdm 5624 ran crn 5625 ↾ cres 5626 Fn wfn 6487 ⟶wf 6488 ‘cfv 6492 (class class class)co 7358 ℂcc 11024 ℝcr 11025 0cc0 11026 1c1 11027 + caddc 11029 · cmul 11031 ≤ cle 11167 abscabs 15157 GrpOpcgr 30564 GIdcgi 30565 AbelOpcablo 30619 NrmCVeccnv 30659 ℋchba 30994 +_ℎ cva 30995 ·_ℎ csm 30996 norm_ℎcno 30998 0_ℎc0v 30999 S_ℋ csh 31003

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103 ax-pre-sup 11104 ax-hilex 31074 ax-hfvadd 31075 ax-hvcom 31076 ax-hvass 31077 ax-hv0cl 31078 ax-hvaddid 31079 ax-hfvmul 31080 ax-hvmulid 31081 ax-hvmulass 31082 ax-hvdistr1 31083 ax-hvdistr2 31084 ax-hvmul0 31085 ax-hfi 31154 ax-his1 31157 ax-his2 31158 ax-his3 31159 ax-his4 31160

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-er 8635 df-en 8884 df-dom 8885 df-sdom 8886 df-sup 9345 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-div 11795 df-nn 12146 df-2 12208 df-3 12209 df-4 12210 df-n0 12402 df-z 12489 df-uz 12752 df-rp 12906 df-seq 13925 df-exp 13985 df-cj 15022 df-re 15023 df-im 15024 df-sqrt 15158 df-abs 15159 df-grpo 30568 df-gid 30569 df-ginv 30570 df-ablo 30620 df-vc 30634 df-nv 30667 df-va 30670 df-ba 30671 df-sm 30672 df-0v 30673 df-nmcv 30675 df-hnorm 31043 df-hba 31044 df-hvsub 31046 df-sh 31282

This theorem is referenced by: hhssnvt 31340 hhssvsf 31348 hhssims 31349 hhssmet 31351 hhssmetdval 31352 hhssbnOLD 31354

W3C validator