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

Theorem frlmphl 18175
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 2438 . 2  |-  ( ph  ->  ( +g  `  Y
)  =  ( +g  `  Y ) )
4 eqidd 2438 . 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 16817 . . . . 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 18147 . . 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 2438 . 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 16815 . . . . 5  |-  ( R  e.  DivRing  ->  R  e.  Ring )
2712, 26syl 16 . . . 4  |-  ( ph  ->  R  e.  Ring )
2814frlmlmod 18143 . . . 4  |-  ( ( R  e.  Ring  /\  I  e.  W )  ->  Y  e.  LMod )
2927, 13, 28syl2anc 661 . . 3  |-  ( ph  ->  Y  e.  LMod )
3016, 12eqeltrrd 2512 . . 3  |-  ( ph  ->  (Scalar `  Y )  e.  DivRing )
31 eqid 2437 . . . 4  |-  (Scalar `  Y )  =  (Scalar `  Y )
3231islvec 17159 . . 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 16923 . 2  |-  ( ph  ->  R  e.  *Ring )
37133ad2ant1 1009 . . . . 5  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  I  e.  W )
38273ad2ant1 1009 . . . . 5  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  R  e.  Ring )
39 simp2 989 . . . . 5  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  g  e.  V )
40 simp3 990 . . . . 5  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  h  e.  V )
4114, 17, 20, 1, 5frlmipval 18173 . . . . 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 1219 . . . 4  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( g  .,  h )  =  ( R  gsumg  ( g  oF  .x.  h ) ) )
4314, 17, 1frlmbasmap 18156 . . . . . . . . 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 7226 . . . . . . . 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 5552 . . . . . . 7  |-  ( g : I --> B  -> 
g  Fn  I )
4846, 47syl 16 . . . . . 6  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  g  Fn  I )
4914, 17, 1frlmbasmap 18156 . . . . . . . . 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 7226 . . . . . . . 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 5552 . . . . . . 7  |-  ( h : I --> B  ->  h  Fn  I )
5452, 53syl 16 . . . . . 6  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  h  Fn  I )
55 inidm 3552 . . . . . 6  |-  ( I  i^i  I )  =  I
56 eqidd 2438 . . . . . 6  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  x  e.  I )  ->  (
g `  x )  =  ( g `  x ) )
57 eqidd 2438 . . . . . 6  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  x  e.  I )  ->  (
h `  x )  =  ( h `  x ) )
5848, 54, 37, 37, 55, 56, 57offval 6322 . . . . 5  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( g  oF  .x.  h )  =  ( x  e.  I  |->  ( ( g `
 x )  .x.  ( h `  x
) ) ) )
5958oveq2d 6102 . . . 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 2469 . . 3  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( g  .,  h )  =  ( R  gsumg  ( x  e.  I  |->  ( ( g `  x )  .x.  (
h `  x )
) ) ) )
61 rngcmn 16661 . . . . . 6  |-  ( R  e.  Ring  ->  R  e. CMnd
)
6227, 61syl 16 . . . . 5  |-  ( ph  ->  R  e. CMnd )
63623ad2ant1 1009 . . . 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 5836 . . . . . 6  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  x  e.  I )  ->  (
g `  x )  e.  B )
6652ffvelrnda 5836 . . . . . 6  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  x  e.  I )  ->  (
h `  x )  e.  B )
6717, 20rngcl 16644 . . . . . 6  |-  ( ( R  e.  Ring  /\  (
g `  x )  e.  B  /\  (
h `  x )  e.  B )  ->  (
( g `  x
)  .x.  ( h `  x ) )  e.  B )
6864, 65, 66, 67syl3anc 1218 . . . . 5  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  x  e.  I )  ->  (
( g `  x
)  .x.  ( h `  x ) )  e.  B )
69 eqid 2437 . . . . 5  |-  ( x  e.  I  |->  ( ( g `  x ) 
.x.  ( h `  x ) ) )  =  ( x  e.  I  |->  ( ( g `
 x )  .x.  ( h `  x
) ) )
7068, 69fmptd 5860 . . . 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 18174 . . . 4  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( x  e.  I  |->  ( ( g `  x ) 
.x.  ( h `  x ) ) ) finSupp  .0.  )
7317, 24, 63, 37, 70, 72gsumcl 16386 . . 3  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( R  gsumg  ( x  e.  I  |->  ( ( g `  x
)  .x.  ( h `  x ) ) ) )  e.  B )
7460, 73eqeltrd 2511 . 2  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( g  .,  h )  e.  B
)
75 eqid 2437 . . . 4  |-  ( +g  `  R )  =  ( +g  `  R )
76623ad2ant1 1009 . . . 4  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  R  e. CMnd )
77133ad2ant1 1009 . . . 4  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  I  e.  W )
78273ad2ant1 1009 . . . . . 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 989 . . . . . 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 1024 . . . . . . . . 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 5836 . . . . . 6  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
g `  x )  e.  B )
86 simp33 1026 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
i  e.  V )
8714, 17, 1frlmbasmap 18156 . . . . . . . . 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 7226 . . . . . . . 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 5836 . . . . . 6  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
i `  x )  e.  B )
9217, 20rngcl 16644 . . . . . 6  |-  ( ( R  e.  Ring  /\  (
g `  x )  e.  B  /\  (
i `  x )  e.  B )  ->  (
( g `  x
)  .x.  ( i `  x ) )  e.  B )
9379, 85, 91, 92syl3anc 1218 . . . . 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 16644 . . . . 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 1218 . . . 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 1025 . . . . . . . 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 5836 . . . . 5  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
h `  x )  e.  B )
10017, 20rngcl 16644 . . . . 5  |-  ( ( R  e.  Ring  /\  (
h `  x )  e.  B  /\  (
i `  x )  e.  B )  ->  (
( h `  x
)  .x.  ( i `  x ) )  e.  B )
10179, 99, 91, 100syl3anc 1218 . . . 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 2438 . . . 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 2438 . . . 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 5684 . . . . . . . . 9  |-  ( x  =  y  ->  (
g `  x )  =  ( g `  y ) )
105104oveq2d 6102 . . . . . . . 8  |-  ( x  =  y  ->  (
k  .x.  ( g `  x ) )  =  ( k  .x.  (
g `  y )
) )
106105cbvmptv 4376 . . . . . . 7  |-  ( x  e.  I  |->  ( k 
.x.  ( g `  x ) ) )  =  ( y  e.  I  |->  ( k  .x.  ( g `  y
) ) )
107106oveq1i 6096 . . . . . 6  |-  ( ( x  e.  I  |->  ( k  .x.  ( g `
 x ) ) )  oF  .x.  i )  =  ( ( y  e.  I  |->  ( k  .x.  (
g `  y )
) )  oF  .x.  i )
10817, 20rngcl 16644 . . . . . . . . . . . 12  |-  ( ( R  e.  Ring  /\  k  e.  B  /\  (
g `  x )  e.  B )  ->  (
k  .x.  ( g `  x ) )  e.  B )
10979, 81, 85, 108syl3anc 1218 . . . . . . . . . . 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 2437 . . . . . . . . . . 11  |-  ( x  e.  I  |->  ( k 
.x.  ( g `  x ) ) )  =  ( x  e.  I  |->  ( k  .x.  ( g `  x
) ) )
111109, 110fmptd 5860 . . . . . . . . . 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 5552 . . . . . . . . . 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 5498 . . . . . . . . 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 5552 . . . . . . . . 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 2438 . . . . . . . . 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 5688 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V
) )  /\  x  e.  I )  /\  y  =  x )  ->  (
g `  y )  =  ( g `  x ) )
121120oveq2d 6102 . . . . . . . . 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 6111 . . . . . . . . . 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 5772 . . . . . . . 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 2438 . . . . . . . 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 6322 . . . . . . 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 16647 . . . . . . . . 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 1220 . . . . . . . 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 4371 . . . . . . 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 2469 . . . . . 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 2481 . . . . 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 6111 . . . . . . 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 5447 . . . . . . 7  |-  Fun  (
z  e.  I  |->  ( ( ( x  e.  I  |->  ( k  .x.  ( g `  x
) ) ) `  z )  .x.  (
i `  z )
) )
136 eqidd 2438 . . . . . . . . 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 2438 . . . . . . . . 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 6322 . . . . . . . 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 5432 . . . . . . 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 990 . . . . . . . . 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 1007 . . . . . . 7  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( I  e.  W  /\  i  e.  V
) )
14414, 24, 1frlmbasfsupp 18154 . . . . . . 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 16652 . . . . . . . 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 16668 . . . . . . . 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 6722 . . . . . 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 7628 . . . . . 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 1219 . . . . 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 4307 . . . 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 988 . . . . 5  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  ph )
155 eleq1 2497 . . . . . . . . 9  |-  ( g  =  h  ->  (
g  e.  V  <->  h  e.  V ) )
156 id 22 . . . . . . . . . . 11  |-  ( g  =  h  ->  g  =  h )
157156, 156oveq12d 6104 . . . . . . . . . 10  |-  ( g  =  h  ->  (
g  .,  g )  =  ( h  .,  h ) )
158157eqeq1d 2445 . . . . . . . . 9  |-  ( g  =  h  ->  (
( g  .,  g
)  =  .0.  <->  ( h  .,  h )  =  .0.  ) )
159155, 1583anbi23d 1292 . . . . . . . 8  |-  ( g  =  h  ->  (
( ph  /\  g  e.  V  /\  (
g  .,  g )  =  .0.  )  <->  ( ph  /\  h  e.  V  /\  ( h  .,  h )  =  .0.  ) ) )
160 eqeq1 2443 . . . . . . . 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 1958 . . . . . 6  |-  ( (
ph  /\  h  e.  V  /\  ( h  .,  h )  =  .0.  )  ->  h  =  O )
16314, 17, 20, 1, 5, 7, 24, 22, 9, 162, 35, 13frlmphllem 18174 . . . . 5  |-  ( (
ph  /\  h  e.  V  /\  i  e.  V
)  ->  ( x  e.  I  |->  ( ( h `  x ) 
.x.  ( i `  x ) ) ) finSupp  .0.  )
164154, 96, 86, 163syl3anc 1218 . . . 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 16403 . . 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 18172 . . . . . . . . 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 2488 . . . . . . 7  |-  ( ph  ->  .,  =  ( g  e.  ( B  ^m  I ) ,  h  e.  ( B  ^m  I
)  |->  ( R  gsumg  ( x  e.  I  |->  ( ( g `  x ) 
.x.  ( h `  x ) ) ) ) ) )
169 fveq1 5683 . . . . . . . . . . 11  |-  ( e  =  g  ->  (
e `  x )  =  ( g `  x ) )
170169oveq1d 6101 . . . . . . . . . 10  |-  ( e  =  g  ->  (
( e `  x
)  .x.  ( f `  x ) )  =  ( ( g `  x )  .x.  (
f `  x )
) )
171170mpteq2dv 4372 . . . . . . . . 9  |-  ( e  =  g  ->  (
x  e.  I  |->  ( ( e `  x
)  .x.  ( f `  x ) ) )  =  ( x  e.  I  |->  ( ( g `
 x )  .x.  ( f `  x
) ) ) )
172171oveq2d 6102 . . . . . . . 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 5683 . . . . . . . . . . 11  |-  ( f  =  h  ->  (
f `  x )  =  ( h `  x ) )
174173oveq2d 6102 . . . . . . . . . 10  |-  ( f  =  h  ->  (
( g `  x
)  .x.  ( f `  x ) )  =  ( ( g `  x )  .x.  (
h `  x )
) )
175174mpteq2dv 4372 . . . . . . . . 9  |-  ( f  =  h  ->  (
x  e.  I  |->  ( ( g `  x
)  .x.  ( f `  x ) ) )  =  ( x  e.  I  |->  ( ( g `
 x )  .x.  ( h `  x
) ) ) )
176175oveq2d 6102 . . . . . . . 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 6161 . . . . . . 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 2487 . . . . . 6  |-  ( ph  ->  .,  =  ( e  e.  ( B  ^m  I ) ,  f  e.  ( B  ^m  I )  |->  ( R 
gsumg  ( x  e.  I  |->  ( ( e `  x )  .x.  (
f `  x )
) ) ) ) )
1791783ad2ant1 1009 . . . . 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 5686 . . . . . . . 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 5686 . . . . . . . 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 6104 . . . . . . 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 4372 . . . . . 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 6102 . . . . 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 1009 . . . . . . 7  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  Y  e.  LMod )
188163ad2ant1 1009 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  R  =  (Scalar `  Y
) )
189188fveq2d 5688 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( Base `  R )  =  ( Base `  (Scalar `  Y ) ) )
19017, 189syl5eq 2481 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  B  =  ( Base `  (Scalar `  Y )
) )
19180, 190eleqtrd 2513 . . . . . . . 8  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
k  e.  ( Base `  (Scalar `  Y )
) )
192 eqid 2437 . . . . . . . . 9  |-  ( .s
`  Y )  =  ( .s `  Y
)
193 eqid 2437 . . . . . . . . 9  |-  ( Base `  (Scalar `  Y )
)  =  ( Base `  (Scalar `  Y )
)
1941, 31, 192, 193lmodvscl 16941 . . . . . . . 8  |-  ( ( Y  e.  LMod  /\  k  e.  ( Base `  (Scalar `  Y ) )  /\  g  e.  V )  ->  ( k ( .s
`  Y ) g )  e.  V )
195187, 191, 82, 194syl3anc 1218 . . . . . . 7  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( k ( .s
`  Y ) g )  e.  V )
196 eqid 2437 . . . . . . . 8  |-  ( +g  `  Y )  =  ( +g  `  Y )
1971, 196lmodvacl 16938 . . . . . . 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 1218 . . . . . 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 18156 . . . . . 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 6111 . . . . . 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 6213 . . . 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 18160 . . . . . . . . . 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 18156 . . . . . . . . . . . . 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 7226 . . . . . . . . . . . 12  |-  ( ( k ( .s `  Y ) g )  e.  ( B  ^m  I )  ->  (
k ( .s `  Y ) g ) : I --> B )
208 ffn 5552 . . . . . . . . . . . 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 18163 . . . . . . . . . . 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 2438 . . . . . . . . . . 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 6322 . . . . . . . . . 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 2469 . . . . . . . . 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 6111 . . . . . . . . . 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 5776 . . . . . . . 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 6101 . . . . . . 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 16650 . . . . . . . 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 1220 . . . . . . 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 6101 . . . . . . 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 2473 . . . . . 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 4371 . . . . 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 6102 . . . 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 2469 . . 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 5686 . . . . . . . . . 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 5686 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  g  /\  f  =  i ) )  ->  ( f `  x )  =  ( i `  x ) )
232229, 231oveq12d 6104 . . . . . . . . 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 4372 . . . . . . . 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 6102 . . . . . . 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 6111 . . . . . . . 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 6213 . . . . . 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 6102 . . . . 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 18174 . . . . . . 7  |-  ( (
ph  /\  g  e.  V  /\  i  e.  V
)  ->  ( x  e.  I  |->  ( ( g `  x ) 
.x.  ( i `  x ) ) ) finSupp  .0.  )
240154, 82, 86, 239syl3anc 1218 . . . . . 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 16682 . . . . 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 2472 . . . 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 5686 . . . . . . . 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 5686 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  h  /\  f  =  i ) )  ->  ( f `  x )  =  ( i `  x ) )
247244, 246oveq12d 6104 . . . . . . 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 4372 . . . . . 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 6102 . . . . 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 6111 . . . . . 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 6213 . . . 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 6104 . . 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 2479 . 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 1009 . . . . . . 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 16645 . . . . . 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 1218 . . . . 5  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  x  e.  I )  ->  (
( h `  x
)  .x.  ( g `  x ) )  =  ( ( g `  x )  .x.  (
h `  x )
) )
259258mpteq2dva 4371 . . . 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 6102 . . 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 1009 . . . 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 5686 . . . . . . 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 5686 . . . . . . 7  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  (
e  =  h  /\  f  =  g )
)  ->  ( f `  x )  =  ( g `  x ) )
266263, 265oveq12d 6104 . . . . . 6  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  (
e  =  h  /\  f  =  g )
)  ->  ( (
e `  x )  .x.  ( f `  x
) )  =  ( ( h `  x
)  .x.  ( g `  x ) ) )
267266mpteq2dv 4372 . . . . 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 6102 . . . 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 6111 . . . . 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 6213 . . 3  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( h  .,  g )  =  ( R  gsumg  ( x  e.  I  |->  ( ( h `  x )  .x.  (
g `  x )
) ) ) )
27235ralrimiva 2793 . . . . . 6  |-  ( ph  ->  A. x  e.  B  (  .*  `  x )  =  x )
2732723ad2ant1 1009 . . . . 5  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  A. x  e.  B  (  .*  `  x )  =  x )
274 fveq2 5684 . . . . . . 7  |-  ( x  =  ( g  .,  h )  ->  (  .*  `  x )  =  (  .*  `  (
g  .,  h )
) )
275 id 22 . . . . . . 7  |-  ( x  =  ( g  .,  h )  ->  x  =  ( g  .,  h ) )
276274, 275eqeq12d 2451 . . . . . 6  |-  ( x  =  ( g  .,  h )  ->  (
(  .*  `  x
)  =  x  <->  (  .*  `  ( g  .,  h
) )  =  ( g  .,  h ) ) )
277276rspcv 3062 . . . . 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 2469 . . 3  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  (  .*  `  ( g  .,  h
) )  =  ( R  gsumg  ( x  e.  I  |->  ( ( g `  x )  .x.  (
h `  x )
) ) ) )
280260, 271, 2793eqtr4rd 2480 . 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 18052 1  |-  ( ph  ->  Y  e.  PreHil )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756   A.wral 2709   _Vcvv 2966    C_ wss 3321   class class class wbr 4285    e. cmpt 4343   Fun wfun 5405    Fn wfn 5406   -->wf 5407   ` cfv 5411  (class class class)co 6086    e. cmpt2 6088    oFcof 6313   supp csupp 6685    ^m cmap 7206   finSupp cfsupp 7612   Basecbs 14166   +g cplusg 14230   .rcmulr 14231   *rcstv 14232  Scalarcsca 14233   .scvsca 14234   .icip 14235   0gc0g 14370    gsumg cgsu 14371  CMndccmn 16266   Ringcrg 16631   CRingccrg 16632   DivRingcdr 16808  Fieldcfield 16809   LModclmod 16924   LVecclvec 17157   PreHilcphl 18022   freeLMod cfrlm 18140
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-rep 4396  ax-sep 4406  ax-nul 4414  ax-pow 4463  ax-pr 4524  ax-un 6367  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3282  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3631  df-if 3785  df-pw 3855  df-sn 3871  df-pr 3873  df-tp 3875  df-op 3877  df-uni 4085  df-int 4122  df-iun 4166  df-br 4286  df-opab 4344  df-mpt 4345  df-tr 4379  df-eprel 4624  df-id 4628  df-po 4633  df-so 4634  df-fr 4671  df-se 4672  df-we 4673  df-ord 4714  df-on 4715  df-lim 4716  df-suc 4717  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5374  df-fun 5413  df-fn 5414  df-f 5415  df-f1 5416  df-fo 5417  df-f1o 5418  df-fv 5419  df-isom 5420  df-riota 6045  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-of 6315  df-om 6472  df-1st 6572  df-2nd 6573  df-supp 6686  df-tpos 6740  df-recs 6824  df-rdg 6858  df-1o 6912  df-oadd 6916  df-er 7093  df-map 7208  df-ixp 7256  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-fsupp 7613  df-sup 7683  df-oi 7716  df-card 8101  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-nn 10315  df-2 10372  df-3 10373  df-4 10374  df-5 10375  df-6 10376  df-7 10377  df-8 10378  df-9 10379  df-10 10380  df-n0 10572  df-z 10639  df-dec 10748  df-uz 10854  df-fz 11430  df-fzo 11541  df-seq 11799  df-hash 12096  df-struct 14168  df-ndx 14169  df-slot 14170  df-base 14171  df-sets 14172  df-ress 14173  df-plusg 14243  df-mulr 14244  df-sca 14246  df-vsca 14247  df-ip 14248  df-tset 14249  df-ple 14250  df-ds 14252  df-hom 14254  df-cco 14255  df-0g 14372  df-gsum 14373  df-prds 14378  df-pws 14380  df-mnd 15407  df-mhm 15456  df-submnd 15457  df-grp 15534  df-minusg 15535  df-sbg 15536  df-subg 15667  df-ghm 15734  df-cntz 15824  df-cmn 16268  df-abl 16269  df-mgp 16578  df-ur 16590  df-rng 16633  df-cring 16634  df-oppr 16701  df-rnghom 16792  df-drng 16810  df-field 16811  df-subrg 16839  df-staf 16906  df-srng 16907  df-lmod 16926  df-lss 16988  df-lmhm 17077  df-lvec 17158  df-sra 17227  df-rgmod 17228  df-phl 18024  df-dsmm 18126  df-frlm 18141
This theorem is referenced by:  rrxcph  20865
  Copyright terms: Public domain W3C validator