MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  frlmphl Structured version   Unicode version

Theorem frlmphl 18619
Description: Conditions for a free module to be a pre-Hilbert space. (Contributed by Thierry Arnoux, 21-Jun-2019.) (Proof shortened by AV, 21-Jul-2019.)
Hypotheses
Ref Expression
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 )
frlmphl.o  |-  O  =  ( 0g `  Y
)
frlmphl.0  |-  .0.  =  ( 0g `  R )
frlmphl.s  |-  .*  =  ( *r `  R )
frlmphl.f  |-  ( ph  ->  R  e. Field )
frlmphl.m  |-  ( (
ph  /\  g  e.  V  /\  ( g  .,  g )  =  .0.  )  ->  g  =  O )
frlmphl.u  |-  ( (
ph  /\  x  e.  B )  ->  (  .*  `  x )  =  x )
frlmphl.i  |-  ( ph  ->  I  e.  W )
Assertion
Ref Expression
frlmphl  |-  ( ph  ->  Y  e.  PreHil )
Distinct variable groups:    B, g, x    g, I, x    R, g, x    g, V, x   
g, W, x    .x. , g, x    g, Y, x    .0. , g, x    ph, g, x    ., , g, x    g, O   
x,  .*
Allowed substitution hints:    .* ( g)    O( x)

Proof of Theorem frlmphl
Dummy variables  f 
e  h  i  y  z  k are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frlmphl.v . . 3  |-  V  =  ( Base `  Y
)
21a1i 11 . 2  |-  ( ph  ->  V  =  ( Base `  Y ) )
3 eqidd 2468 . 2  |-  ( ph  ->  ( +g  `  Y
)  =  ( +g  `  Y ) )
4 eqidd 2468 . 2  |-  ( ph  ->  ( .s `  Y
)  =  ( .s
`  Y ) )
5 frlmphl.j . . 3  |-  .,  =  ( .i `  Y )
65a1i 11 . 2  |-  ( ph  ->  .,  =  ( .i
`  Y ) )
7 frlmphl.o . . 3  |-  O  =  ( 0g `  Y
)
87a1i 11 . 2  |-  ( ph  ->  O  =  ( 0g
`  Y ) )
9 frlmphl.f . . . . 5  |-  ( ph  ->  R  e. Field )
10 isfld 17217 . . . . 5  |-  ( R  e. Field 
<->  ( R  e.  DivRing  /\  R  e.  CRing ) )
119, 10sylib 196 . . . 4  |-  ( ph  ->  ( R  e.  DivRing  /\  R  e.  CRing ) )
1211simpld 459 . . 3  |-  ( ph  ->  R  e.  DivRing )
13 frlmphl.i . . 3  |-  ( ph  ->  I  e.  W )
14 frlmphl.y . . . 4  |-  Y  =  ( R freeLMod  I )
1514frlmsca 18591 . . 3  |-  ( ( R  e.  DivRing  /\  I  e.  W )  ->  R  =  (Scalar `  Y )
)
1612, 13, 15syl2anc 661 . 2  |-  ( ph  ->  R  =  (Scalar `  Y ) )
17 frlmphl.b . . 3  |-  B  =  ( Base `  R
)
1817a1i 11 . 2  |-  ( ph  ->  B  =  ( Base `  R ) )
19 eqidd 2468 . 2  |-  ( ph  ->  ( +g  `  R
)  =  ( +g  `  R ) )
20 frlmphl.t . . 3  |-  .x.  =  ( .r `  R )
2120a1i 11 . 2  |-  ( ph  ->  .x.  =  ( .r
`  R ) )
22 frlmphl.s . . 3  |-  .*  =  ( *r `  R )
2322a1i 11 . 2  |-  ( ph  ->  .*  =  ( *r `  R ) )
24 frlmphl.0 . . 3  |-  .0.  =  ( 0g `  R )
2524a1i 11 . 2  |-  ( ph  ->  .0.  =  ( 0g
`  R ) )
26 drngrng 17215 . . . . 5  |-  ( R  e.  DivRing  ->  R  e.  Ring )
2712, 26syl 16 . . . 4  |-  ( ph  ->  R  e.  Ring )
2814frlmlmod 18587 . . . 4  |-  ( ( R  e.  Ring  /\  I  e.  W )  ->  Y  e.  LMod )
2927, 13, 28syl2anc 661 . . 3  |-  ( ph  ->  Y  e.  LMod )
3016, 12eqeltrrd 2556 . . 3  |-  ( ph  ->  (Scalar `  Y )  e.  DivRing )
31 eqid 2467 . . . 4  |-  (Scalar `  Y )  =  (Scalar `  Y )
3231islvec 17562 . . 3  |-  ( Y  e.  LVec  <->  ( Y  e. 
LMod  /\  (Scalar `  Y
)  e.  DivRing ) )
3329, 30, 32sylanbrc 664 . 2  |-  ( ph  ->  Y  e.  LVec )
3411simprd 463 . . 3  |-  ( ph  ->  R  e.  CRing )
35 frlmphl.u . . 3  |-  ( (
ph  /\  x  e.  B )  ->  (  .*  `  x )  =  x )
3617, 22, 34, 35idsrngd 17323 . 2  |-  ( ph  ->  R  e.  *Ring )
37133ad2ant1 1017 . . . . 5  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  I  e.  W )
38273ad2ant1 1017 . . . . 5  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  R  e.  Ring )
39 simp2 997 . . . . 5  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  g  e.  V )
40 simp3 998 . . . . 5  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  h  e.  V )
4114, 17, 20, 1, 5frlmipval 18617 . . . . 5  |-  ( ( ( I  e.  W  /\  R  e.  Ring )  /\  ( g  e.  V  /\  h  e.  V ) )  -> 
( g  .,  h
)  =  ( R 
gsumg  ( g  oF  .x.  h ) ) )
4237, 38, 39, 40, 41syl22anc 1229 . . . 4  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( g  .,  h )  =  ( R  gsumg  ( g  oF  .x.  h ) ) )
4314, 17, 1frlmbasmap 18600 . . . . . . . . 9  |-  ( ( I  e.  W  /\  g  e.  V )  ->  g  e.  ( B  ^m  I ) )
4437, 39, 43syl2anc 661 . . . . . . . 8  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  g  e.  ( B  ^m  I ) )
45 elmapi 7441 . . . . . . . 8  |-  ( g  e.  ( B  ^m  I )  ->  g : I --> B )
4644, 45syl 16 . . . . . . 7  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  g :
I --> B )
47 ffn 5731 . . . . . . 7  |-  ( g : I --> B  -> 
g  Fn  I )
4846, 47syl 16 . . . . . 6  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  g  Fn  I )
4914, 17, 1frlmbasmap 18600 . . . . . . . . 9  |-  ( ( I  e.  W  /\  h  e.  V )  ->  h  e.  ( B  ^m  I ) )
5037, 40, 49syl2anc 661 . . . . . . . 8  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  h  e.  ( B  ^m  I ) )
51 elmapi 7441 . . . . . . . 8  |-  ( h  e.  ( B  ^m  I )  ->  h : I --> B )
5250, 51syl 16 . . . . . . 7  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  h :
I --> B )
53 ffn 5731 . . . . . . 7  |-  ( h : I --> B  ->  h  Fn  I )
5452, 53syl 16 . . . . . 6  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  h  Fn  I )
55 inidm 3707 . . . . . 6  |-  ( I  i^i  I )  =  I
56 eqidd 2468 . . . . . 6  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  x  e.  I )  ->  (
g `  x )  =  ( g `  x ) )
57 eqidd 2468 . . . . . 6  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  x  e.  I )  ->  (
h `  x )  =  ( h `  x ) )
5848, 54, 37, 37, 55, 56, 57offval 6532 . . . . 5  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( g  oF  .x.  h )  =  ( x  e.  I  |->  ( ( g `
 x )  .x.  ( h `  x
) ) ) )
5958oveq2d 6301 . . . 4  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( R  gsumg  ( g  oF  .x.  h ) )  =  ( R  gsumg  ( x  e.  I  |->  ( ( g `  x )  .x.  (
h `  x )
) ) ) )
6042, 59eqtrd 2508 . . 3  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( g  .,  h )  =  ( R  gsumg  ( x  e.  I  |->  ( ( g `  x )  .x.  (
h `  x )
) ) ) )
61 rngcmn 17042 . . . . . 6  |-  ( R  e.  Ring  ->  R  e. CMnd
)
6227, 61syl 16 . . . . 5  |-  ( ph  ->  R  e. CMnd )
63623ad2ant1 1017 . . . 4  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  R  e. CMnd )
6438adantr 465 . . . . . 6  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  x  e.  I )  ->  R  e.  Ring )
6546ffvelrnda 6022 . . . . . 6  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  x  e.  I )  ->  (
g `  x )  e.  B )
6652ffvelrnda 6022 . . . . . 6  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  x  e.  I )  ->  (
h `  x )  e.  B )
6717, 20rngcl 17025 . . . . . 6  |-  ( ( R  e.  Ring  /\  (
g `  x )  e.  B  /\  (
h `  x )  e.  B )  ->  (
( g `  x
)  .x.  ( h `  x ) )  e.  B )
6864, 65, 66, 67syl3anc 1228 . . . . 5  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  x  e.  I )  ->  (
( g `  x
)  .x.  ( h `  x ) )  e.  B )
69 eqid 2467 . . . . 5  |-  ( x  e.  I  |->  ( ( g `  x ) 
.x.  ( h `  x ) ) )  =  ( x  e.  I  |->  ( ( g `
 x )  .x.  ( h `  x
) ) )
7068, 69fmptd 6046 . . . 4  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( x  e.  I  |->  ( ( g `  x ) 
.x.  ( h `  x ) ) ) : I --> B )
71 frlmphl.m . . . . 5  |-  ( (
ph  /\  g  e.  V  /\  ( g  .,  g )  =  .0.  )  ->  g  =  O )
7214, 17, 20, 1, 5, 7, 24, 22, 9, 71, 35, 13frlmphllem 18618 . . . 4  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( x  e.  I  |->  ( ( g `  x ) 
.x.  ( h `  x ) ) ) finSupp  .0.  )
7317, 24, 63, 37, 70, 72gsumcl 16738 . . 3  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( R  gsumg  ( x  e.  I  |->  ( ( g `  x
)  .x.  ( h `  x ) ) ) )  e.  B )
7460, 73eqeltrd 2555 . 2  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( g  .,  h )  e.  B
)
75 eqid 2467 . . . 4  |-  ( +g  `  R )  =  ( +g  `  R )
76623ad2ant1 1017 . . . 4  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  R  e. CMnd )
77133ad2ant1 1017 . . . 4  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  I  e.  W )
78273ad2ant1 1017 . . . . . 6  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  R  e.  Ring )
7978adantr 465 . . . . 5  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  R  e.  Ring )
80 simp2 997 . . . . . 6  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
k  e.  B )
8180adantr 465 . . . . 5  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  k  e.  B )
82 simp31 1032 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
g  e.  V )
8377, 82, 43syl2anc 661 . . . . . . . 8  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
g  e.  ( B  ^m  I ) )
8483, 45syl 16 . . . . . . 7  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
g : I --> B )
8584ffvelrnda 6022 . . . . . 6  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
g `  x )  e.  B )
86 simp33 1034 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
i  e.  V )
8714, 17, 1frlmbasmap 18600 . . . . . . . . 9  |-  ( ( I  e.  W  /\  i  e.  V )  ->  i  e.  ( B  ^m  I ) )
8877, 86, 87syl2anc 661 . . . . . . . 8  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
i  e.  ( B  ^m  I ) )
89 elmapi 7441 . . . . . . . 8  |-  ( i  e.  ( B  ^m  I )  ->  i : I --> B )
9088, 89syl 16 . . . . . . 7  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
i : I --> B )
9190ffvelrnda 6022 . . . . . 6  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
i `  x )  e.  B )
9217, 20rngcl 17025 . . . . . 6  |-  ( ( R  e.  Ring  /\  (
g `  x )  e.  B  /\  (
i `  x )  e.  B )  ->  (
( g `  x
)  .x.  ( i `  x ) )  e.  B )
9379, 85, 91, 92syl3anc 1228 . . . . 5  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
( g `  x
)  .x.  ( i `  x ) )  e.  B )
9417, 20rngcl 17025 . . . . 5  |-  ( ( R  e.  Ring  /\  k  e.  B  /\  (
( g `  x
)  .x.  ( i `  x ) )  e.  B )  ->  (
k  .x.  ( (
g `  x )  .x.  ( i `  x
) ) )  e.  B )
9579, 81, 93, 94syl3anc 1228 . . . 4  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
k  .x.  ( (
g `  x )  .x.  ( i `  x
) ) )  e.  B )
96 simp32 1033 . . . . . . . 8  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  h  e.  V )
9777, 96, 49syl2anc 661 . . . . . . 7  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  h  e.  ( B  ^m  I ) )
9897, 51syl 16 . . . . . 6  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  h : I --> B )
9998ffvelrnda 6022 . . . . 5  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
h `  x )  e.  B )
10017, 20rngcl 17025 . . . . 5  |-  ( ( R  e.  Ring  /\  (
h `  x )  e.  B  /\  (
i `  x )  e.  B )  ->  (
( h `  x
)  .x.  ( i `  x ) )  e.  B )
10179, 99, 91, 100syl3anc 1228 . . . 4  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
( h `  x
)  .x.  ( i `  x ) )  e.  B )
102 eqidd 2468 . . . 4  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( x  e.  I  |->  ( k  .x.  (
( g `  x
)  .x.  ( i `  x ) ) ) )  =  ( x  e.  I  |->  ( k 
.x.  ( ( g `
 x )  .x.  ( i `  x
) ) ) ) )
103 eqidd 2468 . . . 4  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( x  e.  I  |->  ( ( h `  x )  .x.  (
i `  x )
) )  =  ( x  e.  I  |->  ( ( h `  x
)  .x.  ( i `  x ) ) ) )
104 fveq2 5866 . . . . . . . . 9  |-  ( x  =  y  ->  (
g `  x )  =  ( g `  y ) )
105104oveq2d 6301 . . . . . . . 8  |-  ( x  =  y  ->  (
k  .x.  ( g `  x ) )  =  ( k  .x.  (
g `  y )
) )
106105cbvmptv 4538 . . . . . . 7  |-  ( x  e.  I  |->  ( k 
.x.  ( g `  x ) ) )  =  ( y  e.  I  |->  ( k  .x.  ( g `  y
) ) )
107106oveq1i 6295 . . . . . 6  |-  ( ( x  e.  I  |->  ( k  .x.  ( g `
 x ) ) )  oF  .x.  i )  =  ( ( y  e.  I  |->  ( k  .x.  (
g `  y )
) )  oF  .x.  i )
10817, 20rngcl 17025 . . . . . . . . . . . 12  |-  ( ( R  e.  Ring  /\  k  e.  B  /\  (
g `  x )  e.  B )  ->  (
k  .x.  ( g `  x ) )  e.  B )
10979, 81, 85, 108syl3anc 1228 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
k  .x.  ( g `  x ) )  e.  B )
110 eqid 2467 . . . . . . . . . . 11  |-  ( x  e.  I  |->  ( k 
.x.  ( g `  x ) ) )  =  ( x  e.  I  |->  ( k  .x.  ( g `  x
) ) )
111109, 110fmptd 6046 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( x  e.  I  |->  ( k  .x.  (
g `  x )
) ) : I --> B )
112 ffn 5731 . . . . . . . . . 10  |-  ( ( x  e.  I  |->  ( k  .x.  ( g `
 x ) ) ) : I --> B  -> 
( x  e.  I  |->  ( k  .x.  (
g `  x )
) )  Fn  I
)
113111, 112syl 16 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( x  e.  I  |->  ( k  .x.  (
g `  x )
) )  Fn  I
)
114106fneq1i 5675 . . . . . . . . 9  |-  ( ( x  e.  I  |->  ( k  .x.  ( g `
 x ) ) )  Fn  I  <->  ( y  e.  I  |->  ( k 
.x.  ( g `  y ) ) )  Fn  I )
115113, 114sylib 196 . . . . . . . 8  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( y  e.  I  |->  ( k  .x.  (
g `  y )
) )  Fn  I
)
116 ffn 5731 . . . . . . . . 9  |-  ( i : I --> B  -> 
i  Fn  I )
11790, 116syl 16 . . . . . . . 8  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
i  Fn  I )
118 eqidd 2468 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
y  e.  I  |->  ( k  .x.  ( g `
 y ) ) )  =  ( y  e.  I  |->  ( k 
.x.  ( g `  y ) ) ) )
119 simpr 461 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V
) )  /\  x  e.  I )  /\  y  =  x )  ->  y  =  x )
120119fveq2d 5870 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V
) )  /\  x  e.  I )  /\  y  =  x )  ->  (
g `  y )  =  ( g `  x ) )
121120oveq2d 6301 . . . . . . . . 9  |-  ( ( ( ( ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V
) )  /\  x  e.  I )  /\  y  =  x )  ->  (
k  .x.  ( g `  y ) )  =  ( k  .x.  (
g `  x )
) )
122 simpr 461 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  x  e.  I )
123 ovex 6310 . . . . . . . . . 10  |-  ( k 
.x.  ( g `  x ) )  e. 
_V
124123a1i 11 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
k  .x.  ( g `  x ) )  e. 
_V )
125118, 121, 122, 124fvmptd 5956 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
( y  e.  I  |->  ( k  .x.  (
g `  y )
) ) `  x
)  =  ( k 
.x.  ( g `  x ) ) )
126 eqidd 2468 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
i `  x )  =  ( i `  x ) )
127115, 117, 77, 77, 55, 125, 126offval 6532 . . . . . . 7  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( ( y  e.  I  |->  ( k  .x.  ( g `  y
) ) )  oF  .x.  i )  =  ( x  e.  I  |->  ( ( k 
.x.  ( g `  x ) )  .x.  ( i `  x
) ) ) )
12817, 20rngass 17028 . . . . . . . . 9  |-  ( ( R  e.  Ring  /\  (
k  e.  B  /\  ( g `  x
)  e.  B  /\  ( i `  x
)  e.  B ) )  ->  ( (
k  .x.  ( g `  x ) )  .x.  ( i `  x
) )  =  ( k  .x.  ( ( g `  x ) 
.x.  ( i `  x ) ) ) )
12979, 81, 85, 91, 128syl13anc 1230 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
( k  .x.  (
g `  x )
)  .x.  ( i `  x ) )  =  ( k  .x.  (
( g `  x
)  .x.  ( i `  x ) ) ) )
130129mpteq2dva 4533 . . . . . . 7  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( x  e.  I  |->  ( ( k  .x.  ( g `  x
) )  .x.  (
i `  x )
) )  =  ( x  e.  I  |->  ( k  .x.  ( ( g `  x ) 
.x.  ( i `  x ) ) ) ) )
131127, 130eqtrd 2508 . . . . . 6  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( ( y  e.  I  |->  ( k  .x.  ( g `  y
) ) )  oF  .x.  i )  =  ( x  e.  I  |->  ( k  .x.  ( ( g `  x )  .x.  (
i `  x )
) ) ) )
132107, 131syl5eq 2520 . . . . 5  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( ( x  e.  I  |->  ( k  .x.  ( g `  x
) ) )  oF  .x.  i )  =  ( x  e.  I  |->  ( k  .x.  ( ( g `  x )  .x.  (
i `  x )
) ) ) )
133 ovex 6310 . . . . . . 7  |-  ( ( x  e.  I  |->  ( k  .x.  ( g `
 x ) ) )  oF  .x.  i )  e.  _V
134133a1i 11 . . . . . 6  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( ( x  e.  I  |->  ( k  .x.  ( g `  x
) ) )  oF  .x.  i )  e.  _V )
135 funmpt 5624 . . . . . . 7  |-  Fun  (
z  e.  I  |->  ( ( ( x  e.  I  |->  ( k  .x.  ( g `  x
) ) ) `  z )  .x.  (
i `  z )
) )
136 eqidd 2468 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  z  e.  I )  ->  (
( x  e.  I  |->  ( k  .x.  (
g `  x )
) ) `  z
)  =  ( ( x  e.  I  |->  ( k  .x.  ( g `
 x ) ) ) `  z ) )
137 eqidd 2468 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  z  e.  I )  ->  (
i `  z )  =  ( i `  z ) )
138113, 117, 77, 77, 55, 136, 137offval 6532 . . . . . . . 8  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( ( x  e.  I  |->  ( k  .x.  ( g `  x
) ) )  oF  .x.  i )  =  ( z  e.  I  |->  ( ( ( x  e.  I  |->  ( k  .x.  ( g `
 x ) ) ) `  z ) 
.x.  ( i `  z ) ) ) )
139138funeqd 5609 . . . . . . 7  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( Fun  ( (
x  e.  I  |->  ( k  .x.  ( g `
 x ) ) )  oF  .x.  i )  <->  Fun  ( z  e.  I  |->  ( ( ( x  e.  I  |->  ( k  .x.  (
g `  x )
) ) `  z
)  .x.  ( i `  z ) ) ) ) )
140135, 139mpbiri 233 . . . . . 6  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  Fun  ( ( x  e.  I  |->  ( k  .x.  ( g `  x
) ) )  oF  .x.  i ) )
141 simp3 998 . . . . . . . . 9  |-  ( ( g  e.  V  /\  h  e.  V  /\  i  e.  V )  ->  i  e.  V )
14213, 141anim12i 566 . . . . . . . 8  |-  ( (
ph  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( I  e.  W  /\  i  e.  V
) )
1431423adant2 1015 . . . . . . 7  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( I  e.  W  /\  i  e.  V
) )
14414, 24, 1frlmbasfsupp 18598 . . . . . . 7  |-  ( ( I  e.  W  /\  i  e.  V )  ->  i finSupp  .0.  )
145143, 144syl 16 . . . . . 6  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
i finSupp  .0.  )
14617, 24rng0cl 17033 . . . . . . . 8  |-  ( R  e.  Ring  ->  .0.  e.  B )
14778, 146syl 16 . . . . . . 7  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  .0.  e.  B )
14817, 20, 24rngrz 17049 . . . . . . . 8  |-  ( ( R  e.  Ring  /\  y  e.  B )  ->  (
y  .x.  .0.  )  =  .0.  )
14978, 148sylan 471 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  y  e.  B )  ->  (
y  .x.  .0.  )  =  .0.  )
15077, 147, 111, 90, 149suppofss2d 6939 . . . . . 6  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( ( ( x  e.  I  |->  ( k 
.x.  ( g `  x ) ) )  oF  .x.  i
) supp  .0.  )  C_  ( i supp  .0.  )
)
151 fsuppsssupp 7846 . . . . . 6  |-  ( ( ( ( ( x  e.  I  |->  ( k 
.x.  ( g `  x ) ) )  oF  .x.  i
)  e.  _V  /\  Fun  ( ( x  e.  I  |->  ( k  .x.  ( g `  x
) ) )  oF  .x.  i ) )  /\  ( i finSupp  .0.  /\  ( ( ( x  e.  I  |->  ( k  .x.  ( g `
 x ) ) )  oF  .x.  i ) supp  .0.  )  C_  ( i supp  .0.  )
) )  ->  (
( x  e.  I  |->  ( k  .x.  (
g `  x )
) )  oF  .x.  i ) finSupp  .0.  )
152134, 140, 145, 150, 151syl22anc 1229 . . . . 5  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( ( x  e.  I  |->  ( k  .x.  ( g `  x
) ) )  oF  .x.  i ) finSupp  .0.  )
153132, 152eqbrtrrd 4469 . . . 4  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( x  e.  I  |->  ( k  .x.  (
( g `  x
)  .x.  ( i `  x ) ) ) ) finSupp  .0.  )
154 simp1 996 . . . . 5  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  ph )
155 eleq1 2539 . . . . . . . . 9  |-  ( g  =  h  ->  (
g  e.  V  <->  h  e.  V ) )
156 id 22 . . . . . . . . . . 11  |-  ( g  =  h  ->  g  =  h )
157156, 156oveq12d 6303 . . . . . . . . . 10  |-  ( g  =  h  ->  (
g  .,  g )  =  ( h  .,  h ) )
158157eqeq1d 2469 . . . . . . . . 9  |-  ( g  =  h  ->  (
( g  .,  g
)  =  .0.  <->  ( h  .,  h )  =  .0.  ) )
159155, 1583anbi23d 1302 . . . . . . . 8  |-  ( g  =  h  ->  (
( ph  /\  g  e.  V  /\  (
g  .,  g )  =  .0.  )  <->  ( ph  /\  h  e.  V  /\  ( h  .,  h )  =  .0.  ) ) )
160 eqeq1 2471 . . . . . . . 8  |-  ( g  =  h  ->  (
g  =  O  <->  h  =  O ) )
161159, 160imbi12d 320 . . . . . . 7  |-  ( g  =  h  ->  (
( ( ph  /\  g  e.  V  /\  ( g  .,  g
)  =  .0.  )  ->  g  =  O )  <-> 
( ( ph  /\  h  e.  V  /\  ( h  .,  h )  =  .0.  )  ->  h  =  O )
) )
162161, 71chvarv 1983 . . . . . 6  |-  ( (
ph  /\  h  e.  V  /\  ( h  .,  h )  =  .0.  )  ->  h  =  O )
16314, 17, 20, 1, 5, 7, 24, 22, 9, 162, 35, 13frlmphllem 18618 . . . . 5  |-  ( (
ph  /\  h  e.  V  /\  i  e.  V
)  ->  ( x  e.  I  |->  ( ( h `  x ) 
.x.  ( i `  x ) ) ) finSupp  .0.  )
164154, 96, 86, 163syl3anc 1228 . . . 4  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( x  e.  I  |->  ( ( h `  x )  .x.  (
i `  x )
) ) finSupp  .0.  )
16517, 24, 75, 76, 77, 95, 101, 102, 103, 153, 164gsummptfsadd 16755 . . 3  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( R  gsumg  ( x  e.  I  |->  ( ( k  .x.  ( ( g `  x )  .x.  (
i `  x )
) ) ( +g  `  R ) ( ( h `  x ) 
.x.  ( i `  x ) ) ) ) )  =  ( ( R  gsumg  ( x  e.  I  |->  ( k  .x.  (
( g `  x
)  .x.  ( i `  x ) ) ) ) ) ( +g  `  R ) ( R 
gsumg  ( x  e.  I  |->  ( ( h `  x )  .x.  (
i `  x )
) ) ) ) )
16614, 17, 20frlmip 18616 . . . . . . . . 9  |-  ( ( I  e.  W  /\  R  e.  DivRing )  -> 
( g  e.  ( B  ^m  I ) ,  h  e.  ( B  ^m  I ) 
|->  ( R  gsumg  ( x  e.  I  |->  ( ( g `  x )  .x.  (
h `  x )
) ) ) )  =  ( .i `  Y ) )
16713, 12, 166syl2anc 661 . . . . . . . 8  |-  ( ph  ->  ( g  e.  ( B  ^m  I ) ,  h  e.  ( B  ^m  I ) 
|->  ( R  gsumg  ( x  e.  I  |->  ( ( g `  x )  .x.  (
h `  x )
) ) ) )  =  ( .i `  Y ) )
168167, 5syl6reqr 2527 . . . . . . 7  |-  ( ph  ->  .,  =  ( g  e.  ( B  ^m  I ) ,  h  e.  ( B  ^m  I
)  |->  ( R  gsumg  ( x  e.  I  |->  ( ( g `  x ) 
.x.  ( h `  x ) ) ) ) ) )
169 fveq1 5865 . . . . . . . . . . 11  |-  ( e  =  g  ->  (
e `  x )  =  ( g `  x ) )
170169oveq1d 6300 . . . . . . . . . 10  |-  ( e  =  g  ->  (
( e `  x
)  .x.  ( f `  x ) )  =  ( ( g `  x )  .x.  (
f `  x )
) )
171170mpteq2dv 4534 . . . . . . . . 9  |-  ( e  =  g  ->  (
x  e.  I  |->  ( ( e `  x
)  .x.  ( f `  x ) ) )  =  ( x  e.  I  |->  ( ( g `
 x )  .x.  ( f `  x
) ) ) )
172171oveq2d 6301 . . . . . . . 8  |-  ( e  =  g  ->  ( R  gsumg  ( x  e.  I  |->  ( ( e `  x )  .x.  (
f `  x )
) ) )  =  ( R  gsumg  ( x  e.  I  |->  ( ( g `  x )  .x.  (
f `  x )
) ) ) )
173 fveq1 5865 . . . . . . . . . . 11  |-  ( f  =  h  ->  (
f `  x )  =  ( h `  x ) )
174173oveq2d 6301 . . . . . . . . . 10  |-  ( f  =  h  ->  (
( g `  x
)  .x.  ( f `  x ) )  =  ( ( g `  x )  .x.  (
h `  x )
) )
175174mpteq2dv 4534 . . . . . . . . 9  |-  ( f  =  h  ->  (
x  e.  I  |->  ( ( g `  x
)  .x.  ( f `  x ) ) )  =  ( x  e.  I  |->  ( ( g `
 x )  .x.  ( h `  x
) ) ) )
176175oveq2d 6301 . . . . . . . 8  |-  ( f  =  h  ->  ( R  gsumg  ( x  e.  I  |->  ( ( g `  x )  .x.  (
f `  x )
) ) )  =  ( R  gsumg  ( x  e.  I  |->  ( ( g `  x )  .x.  (
h `  x )
) ) ) )
177172, 176cbvmpt2v 6362 . . . . . . 7  |-  ( e  e.  ( B  ^m  I ) ,  f  e.  ( B  ^m  I )  |->  ( R 
gsumg  ( x  e.  I  |->  ( ( e `  x )  .x.  (
f `  x )
) ) ) )  =  ( g  e.  ( B  ^m  I
) ,  h  e.  ( B  ^m  I
)  |->  ( R  gsumg  ( x  e.  I  |->  ( ( g `  x ) 
.x.  ( h `  x ) ) ) ) )
178168, 177syl6eqr 2526 . . . . . 6  |-  ( ph  ->  .,  =  ( e  e.  ( B  ^m  I ) ,  f  e.  ( B  ^m  I )  |->  ( R 
gsumg  ( x  e.  I  |->  ( ( e `  x )  .x.  (
f `  x )
) ) ) ) )
1791783ad2ant1 1017 . . . . 5  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  .,  =  ( e  e.  ( B  ^m  I
) ,  f  e.  ( B  ^m  I
)  |->  ( R  gsumg  ( x  e.  I  |->  ( ( e `  x ) 
.x.  ( f `  x ) ) ) ) ) )
180 simprl 755 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  ( ( k ( .s `  Y
) g ) ( +g  `  Y ) h )  /\  f  =  i ) )  ->  e  =  ( ( k ( .s
`  Y ) g ) ( +g  `  Y
) h ) )
181180fveq1d 5868 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  ( ( k ( .s `  Y
) g ) ( +g  `  Y ) h )  /\  f  =  i ) )  ->  ( e `  x )  =  ( ( ( k ( .s `  Y ) g ) ( +g  `  Y ) h ) `
 x ) )
182 simprr 756 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  ( ( k ( .s `  Y
) g ) ( +g  `  Y ) h )  /\  f  =  i ) )  ->  f  =  i )
183182fveq1d 5868 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  ( ( k ( .s `  Y
) g ) ( +g  `  Y ) h )  /\  f  =  i ) )  ->  ( f `  x )  =  ( i `  x ) )
184181, 183oveq12d 6303 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  ( ( k ( .s `  Y
) g ) ( +g  `  Y ) h )  /\  f  =  i ) )  ->  ( ( e `
 x )  .x.  ( f `  x
) )  =  ( ( ( ( k ( .s `  Y
) g ) ( +g  `  Y ) h ) `  x
)  .x.  ( i `  x ) ) )
185184mpteq2dv 4534 . . . . . 6  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  ( ( k ( .s `  Y
) g ) ( +g  `  Y ) h )  /\  f  =  i ) )  ->  ( x  e.  I  |->  ( ( e `
 x )  .x.  ( f `  x
) ) )  =  ( x  e.  I  |->  ( ( ( ( k ( .s `  Y ) g ) ( +g  `  Y
) h ) `  x )  .x.  (
i `  x )
) ) )
186185oveq2d 6301 . . . . 5  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  ( ( k ( .s `  Y
) g ) ( +g  `  Y ) h )  /\  f  =  i ) )  ->  ( R  gsumg  ( x  e.  I  |->  ( ( e `  x ) 
.x.  ( f `  x ) ) ) )  =  ( R 
gsumg  ( x  e.  I  |->  ( ( ( ( k ( .s `  Y ) g ) ( +g  `  Y
) h ) `  x )  .x.  (
i `  x )
) ) ) )
187293ad2ant1 1017 . . . . . . 7  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  Y  e.  LMod )
188163ad2ant1 1017 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  R  =  (Scalar `  Y
) )
189188fveq2d 5870 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( Base `  R )  =  ( Base `  (Scalar `  Y ) ) )
19017, 189syl5eq 2520 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  B  =  ( Base `  (Scalar `  Y )
) )
19180, 190eleqtrd 2557 . . . . . . . 8  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
k  e.  ( Base `  (Scalar `  Y )
) )
192 eqid 2467 . . . . . . . . 9  |-  ( .s
`  Y )  =  ( .s `  Y
)
193 eqid 2467 . . . . . . . . 9  |-  ( Base `  (Scalar `  Y )
)  =  ( Base `  (Scalar `  Y )
)
1941, 31, 192, 193lmodvscl 17341 . . . . . . . 8  |-  ( ( Y  e.  LMod  /\  k  e.  ( Base `  (Scalar `  Y ) )  /\  g  e.  V )  ->  ( k ( .s
`  Y ) g )  e.  V )
195187, 191, 82, 194syl3anc 1228 . . . . . . 7  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( k ( .s
`  Y ) g )  e.  V )
196 eqid 2467 . . . . . . . 8  |-  ( +g  `  Y )  =  ( +g  `  Y )
1971, 196lmodvacl 17338 . . . . . . 7  |-  ( ( Y  e.  LMod  /\  (
k ( .s `  Y ) g )  e.  V  /\  h  e.  V )  ->  (
( k ( .s
`  Y ) g ) ( +g  `  Y
) h )  e.  V )
198187, 195, 96, 197syl3anc 1228 . . . . . 6  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( ( k ( .s `  Y ) g ) ( +g  `  Y ) h )  e.  V )
19914, 17, 1frlmbasmap 18600 . . . . . 6  |-  ( ( I  e.  W  /\  ( ( k ( .s `  Y ) g ) ( +g  `  Y ) h )  e.  V )  -> 
( ( k ( .s `  Y ) g ) ( +g  `  Y ) h )  e.  ( B  ^m  I ) )
20077, 198, 199syl2anc 661 . . . . 5  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( ( k ( .s `  Y ) g ) ( +g  `  Y ) h )  e.  ( B  ^m  I ) )
201 ovex 6310 . . . . . 6  |-  ( R 
gsumg  ( x  e.  I  |->  ( ( ( ( k ( .s `  Y ) g ) ( +g  `  Y
) h ) `  x )  .x.  (
i `  x )
) ) )  e. 
_V
202201a1i 11 . . . . 5  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( R  gsumg  ( x  e.  I  |->  ( ( ( ( k ( .s `  Y ) g ) ( +g  `  Y
) h ) `  x )  .x.  (
i `  x )
) ) )  e. 
_V )
203179, 186, 200, 88, 202ovmpt2d 6415 . . . 4  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( ( ( k ( .s `  Y
) g ) ( +g  `  Y ) h )  .,  i
)  =  ( R 
gsumg  ( x  e.  I  |->  ( ( ( ( k ( .s `  Y ) g ) ( +g  `  Y
) h ) `  x )  .x.  (
i `  x )
) ) ) )
20414, 1, 78, 77, 195, 96, 75, 196frlmplusgval 18604 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( ( k ( .s `  Y ) g ) ( +g  `  Y ) h )  =  ( ( k ( .s `  Y
) g )  oF ( +g  `  R
) h ) )
20514, 17, 1frlmbasmap 18600 . . . . . . . . . . . . 13  |-  ( ( I  e.  W  /\  ( k ( .s
`  Y ) g )  e.  V )  ->  ( k ( .s `  Y ) g )  e.  ( B  ^m  I ) )
20677, 195, 205syl2anc 661 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( k ( .s
`  Y ) g )  e.  ( B  ^m  I ) )
207 elmapi 7441 . . . . . . . . . . . 12  |-  ( ( k ( .s `  Y ) g )  e.  ( B  ^m  I )  ->  (
k ( .s `  Y ) g ) : I --> B )
208 ffn 5731 . . . . . . . . . . . 12  |-  ( ( k ( .s `  Y ) g ) : I --> B  -> 
( k ( .s
`  Y ) g )  Fn  I )
209206, 207, 2083syl 20 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( k ( .s
`  Y ) g )  Fn  I )
21098, 53syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  h  Fn  I )
21177adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  I  e.  W )
21282adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  g  e.  V )
21314, 1, 17, 211, 81, 212, 122, 192, 20frlmvscaval 18607 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
( k ( .s
`  Y ) g ) `  x )  =  ( k  .x.  ( g `  x
) ) )
214 eqidd 2468 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
h `  x )  =  ( h `  x ) )
215209, 210, 77, 77, 55, 213, 214offval 6532 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( ( k ( .s `  Y ) g )  oF ( +g  `  R
) h )  =  ( x  e.  I  |->  ( ( k  .x.  ( g `  x
) ) ( +g  `  R ) ( h `
 x ) ) ) )
216204, 215eqtrd 2508 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( ( k ( .s `  Y ) g ) ( +g  `  Y ) h )  =  ( x  e.  I  |->  ( ( k 
.x.  ( g `  x ) ) ( +g  `  R ) ( h `  x
) ) ) )
217 ovex 6310 . . . . . . . . . 10  |-  ( ( k  .x.  ( g `
 x ) ) ( +g  `  R
) ( h `  x ) )  e. 
_V
218217a1i 11 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
( k  .x.  (
g `  x )
) ( +g  `  R
) ( h `  x ) )  e. 
_V )
219216, 218fvmpt2d 5960 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
( ( k ( .s `  Y ) g ) ( +g  `  Y ) h ) `
 x )  =  ( ( k  .x.  ( g `  x
) ) ( +g  `  R ) ( h `
 x ) ) )
220219oveq1d 6300 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
( ( ( k ( .s `  Y
) g ) ( +g  `  Y ) h ) `  x
)  .x.  ( i `  x ) )  =  ( ( ( k 
.x.  ( g `  x ) ) ( +g  `  R ) ( h `  x
) )  .x.  (
i `  x )
) )
22117, 75, 20rngdir 17031 . . . . . . . 8  |-  ( ( R  e.  Ring  /\  (
( k  .x.  (
g `  x )
)  e.  B  /\  ( h `  x
)  e.  B  /\  ( i `  x
)  e.  B ) )  ->  ( (
( k  .x.  (
g `  x )
) ( +g  `  R
) ( h `  x ) )  .x.  ( i `  x
) )  =  ( ( ( k  .x.  ( g `  x
) )  .x.  (
i `  x )
) ( +g  `  R
) ( ( h `
 x )  .x.  ( i `  x
) ) ) )
22279, 109, 99, 91, 221syl13anc 1230 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
( ( k  .x.  ( g `  x
) ) ( +g  `  R ) ( h `
 x ) ) 
.x.  ( i `  x ) )  =  ( ( ( k 
.x.  ( g `  x ) )  .x.  ( i `  x
) ) ( +g  `  R ) ( ( h `  x ) 
.x.  ( i `  x ) ) ) )
223129oveq1d 6300 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
( ( k  .x.  ( g `  x
) )  .x.  (
i `  x )
) ( +g  `  R
) ( ( h `
 x )  .x.  ( i `  x
) ) )  =  ( ( k  .x.  ( ( g `  x )  .x.  (
i `  x )
) ) ( +g  `  R ) ( ( h `  x ) 
.x.  ( i `  x ) ) ) )
224220, 222, 2233eqtrd 2512 . . . . . 6  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
( ( ( k ( .s `  Y
) g ) ( +g  `  Y ) h ) `  x
)  .x.  ( i `  x ) )  =  ( ( k  .x.  ( ( g `  x )  .x.  (
i `  x )
) ) ( +g  `  R ) ( ( h `  x ) 
.x.  ( i `  x ) ) ) )
225224mpteq2dva 4533 . . . . 5  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( x  e.  I  |->  ( ( ( ( k ( .s `  Y ) g ) ( +g  `  Y
) h ) `  x )  .x.  (
i `  x )
) )  =  ( x  e.  I  |->  ( ( k  .x.  (
( g `  x
)  .x.  ( i `  x ) ) ) ( +g  `  R
) ( ( h `
 x )  .x.  ( i `  x
) ) ) ) )
226225oveq2d 6301 . . . 4  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( R  gsumg  ( x  e.  I  |->  ( ( ( ( k ( .s `  Y ) g ) ( +g  `  Y
) h ) `  x )  .x.  (
i `  x )
) ) )  =  ( R  gsumg  ( x  e.  I  |->  ( ( k  .x.  ( ( g `  x )  .x.  (
i `  x )
) ) ( +g  `  R ) ( ( h `  x ) 
.x.  ( i `  x ) ) ) ) ) )
227203, 226eqtrd 2508 . . 3  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( ( ( k ( .s `  Y
) g ) ( +g  `  Y ) h )  .,  i
)  =  ( R 
gsumg  ( x  e.  I  |->  ( ( k  .x.  ( ( g `  x )  .x.  (
i `  x )
) ) ( +g  `  R ) ( ( h `  x ) 
.x.  ( i `  x ) ) ) ) ) )
228 simprl 755 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  g  /\  f  =  i ) )  ->  e  =  g )
229228fveq1d 5868 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  g  /\  f  =  i ) )  ->  ( e `  x )  =  ( g `  x ) )
230 simprr 756 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  g  /\  f  =  i ) )  ->  f  =  i )
231230fveq1d 5868 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  g  /\  f  =  i ) )  ->  ( f `  x )  =  ( i `  x ) )
232229, 231oveq12d 6303 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  g  /\  f  =  i ) )  ->  ( ( e `
 x )  .x.  ( f `  x
) )  =  ( ( g `  x
)  .x.  ( i `  x ) ) )
233232mpteq2dv 4534 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  g  /\  f  =  i ) )  ->  ( x  e.  I  |->  ( ( e `
 x )  .x.  ( f `  x
) ) )  =  ( x  e.  I  |->  ( ( g `  x )  .x.  (
i `  x )
) ) )
234233oveq2d 6301 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  g  /\  f  =  i ) )  ->  ( R  gsumg  ( x  e.  I  |->  ( ( e `  x ) 
.x.  ( f `  x ) ) ) )  =  ( R 
gsumg  ( x  e.  I  |->  ( ( g `  x )  .x.  (
i `  x )
) ) ) )
235 ovex 6310 . . . . . . . 8  |-  ( R 
gsumg  ( x  e.  I  |->  ( ( g `  x )  .x.  (
i `  x )
) ) )  e. 
_V
236235a1i 11 . . . . . . 7  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( R  gsumg  ( x  e.  I  |->  ( ( g `  x )  .x.  (
i `  x )
) ) )  e. 
_V )
237179, 234, 83, 88, 236ovmpt2d 6415 . . . . . 6  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( g  .,  i
)  =  ( R 
gsumg  ( x  e.  I  |->  ( ( g `  x )  .x.  (
i `  x )
) ) ) )
238237oveq2d 6301 . . . . 5  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( k  .x.  (
g  .,  i )
)  =  ( k 
.x.  ( R  gsumg  ( x  e.  I  |->  ( ( g `  x ) 
.x.  ( i `  x ) ) ) ) ) )
23914, 17, 20, 1, 5, 7, 24, 22, 9, 71, 35, 13frlmphllem 18618 . . . . . . 7  |-  ( (
ph  /\  g  e.  V  /\  i  e.  V
)  ->  ( x  e.  I  |->  ( ( g `  x ) 
.x.  ( i `  x ) ) ) finSupp  .0.  )
240154, 82, 86, 239syl3anc 1228 . . . . . 6  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( x  e.  I  |->  ( ( g `  x )  .x.  (
i `  x )
) ) finSupp  .0.  )
24117, 24, 75, 20, 78, 77, 80, 93, 240gsummulc2 17066 . . . . 5  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( R  gsumg  ( x  e.  I  |->  ( k  .x.  (
( g `  x
)  .x.  ( i `  x ) ) ) ) )  =  ( k  .x.  ( R 
gsumg  ( x  e.  I  |->  ( ( g `  x )  .x.  (
i `  x )
) ) ) ) )
242238, 241eqtr4d 2511 . . . 4  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( k  .x.  (
g  .,  i )
)  =  ( R 
gsumg  ( x  e.  I  |->  ( k  .x.  (
( g `  x
)  .x.  ( i `  x ) ) ) ) ) )
243 simprl 755 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  h  /\  f  =  i ) )  ->  e  =  h )
244243fveq1d 5868 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  h  /\  f  =  i ) )  ->  ( e `  x )  =  ( h `  x ) )
245 simprr 756 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  h  /\  f  =  i ) )  ->  f  =  i )
246245fveq1d 5868 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  h  /\  f  =  i ) )  ->  ( f `  x )  =  ( i `  x ) )
247244, 246oveq12d 6303 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  h  /\  f  =  i ) )  ->  ( ( e `
 x )  .x.  ( f `  x
) )  =  ( ( h `  x
)  .x.  ( i `  x ) ) )
248247mpteq2dv 4534 . . . . . 6  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  h  /\  f  =  i ) )  ->  ( x  e.  I  |->  ( ( e `
 x )  .x.  ( f `  x
) ) )  =  ( x  e.  I  |->  ( ( h `  x )  .x.  (
i `  x )
) ) )
249248oveq2d 6301 . . . . 5  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  h  /\  f  =  i ) )  ->  ( R  gsumg  ( x  e.  I  |->  ( ( e `  x ) 
.x.  ( f `  x ) ) ) )  =  ( R 
gsumg  ( x  e.  I  |->  ( ( h `  x )  .x.  (
i `  x )
) ) ) )
250 ovex 6310 . . . . . 6  |-  ( R 
gsumg  ( x  e.  I  |->  ( ( h `  x )  .x.  (
i `  x )
) ) )  e. 
_V
251250a1i 11 . . . . 5  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( R  gsumg  ( x  e.  I  |->  ( ( h `  x )  .x.  (
i `  x )
) ) )  e. 
_V )
252179, 249, 97, 88, 251ovmpt2d 6415 . . . 4  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( h  .,  i
)  =  ( R 
gsumg  ( x  e.  I  |->  ( ( h `  x )  .x.  (
i `  x )
) ) ) )
253242, 252oveq12d 6303 . . 3  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( ( k  .x.  ( g  .,  i
) ) ( +g  `  R ) ( h 
.,  i ) )  =  ( ( R 
gsumg  ( x  e.  I  |->  ( k  .x.  (
( g `  x
)  .x.  ( i `  x ) ) ) ) ) ( +g  `  R ) ( R 
gsumg  ( x  e.  I  |->  ( ( h `  x )  .x.  (
i `  x )
) ) ) ) )
254165, 227, 2533eqtr4d 2518 . 2  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( ( ( k ( .s `  Y
) g ) ( +g  `  Y ) h )  .,  i
)  =  ( ( k  .x.  ( g 
.,  i ) ) ( +g  `  R
) ( h  .,  i ) ) )
255343ad2ant1 1017 . . . . . . 7  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  R  e.  CRing
)
256255adantr 465 . . . . . 6  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  x  e.  I )  ->  R  e.  CRing )
25717, 20crngcom 17026 . . . . . 6  |-  ( ( R  e.  CRing  /\  (
h `  x )  e.  B  /\  (
g `  x )  e.  B )  ->  (
( h `  x
)  .x.  ( g `  x ) )  =  ( ( g `  x )  .x.  (
h `  x )
) )
258256, 66, 65, 257syl3anc 1228 . . . . 5  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  x  e.  I )  ->  (
( h `  x
)  .x.  ( g `  x ) )  =  ( ( g `  x )  .x.  (
h `  x )
) )
259258mpteq2dva 4533 . . . 4  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( x  e.  I  |->  ( ( h `  x ) 
.x.  ( g `  x ) ) )  =  ( x  e.  I  |->  ( ( g `
 x )  .x.  ( h `  x
) ) ) )
260259oveq2d 6301 . . 3  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( R  gsumg  ( x  e.  I  |->  ( ( h `  x
)  .x.  ( g `  x ) ) ) )  =  ( R 
gsumg  ( x  e.  I  |->  ( ( g `  x )  .x.  (
h `  x )
) ) ) )
2611783ad2ant1 1017 . . . 4  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  .,  =  ( e  e.  ( B  ^m  I ) ,  f  e.  ( B  ^m  I )  |->  ( R  gsumg  ( x  e.  I  |->  ( ( e `  x )  .x.  (
f `  x )
) ) ) ) )
262 simprl 755 . . . . . . . 8  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  (
e  =  h  /\  f  =  g )
)  ->  e  =  h )
263262fveq1d 5868 . . . . . . 7  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  (
e  =  h  /\  f  =  g )
)  ->  ( e `  x )  =  ( h `  x ) )
264 simprr 756 . . . . . . . 8  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  (
e  =  h  /\  f  =  g )
)  ->  f  =  g )
265264fveq1d 5868 . . . . . . 7  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  (
e  =  h  /\  f  =  g )
)  ->  ( f `  x )  =  ( g `  x ) )
266263, 265oveq12d 6303 . . . . . 6  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  (
e  =  h  /\  f  =  g )
)  ->  ( (
e `  x )  .x.  ( f `  x
) )  =  ( ( h `  x
)  .x.  ( g `  x ) ) )
267266mpteq2dv 4534 . . . . 5  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  (
e  =  h  /\  f  =  g )
)  ->  ( x  e.  I  |->  ( ( e `  x ) 
.x.  ( f `  x ) ) )  =  ( x  e.  I  |->  ( ( h `
 x )  .x.  ( g `  x
) ) ) )
268267oveq2d 6301 . . . 4  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  (
e  =  h  /\  f  =  g )
)  ->  ( R  gsumg  ( x  e.  I  |->  ( ( e `  x
)  .x.  ( f `  x ) ) ) )  =  ( R 
gsumg  ( x  e.  I  |->  ( ( h `  x )  .x.  (
g `  x )
) ) ) )
269 ovex 6310 . . . . 5  |-  ( R 
gsumg  ( x  e.  I  |->  ( ( h `  x )  .x.  (
g `  x )
) ) )  e. 
_V
270269a1i 11 . . . 4  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( R  gsumg  ( x  e.  I  |->  ( ( h `  x
)  .x.  ( g `  x ) ) ) )  e.  _V )
271261, 268, 50, 44, 270ovmpt2d 6415 . . 3  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( h  .,  g )  =  ( R  gsumg  ( x  e.  I  |->  ( ( h `  x )  .x.  (
g `  x )
) ) ) )
27235ralrimiva 2878 . . . . . 6  |-  ( ph  ->  A. x  e.  B  (  .*  `  x )  =  x )
2732723ad2ant1 1017 . . . . 5  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  A. x  e.  B  (  .*  `  x )  =  x )
274 fveq2 5866 . . . . . . 7  |-  ( x  =  ( g  .,  h )  ->  (  .*  `  x )  =  (  .*  `  (
g  .,  h )
) )
275 id 22 . . . . . . 7  |-  ( x  =  ( g  .,  h )  ->  x  =  ( g  .,  h ) )
276274, 275eqeq12d 2489 . . . . . 6  |-  ( x  =  ( g  .,  h )  ->  (
(  .*  `  x
)  =  x  <->  (  .*  `  ( g  .,  h
) )  =  ( g  .,  h ) ) )
277276rspcv 3210 . . . . 5  |-  ( ( g  .,  h )  e.  B  ->  ( A. x  e.  B  (  .*  `  x )  =  x  ->  (  .*  `  ( g  .,  h ) )  =  ( g  .,  h
) ) )
27874, 273, 277sylc 60 . . . 4  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  (  .*  `  ( g  .,  h
) )  =  ( g  .,  h ) )
279278, 60eqtrd 2508 . . 3  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  (  .*  `  ( g  .,  h
) )  =  ( R  gsumg  ( x  e.  I  |->  ( ( g `  x )  .x.  (
h `  x )
) ) ) )
280260, 271, 2793eqtr4rd 2519 . 2  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  (  .*  `  ( g  .,  h
) )  =  ( h  .,  g ) )
2812, 3, 4, 6, 8, 16, 18, 19, 21, 23, 25, 33, 36, 74, 254, 71, 280isphld 18496 1  |-  ( ph  ->  Y  e.  PreHil )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973    = wceq 1379    e. wcel 1767   A.wral 2814   _Vcvv 3113    C_ wss 3476   class class class wbr 4447    |-> cmpt 4505   Fun wfun 5582    Fn wfn 5583   -->wf 5584   ` cfv 5588  (class class class)co 6285    |-> cmpt2 6287    oFcof 6523   supp csupp 6902    ^m cmap 7421   finSupp cfsupp 7830   Basecbs 14493   +g cplusg 14558   .rcmulr 14559   *rcstv 14560  Scalarcsca 14561   .scvsca 14562   .icip 14563   0gc0g 14698    gsumg cgsu 14699  CMndccmn 16613   Ringcrg 17012   CRingccrg 17013   DivRingcdr 17208  Fieldcfield 17209   LModclmod 17324   LVecclvec 17560   PreHilcphl 18466   freeLMod cfrlm 18584
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6577  ax-cnex 9549  ax-resscn 9550  ax-1cn 9551  ax-icn 9552  ax-addcl 9553  ax-addrcl 9554  ax-mulcl 9555  ax-mulrcl 9556  ax-mulcom 9557  ax-addass 9558  ax-mulass 9559  ax-distr 9560  ax-i2m1 9561  ax-1ne0 9562  ax-1rid 9563  ax-rnegex 9564  ax-rrecex 9565  ax-cnre 9566  ax-pre-lttri 9567  ax-pre-lttrn 9568  ax-pre-ltadd 9569  ax-pre-mulgt0 9570
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-isom 5597  df-riota 6246  df-ov 6288  df-oprab 6289  df-mpt2 6290  df-of 6525  df-om 6686  df-1st 6785  df-2nd 6786  df-supp 6903  df-tpos 6956  df-recs 7043  df-rdg 7077  df-1o 7131  df-oadd 7135  df-er 7312  df-map 7423  df-ixp 7471  df-en 7518  df-dom 7519  df-sdom 7520  df-fin 7521  df-fsupp 7831  df-sup 7902  df-oi 7936  df-card 8321  df-pnf 9631  df-mnf 9632  df-xr 9633  df-ltxr 9634  df-le 9635  df-sub 9808  df-neg 9809  df-nn 10538  df-2 10595  df-3 10596  df-4 10597  df-5 10598  df-6 10599  df-7 10600  df-8 10601  df-9 10602  df-10 10603  df-n0 10797  df-z 10866  df-dec 10978  df-uz 11084  df-fz 11674  df-fzo 11794  df-seq 12077  df-hash 12375  df-struct 14495  df-ndx 14496  df-slot 14497  df-base 14498  df-sets 14499  df-ress 14500  df-plusg 14571  df-mulr 14572  df-sca 14574  df-vsca 14575  df-ip 14576  df-tset 14577  df-ple 14578  df-ds 14580  df-hom 14582  df-cco 14583  df-0g 14700  df-gsum 14701  df-prds 14706  df-pws 14708  df-mnd 15735  df-mhm 15789  df-submnd 15790  df-grp 15871  df-minusg 15872  df-sbg 15873  df-subg 16012  df-ghm 16079  df-cntz 16169  df-cmn 16615  df-abl 16616  df-mgp 16956  df-ur 16968  df-rng 17014  df-cring 17015  df-oppr 17085  df-rnghom 17177  df-drng 17210  df-field 17211  df-subrg 17239  df-staf 17306  df-srng 17307  df-lmod 17326  df-lss 17391  df-lmhm 17480  df-lvec 17561  df-sra 17630  df-rgmod 17631  df-phl 18468  df-dsmm 18570  df-frlm 18585
This theorem is referenced by:  rrxcph  21651
  Copyright terms: Public domain W3C validator