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	$⊢ W = ⟨⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩, {{norm}_{ℎ} ↾}_{H}⟩$
	hhssnv.2	$⊢ H \in S_{ℋ}$
Assertion	hhssnv	$⊢ W \in NrmCVec$

Proof

Step	Hyp	Ref	Expression
1		hhssnvt.1	$⊢ W = ⟨⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩, {{norm}_{ℎ} ↾}_{H}⟩$
2		hhssnv.2	$⊢ H \in S_{ℋ}$
3	2	hhssabloi	$⊢ {+_{ℎ} ↾}_{(H \times H)} \in AbelOp$
4		ablogrpo	$⊢ {+_{ℎ} ↾}_{(H \times H)} \in AbelOp \to {+_{ℎ} ↾}_{(H \times H)} \in GrpOp$
5	3 4	ax-mp	$⊢ {+_{ℎ} ↾}_{(H \times H)} \in GrpOp$
6	2	shssii	$⊢ H \subseteq ℋ$
7		xpss12	$⊢ (H \subseteq ℋ \land H \subseteq ℋ) \to H \times H \subseteq ℋ \times ℋ$
8	6 6 7	mp2an	$⊢ H \times H \subseteq ℋ \times ℋ$
9		ax-hfvadd	$⊢ +_{ℎ} : ℋ \times ℋ ⟶ ℋ$
10	9	fdmi	$⊢ dom +_{ℎ} = ℋ \times ℋ$
11	8 10	sseqtrri	$⊢ H \times H \subseteq dom +_{ℎ}$
12		ssdmres	$⊢ H \times H \subseteq dom +_{ℎ} \leftrightarrow dom ({+_{ℎ} ↾}_{(H \times H)}) = H \times H$
13	11 12	mpbi	$⊢ dom ({+_{ℎ} ↾}_{(H \times H)}) = H \times H$
14	5 13	grporn	$⊢ H = ran ({+_{ℎ} ↾}_{(H \times H)})$
15		sh0	$⊢ H \in S_{ℋ} \to 0_{ℎ} \in H$
16	2 15	ax-mp	$⊢ 0_{ℎ} \in H$
17		ovres	$⊢ (0_{ℎ} \in H \land 0_{ℎ} \in H) \to 0_{ℎ} ({+_{ℎ} ↾}_{(H \times H)}) 0_{ℎ} = 0_{ℎ} +_{ℎ} 0_{ℎ}$
18	16 16 17	mp2an	$⊢ 0_{ℎ} ({+_{ℎ} ↾}_{(H \times H)}) 0_{ℎ} = 0_{ℎ} +_{ℎ} 0_{ℎ}$
19		ax-hv0cl	$⊢ 0_{ℎ} \in ℋ$
20	19	hvaddlidi	$⊢ 0_{ℎ} +_{ℎ} 0_{ℎ} = 0_{ℎ}$
21	18 20	eqtri	$⊢ 0_{ℎ} ({+_{ℎ} ↾}_{(H \times H)}) 0_{ℎ} = 0_{ℎ}$
22		eqid	$⊢ GId ({+_{ℎ} ↾}_{(H \times H)}) = GId ({+_{ℎ} ↾}_{(H \times H)})$
23	14 22	grpoid	$⊢ ({+_{ℎ} ↾}_{(H \times H)} \in GrpOp \land 0_{ℎ} \in H) \to (0_{ℎ} = GId ({+_{ℎ} ↾}_{(H \times H)}) \leftrightarrow 0_{ℎ} ({+_{ℎ} ↾}_{(H \times H)}) 0_{ℎ} = 0_{ℎ})$
24	5 16 23	mp2an	$⊢ 0_{ℎ} = GId ({+_{ℎ} ↾}_{(H \times H)}) \leftrightarrow 0_{ℎ} ({+_{ℎ} ↾}_{(H \times H)}) 0_{ℎ} = 0_{ℎ}$
25	21 24	mpbir	$⊢ 0_{ℎ} = GId ({+_{ℎ} ↾}_{(H \times H)})$
26		ax-hfvmul	$⊢ \cdot_{ℎ} : ℂ \times ℋ ⟶ ℋ$
27		ffn	$⊢ \cdot_{ℎ} : ℂ \times ℋ ⟶ ℋ \to \cdot_{ℎ} Fn (ℂ \times ℋ)$
28	26 27	ax-mp	$⊢ \cdot_{ℎ} Fn (ℂ \times ℋ)$
29		ssid	$⊢ ℂ \subseteq ℂ$
30		xpss12	$⊢ (ℂ \subseteq ℂ \land H \subseteq ℋ) \to ℂ \times H \subseteq ℂ \times ℋ$
31	29 6 30	mp2an	$⊢ ℂ \times H \subseteq ℂ \times ℋ$
32		fnssres	$⊢ (\cdot_{ℎ} Fn (ℂ \times ℋ) \land ℂ \times H \subseteq ℂ \times ℋ) \to ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) Fn (ℂ \times H)$
33	28 31 32	mp2an	$⊢ ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) Fn (ℂ \times H)$
34		ovelrn	$⊢ ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) Fn (ℂ \times H) \to (z \in ran ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) \leftrightarrow \exists x \in ℂ \exists y \in H z = x ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) y)$
35	33 34	ax-mp	$⊢ z \in ran ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) \leftrightarrow \exists x \in ℂ \exists y \in H z = x ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) y$
36		ovres	$⊢ (x \in ℂ \land y \in H) \to x ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) y = x \cdot_{ℎ} y$
37		shmulcl	$⊢ (H \in S_{ℋ} \land x \in ℂ \land y \in H) \to x \cdot_{ℎ} y \in H$
38	2 37	mp3an1	$⊢ (x \in ℂ \land y \in H) \to x \cdot_{ℎ} y \in H$
39	36 38	eqeltrd	$⊢ (x \in ℂ \land y \in H) \to x ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) y \in H$
40		eleq1	$⊢ z = x ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) y \to (z \in H \leftrightarrow x ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) y \in H)$
41	39 40	syl5ibrcom	$⊢ (x \in ℂ \land y \in H) \to (z = x ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) y \to z \in H)$
42	41	rexlimivv	$⊢ \exists x \in ℂ \exists y \in H z = x ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) y \to z \in H$
43	35 42	sylbi	$⊢ z \in ran ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) \to z \in H$
44	43	ssriv	$⊢ ran ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) \subseteq H$
45		df-f	$⊢ ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) : ℂ \times H ⟶ H \leftrightarrow (({\cdot_{ℎ} ↾}_{(ℂ \times H)}) Fn (ℂ \times H) \land ran ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) \subseteq H)$
46	33 44 45	mpbir2an	$⊢ ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) : ℂ \times H ⟶ H$
47		ax-1cn	$⊢ 1 \in ℂ$
48		ovres	$⊢ (1 \in ℂ \land x \in H) \to 1 ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x = 1 \cdot_{ℎ} x$
49	47 48	mpan	$⊢ x \in H \to 1 ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x = 1 \cdot_{ℎ} x$
50	2	sheli	$⊢ x \in H \to x \in ℋ$
51		ax-hvmulid	$⊢ x \in ℋ \to 1 \cdot_{ℎ} x = x$
52	50 51	syl	$⊢ x \in H \to 1 \cdot_{ℎ} x = x$
53	49 52	eqtrd	$⊢ x \in H \to 1 ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x = x$
54		id	$⊢ y \in ℂ \to y \in ℂ$
55	2	sheli	$⊢ z \in H \to z \in ℋ$
56		ax-hvdistr1	$⊢ (y \in ℂ \land x \in ℋ \land z \in ℋ) \to y \cdot_{ℎ} (x +_{ℎ} z) = (y \cdot_{ℎ} x) +_{ℎ} (y \cdot_{ℎ} z)$
57	54 50 55 56	syl3an	$⊢ (y \in ℂ \land x \in H \land z \in H) \to y \cdot_{ℎ} (x +_{ℎ} z) = (y \cdot_{ℎ} x) +_{ℎ} (y \cdot_{ℎ} z)$
58		ovres	$⊢ (x \in H \land z \in H) \to x ({+_{ℎ} ↾}_{(H \times H)}) z = x +_{ℎ} z$
59	58	3adant1	$⊢ (y \in ℂ \land x \in H \land z \in H) \to x ({+_{ℎ} ↾}_{(H \times H)}) z = x +_{ℎ} z$
60	59	oveq2d	$⊢ (y \in ℂ \land x \in H \land z \in H) \to y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) (x ({+_{ℎ} ↾}_{(H \times H)}) z) = y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) (x +_{ℎ} z)$
61		shaddcl	$⊢ (H \in S_{ℋ} \land x \in H \land z \in H) \to x +_{ℎ} z \in H$
62	2 61	mp3an1	$⊢ (x \in H \land z \in H) \to x +_{ℎ} z \in H$
63		ovres	$⊢ (y \in ℂ \land x +_{ℎ} z \in H) \to y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) (x +_{ℎ} z) = y \cdot_{ℎ} (x +_{ℎ} z)$
64	62 63	sylan2	$⊢ (y \in ℂ \land (x \in H \land z \in H)) \to y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) (x +_{ℎ} z) = y \cdot_{ℎ} (x +_{ℎ} z)$
65	64	3impb	$⊢ (y \in ℂ \land x \in H \land z \in H) \to y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) (x +_{ℎ} z) = y \cdot_{ℎ} (x +_{ℎ} z)$
66	60 65	eqtrd	$⊢ (y \in ℂ \land x \in H \land z \in H) \to y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) (x ({+_{ℎ} ↾}_{(H \times H)}) z) = y \cdot_{ℎ} (x +_{ℎ} z)$
67		ovres	$⊢ (y \in ℂ \land x \in H) \to y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x = y \cdot_{ℎ} x$
68	67	3adant3	$⊢ (y \in ℂ \land x \in H \land z \in H) \to y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x = y \cdot_{ℎ} x$
69		ovres	$⊢ (y \in ℂ \land z \in H) \to y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) z = y \cdot_{ℎ} z$
70	69	3adant2	$⊢ (y \in ℂ \land x \in H \land z \in H) \to y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) z = y \cdot_{ℎ} z$
71	68 70	oveq12d	$⊢ (y \in ℂ \land x \in H \land z \in H) \to (y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x) ({+_{ℎ} ↾}_{(H \times H)}) (y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) z) = (y \cdot_{ℎ} x) ({+_{ℎ} ↾}_{(H \times H)}) (y \cdot_{ℎ} z)$
72		shmulcl	$⊢ (H \in S_{ℋ} \land y \in ℂ \land x \in H) \to y \cdot_{ℎ} x \in H$
73	2 72	mp3an1	$⊢ (y \in ℂ \land x \in H) \to y \cdot_{ℎ} x \in H$
74	73	3adant3	$⊢ (y \in ℂ \land x \in H \land z \in H) \to y \cdot_{ℎ} x \in H$
75		shmulcl	$⊢ (H \in S_{ℋ} \land y \in ℂ \land z \in H) \to y \cdot_{ℎ} z \in H$
76	2 75	mp3an1	$⊢ (y \in ℂ \land z \in H) \to y \cdot_{ℎ} z \in H$
77	76	3adant2	$⊢ (y \in ℂ \land x \in H \land z \in H) \to y \cdot_{ℎ} z \in H$
78	74 77	ovresd	$⊢ (y \in ℂ \land x \in H \land z \in H) \to (y \cdot_{ℎ} x) ({+_{ℎ} ↾}_{(H \times H)}) (y \cdot_{ℎ} z) = (y \cdot_{ℎ} x) +_{ℎ} (y \cdot_{ℎ} z)$
79	71 78	eqtrd	$⊢ (y \in ℂ \land x \in H \land z \in H) \to (y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x) ({+_{ℎ} ↾}_{(H \times H)}) (y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) z) = (y \cdot_{ℎ} x) +_{ℎ} (y \cdot_{ℎ} z)$
80	57 66 79	3eqtr4d	$⊢ (y \in ℂ \land x \in H \land z \in H) \to y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) (x ({+_{ℎ} ↾}_{(H \times H)}) z) = (y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x) ({+_{ℎ} ↾}_{(H \times H)}) (y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) z)$
81		ax-hvdistr2	$⊢ (y \in ℂ \land z \in ℂ \land x \in ℋ) \to (y + z) \cdot_{ℎ} x = (y \cdot_{ℎ} x) +_{ℎ} (z \cdot_{ℎ} x)$
82	50 81	syl3an3	$⊢ (y \in ℂ \land z \in ℂ \land x \in H) \to (y + z) \cdot_{ℎ} x = (y \cdot_{ℎ} x) +_{ℎ} (z \cdot_{ℎ} x)$
83		addcl	$⊢ (y \in ℂ \land z \in ℂ) \to y + z \in ℂ$
84		ovres	$⊢ (y + z \in ℂ \land x \in H) \to (y + z) ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x = (y + z) \cdot_{ℎ} x$
85	83 84	stoic3	$⊢ (y \in ℂ \land z \in ℂ \land x \in H) \to (y + z) ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x = (y + z) \cdot_{ℎ} x$
86	67	3adant2	$⊢ (y \in ℂ \land z \in ℂ \land x \in H) \to y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x = y \cdot_{ℎ} x$
87		ovres	$⊢ (z \in ℂ \land x \in H) \to z ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x = z \cdot_{ℎ} x$
88	87	3adant1	$⊢ (y \in ℂ \land z \in ℂ \land x \in H) \to z ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x = z \cdot_{ℎ} x$
89	86 88	oveq12d	$⊢ (y \in ℂ \land z \in ℂ \land x \in H) \to (y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x) ({+_{ℎ} ↾}_{(H \times H)}) (z ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x) = (y \cdot_{ℎ} x) ({+_{ℎ} ↾}_{(H \times H)}) (z \cdot_{ℎ} x)$
90	73	3adant2	$⊢ (y \in ℂ \land z \in ℂ \land x \in H) \to y \cdot_{ℎ} x \in H$
91		shmulcl	$⊢ (H \in S_{ℋ} \land z \in ℂ \land x \in H) \to z \cdot_{ℎ} x \in H$
92	2 91	mp3an1	$⊢ (z \in ℂ \land x \in H) \to z \cdot_{ℎ} x \in H$
93	92	3adant1	$⊢ (y \in ℂ \land z \in ℂ \land x \in H) \to z \cdot_{ℎ} x \in H$
94	90 93	ovresd	$⊢ (y \in ℂ \land z \in ℂ \land x \in H) \to (y \cdot_{ℎ} x) ({+_{ℎ} ↾}_{(H \times H)}) (z \cdot_{ℎ} x) = (y \cdot_{ℎ} x) +_{ℎ} (z \cdot_{ℎ} x)$
95	89 94	eqtrd	$⊢ (y \in ℂ \land z \in ℂ \land x \in H) \to (y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x) ({+_{ℎ} ↾}_{(H \times H)}) (z ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x) = (y \cdot_{ℎ} x) +_{ℎ} (z \cdot_{ℎ} x)$
96	82 85 95	3eqtr4d	$⊢ (y \in ℂ \land z \in ℂ \land x \in H) \to (y + z) ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x = (y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x) ({+_{ℎ} ↾}_{(H \times H)}) (z ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x)$
97		ax-hvmulass	$⊢ (y \in ℂ \land z \in ℂ \land x \in ℋ) \to y z \cdot_{ℎ} x = y \cdot_{ℎ} (z \cdot_{ℎ} x)$
98	50 97	syl3an3	$⊢ (y \in ℂ \land z \in ℂ \land x \in H) \to y z \cdot_{ℎ} x = y \cdot_{ℎ} (z \cdot_{ℎ} x)$
99		mulcl	$⊢ (y \in ℂ \land z \in ℂ) \to y z \in ℂ$
100		ovres	$⊢ (y z \in ℂ \land x \in H) \to y z ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x = y z \cdot_{ℎ} x$
101	99 100	stoic3	$⊢ (y \in ℂ \land z \in ℂ \land x \in H) \to y z ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x = y z \cdot_{ℎ} x$
102	88	oveq2d	$⊢ (y \in ℂ \land z \in ℂ \land x \in H) \to y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) (z ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x) = y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) (z \cdot_{ℎ} x)$
103		ovres	$⊢ (y \in ℂ \land z \cdot_{ℎ} x \in H) \to y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) (z \cdot_{ℎ} x) = y \cdot_{ℎ} (z \cdot_{ℎ} x)$
104	92 103	sylan2	$⊢ (y \in ℂ \land (z \in ℂ \land x \in H)) \to y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) (z \cdot_{ℎ} x) = y \cdot_{ℎ} (z \cdot_{ℎ} x)$
105	104	3impb	$⊢ (y \in ℂ \land z \in ℂ \land x \in H) \to y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) (z \cdot_{ℎ} x) = y \cdot_{ℎ} (z \cdot_{ℎ} x)$
106	102 105	eqtrd	$⊢ (y \in ℂ \land z \in ℂ \land x \in H) \to y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) (z ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x) = y \cdot_{ℎ} (z \cdot_{ℎ} x)$
107	98 101 106	3eqtr4d	$⊢ (y \in ℂ \land z \in ℂ \land x \in H) \to y z ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x = y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) (z ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x)$
108		eqid	$⊢ ⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩ = ⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩$
109	3 13 46 53 80 96 107 108	isvciOLD	$⊢ ⟨{+_{ℎ} ↾}_{(H \times H)}, {\cdot_{ℎ} ↾}_{(ℂ \times H)}⟩ \in {CVec}_{OLD}$
110		normf	$⊢ {norm}_{ℎ} : ℋ ⟶ ℝ$
111		fssres	$⊢ ({norm}_{ℎ} : ℋ ⟶ ℝ \land H \subseteq ℋ) \to ({{norm}_{ℎ} ↾}_{H}) : H ⟶ ℝ$
112	110 6 111	mp2an	$⊢ ({{norm}_{ℎ} ↾}_{H}) : H ⟶ ℝ$
113		fvres	$⊢ x \in H \to ({{norm}_{ℎ} ↾}_{H}) (x) = {norm}_{ℎ} (x)$
114	113	eqeq1d	$⊢ x \in H \to (({{norm}_{ℎ} ↾}_{H}) (x) = 0 \leftrightarrow {norm}_{ℎ} (x) = 0)$
115		norm-i	$⊢ x \in ℋ \to ({norm}_{ℎ} (x) = 0 \leftrightarrow x = 0_{ℎ})$
116	50 115	syl	$⊢ x \in H \to ({norm}_{ℎ} (x) = 0 \leftrightarrow x = 0_{ℎ})$
117	114 116	bitrd	$⊢ x \in H \to (({{norm}_{ℎ} ↾}_{H}) (x) = 0 \leftrightarrow x = 0_{ℎ})$
118	117	biimpa	$⊢ (x \in H \land ({{norm}_{ℎ} ↾}_{H}) (x) = 0) \to x = 0_{ℎ}$
119		norm-iii	$⊢ (y \in ℂ \land x \in ℋ) \to {norm}_{ℎ} (y \cdot_{ℎ} x) = \|y\| {norm}_{ℎ} (x)$
120	50 119	sylan2	$⊢ (y \in ℂ \land x \in H) \to {norm}_{ℎ} (y \cdot_{ℎ} x) = \|y\| {norm}_{ℎ} (x)$
121	67	fveq2d	$⊢ (y \in ℂ \land x \in H) \to ({{norm}_{ℎ} ↾}_{H}) (y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x) = ({{norm}_{ℎ} ↾}_{H}) (y \cdot_{ℎ} x)$
122		fvres	$⊢ y \cdot_{ℎ} x \in H \to ({{norm}_{ℎ} ↾}_{H}) (y \cdot_{ℎ} x) = {norm}_{ℎ} (y \cdot_{ℎ} x)$
123	73 122	syl	$⊢ (y \in ℂ \land x \in H) \to ({{norm}_{ℎ} ↾}_{H}) (y \cdot_{ℎ} x) = {norm}_{ℎ} (y \cdot_{ℎ} x)$
124	121 123	eqtrd	$⊢ (y \in ℂ \land x \in H) \to ({{norm}_{ℎ} ↾}_{H}) (y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x) = {norm}_{ℎ} (y \cdot_{ℎ} x)$
125	113	adantl	$⊢ (y \in ℂ \land x \in H) \to ({{norm}_{ℎ} ↾}_{H}) (x) = {norm}_{ℎ} (x)$
126	125	oveq2d	$⊢ (y \in ℂ \land x \in H) \to \|y\| ({{norm}_{ℎ} ↾}_{H}) (x) = \|y\| {norm}_{ℎ} (x)$
127	120 124 126	3eqtr4d	$⊢ (y \in ℂ \land x \in H) \to ({{norm}_{ℎ} ↾}_{H}) (y ({\cdot_{ℎ} ↾}_{(ℂ \times H)}) x) = \|y\| ({{norm}_{ℎ} ↾}_{H}) (x)$
128	2	sheli	$⊢ y \in H \to y \in ℋ$
129		norm-ii	$⊢ (x \in ℋ \land y \in ℋ) \to {norm}_{ℎ} (x +_{ℎ} y) \leq {norm}_{ℎ} (x) + {norm}_{ℎ} (y)$
130	50 128 129	syl2an	$⊢ (x \in H \land y \in H) \to {norm}_{ℎ} (x +_{ℎ} y) \leq {norm}_{ℎ} (x) + {norm}_{ℎ} (y)$
131		ovres	$⊢ (x \in H \land y \in H) \to x ({+_{ℎ} ↾}_{(H \times H)}) y = x +_{ℎ} y$
132	131	fveq2d	$⊢ (x \in H \land y \in H) \to ({{norm}_{ℎ} ↾}_{H}) (x ({+_{ℎ} ↾}_{(H \times H)}) y) = ({{norm}_{ℎ} ↾}_{H}) (x +_{ℎ} y)$
133		shaddcl	$⊢ (H \in S_{ℋ} \land x \in H \land y \in H) \to x +_{ℎ} y \in H$
134	2 133	mp3an1	$⊢ (x \in H \land y \in H) \to x +_{ℎ} y \in H$
135		fvres	$⊢ x +_{ℎ} y \in H \to ({{norm}_{ℎ} ↾}_{H}) (x +_{ℎ} y) = {norm}_{ℎ} (x +_{ℎ} y)$
136	134 135	syl	$⊢ (x \in H \land y \in H) \to ({{norm}_{ℎ} ↾}_{H}) (x +_{ℎ} y) = {norm}_{ℎ} (x +_{ℎ} y)$
137	132 136	eqtrd	$⊢ (x \in H \land y \in H) \to ({{norm}_{ℎ} ↾}_{H}) (x ({+_{ℎ} ↾}_{(H \times H)}) y) = {norm}_{ℎ} (x +_{ℎ} y)$
138		fvres	$⊢ y \in H \to ({{norm}_{ℎ} ↾}_{H}) (y) = {norm}_{ℎ} (y)$
139	113 138	oveqan12d	$⊢ (x \in H \land y \in H) \to ({{norm}_{ℎ} ↾}_{H}) (x) + ({{norm}_{ℎ} ↾}_{H}) (y) = {norm}_{ℎ} (x) + {norm}_{ℎ} (y)$
140	130 137 139	3brtr4d	$⊢ (x \in H \land y \in H) \to ({{norm}_{ℎ} ↾}_{H}) (x ({+_{ℎ} ↾}_{(H \times H)}) y) \leq ({{norm}_{ℎ} ↾}_{H}) (x) + ({{norm}_{ℎ} ↾}_{H}) (y)$
141	14 25 109 112 118 127 140 1	isnvi	$⊢ W \in NrmCVec$

Metamath Proof Explorer

Theorem hhssnv

Proof