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

Theorem frlmphl 18983
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 2455 . 2  |-  ( ph  ->  ( +g  `  Y
)  =  ( +g  `  Y ) )
4 eqidd 2455 . 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 17600 . . . . 5  |-  ( R  e. Field 
<->  ( R  e.  DivRing  /\  R  e.  CRing ) )
119, 10sylib 196 . . . 4  |-  ( ph  ->  ( R  e.  DivRing  /\  R  e.  CRing ) )
1211simpld 457 . . 3  |-  ( ph  ->  R  e.  DivRing )
13 frlmphl.i . . 3  |-  ( ph  ->  I  e.  W )
14 frlmphl.y . . . 4  |-  Y  =  ( R freeLMod  I )
1514frlmsca 18957 . . 3  |-  ( ( R  e.  DivRing  /\  I  e.  W )  ->  R  =  (Scalar `  Y )
)
1612, 13, 15syl2anc 659 . 2  |-  ( ph  ->  R  =  (Scalar `  Y ) )
17 frlmphl.b . . 3  |-  B  =  ( Base `  R
)
1817a1i 11 . 2  |-  ( ph  ->  B  =  ( Base `  R ) )
19 eqidd 2455 . 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 drngring 17598 . . . . 5  |-  ( R  e.  DivRing  ->  R  e.  Ring )
2712, 26syl 16 . . . 4  |-  ( ph  ->  R  e.  Ring )
2814frlmlmod 18953 . . . 4  |-  ( ( R  e.  Ring  /\  I  e.  W )  ->  Y  e.  LMod )
2927, 13, 28syl2anc 659 . . 3  |-  ( ph  ->  Y  e.  LMod )
3016, 12eqeltrrd 2543 . . 3  |-  ( ph  ->  (Scalar `  Y )  e.  DivRing )
31 eqid 2454 . . . 4  |-  (Scalar `  Y )  =  (Scalar `  Y )
3231islvec 17945 . . 3  |-  ( Y  e.  LVec  <->  ( Y  e. 
LMod  /\  (Scalar `  Y
)  e.  DivRing ) )
3329, 30, 32sylanbrc 662 . 2  |-  ( ph  ->  Y  e.  LVec )
3411simprd 461 . . 3  |-  ( ph  ->  R  e.  CRing )
35 frlmphl.u . . 3  |-  ( (
ph  /\  x  e.  B )  ->  (  .*  `  x )  =  x )
3617, 22, 34, 35idsrngd 17706 . 2  |-  ( ph  ->  R  e.  *Ring )
37133ad2ant1 1015 . . . . 5  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  I  e.  W )
38273ad2ant1 1015 . . . . 5  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  R  e.  Ring )
39 simp2 995 . . . . 5  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  g  e.  V )
40 simp3 996 . . . . 5  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  h  e.  V )
4114, 17, 20, 1, 5frlmipval 18981 . . . . 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 1227 . . . 4  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( g  .,  h )  =  ( R  gsumg  ( g  oF  .x.  h ) ) )
4314, 17, 1frlmbasmap 18964 . . . . . . . . 9  |-  ( ( I  e.  W  /\  g  e.  V )  ->  g  e.  ( B  ^m  I ) )
4437, 39, 43syl2anc 659 . . . . . . . 8  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  g  e.  ( B  ^m  I ) )
45 elmapi 7433 . . . . . . . 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 5713 . . . . . . 7  |-  ( g : I --> B  -> 
g  Fn  I )
4846, 47syl 16 . . . . . 6  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  g  Fn  I )
4914, 17, 1frlmbasmap 18964 . . . . . . . . 9  |-  ( ( I  e.  W  /\  h  e.  V )  ->  h  e.  ( B  ^m  I ) )
5037, 40, 49syl2anc 659 . . . . . . . 8  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  h  e.  ( B  ^m  I ) )
51 elmapi 7433 . . . . . . . 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 5713 . . . . . . 7  |-  ( h : I --> B  ->  h  Fn  I )
5452, 53syl 16 . . . . . 6  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  h  Fn  I )
55 inidm 3693 . . . . . 6  |-  ( I  i^i  I )  =  I
56 eqidd 2455 . . . . . 6  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  x  e.  I )  ->  (
g `  x )  =  ( g `  x ) )
57 eqidd 2455 . . . . . 6  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  x  e.  I )  ->  (
h `  x )  =  ( h `  x ) )
5848, 54, 37, 37, 55, 56, 57offval 6520 . . . . 5  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( g  oF  .x.  h )  =  ( x  e.  I  |->  ( ( g `
 x )  .x.  ( h `  x
) ) ) )
5958oveq2d 6286 . . . 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 2495 . . 3  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( g  .,  h )  =  ( R  gsumg  ( x  e.  I  |->  ( ( g `  x )  .x.  (
h `  x )
) ) ) )
61 ringcmn 17424 . . . . . 6  |-  ( R  e.  Ring  ->  R  e. CMnd
)
6227, 61syl 16 . . . . 5  |-  ( ph  ->  R  e. CMnd )
63623ad2ant1 1015 . . . 4  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  R  e. CMnd )
6438adantr 463 . . . . . 6  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  x  e.  I )  ->  R  e.  Ring )
6546ffvelrnda 6007 . . . . . 6  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  x  e.  I )  ->  (
g `  x )  e.  B )
6652ffvelrnda 6007 . . . . . 6  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  x  e.  I )  ->  (
h `  x )  e.  B )
6717, 20ringcl 17407 . . . . . 6  |-  ( ( R  e.  Ring  /\  (
g `  x )  e.  B  /\  (
h `  x )  e.  B )  ->  (
( g `  x
)  .x.  ( h `  x ) )  e.  B )
6864, 65, 66, 67syl3anc 1226 . . . . 5  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  x  e.  I )  ->  (
( g `  x
)  .x.  ( h `  x ) )  e.  B )
69 eqid 2454 . . . . 5  |-  ( x  e.  I  |->  ( ( g `  x ) 
.x.  ( h `  x ) ) )  =  ( x  e.  I  |->  ( ( g `
 x )  .x.  ( h `  x
) ) )
7068, 69fmptd 6031 . . . 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 18982 . . . 4  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( x  e.  I  |->  ( ( g `  x ) 
.x.  ( h `  x ) ) ) finSupp  .0.  )
7317, 24, 63, 37, 70, 72gsumcl 17122 . . 3  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( R  gsumg  ( x  e.  I  |->  ( ( g `  x
)  .x.  ( h `  x ) ) ) )  e.  B )
7460, 73eqeltrd 2542 . 2  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( g  .,  h )  e.  B
)
75 eqid 2454 . . . 4  |-  ( +g  `  R )  =  ( +g  `  R )
76623ad2ant1 1015 . . . 4  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  R  e. CMnd )
77133ad2ant1 1015 . . . 4  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  I  e.  W )
78273ad2ant1 1015 . . . . . 6  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  R  e.  Ring )
7978adantr 463 . . . . 5  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  R  e.  Ring )
80 simp2 995 . . . . . 6  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
k  e.  B )
8180adantr 463 . . . . 5  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  k  e.  B )
82 simp31 1030 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
g  e.  V )
8377, 82, 43syl2anc 659 . . . . . . . 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 6007 . . . . . 6  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
g `  x )  e.  B )
86 simp33 1032 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
i  e.  V )
8714, 17, 1frlmbasmap 18964 . . . . . . . . 9  |-  ( ( I  e.  W  /\  i  e.  V )  ->  i  e.  ( B  ^m  I ) )
8877, 86, 87syl2anc 659 . . . . . . . 8  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
i  e.  ( B  ^m  I ) )
89 elmapi 7433 . . . . . . . 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 6007 . . . . . 6  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
i `  x )  e.  B )
9217, 20ringcl 17407 . . . . . 6  |-  ( ( R  e.  Ring  /\  (
g `  x )  e.  B  /\  (
i `  x )  e.  B )  ->  (
( g `  x
)  .x.  ( i `  x ) )  e.  B )
9379, 85, 91, 92syl3anc 1226 . . . . 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, 20ringcl 17407 . . . . 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 1226 . . . 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 1031 . . . . . . . 8  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  h  e.  V )
9777, 96, 49syl2anc 659 . . . . . . 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 6007 . . . . 5  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  (
h `  x )  e.  B )
10017, 20ringcl 17407 . . . . 5  |-  ( ( R  e.  Ring  /\  (
h `  x )  e.  B  /\  (
i `  x )  e.  B )  ->  (
( h `  x
)  .x.  ( i `  x ) )  e.  B )
10179, 99, 91, 100syl3anc 1226 . . . 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 2455 . . . 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 2455 . . . 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 5848 . . . . . . . . 9  |-  ( x  =  y  ->  (
g `  x )  =  ( g `  y ) )
105104oveq2d 6286 . . . . . . . 8  |-  ( x  =  y  ->  (
k  .x.  ( g `  x ) )  =  ( k  .x.  (
g `  y )
) )
106105cbvmptv 4530 . . . . . . 7  |-  ( x  e.  I  |->  ( k 
.x.  ( g `  x ) ) )  =  ( y  e.  I  |->  ( k  .x.  ( g `  y
) ) )
107106oveq1i 6280 . . . . . 6  |-  ( ( x  e.  I  |->  ( k  .x.  ( g `
 x ) ) )  oF  .x.  i )  =  ( ( y  e.  I  |->  ( k  .x.  (
g `  y )
) )  oF  .x.  i )
10817, 20ringcl 17407 . . . . . . . . . . . 12  |-  ( ( R  e.  Ring  /\  k  e.  B  /\  (
g `  x )  e.  B )  ->  (
k  .x.  ( g `  x ) )  e.  B )
10979, 81, 85, 108syl3anc 1226 . . . . . . . . . . 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 2454 . . . . . . . . . . 11  |-  ( x  e.  I  |->  ( k 
.x.  ( g `  x ) ) )  =  ( x  e.  I  |->  ( k  .x.  ( g `  x
) ) )
111109, 110fmptd 6031 . . . . . . . . . 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 5713 . . . . . . . . . 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 5657 . . . . . . . . 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 5713 . . . . . . . . 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 2455 . . . . . . . . 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 459 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V
) )  /\  x  e.  I )  /\  y  =  x )  ->  y  =  x )
120119fveq2d 5852 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V
) )  /\  x  e.  I )  /\  y  =  x )  ->  (
g `  y )  =  ( g `  x ) )
121120oveq2d 6286 . . . . . . . . 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 459 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  x  e.  I )
123 ovex 6298 . . . . . . . . . 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 5936 . . . . . . . 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 2455 . . . . . . . 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 6520 . . . . . . 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, 20ringass 17410 . . . . . . . . 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 1228 . . . . . . . 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 4525 . . . . . . 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 2495 . . . . . 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 2507 . . . . 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 6298 . . . . . . 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 5606 . . . . . . 7  |-  Fun  (
z  e.  I  |->  ( ( ( x  e.  I  |->  ( k  .x.  ( g `  x
) ) ) `  z )  .x.  (
i `  z )
) )
136 eqidd 2455 . . . . . . . . 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 2455 . . . . . . . . 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 6520 . . . . . . . 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 5591 . . . . . . 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 996 . . . . . . . . 9  |-  ( ( g  e.  V  /\  h  e.  V  /\  i  e.  V )  ->  i  e.  V )
14213, 141anim12i 564 . . . . . . . 8  |-  ( (
ph  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( I  e.  W  /\  i  e.  V
) )
1431423adant2 1013 . . . . . . 7  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( I  e.  W  /\  i  e.  V
) )
14414, 24, 1frlmbasfsupp 18963 . . . . . . 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, 24ring0cl 17415 . . . . . . . 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, 24ringrz 17431 . . . . . . . 8  |-  ( ( R  e.  Ring  /\  y  e.  B )  ->  (
y  .x.  .0.  )  =  .0.  )
14978, 148sylan 469 . . . . . . 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 6930 . . . . . 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 7837 . . . . . 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 1227 . . . . 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 4461 . . . 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 994 . . . . 5  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  ph )
155 eleq1 2526 . . . . . . . . 9  |-  ( g  =  h  ->  (
g  e.  V  <->  h  e.  V ) )
156 id 22 . . . . . . . . . . 11  |-  ( g  =  h  ->  g  =  h )
157156, 156oveq12d 6288 . . . . . . . . . 10  |-  ( g  =  h  ->  (
g  .,  g )  =  ( h  .,  h ) )
158157eqeq1d 2456 . . . . . . . . 9  |-  ( g  =  h  ->  (
( g  .,  g
)  =  .0.  <->  ( h  .,  h )  =  .0.  ) )
159155, 1583anbi23d 1300 . . . . . . . 8  |-  ( g  =  h  ->  (
( ph  /\  g  e.  V  /\  (
g  .,  g )  =  .0.  )  <->  ( ph  /\  h  e.  V  /\  ( h  .,  h )  =  .0.  ) ) )
160 eqeq1 2458 . . . . . . . 8  |-  ( g  =  h  ->  (
g  =  O  <->  h  =  O ) )
161159, 160imbi12d 318 . . . . . . 7  |-  ( g  =  h  ->  (
( ( ph  /\  g  e.  V  /\  ( g  .,  g
)  =  .0.  )  ->  g  =  O )  <-> 
( ( ph  /\  h  e.  V  /\  ( h  .,  h )  =  .0.  )  ->  h  =  O )
) )
162161, 71chvarv 2019 . . . . . 6  |-  ( (
ph  /\  h  e.  V  /\  ( h  .,  h )  =  .0.  )  ->  h  =  O )
16314, 17, 20, 1, 5, 7, 24, 22, 9, 162, 35, 13frlmphllem 18982 . . . . 5  |-  ( (
ph  /\  h  e.  V  /\  i  e.  V
)  ->  ( x  e.  I  |->  ( ( h `  x ) 
.x.  ( i `  x ) ) ) finSupp  .0.  )
164154, 96, 86, 163syl3anc 1226 . . . 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 17139 . . 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 18980 . . . . . . . . 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 659 . . . . . . . 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 2514 . . . . . . 7  |-  ( ph  ->  .,  =  ( g  e.  ( B  ^m  I ) ,  h  e.  ( B  ^m  I
)  |->  ( R  gsumg  ( x  e.  I  |->  ( ( g `  x ) 
.x.  ( h `  x ) ) ) ) ) )
169 fveq1 5847 . . . . . . . . . . 11  |-  ( e  =  g  ->  (
e `  x )  =  ( g `  x ) )
170169oveq1d 6285 . . . . . . . . . 10  |-  ( e  =  g  ->  (
( e `  x
)  .x.  ( f `  x ) )  =  ( ( g `  x )  .x.  (
f `  x )
) )
171170mpteq2dv 4526 . . . . . . . . 9  |-  ( e  =  g  ->  (
x  e.  I  |->  ( ( e `  x
)  .x.  ( f `  x ) ) )  =  ( x  e.  I  |->  ( ( g `
 x )  .x.  ( f `  x
) ) ) )
172171oveq2d 6286 . . . . . . . 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 5847 . . . . . . . . . . 11  |-  ( f  =  h  ->  (
f `  x )  =  ( h `  x ) )
174173oveq2d 6286 . . . . . . . . . 10  |-  ( f  =  h  ->  (
( g `  x
)  .x.  ( f `  x ) )  =  ( ( g `  x )  .x.  (
h `  x )
) )
175174mpteq2dv 4526 . . . . . . . . 9  |-  ( f  =  h  ->  (
x  e.  I  |->  ( ( g `  x
)  .x.  ( f `  x ) ) )  =  ( x  e.  I  |->  ( ( g `
 x )  .x.  ( h `  x
) ) ) )
176175oveq2d 6286 . . . . . . . 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 6350 . . . . . . 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 2513 . . . . . 6  |-  ( ph  ->  .,  =  ( e  e.  ( B  ^m  I ) ,  f  e.  ( B  ^m  I )  |->  ( R 
gsumg  ( x  e.  I  |->  ( ( e `  x )  .x.  (
f `  x )
) ) ) ) )
1791783ad2ant1 1015 . . . . 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 754 . . . . . . . . 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 5850 . . . . . . . 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 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 ) )  ->  f  =  i )
183182fveq1d 5850 . . . . . . . 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 6288 . . . . . . 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 4526 . . . . . 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 6286 . . . . 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 1015 . . . . . . 7  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  Y  e.  LMod )
188163ad2ant1 1015 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  R  =  (Scalar `  Y
) )
189188fveq2d 5852 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( Base `  R )  =  ( Base `  (Scalar `  Y ) ) )
19017, 189syl5eq 2507 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  ->  B  =  ( Base `  (Scalar `  Y )
) )
19180, 190eleqtrd 2544 . . . . . . . 8  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
k  e.  ( Base `  (Scalar `  Y )
) )
192 eqid 2454 . . . . . . . . 9  |-  ( .s
`  Y )  =  ( .s `  Y
)
193 eqid 2454 . . . . . . . . 9  |-  ( Base `  (Scalar `  Y )
)  =  ( Base `  (Scalar `  Y )
)
1941, 31, 192, 193lmodvscl 17724 . . . . . . . 8  |-  ( ( Y  e.  LMod  /\  k  e.  ( Base `  (Scalar `  Y ) )  /\  g  e.  V )  ->  ( k ( .s
`  Y ) g )  e.  V )
195187, 191, 82, 194syl3anc 1226 . . . . . . 7  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( k ( .s
`  Y ) g )  e.  V )
196 eqid 2454 . . . . . . . 8  |-  ( +g  `  Y )  =  ( +g  `  Y )
1971, 196lmodvacl 17721 . . . . . . 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 1226 . . . . . 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 18964 . . . . . 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 659 . . . . 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 6298 . . . . . 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 6403 . . . 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 18968 . . . . . . . . . 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 18964 . . . . . . . . . . . . 13  |-  ( ( I  e.  W  /\  ( k ( .s
`  Y ) g )  e.  V )  ->  ( k ( .s `  Y ) g )  e.  ( B  ^m  I ) )
20677, 195, 205syl2anc 659 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  B  /\  ( g  e.  V  /\  h  e.  V  /\  i  e.  V ) )  -> 
( k ( .s
`  Y ) g )  e.  ( B  ^m  I ) )
207 elmapi 7433 . . . . . . . . . . . 12  |-  ( ( k ( .s `  Y ) g )  e.  ( B  ^m  I )  ->  (
k ( .s `  Y ) g ) : I --> B )
208 ffn 5713 . . . . . . . . . . . 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 463 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  x  e.  I )  ->  I  e.  W )
21282adantr 463 . . . . . . . . . . . 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 18971 . . . . . . . . . . 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 2455 . . . . . . . . . . 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 6520 . . . . . . . . . 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 2495 . . . . . . . . 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 6298 . . . . . . . . . 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 5941 . . . . . . . 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 6285 . . . . . . 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, 20ringdir 17413 . . . . . . . 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 1228 . . . . . . 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 6285 . . . . . . 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 2499 . . . . . 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 4525 . . . . 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 6286 . . . 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 2495 . . 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 754 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  g  /\  f  =  i ) )  ->  e  =  g )
229228fveq1d 5850 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  g  /\  f  =  i ) )  ->  ( e `  x )  =  ( g `  x ) )
230 simprr 755 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  g  /\  f  =  i ) )  ->  f  =  i )
231230fveq1d 5850 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  g  /\  f  =  i ) )  ->  ( f `  x )  =  ( i `  x ) )
232229, 231oveq12d 6288 . . . . . . . . 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 4526 . . . . . . . 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 6286 . . . . . . 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 6298 . . . . . . . 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 6403 . . . . . 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 6286 . . . . 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 18982 . . . . . . 7  |-  ( (
ph  /\  g  e.  V  /\  i  e.  V
)  ->  ( x  e.  I  |->  ( ( g `  x ) 
.x.  ( i `  x ) ) ) finSupp  .0.  )
240154, 82, 86, 239syl3anc 1226 . . . . . 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 17448 . . . . 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 2498 . . . 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 754 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  h  /\  f  =  i ) )  ->  e  =  h )
244243fveq1d 5850 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  h  /\  f  =  i ) )  ->  ( e `  x )  =  ( h `  x ) )
245 simprr 755 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  h  /\  f  =  i ) )  ->  f  =  i )
246245fveq1d 5850 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  B  /\  (
g  e.  V  /\  h  e.  V  /\  i  e.  V )
)  /\  ( e  =  h  /\  f  =  i ) )  ->  ( f `  x )  =  ( i `  x ) )
247244, 246oveq12d 6288 . . . . . . 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 4526 . . . . . 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 6286 . . . . 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 6298 . . . . . 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 6403 . . . 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 6288 . . 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 2505 . 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 1015 . . . . . . 7  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  R  e.  CRing
)
256255adantr 463 . . . . . 6  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  x  e.  I )  ->  R  e.  CRing )
25717, 20crngcom 17408 . . . . . 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 1226 . . . . 5  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  x  e.  I )  ->  (
( h `  x
)  .x.  ( g `  x ) )  =  ( ( g `  x )  .x.  (
h `  x )
) )
259258mpteq2dva 4525 . . . 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 6286 . . 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 1015 . . . 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 754 . . . . . . . 8  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  (
e  =  h  /\  f  =  g )
)  ->  e  =  h )
263262fveq1d 5850 . . . . . . 7  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  (
e  =  h  /\  f  =  g )
)  ->  ( e `  x )  =  ( h `  x ) )
264 simprr 755 . . . . . . . 8  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  (
e  =  h  /\  f  =  g )
)  ->  f  =  g )
265264fveq1d 5850 . . . . . . 7  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  (
e  =  h  /\  f  =  g )
)  ->  ( f `  x )  =  ( g `  x ) )
266263, 265oveq12d 6288 . . . . . 6  |-  ( ( ( ph  /\  g  e.  V  /\  h  e.  V )  /\  (
e  =  h  /\  f  =  g )
)  ->  ( (
e `  x )  .x.  ( f `  x
) )  =  ( ( h `  x
)  .x.  ( g `  x ) ) )
267266mpteq2dv 4526 . . . . 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 6286 . . . 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 6298 . . . . 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 6403 . . 3  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  ( h  .,  g )  =  ( R  gsumg  ( x  e.  I  |->  ( ( h `  x )  .x.  (
g `  x )
) ) ) )
27235ralrimiva 2868 . . . . . 6  |-  ( ph  ->  A. x  e.  B  (  .*  `  x )  =  x )
2732723ad2ant1 1015 . . . . 5  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  A. x  e.  B  (  .*  `  x )  =  x )
274 fveq2 5848 . . . . . . 7  |-  ( x  =  ( g  .,  h )  ->  (  .*  `  x )  =  (  .*  `  (
g  .,  h )
) )
275 id 22 . . . . . . 7  |-  ( x  =  ( g  .,  h )  ->  x  =  ( g  .,  h ) )
276274, 275eqeq12d 2476 . . . . . 6  |-  ( x  =  ( g  .,  h )  ->  (
(  .*  `  x
)  =  x  <->  (  .*  `  ( g  .,  h
) )  =  ( g  .,  h ) ) )
277276rspcv 3203 . . . . 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 2495 . . 3  |-  ( (
ph  /\  g  e.  V  /\  h  e.  V
)  ->  (  .*  `  ( g  .,  h
) )  =  ( R  gsumg  ( x  e.  I  |->  ( ( g `  x )  .x.  (
h `  x )
) ) ) )
280260, 271, 2793eqtr4rd 2506 . 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 18862 1  |-  ( ph  ->  Y  e.  PreHil )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971    = wceq 1398    e. wcel 1823   A.wral 2804   _Vcvv 3106    C_ wss 3461   class class class wbr 4439    |-> cmpt 4497   Fun wfun 5564    Fn wfn 5565   -->wf 5566   ` cfv 5570  (class class class)co 6270    |-> cmpt2 6272    oFcof 6511   supp csupp 6891    ^m cmap 7412   finSupp cfsupp 7821   Basecbs 14716   +g cplusg 14784   .rcmulr 14785   *rcstv 14786  Scalarcsca 14787   .scvsca 14788   .icip 14789   0gc0g 14929    gsumg cgsu 14930  CMndccmn 16997   Ringcrg 17393   CRingccrg 17394   DivRingcdr 17591  Fieldcfield 17592   LModclmod 17707   LVecclvec 17943   PreHilcphl 18832   freeLMod cfrlm 18950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rmo 2812  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-int 4272  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-se 4828  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-isom 5579  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-of 6513  df-om 6674  df-1st 6773  df-2nd 6774  df-supp 6892  df-tpos 6947  df-recs 7034  df-rdg 7068  df-1o 7122  df-oadd 7126  df-er 7303  df-map 7414  df-ixp 7463  df-en 7510  df-dom 7511  df-sdom 7512  df-fin 7513  df-fsupp 7822  df-sup 7893  df-oi 7927  df-card 8311  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9798  df-neg 9799  df-nn 10532  df-2 10590  df-3 10591  df-4 10592  df-5 10593  df-6 10594  df-7 10595  df-8 10596  df-9 10597  df-10 10598  df-n0 10792  df-z 10861  df-dec 10977  df-uz 11083  df-fz 11676  df-fzo 11800  df-seq 12090  df-hash 12388  df-struct 14718  df-ndx 14719  df-slot 14720  df-base 14721  df-sets 14722  df-ress 14723  df-plusg 14797  df-mulr 14798  df-sca 14800  df-vsca 14801  df-ip 14802  df-tset 14803  df-ple 14804  df-ds 14806  df-hom 14808  df-cco 14809  df-0g 14931  df-gsum 14932  df-prds 14937  df-pws 14939  df-mgm 16071  df-sgrp 16110  df-mnd 16120  df-mhm 16165  df-submnd 16166  df-grp 16256  df-minusg 16257  df-sbg 16258  df-subg 16397  df-ghm 16464  df-cntz 16554  df-cmn 16999  df-abl 17000  df-mgp 17337  df-ur 17349  df-ring 17395  df-cring 17396  df-oppr 17467  df-rnghom 17559  df-drng 17593  df-field 17594  df-subrg 17622  df-staf 17689  df-srng 17690  df-lmod 17709  df-lss 17774  df-lmhm 17863  df-lvec 17944  df-sra 18013  df-rgmod 18014  df-phl 18834  df-dsmm 18936  df-frlm 18951
This theorem is referenced by:  rrxcph  21990
  Copyright terms: Public domain W3C validator