Metamath Proof Explorer

Theorem frlmip

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

Ref Expression
Hypotheses frlmphl.y 
|- Y = ( R freeLMod I )
frlmphl.b 
|- B = ( Base ` R )
frlmphl.t 
|- .x. = ( .r ` R )
Assertion frlmip 
|- ( ( I e. W /\ R e. V ) -> ( f e. ( B ^m I ) , g e. ( B ^m I ) |-> ( R gsum ( x e. I |-> ( ( f ` x ) .x. ( g ` x ) ) ) ) ) = ( .i ` Y ) )

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 eqid 
 |-  ( R freeLMod I ) = ( R freeLMod I )
5 eqid 
 |-  ( Base ` ( R freeLMod I ) ) = ( Base ` ( R freeLMod I ) )
6 4 5 frlmpws 
 |-  ( ( R e. V /\ I e. W ) -> ( R freeLMod I ) = ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` ( R freeLMod I ) ) ) )
7 6 ancoms 
 |-  ( ( I e. W /\ R e. V ) -> ( R freeLMod I ) = ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` ( R freeLMod I ) ) ) )
8 2 ressid 
 |-  ( R e. V -> ( R |`s B ) = R )
9 eqidd 
 |-  ( R e. V -> ( ( subringAlg ` R ) ` B ) = ( ( subringAlg ` R ) ` B ) )
10 2 eqimssi 
 |-  B C_ ( Base ` R )
11 10 a1i 
 |-  ( R e. V -> B C_ ( Base ` R ) )
12 9 11 srasca 
 |-  ( R e. V -> ( R |`s B ) = ( Scalar ` ( ( subringAlg ` R ) ` B ) ) )
13 8 12 eqtr3d 
 |-  ( R e. V -> R = ( Scalar ` ( ( subringAlg ` R ) ` B ) ) )
14 13 oveq1d 
 |-  ( R e. V -> ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) = ( ( Scalar ` ( ( subringAlg ` R ) ` B ) ) Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) )
15 14 adantl 
 |-  ( ( I e. W /\ R e. V ) -> ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) = ( ( Scalar ` ( ( subringAlg ` R ) ` B ) ) Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) )
16 fvex 
 |-  ( ( subringAlg ` R ) ` B ) e. _V
17 rlmval 
 |-  ( ringLMod ` R ) = ( ( subringAlg ` R ) ` ( Base ` R ) )
18 2 fveq2i 
 |-  ( ( subringAlg ` R ) ` B ) = ( ( subringAlg ` R ) ` ( Base ` R ) )
19 17 18 eqtr4i 
 |-  ( ringLMod ` R ) = ( ( subringAlg ` R ) ` B )
20 19 oveq1i 
 |-  ( ( ringLMod ` R ) ^s I ) = ( ( ( subringAlg ` R ) ` B ) ^s I )
21 eqid 
 |-  ( Scalar ` ( ( subringAlg ` R ) ` B ) ) = ( Scalar ` ( ( subringAlg ` R ) ` B ) )
22 20 21 pwsval 
 |-  ( ( ( ( subringAlg ` R ) ` B ) e. _V /\ I e. W ) -> ( ( ringLMod ` R ) ^s I ) = ( ( Scalar ` ( ( subringAlg ` R ) ` B ) ) Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) )
23 16 22 mpan 
 |-  ( I e. W -> ( ( ringLMod ` R ) ^s I ) = ( ( Scalar ` ( ( subringAlg ` R ) ` B ) ) Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) )
24 23 adantr 
 |-  ( ( I e. W /\ R e. V ) -> ( ( ringLMod ` R ) ^s I ) = ( ( Scalar ` ( ( subringAlg ` R ) ` B ) ) Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) )
25 15 24 eqtr4d 
 |-  ( ( I e. W /\ R e. V ) -> ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) = ( ( ringLMod ` R ) ^s I ) )
26 1 fveq2i 
 |-  ( Base ` Y ) = ( Base ` ( R freeLMod I ) )
27 26 a1i 
 |-  ( ( I e. W /\ R e. V ) -> ( Base ` Y ) = ( Base ` ( R freeLMod I ) ) )
28 25 27 oveq12d 
 |-  ( ( I e. W /\ R e. V ) -> ( ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) |`s ( Base ` Y ) ) = ( ( ( ringLMod ` R ) ^s I ) |`s ( Base ` ( R freeLMod I ) ) ) )
29 7 28 eqtr4d 
 |-  ( ( I e. W /\ R e. V ) -> ( R freeLMod I ) = ( ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) |`s ( Base ` Y ) ) )
30 1 29 syl5eq 
 |-  ( ( I e. W /\ R e. V ) -> Y = ( ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) |`s ( Base ` Y ) ) )
31 30 fveq2d 
 |-  ( ( I e. W /\ R e. V ) -> ( .i ` Y ) = ( .i ` ( ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) |`s ( Base ` Y ) ) ) )
32 fvex 
 |-  ( Base ` Y ) e. _V
33 eqid 
 |-  ( ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) |`s ( Base ` Y ) ) = ( ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) |`s ( Base ` Y ) )
34 eqid 
 |-  ( .i ` ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) ) = ( .i ` ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) )
35 33 34 ressip 
 |-  ( ( Base ` Y ) e. _V -> ( .i ` ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) ) = ( .i ` ( ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) |`s ( Base ` Y ) ) ) )
36 32 35 ax-mp 
 |-  ( .i ` ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) ) = ( .i ` ( ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) |`s ( Base ` Y ) ) )
37 eqid 
 |-  ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) = ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) )
38 simpr 
 |-  ( ( I e. W /\ R e. V ) -> R e. V )
39 snex 
 |-  { ( ( subringAlg ` R ) ` B ) } e. _V
40 xpexg 
 |-  ( ( I e. W /\ { ( ( subringAlg ` R ) ` B ) } e. _V ) -> ( I X. { ( ( subringAlg ` R ) ` B ) } ) e. _V )
41 39 40 mpan2 
 |-  ( I e. W -> ( I X. { ( ( subringAlg ` R ) ` B ) } ) e. _V )
42 41 adantr 
 |-  ( ( I e. W /\ R e. V ) -> ( I X. { ( ( subringAlg ` R ) ` B ) } ) e. _V )
43 eqid 
 |-  ( Base ` ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) ) = ( Base ` ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) )
44 16 snnz 
 |-  { ( ( subringAlg ` R ) ` B ) } =/= (/)
45 dmxp 
 |-  ( { ( ( subringAlg ` R ) ` B ) } =/= (/) -> dom ( I X. { ( ( subringAlg ` R ) ` B ) } ) = I )
46 44 45 mp1i 
 |-  ( ( I e. W /\ R e. V ) -> dom ( I X. { ( ( subringAlg ` R ) ` B ) } ) = I )
47 37 38 42 43 46 34 prdsip 
 |-  ( ( I e. W /\ R e. V ) -> ( .i ` ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) ) = ( f e. ( Base ` ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) ) , g e. ( Base ` ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) ) |-> ( R gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( ( I X. { ( ( subringAlg ` R ) ` B ) } ) ` x ) ) ( g ` x ) ) ) ) ) )
48 37 38 42 43 46 prdsbas 
 |-  ( ( I e. W /\ R e. V ) -> ( Base ` ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) ) = X_ x e. I ( Base ` ( ( I X. { ( ( subringAlg ` R ) ` B ) } ) ` x ) ) )
49 eqidd 
 |-  ( x e. I -> ( ( subringAlg ` R ) ` B ) = ( ( subringAlg ` R ) ` B ) )
50 10 a1i 
 |-  ( x e. I -> B C_ ( Base ` R ) )
51 49 50 srabase 
 |-  ( x e. I -> ( Base ` R ) = ( Base ` ( ( subringAlg ` R ) ` B ) ) )
52 2 a1i 
 |-  ( x e. I -> B = ( Base ` R ) )
53 16 fvconst2 
 |-  ( x e. I -> ( ( I X. { ( ( subringAlg ` R ) ` B ) } ) ` x ) = ( ( subringAlg ` R ) ` B ) )
54 53 fveq2d 
 |-  ( x e. I -> ( Base ` ( ( I X. { ( ( subringAlg ` R ) ` B ) } ) ` x ) ) = ( Base ` ( ( subringAlg ` R ) ` B ) ) )
55 51 52 54 3eqtr4rd 
 |-  ( x e. I -> ( Base ` ( ( I X. { ( ( subringAlg ` R ) ` B ) } ) ` x ) ) = B )
56 55 adantl 
 |-  ( ( ( I e. W /\ R e. V ) /\ x e. I ) -> ( Base ` ( ( I X. { ( ( subringAlg ` R ) ` B ) } ) ` x ) ) = B )
57 56 ixpeq2dva 
 |-  ( ( I e. W /\ R e. V ) -> X_ x e. I ( Base ` ( ( I X. { ( ( subringAlg ` R ) ` B ) } ) ` x ) ) = X_ x e. I B )
58 2 fvexi 
 |-  B e. _V
59 ixpconstg 
 |-  ( ( I e. W /\ B e. _V ) -> X_ x e. I B = ( B ^m I ) )
60 58 59 mpan2 
 |-  ( I e. W -> X_ x e. I B = ( B ^m I ) )
61 60 adantr 
 |-  ( ( I e. W /\ R e. V ) -> X_ x e. I B = ( B ^m I ) )
62 48 57 61 3eqtrd 
 |-  ( ( I e. W /\ R e. V ) -> ( Base ` ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) ) = ( B ^m I ) )
63 53 50 sraip 
 |-  ( x e. I -> ( .r ` R ) = ( .i ` ( ( I X. { ( ( subringAlg ` R ) ` B ) } ) ` x ) ) )
64 3 63 syl5req 
 |-  ( x e. I -> ( .i ` ( ( I X. { ( ( subringAlg ` R ) ` B ) } ) ` x ) ) = .x. )
65 64 oveqd 
 |-  ( x e. I -> ( ( f ` x ) ( .i ` ( ( I X. { ( ( subringAlg ` R ) ` B ) } ) ` x ) ) ( g ` x ) ) = ( ( f ` x ) .x. ( g ` x ) ) )
66 65 mpteq2ia 
 |-  ( x e. I |-> ( ( f ` x ) ( .i ` ( ( I X. { ( ( subringAlg ` R ) ` B ) } ) ` x ) ) ( g ` x ) ) ) = ( x e. I |-> ( ( f ` x ) .x. ( g ` x ) ) )
67 66 oveq2i 
 |-  ( R gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( ( I X. { ( ( subringAlg ` R ) ` B ) } ) ` x ) ) ( g ` x ) ) ) ) = ( R gsum ( x e. I |-> ( ( f ` x ) .x. ( g ` x ) ) ) )
68 67 a1i 
 |-  ( ( I e. W /\ R e. V ) -> ( R gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( ( I X. { ( ( subringAlg ` R ) ` B ) } ) ` x ) ) ( g ` x ) ) ) ) = ( R gsum ( x e. I |-> ( ( f ` x ) .x. ( g ` x ) ) ) ) )
69 62 62 68 mpoeq123dv 
 |-  ( ( I e. W /\ R e. V ) -> ( f e. ( Base ` ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) ) , g e. ( Base ` ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) ) |-> ( R gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( ( I X. { ( ( subringAlg ` R ) ` B ) } ) ` x ) ) ( g ` x ) ) ) ) ) = ( f e. ( B ^m I ) , g e. ( B ^m I ) |-> ( R gsum ( x e. I |-> ( ( f ` x ) .x. ( g ` x ) ) ) ) ) )
70 47 69 eqtrd 
 |-  ( ( I e. W /\ R e. V ) -> ( .i ` ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) ) = ( f e. ( B ^m I ) , g e. ( B ^m I ) |-> ( R gsum ( x e. I |-> ( ( f ` x ) .x. ( g ` x ) ) ) ) ) )
71 36 70 eqtr3id 
 |-  ( ( I e. W /\ R e. V ) -> ( .i ` ( ( R Xs_ ( I X. { ( ( subringAlg ` R ) ` B ) } ) ) |`s ( Base ` Y ) ) ) = ( f e. ( B ^m I ) , g e. ( B ^m I ) |-> ( R gsum ( x e. I |-> ( ( f ` x ) .x. ( g ` x ) ) ) ) ) )
72 31 71 eqtr2d 
 |-  ( ( I e. W /\ R e. V ) -> ( f e. ( B ^m I ) , g e. ( B ^m I ) |-> ( R gsum ( x e. I |-> ( ( f ` x ) .x. ( g ` x ) ) ) ) ) = ( .i ` Y ) )