Metamath Proof Explorer

Theorem frlmipval

Description: The inner product of a free module. (Contributed by Thierry Arnoux, 21-Jun-2019)

Ref Expression
Hypotheses frlmphl.y 
|- Y = ( R freeLMod I )
frlmphl.b 
|- B = ( Base ` R )
frlmphl.t 
|- .x. = ( .r ` R )
frlmphl.v 
|- V = ( Base ` Y )
frlmphl.j 
|- ., = ( .i ` Y )
Assertion frlmipval 
|- ( ( ( I e. W /\ R e. X ) /\ ( F e. V /\ G e. V ) ) -> ( F ., G ) = ( R gsum ( F oF .x. G ) ) )

Proof

Step Hyp Ref Expression
1 frlmphl.y 
 |-  Y = ( R freeLMod I )
2 frlmphl.b 
 |-  B = ( Base ` R )
3 frlmphl.t 
 |-  .x. = ( .r ` R )
4 frlmphl.v 
 |-  V = ( Base ` Y )
5 frlmphl.j 
 |-  ., = ( .i ` Y )
6 1 2 4 frlmbasmap 
 |-  ( ( I e. W /\ F e. V ) -> F e. ( B ^m I ) )
7 6 ad2ant2r 
 |-  ( ( ( I e. W /\ R e. X ) /\ ( F e. V /\ G e. V ) ) -> F e. ( B ^m I ) )
8 elmapi 
 |-  ( F e. ( B ^m I ) -> F : I --> B )
9 ffn 
 |-  ( F : I --> B -> F Fn I )
10 7 8 9 3syl 
 |-  ( ( ( I e. W /\ R e. X ) /\ ( F e. V /\ G e. V ) ) -> F Fn I )
11 1 2 4 frlmbasmap 
 |-  ( ( I e. W /\ G e. V ) -> G e. ( B ^m I ) )
12 11 ad2ant2rl 
 |-  ( ( ( I e. W /\ R e. X ) /\ ( F e. V /\ G e. V ) ) -> G e. ( B ^m I ) )
13 elmapi 
 |-  ( G e. ( B ^m I ) -> G : I --> B )
14 ffn 
 |-  ( G : I --> B -> G Fn I )
15 12 13 14 3syl 
 |-  ( ( ( I e. W /\ R e. X ) /\ ( F e. V /\ G e. V ) ) -> G Fn I )
16 simpll 
 |-  ( ( ( I e. W /\ R e. X ) /\ ( F e. V /\ G e. V ) ) -> I e. W )
17 inidm 
 |-  ( I i^i I ) = I
18 eqidd 
 |-  ( ( ( ( I e. W /\ R e. X ) /\ ( F e. V /\ G e. V ) ) /\ x e. I ) -> ( F ` x ) = ( F ` x ) )
19 eqidd 
 |-  ( ( ( ( I e. W /\ R e. X ) /\ ( F e. V /\ G e. V ) ) /\ x e. I ) -> ( G ` x ) = ( G ` x ) )
20 10 15 16 16 17 18 19 offval 
 |-  ( ( ( I e. W /\ R e. X ) /\ ( F e. V /\ G e. V ) ) -> ( F oF .x. G ) = ( x e. I |-> ( ( F ` x ) .x. ( G ` x ) ) ) )
21 20 oveq2d 
 |-  ( ( ( I e. W /\ R e. X ) /\ ( F e. V /\ G e. V ) ) -> ( R gsum ( F oF .x. G ) ) = ( R gsum ( x e. I |-> ( ( F ` x ) .x. ( G ` x ) ) ) ) )
22 ovexd 
 |-  ( ( ( I e. W /\ R e. X ) /\ ( F e. V /\ G e. V ) ) -> ( R gsum ( x e. I |-> ( ( F ` x ) .x. ( G ` x ) ) ) ) e. _V )
23 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
24 23 oveq1d 
 |-  ( f = F -> ( ( f ` x ) .x. ( g ` x ) ) = ( ( F ` x ) .x. ( g ` x ) ) )
25 24 mpteq2dv 
 |-  ( f = F -> ( x e. I |-> ( ( f ` x ) .x. ( g ` x ) ) ) = ( x e. I |-> ( ( F ` x ) .x. ( g ` x ) ) ) )
26 25 oveq2d 
 |-  ( f = F -> ( R gsum ( x e. I |-> ( ( f ` x ) .x. ( g ` x ) ) ) ) = ( R gsum ( x e. I |-> ( ( F ` x ) .x. ( g ` x ) ) ) ) )
27 fveq1 
 |-  ( g = G -> ( g ` x ) = ( G ` x ) )
28 27 oveq2d 
 |-  ( g = G -> ( ( F ` x ) .x. ( g ` x ) ) = ( ( F ` x ) .x. ( G ` x ) ) )
29 28 mpteq2dv 
 |-  ( g = G -> ( x e. I |-> ( ( F ` x ) .x. ( g ` x ) ) ) = ( x e. I |-> ( ( F ` x ) .x. ( G ` x ) ) ) )
30 29 oveq2d 
 |-  ( g = G -> ( R gsum ( x e. I |-> ( ( F ` x ) .x. ( g ` x ) ) ) ) = ( R gsum ( x e. I |-> ( ( F ` x ) .x. ( G ` x ) ) ) ) )
31 eqid 
 |-  ( f e. ( B ^m I ) , g e. ( B ^m I ) |-> ( R gsum ( x e. I |-> ( ( f ` x ) .x. ( g ` x ) ) ) ) ) = ( f e. ( B ^m I ) , g e. ( B ^m I ) |-> ( R gsum ( x e. I |-> ( ( f ` x ) .x. ( g ` x ) ) ) ) )
32 26 30 31 ovmpog 
 |-  ( ( F e. ( B ^m I ) /\ G e. ( B ^m I ) /\ ( R gsum ( x e. I |-> ( ( F ` x ) .x. ( G ` x ) ) ) ) e. _V ) -> ( F ( f e. ( B ^m I ) , g e. ( B ^m I ) |-> ( R gsum ( x e. I |-> ( ( f ` x ) .x. ( g ` x ) ) ) ) ) G ) = ( R gsum ( x e. I |-> ( ( F ` x ) .x. ( G ` x ) ) ) ) )
33 7 12 22 32 syl3anc 
 |-  ( ( ( I e. W /\ R e. X ) /\ ( F e. V /\ G e. V ) ) -> ( F ( f e. ( B ^m I ) , g e. ( B ^m I ) |-> ( R gsum ( x e. I |-> ( ( f ` x ) .x. ( g ` x ) ) ) ) ) G ) = ( R gsum ( x e. I |-> ( ( F ` x ) .x. ( G ` x ) ) ) ) )
34 1 2 3 frlmip 
 |-  ( ( I e. W /\ R e. X ) -> ( f e. ( B ^m I ) , g e. ( B ^m I ) |-> ( R gsum ( x e. I |-> ( ( f ` x ) .x. ( g ` x ) ) ) ) ) = ( .i ` Y ) )
35 34 adantr 
 |-  ( ( ( I e. W /\ R e. X ) /\ ( F e. V /\ G e. V ) ) -> ( f e. ( B ^m I ) , g e. ( B ^m I ) |-> ( R gsum ( x e. I |-> ( ( f ` x ) .x. ( g ` x ) ) ) ) ) = ( .i ` Y ) )
36 35 5 eqtr4di 
 |-  ( ( ( I e. W /\ R e. X ) /\ ( F e. V /\ G e. V ) ) -> ( f e. ( B ^m I ) , g e. ( B ^m I ) |-> ( R gsum ( x e. I |-> ( ( f ` x ) .x. ( g ` x ) ) ) ) ) = ., )
37 36 oveqd 
 |-  ( ( ( I e. W /\ R e. X ) /\ ( F e. V /\ G e. V ) ) -> ( F ( f e. ( B ^m I ) , g e. ( B ^m I ) |-> ( R gsum ( x e. I |-> ( ( f ` x ) .x. ( g ` x ) ) ) ) ) G ) = ( F ., G ) )
38 21 33 37 3eqtr2rd 
 |-  ( ( ( I e. W /\ R e. X ) /\ ( F e. V /\ G e. V ) ) -> ( F ., G ) = ( R gsum ( F oF .x. G ) ) )