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 ) ) )