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 \|` ( H X. H ) ) , ( .h \|` ( CC X. H ) ) >. , ( normh \|` H ) >.
	hhssnv.2	\|- H e. SH
Assertion	hhssnv	\|- W e. NrmCVec

Proof

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

Metamath Proof Explorer

Theorem hhssnv

Proof