Theorem hhssva

Description: The vector addition operation on a subspace. (Contributed by NM, 8-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hhss.1	|- W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.
Assertion	hhssva	|- ( +h |` ( H X. H ) ) = ( +v ` W )

Proof

Step	Hyp	Ref	Expression
1		hhss.1	|- W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.
2		eqid	|- ( +v ` W ) = ( +v ` W )
3	2	vafval	|- ( +v ` W ) = ( 1st ` ( 1st ` W ) )
4	1	fveq2i	|- ( 1st ` W ) = ( 1st ` <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. )
5		opex	|- <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. e. _V
6		normf	|- normh : ~H --> RR
7		ax-hilex	|- ~H e. _V
8		fex	|- ( ( normh : ~H --> RR /\ ~H e. _V ) -> normh e. _V )
9	6 7 8	mp2an	|- normh e. _V
10	9	resex	|- ( normh |` H ) e. _V
11	5 10	op1st	|- ( 1st ` <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. ) = <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >.
12	4 11	eqtri	|- ( 1st ` W ) = <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >.
13	12	fveq2i	|- ( 1st ` ( 1st ` W ) ) = ( 1st ` <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. )
14		hilablo	|- +h e. AbelOp
15		resexg	|- ( +h e. AbelOp -> ( +h |` ( H X. H ) ) e. _V )
16	14 15	ax-mp	|- ( +h |` ( H X. H ) ) e. _V
17		hvmulex	|- .h e. _V
18	17	resex	|- ( .h |` ( CC X. H ) ) e. _V
19	16 18	op1st	|- ( 1st ` <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. ) = ( +h |` ( H X. H ) )
20	3 13 19	3eqtrri	|- ( +h |` ( H X. H ) ) = ( +v ` W )