Theorem hhssnv 9073

Description: Normed complex vector space property of a subspace.

Hypotheses

Ref	Expression
hhssnvt.1	|- W = <.<.( +h |` (H X. H)), ( .h |` (CC X. H))>., (normh |` H)>.
hhssnv.2	|- H e. SH

Assertion

Ref	Expression
hhssnv	|- W e. NrmCVec

Proof of Theorem hhssnv

Step	Hyp	Ref	Expression
1		hhssnv.2	. . . . 5 |- H e. SH
2	1	hhssabl 9071	. . . 4 |- ( +h |` (H X. H)) e. Abel
3		ablgrp 8053	. . . 4 |- (( +h |` (H X. H)) e. Abel -> ( +h |` (H X. H)) e. Grp)
4	2, 3	ax-mp 7	. . 3 |- ( +h |` (H X. H)) e. Grp
5	1	shssi 9020	. . . . . 6 |- H (_ H~
6		ssxp 3251	. . . . . 6 |- ((H (_ H~ /\ H (_ H~) -> (H X. H) (_ (H~ X. H~))
7	5, 5, 6	mp2an 696	. . . . 5 |- (H X. H) (_ (H~ X. H~)
8		ax-hfvadd 8809	. . . . . 6 |- +h :(H~ X. H~)-->H~
9		fdm 3623	. . . . . 6 |- ( +h :(H~ X. H~)-->H~ -> dom +h = (H~ X. H~))
10	8, 9	ax-mp 7	. . . . 5 |- dom +h = (H~ X. H~)
11	7, 10	sseqtr4 2090	. . . 4 |- (H X. H) (_ dom +h
12		ssdmres 3373	. . . 4 |- ((H X. H) (_ dom +h <-> dom ( +h |` (H X. H)) = (H X. H))
13	11, 12	mpbi 189	. . 3 |- dom ( +h |` (H X. H)) = (H X. H)
14	4, 13	grprn 8006	. 2 |- H = ran ( +h |` (H X. H))
15		sh0 9023	. . . . . 6 |- (H e. SH -> 0h e. H)
16	1, 15	ax-mp 7	. . . . 5 |- 0h e. H
17		oprvalres 4024	. . . . 5 |- ((0h e. H /\ 0h e. H) -> (0h( +h |` (H X. H))0h) = (0h +h 0h))
18	16, 16, 17	mp2an 696	. . . 4 |- (0h( +h |` (H X. H))0h) = (0h +h 0h)
19		ax-hv0cl 8812	. . . . 5 |- 0h e. H~
20	19	hvaddid2 8837	. . . 4 |- (0h +h 0h) = 0h
21	18, 20	eqtr 1492	. . 3 |- (0h( +h |` (H X. H))0h) = 0h
22		eqid 1473	. . . . 5 |- (Id` ( +h |` (H X. H))) = (Id` ( +h |` (H X. H)))
23	14, 22	grpid 8015	. . . 4 |- ((( +h |` (H X. H)) e. Grp /\ 0h e. H) -> (0h = (Id` ( +h |` (H X. H))) <-> (0h( +h |` (H X. H))0h) = 0h))
24	4, 16, 23	mp2an 696	. . 3 |- (0h = (Id` ( +h |` (H X. H))) <-> (0h( +h |` (H X. H))0h) = 0h)
25	21, 24	mpbir 190	. 2 |- 0h = (Id` ( +h |` (H X. H)))
26		df-f 3189	. . . 4 |- (( .h |` (CC X. H)):(CC X. H)-->H <-> (( .h |` (CC X. H)) Fn (CC X. H) /\ ran ( .h |` (CC X. H)) (_ H))
27		ax-hfvmul 8814	. . . . . 6 |- .h :(CC X. H~)-->H~
28		ffn 3619	. . . . . 6 |- ( .h :(CC X. H~)-->H~ -> .h Fn (CC X. H~))
29	27, 28	ax-mp 7	. . . . 5 |- .h Fn (CC X. H~)
30		ssid 2076	. . . . . 6 |- CC (_ CC
31		ssxp 3251	. . . . . 6 |- ((CC (_ CC /\ H (_ H~) -> (CC X. H) (_ (CC X. H~))
32	30, 5, 31	mp2an 696	. . . . 5 |- (CC X. H) (_ (CC X. H~)
33		fnssres 3592	. . . . 5 |- (( .h Fn (CC X. H~) /\ (CC X. H) (_ (CC X. H~)) -> ( .h |` (CC X. H)) Fn (CC X. H))
34	29, 32, 33	mp2an 696	. . . 4 |- ( .h |` (CC X. H)) Fn (CC X. H)
35		oprvalelrn 4030	. . . . . . 7 |- (( .h |` (CC X. H)) Fn (CC X. H) -> (z e. ran ( .h |` (CC X. H)) <-> E.x e. CC E.y e. H (x( .h |` (CC X. H))y) = z))
36	34, 35	ax-mp 7	. . . . . 6 |- (z e. ran ( .h |` (CC X. H)) <-> E.x e. CC E.y e. H (x( .h |` (CC X. H))y) = z)
37		eleq1 1531	. . . . . . . 8 |- ((x( .h |` (CC X. H))y) = z -> ((x( .h |` (CC X. H))y) e. H <-> z e. H))
38		oprvalres 4024	. . . . . . . . 9 |- ((x e. CC /\ y e. H) -> (x( .h |` (CC X. H))y) = (x .h y))
39		shmulclt 9026	. . . . . . . . . 10 |- ((H e. SH /\ x e. CC /\ y e. H) -> (x .h y) e. H)
40	1, 39	mp3an1 901	. . . . . . . . 9 |- ((x e. CC /\ y e. H) -> (x .h y) e. H)
41	38, 40	eqeltrd 1545	. . . . . . . 8 |- ((x e. CC /\ y e. H) -> (x( .h |` (CC X. H))y) e. H)
42	37, 41	syl5cbi 209	. . . . . . 7 |- ((x e. CC /\ y e. H) -> ((x( .h |` (CC X. H))y) = z -> z e. H))
43	42	r19.23aivv 1745	. . . . . 6 |- (E.x e. CC E.y e. H (x( .h |` (CC X. H))y) = z -> z e. H)
44	36, 43	sylbi 199	. . . . 5 |- (z e. ran ( .h |` (CC X. H)) -> z e. H)
45	44	ssriv 2065	. . . 4 |- ran ( .h |` (CC X. H)) (_ H
46	26, 34, 45	mpbir2an 729	. . 3 |- ( .h |` (CC X. H)):(CC X. H)-->H
47		ax1cn 5249	. . . . 5 |- 1 e. CC
48		oprvalres 4024	. . . . 5 |- ((1 e. CC /\ x e. H) -> (1( .h |` (CC X. H))x) = (1 .h x))
49	47, 48	mpan 694	. . . 4 |- (x e. H -> (1( .h |` (CC X. H))x) = (1 .h x))
50	1	shel 9021	. . . . 5 |- (x e. H -> x e. H~)
51		ax-hvmulid 8815	. . . . 5 |- (x e. H~ -> (1 .h x) = x)
52	50, 51	syl 10	. . . 4 |- (x e. H -> (1 .h x) = x)
53	49, 52	eqtrd 1504	. . 3 |- (x e. H -> (1( .h |` (CC X. H))x) = x)
54		ax-hvdistr1 8817	. . . . 5 |- ((y e. CC /\ x e. H~ /\ z e. H~) -> (y .h (x +h z)) = ((y .h x) +h (y .h z)))
55		id 59	. . . . 5 |- (y e. CC -> y e. CC)
56	1	shel 9021	. . . . 5 |- (z e. H -> z e. H~)
57	54, 55, 50, 56	syl3an 867	. . . 4 |- ((y e. CC /\ x e. H /\ z e. H) -> (y .h (x +h z)) = ((y .h x) +h (y .h z)))
58		oprvalres 4024	. . . . . . 7 |- ((x e. H /\ z e. H) -> (x( +h |` (H X. H))z) = (x +h z))
59	58	3adant1 796	. . . . . 6 |- ((y e. CC /\ x e. H /\ z e. H) -> (x( +h |` (H X. H))z) = (x +h z))
60	59	opreq2d 3967	. . . . 5 |- ((y e. CC /\ x e. H /\ z e. H) -> (y( .h |` (CC X. H))(x( +h |` (H X. H))z)) = (y( .h |` (CC X. H))(x +h z)))
61		oprvalres 4024	. . . . . . 7 |- ((y e. CC /\ (x +h z) e. H) -> (y( .h |` (CC X. H))(x +h z)) = (y .h (x +h z)))
62		shaddclt 9024	. . . . . . . 8 |- ((H e. SH /\ x e. H /\ z e. H) -> (x +h z) e. H)
63	1, 62	mp3an1 901	. . . . . . 7 |- ((x e. H /\ z e. H) -> (x +h z) e. H)
64	61, 63	sylan2 451	. . . . . 6 |- ((y e. CC /\ (x e. H /\ z e. H)) -> (y( .h |` (CC X. H))(x +h z)) = (y .h (x +h z)))
65	64	3impb 828	. . . . 5 |- ((y e. CC /\ x e. H /\ z e. H) -> (y( .h |` (CC X. H))(x +h z)) = (y .h (x +h z)))
66	60, 65	eqtrd 1504	. . . 4 |- ((y e. CC /\ x e. H /\ z e. H) -> (y( .h |` (CC X. H))(x( +h |` (H X. H))z)) = (y .h (x +h z)))
67		oprvalres 4024	. . . . . . 7 |- ((y e. CC /\ x e. H) -> (y( .h |` (CC X. H))x) = (y .h x))
68	67	3adant3 798	. . . . . 6 |- ((y e. CC /\ x e. H /\ z e. H) -> (y( .h |` (CC X. H))x) = (y .h x))
69		oprvalres 4024	. . . . . . 7 |- ((y e. CC /\ z e. H) -> (y( .h |` (CC X. H))z) = (y .h z))
70	69	3adant2 797	. . . . . 6 |- ((y e. CC /\ x e. H /\ z e. H) -> (y( .h |` (CC X. H))z) = (y .h z))
71	68, 70	opreq12d 3969	. . . . 5 |- ((y e. CC /\ x e. H /\ z e. H) -> ((y( .h |` (CC X. H))x)( +h |` (H X. H))(y( .h |` (CC X. H))z)) = ((y .h x)( +h |` (H X. H))(y .h z)))
72		oprvalres 4024	. . . . . 6 |- (((y .h x) e. H /\ (y .h z) e. H) -> ((y .h x)( +h |` (H X. H))(y .h z)) = ((y .h x) +h (y .h z)))
73		shmulclt 9026	. . . . . . . 8 |- ((H e. SH /\ y e. CC /\ x e. H) -> (y .h x) e. H)
74	1, 73	mp3an1 901	. . . . . . 7 |- ((y e. CC /\ x e. H) -> (y .h x) e. H)
75	74	3adant3 798	. . . . . 6 |- ((y e. CC /\ x e. H /\ z e. H) -> (y .h x) e. H)
76		shmulclt 9026	. . . . . . . 8 |- ((H e. SH /\ y e. CC /\ z e. H) -> (y .h z) e.