Metamath Proof Explorer

Theorem sspmlem

Description: Lemma for sspm and others. (Contributed by NM, 1-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses sspmlem.y 
|- Y = ( BaseSet ` W )
sspmlem.h 
|- H = ( SubSp ` U )
sspmlem.1 
|- ( ( ( U e. NrmCVec /\ W e. H ) /\ ( x e. Y /\ y e. Y ) ) -> ( x F y ) = ( x G y ) )
sspmlem.2 
|- ( W e. NrmCVec -> F : ( Y X. Y ) --> R )
sspmlem.3 
|- ( U e. NrmCVec -> G : ( ( BaseSet ` U ) X. ( BaseSet ` U ) ) --> S )
Assertion sspmlem 
|- ( ( U e. NrmCVec /\ W e. H ) -> F = ( G |` ( Y X. Y ) ) )

Proof

Step Hyp Ref Expression
1 sspmlem.y 
 |-  Y = ( BaseSet ` W )
2 sspmlem.h 
 |-  H = ( SubSp ` U )
3 sspmlem.1 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( x e. Y /\ y e. Y ) ) -> ( x F y ) = ( x G y ) )
4 sspmlem.2 
 |-  ( W e. NrmCVec -> F : ( Y X. Y ) --> R )
5 sspmlem.3 
 |-  ( U e. NrmCVec -> G : ( ( BaseSet ` U ) X. ( BaseSet ` U ) ) --> S )
6 ovres 
 |-  ( ( x e. Y /\ y e. Y ) -> ( x ( G |` ( Y X. Y ) ) y ) = ( x G y ) )
7 6 adantl 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( x e. Y /\ y e. Y ) ) -> ( x ( G |` ( Y X. Y ) ) y ) = ( x G y ) )
8 3 7 eqtr4d 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( x e. Y /\ y e. Y ) ) -> ( x F y ) = ( x ( G |` ( Y X. Y ) ) y ) )
9 8 ralrimivva 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> A. x e. Y A. y e. Y ( x F y ) = ( x ( G |` ( Y X. Y ) ) y ) )
10 eqid 
 |-  ( Y X. Y ) = ( Y X. Y )
11 9 10 jctil 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( ( Y X. Y ) = ( Y X. Y ) /\ A. x e. Y A. y e. Y ( x F y ) = ( x ( G |` ( Y X. Y ) ) y ) ) )
12 2 sspnv 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> W e. NrmCVec )
13 ffn 
 |-  ( F : ( Y X. Y ) --> R -> F Fn ( Y X. Y ) )
14 12 4 13 3syl 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> F Fn ( Y X. Y ) )
15 5 ffnd 
 |-  ( U e. NrmCVec -> G Fn ( ( BaseSet ` U ) X. ( BaseSet ` U ) ) )
16 15 adantr 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> G Fn ( ( BaseSet ` U ) X. ( BaseSet ` U ) ) )
17 eqid 
 |-  ( BaseSet ` U ) = ( BaseSet ` U )
18 17 1 2 sspba 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> Y C_ ( BaseSet ` U ) )
19 xpss12 
 |-  ( ( Y C_ ( BaseSet ` U ) /\ Y C_ ( BaseSet ` U ) ) -> ( Y X. Y ) C_ ( ( BaseSet ` U ) X. ( BaseSet ` U ) ) )
20 18 18 19 syl2anc 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( Y X. Y ) C_ ( ( BaseSet ` U ) X. ( BaseSet ` U ) ) )
21 fnssres 
 |-  ( ( G Fn ( ( BaseSet ` U ) X. ( BaseSet ` U ) ) /\ ( Y X. Y ) C_ ( ( BaseSet ` U ) X. ( BaseSet ` U ) ) ) -> ( G |` ( Y X. Y ) ) Fn ( Y X. Y ) )
22 16 20 21 syl2anc 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( G |` ( Y X. Y ) ) Fn ( Y X. Y ) )
23 eqfnov 
 |-  ( ( F Fn ( Y X. Y ) /\ ( G |` ( Y X. Y ) ) Fn ( Y X. Y ) ) -> ( F = ( G |` ( Y X. Y ) ) <-> ( ( Y X. Y ) = ( Y X. Y ) /\ A. x e. Y A. y e. Y ( x F y ) = ( x ( G |` ( Y X. Y ) ) y ) ) ) )
24 14 22 23 syl2anc 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( F = ( G |` ( Y X. Y ) ) <-> ( ( Y X. Y ) = ( Y X. Y ) /\ A. x e. Y A. y e. Y ( x F y ) = ( x ( G |` ( Y X. Y ) ) y ) ) ) )
25 11 24 mpbird 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> F = ( G |` ( Y X. Y ) ) )