Theorem cnlnadjlem3

Description: Lemma for cnlnadji . By riesz4 , B is the unique vector such that ( Tv ) .ih y ) = ( v .ih w ) for all v . (Contributed by NM, 17-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cnlnadjlem.1	|- T e. LinOp
	cnlnadjlem.2	|- T e. ContOp
	cnlnadjlem.3	|- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )
	cnlnadjlem.4	|- B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )
Assertion	cnlnadjlem3	|- ( y e. ~H -> B e. ~H )

Proof

Step	Hyp	Ref	Expression
1		cnlnadjlem.1	|- T e. LinOp
2		cnlnadjlem.2	|- T e. ContOp
3		cnlnadjlem.3	|- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )
4		cnlnadjlem.4	|- B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )
5	1 2 3	cnlnadjlem2	|- ( y e. ~H -> ( G e. LinFn /\ G e. ContFn ) )
6		elin	|- ( G e. ( LinFn i^i ContFn ) <-> ( G e. LinFn /\ G e. ContFn ) )
7	5 6	sylibr	|- ( y e. ~H -> G e. ( LinFn i^i ContFn ) )
8		riesz4	|- ( G e. ( LinFn i^i ContFn ) -> E! w e. ~H A. v e. ~H ( G ` v ) = ( v .ih w ) )
9	7 8	syl	|- ( y e. ~H -> E! w e. ~H A. v e. ~H ( G ` v ) = ( v .ih w ) )
10	1 2 3	cnlnadjlem1	|- ( v e. ~H -> ( G ` v ) = ( ( T ` v ) .ih y ) )
11	10	eqeq1d	|- ( v e. ~H -> ( ( G ` v ) = ( v .ih w ) <-> ( ( T ` v ) .ih y ) = ( v .ih w ) ) )
12	11	ralbiia	|- ( A. v e. ~H ( G ` v ) = ( v .ih w ) <-> A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )
13	12	reubii	|- ( E! w e. ~H A. v e. ~H ( G ` v ) = ( v .ih w ) <-> E! w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )
14	9 13	sylib	|- ( y e. ~H -> E! w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )
15		riotacl	|- ( E! w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) -> ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) ) e. ~H )
16	14 15	syl	|- ( y e. ~H -> ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) ) e. ~H )
17	4 16	eqeltrid	|- ( y e. ~H -> B e. ~H )