Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  frlmup1 Unicode version

Theorem frlmup1 27250
Description: Any assignment of unit vectors to target vectors can be extended (uniquely) to a homomorphism from a free module to an arbitrary other module on the same base ring. (Contributed by Stefan O'Rear, 7-Feb-2015.)
Hypotheses
Ref Expression
frlmup.f  |-  F  =  ( R freeLMod  I )
frlmup.b  |-  B  =  ( Base `  F
)
frlmup.c  |-  C  =  ( Base `  T
)
frlmup.v  |-  .x.  =  ( .s `  T )
frlmup.e  |-  E  =  ( x  e.  B  |->  ( T  gsumg  ( x  o F 
.x.  A ) ) )
frlmup.t  |-  ( ph  ->  T  e.  LMod )
frlmup.i  |-  ( ph  ->  I  e.  X )
frlmup.r  |-  ( ph  ->  R  =  (Scalar `  T ) )
frlmup.a  |-  ( ph  ->  A : I --> C )
Assertion
Ref Expression
frlmup1  |-  ( ph  ->  E  e.  ( F LMHom 
T ) )
Distinct variable groups:    x, R    x, I    x, F    x, B    x, C    x,  .x.    x, A    x, X    ph, x    x, T
Allowed substitution hint:    E( x)

Proof of Theorem frlmup1
Dummy variables  y 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frlmup.b . 2  |-  B  =  ( Base `  F
)
2 eqid 2283 . 2  |-  ( .s
`  F )  =  ( .s `  F
)
3 frlmup.v . 2  |-  .x.  =  ( .s `  T )
4 eqid 2283 . 2  |-  (Scalar `  F )  =  (Scalar `  F )
5 eqid 2283 . 2  |-  (Scalar `  T )  =  (Scalar `  T )
6 eqid 2283 . 2  |-  ( Base `  (Scalar `  F )
)  =  ( Base `  (Scalar `  F )
)
7 frlmup.r . . . 4  |-  ( ph  ->  R  =  (Scalar `  T ) )
8 frlmup.t . . . . 5  |-  ( ph  ->  T  e.  LMod )
95lmodrng 15635 . . . . 5  |-  ( T  e.  LMod  ->  (Scalar `  T )  e.  Ring )
108, 9syl 15 . . . 4  |-  ( ph  ->  (Scalar `  T )  e.  Ring )
117, 10eqeltrd 2357 . . 3  |-  ( ph  ->  R  e.  Ring )
12 frlmup.i . . 3  |-  ( ph  ->  I  e.  X )
13 frlmup.f . . . 4  |-  F  =  ( R freeLMod  I )
1413frlmlmod 27217 . . 3  |-  ( ( R  e.  Ring  /\  I  e.  X )  ->  F  e.  LMod )
1511, 12, 14syl2anc 642 . 2  |-  ( ph  ->  F  e.  LMod )
1613frlmsca 27221 . . . 4  |-  ( ( R  e.  Ring  /\  I  e.  X )  ->  R  =  (Scalar `  F )
)
1711, 12, 16syl2anc 642 . . 3  |-  ( ph  ->  R  =  (Scalar `  F ) )
187, 17eqtr3d 2317 . 2  |-  ( ph  ->  (Scalar `  T )  =  (Scalar `  F )
)
19 frlmup.c . . 3  |-  C  =  ( Base `  T
)
20 eqid 2283 . . 3  |-  ( +g  `  F )  =  ( +g  `  F )
21 eqid 2283 . . 3  |-  ( +g  `  T )  =  ( +g  `  T )
22 lmodgrp 15634 . . . 4  |-  ( F  e.  LMod  ->  F  e. 
Grp )
2315, 22syl 15 . . 3  |-  ( ph  ->  F  e.  Grp )
24 lmodgrp 15634 . . . 4  |-  ( T  e.  LMod  ->  T  e. 
Grp )
258, 24syl 15 . . 3  |-  ( ph  ->  T  e.  Grp )
26 eleq1 2343 . . . . . . 7  |-  ( z  =  x  ->  (
z  e.  B  <->  x  e.  B ) )
2726anbi2d 684 . . . . . 6  |-  ( z  =  x  ->  (
( ph  /\  z  e.  B )  <->  ( ph  /\  x  e.  B ) ) )
28 oveq1 5865 . . . . . . . 8  |-  ( z  =  x  ->  (
z  o F  .x.  A )  =  ( x  o F  .x.  A ) )
2928oveq2d 5874 . . . . . . 7  |-  ( z  =  x  ->  ( T  gsumg  ( z  o F 
.x.  A ) )  =  ( T  gsumg  ( x  o F  .x.  A
) ) )
3029eleq1d 2349 . . . . . 6  |-  ( z  =  x  ->  (
( T  gsumg  ( z  o F 
.x.  A ) )  e.  C  <->  ( T  gsumg  ( x  o F  .x.  A ) )  e.  C ) )
3127, 30imbi12d 311 . . . . 5  |-  ( z  =  x  ->  (
( ( ph  /\  z  e.  B )  ->  ( T  gsumg  ( z  o F 
.x.  A ) )  e.  C )  <->  ( ( ph  /\  x  e.  B
)  ->  ( T  gsumg  ( x  o F  .x.  A ) )  e.  C ) ) )
32 eqid 2283 . . . . . 6  |-  ( 0g
`  T )  =  ( 0g `  T
)
33 lmodcmn 15673 . . . . . . . 8  |-  ( T  e.  LMod  ->  T  e. CMnd
)
348, 33syl 15 . . . . . . 7  |-  ( ph  ->  T  e. CMnd )
3534adantr 451 . . . . . 6  |-  ( (
ph  /\  z  e.  B )  ->  T  e. CMnd )
3612adantr 451 . . . . . 6  |-  ( (
ph  /\  z  e.  B )  ->  I  e.  X )
378ad2antrr 706 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  B )  /\  (
x  e.  ( Base `  R )  /\  y  e.  C ) )  ->  T  e.  LMod )
38 simprl 732 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  B )  /\  (
x  e.  ( Base `  R )  /\  y  e.  C ) )  ->  x  e.  ( Base `  R ) )
397fveq2d 5529 . . . . . . . . . 10  |-  ( ph  ->  ( Base `  R
)  =  ( Base `  (Scalar `  T )
) )
4039ad2antrr 706 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  B )  /\  (
x  e.  ( Base `  R )  /\  y  e.  C ) )  -> 
( Base `  R )  =  ( Base `  (Scalar `  T ) ) )
4138, 40eleqtrd 2359 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  B )  /\  (
x  e.  ( Base `  R )  /\  y  e.  C ) )  ->  x  e.  ( Base `  (Scalar `  T )
) )
42 simprr 733 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  B )  /\  (
x  e.  ( Base `  R )  /\  y  e.  C ) )  -> 
y  e.  C )
43 eqid 2283 . . . . . . . . 9  |-  ( Base `  (Scalar `  T )
)  =  ( Base `  (Scalar `  T )
)
4419, 5, 3, 43lmodvscl 15644 . . . . . . . 8  |-  ( ( T  e.  LMod  /\  x  e.  ( Base `  (Scalar `  T ) )  /\  y  e.  C )  ->  ( x  .x.  y
)  e.  C )
4537, 41, 42, 44syl3anc 1182 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  B )  /\  (
x  e.  ( Base `  R )  /\  y  e.  C ) )  -> 
( x  .x.  y
)  e.  C )
46 eqid 2283 . . . . . . . . 9  |-  ( Base `  R )  =  (
Base `  R )
4713, 46, 1frlmbasf 27228 . . . . . . . 8  |-  ( ( I  e.  X  /\  z  e.  B )  ->  z : I --> ( Base `  R ) )
4812, 47sylan 457 . . . . . . 7  |-  ( (
ph  /\  z  e.  B )  ->  z : I --> ( Base `  R ) )
49 frlmup.a . . . . . . . 8  |-  ( ph  ->  A : I --> C )
5049adantr 451 . . . . . . 7  |-  ( (
ph  /\  z  e.  B )  ->  A : I --> C )
51 inidm 3378 . . . . . . 7  |-  ( I  i^i  I )  =  I
5245, 48, 50, 36, 36, 51off 6093 . . . . . 6  |-  ( (
ph  /\  z  e.  B )  ->  (
z  o F  .x.  A ) : I --> C )
537fveq2d 5529 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0g `  R
)  =  ( 0g
`  (Scalar `  T )
) )
5453sneqd 3653 . . . . . . . . . . 11  |-  ( ph  ->  { ( 0g `  R ) }  =  { ( 0g `  (Scalar `  T ) ) } )
5554difeq2d 3294 . . . . . . . . . 10  |-  ( ph  ->  ( _V  \  {
( 0g `  R
) } )  =  ( _V  \  {
( 0g `  (Scalar `  T ) ) } ) )
5655imaeq2d 5012 . . . . . . . . 9  |-  ( ph  ->  ( `' z "
( _V  \  {
( 0g `  R
) } ) )  =  ( `' z
" ( _V  \  { ( 0g `  (Scalar `  T ) ) } ) ) )
5756adantr 451 . . . . . . . 8  |-  ( (
ph  /\  z  e.  B )  ->  ( `' z " ( _V  \  { ( 0g
`  R ) } ) )  =  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) )
58 eqid 2283 . . . . . . . . . 10  |-  ( 0g
`  R )  =  ( 0g `  R
)
5913, 58, 1frlmbassup 27226 . . . . . . . . 9  |-  ( ( I  e.  X  /\  z  e.  B )  ->  ( `' z "
( _V  \  {
( 0g `  R
) } ) )  e.  Fin )
6012, 59sylan 457 . . . . . . . 8  |-  ( (
ph  /\  z  e.  B )  ->  ( `' z " ( _V  \  { ( 0g
`  R ) } ) )  e.  Fin )
6157, 60eqeltrrd 2358 . . . . . . 7  |-  ( (
ph  /\  z  e.  B )  ->  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) )  e.  Fin )
62 ffn 5389 . . . . . . . . . . . 12  |-  ( z : I --> ( Base `  R )  ->  z  Fn  I )
6348, 62syl 15 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  B )  ->  z  Fn  I )
6463adantr 451 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  ( I  \  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) ) )  ->  z  Fn  I )
65 ffn 5389 . . . . . . . . . . . 12  |-  ( A : I --> C  ->  A  Fn  I )
6649, 65syl 15 . . . . . . . . . . 11  |-  ( ph  ->  A  Fn  I )
6766ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  ( I  \  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) ) )  ->  A  Fn  I )
6812ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  ( I  \  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) ) )  ->  I  e.  X )
69 eldifi 3298 . . . . . . . . . . 11  |-  ( x  e.  ( I  \ 
( `' z "
( _V  \  {
( 0g `  (Scalar `  T ) ) } ) ) )  ->  x  e.  I )
7069adantl 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  ( I  \  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) ) )  ->  x  e.  I )
71 fnfvof 6090 . . . . . . . . . 10  |-  ( ( ( z  Fn  I  /\  A  Fn  I
)  /\  ( I  e.  X  /\  x  e.  I ) )  -> 
( ( z  o F  .x.  A ) `
 x )  =  ( ( z `  x )  .x.  ( A `  x )
) )
7264, 67, 68, 70, 71syl22anc 1183 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  ( I  \  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) ) )  ->  (
( z  o F 
.x.  A ) `  x )  =  ( ( z `  x
)  .x.  ( A `  x ) ) )
73 ssid 3197 . . . . . . . . . . . 12  |-  ( `' z " ( _V 
\  { ( 0g
`  (Scalar `  T )
) } ) ) 
C_  ( `' z
" ( _V  \  { ( 0g `  (Scalar `  T ) ) } ) )
7473a1i 10 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  B )  ->  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) 
C_  ( `' z
" ( _V  \  { ( 0g `  (Scalar `  T ) ) } ) ) )
7548, 74suppssr 5659 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  ( I  \  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) ) )  ->  (
z `  x )  =  ( 0g `  (Scalar `  T ) ) )
7675oveq1d 5873 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  ( I  \  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) ) )  ->  (
( z `  x
)  .x.  ( A `  x ) )  =  ( ( 0g `  (Scalar `  T ) ) 
.x.  ( A `  x ) ) )
778ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  ( I  \  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) ) )  ->  T  e.  LMod )
78 ffvelrn 5663 . . . . . . . . . . 11  |-  ( ( A : I --> C  /\  x  e.  I )  ->  ( A `  x
)  e.  C )
7950, 69, 78syl2an 463 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  ( I  \  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) ) )  ->  ( A `  x )  e.  C )
80 eqid 2283 . . . . . . . . . . 11  |-  ( 0g
`  (Scalar `  T )
)  =  ( 0g
`  (Scalar `  T )
)
8119, 5, 3, 80, 32lmod0vs 15663 . . . . . . . . . 10  |-  ( ( T  e.  LMod  /\  ( A `  x )  e.  C )  ->  (
( 0g `  (Scalar `  T ) )  .x.  ( A `  x ) )  =  ( 0g
`  T ) )
8277, 79, 81syl2anc 642 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  ( I  \  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) ) )  ->  (
( 0g `  (Scalar `  T ) )  .x.  ( A `  x ) )  =  ( 0g
`  T ) )
8372, 76, 823eqtrd 2319 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  ( I  \  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) ) )  ->  (
( z  o F 
.x.  A ) `  x )  =  ( 0g `  T ) )
8452, 83suppss 5658 . . . . . . 7  |-  ( (
ph  /\  z  e.  B )  ->  ( `' ( z  o F  .x.  A )
" ( _V  \  { ( 0g `  T ) } ) )  C_  ( `' z " ( _V  \  { ( 0g `  (Scalar `  T ) ) } ) ) )
85 ssfi 7083 . . . . . . 7  |-  ( ( ( `' z "
( _V  \  {
( 0g `  (Scalar `  T ) ) } ) )  e.  Fin  /\  ( `' ( z  o F  .x.  A
) " ( _V 
\  { ( 0g
`  T ) } ) )  C_  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) )  ->  ( `' ( z  o F 
.x.  A ) "
( _V  \  {
( 0g `  T
) } ) )  e.  Fin )
8661, 84, 85syl2anc 642 . . . . . 6  |-  ( (
ph  /\  z  e.  B )  ->  ( `' ( z  o F  .x.  A )
" ( _V  \  { ( 0g `  T ) } ) )  e.  Fin )
8719, 32, 35, 36, 52, 86gsumcl 15198 . . . . 5  |-  ( (
ph  /\  z  e.  B )  ->  ( T  gsumg  ( z  o F 
.x.  A ) )  e.  C )
8831, 87chvarv 1953 . . . 4  |-  ( (
ph  /\  x  e.  B )  ->  ( T  gsumg  ( x  o F 
.x.  A ) )  e.  C )
89 frlmup.e . . . 4  |-  E  =  ( x  e.  B  |->  ( T  gsumg  ( x  o F 
.x.  A ) ) )
9088, 89fmptd 5684 . . 3  |-  ( ph  ->  E : B --> C )
9134adantr 451 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  ->  T  e. CMnd )
9212adantr 451 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  ->  I  e.  X )
93 eleq1 2343 . . . . . . . . 9  |-  ( z  =  y  ->  (
z  e.  B  <->  y  e.  B ) )
9493anbi2d 684 . . . . . . . 8  |-  ( z  =  y  ->  (
( ph  /\  z  e.  B )  <->  ( ph  /\  y  e.  B ) ) )
95 oveq1 5865 . . . . . . . . 9  |-  ( z  =  y  ->  (
z  o F  .x.  A )  =  ( y  o F  .x.  A ) )
9695feq1d 5379 . . . . . . . 8  |-  ( z  =  y  ->  (
( z  o F 
.x.  A ) : I --> C  <->  ( y  o F  .x.  A ) : I --> C ) )
9794, 96imbi12d 311 . . . . . . 7  |-  ( z  =  y  ->  (
( ( ph  /\  z  e.  B )  ->  ( z  o F 
.x.  A ) : I --> C )  <->  ( ( ph  /\  y  e.  B
)  ->  ( y  o F  .x.  A ) : I --> C ) ) )
9897, 52chvarv 1953 . . . . . 6  |-  ( (
ph  /\  y  e.  B )  ->  (
y  o F  .x.  A ) : I --> C )
9998adantrr 697 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( y  o F 
.x.  A ) : I --> C )
10052adantrl 696 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( z  o F 
.x.  A ) : I --> C )
10195cnveqd 4857 . . . . . . . . . 10  |-  ( z  =  y  ->  `' ( z  o F 
.x.  A )  =  `' ( y  o F  .x.  A ) )
102101imaeq1d 5011 . . . . . . . . 9  |-  ( z  =  y  ->  ( `' ( z  o F  .x.  A )
" ( _V  \  { ( 0g `  T ) } ) )  =  ( `' ( y  o F 
.x.  A ) "
( _V  \  {
( 0g `  T
) } ) ) )
103102eleq1d 2349 . . . . . . . 8  |-  ( z  =  y  ->  (
( `' ( z  o F  .x.  A
) " ( _V 
\  { ( 0g
`  T ) } ) )  e.  Fin  <->  ( `' ( y  o F  .x.  A )
" ( _V  \  { ( 0g `  T ) } ) )  e.  Fin )
)
10494, 103imbi12d 311 . . . . . . 7  |-  ( z  =  y  ->  (
( ( ph  /\  z  e.  B )  ->  ( `' ( z  o F  .x.  A
) " ( _V 
\  { ( 0g
`  T ) } ) )  e.  Fin ) 
<->  ( ( ph  /\  y  e.  B )  ->  ( `' ( y  o F  .x.  A
) " ( _V 
\  { ( 0g
`  T ) } ) )  e.  Fin ) ) )
105104, 86chvarv 1953 . . . . . 6  |-  ( (
ph  /\  y  e.  B )  ->  ( `' ( y  o F  .x.  A )
" ( _V  \  { ( 0g `  T ) } ) )  e.  Fin )
106105adantrr 697 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( `' ( y  o F  .x.  A
) " ( _V 
\  { ( 0g
`  T ) } ) )  e.  Fin )
10786adantrl 696 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( `' ( z  o F  .x.  A
) " ( _V 
\  { ( 0g
`  T ) } ) )  e.  Fin )
10819, 32, 21, 91, 92, 99, 100, 106, 107gsumadd 15205 . . . 4  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( T  gsumg  ( ( y  o F  .x.  A )  o F ( +g  `  T ) ( z  o F  .x.  A
) ) )  =  ( ( T  gsumg  ( y  o F  .x.  A
) ) ( +g  `  T ) ( T 
gsumg  ( z  o F 
.x.  A ) ) ) )
1091, 20lmodvacl 15641 . . . . . . . 8  |-  ( ( F  e.  LMod  /\  y  e.  B  /\  z  e.  B )  ->  (
y ( +g  `  F
) z )  e.  B )
1101093expb 1152 . . . . . . 7  |-  ( ( F  e.  LMod  /\  (
y  e.  B  /\  z  e.  B )
)  ->  ( y
( +g  `  F ) z )  e.  B
)
11115, 110sylan 457 . . . . . 6  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( y ( +g  `  F ) z )  e.  B )
112 oveq1 5865 . . . . . . . 8  |-  ( x  =  ( y ( +g  `  F ) z )  ->  (
x  o F  .x.  A )  =  ( ( y ( +g  `  F ) z )  o F  .x.  A
) )
113112oveq2d 5874 . . . . . . 7  |-  ( x  =  ( y ( +g  `  F ) z )  ->  ( T  gsumg  ( x  o F 
.x.  A ) )  =  ( T  gsumg  ( ( y ( +g  `  F
) z )  o F  .x.  A ) ) )
114 ovex 5883 . . . . . . 7  |-  ( T 
gsumg  ( ( y ( +g  `  F ) z )  o F 
.x.  A ) )  e.  _V
115113, 89, 114fvmpt 5602 . . . . . 6  |-  ( ( y ( +g  `  F
) z )  e.  B  ->  ( E `  ( y ( +g  `  F ) z ) )  =  ( T 
gsumg  ( ( y ( +g  `  F ) z )  o F 
.x.  A ) ) )
116111, 115syl 15 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( E `  (
y ( +g  `  F
) z ) )  =  ( T  gsumg  ( ( y ( +g  `  F
) z )  o F  .x.  A ) ) )
11711adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  ->  R  e.  Ring )
118 simprl 732 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
y  e.  B )
119 simprr 733 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
z  e.  B )
120 eqid 2283 . . . . . . . . 9  |-  ( +g  `  R )  =  ( +g  `  R )
12113, 1, 117, 92, 118, 119, 120, 20frlmplusgval 27229 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( y ( +g  `  F ) z )  =  ( y  o F ( +g  `  R
) z ) )
122121oveq1d 5873 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( ( y ( +g  `  F ) z )  o F 
.x.  A )  =  ( ( y  o F ( +g  `  R
) z )  o F  .x.  A ) )
12313, 46, 1frlmbasf 27228 . . . . . . . . . . . . 13  |-  ( ( I  e.  X  /\  y  e.  B )  ->  y : I --> ( Base `  R ) )
12412, 123sylan 457 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  B )  ->  y : I --> ( Base `  R ) )
125124adantrr 697 . . . . . . . . . . 11  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
y : I --> ( Base `  R ) )
126 ffn 5389 . . . . . . . . . . 11  |-  ( y : I --> ( Base `  R )  ->  y  Fn  I )
127125, 126syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
y  Fn  I )
12848adantrl 696 . . . . . . . . . . 11  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
z : I --> ( Base `  R ) )
129128, 62syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
z  Fn  I )
130127, 129, 92, 92, 51offn 6089 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( y  o F ( +g  `  R
) z )  Fn  I )
13166adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  ->  A  Fn  I )
132130, 131, 92, 92, 51offn 6089 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( ( y  o F ( +g  `  R
) z )  o F  .x.  A )  Fn  I )
133 ffn 5389 . . . . . . . . . . 11  |-  ( ( y  o F  .x.  A ) : I --> C  ->  ( y  o F  .x.  A )  Fn  I )
13498, 133syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  B )  ->  (
y  o F  .x.  A )  Fn  I
)
135134adantrr 697 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( y  o F 
.x.  A )  Fn  I )
136 ffn 5389 . . . . . . . . . . 11  |-  ( ( z  o F  .x.  A ) : I --> C  ->  ( z  o F  .x.  A )  Fn  I )
13752, 136syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  B )  ->  (
z  o F  .x.  A )  Fn  I
)
138137adantrl 696 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( z  o F 
.x.  A )  Fn  I )
139135, 138, 92, 92, 51offn 6089 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( ( y  o F  .x.  A )  o F ( +g  `  T ) ( z  o F  .x.  A
) )  Fn  I
)
1407fveq2d 5529 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( +g  `  R
)  =  ( +g  `  (Scalar `  T )
) )
141140ad2antrr 706 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  ( +g  `  R )  =  ( +g  `  (Scalar `  T ) ) )
142141oveqd 5875 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( y `  x
) ( +g  `  R
) ( z `  x ) )  =  ( ( y `  x ) ( +g  `  (Scalar `  T )
) ( z `  x ) ) )
143142oveq1d 5873 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( ( y `  x ) ( +g  `  R ) ( z `
 x ) ) 
.x.  ( A `  x ) )  =  ( ( ( y `
 x ) ( +g  `  (Scalar `  T ) ) ( z `  x ) )  .x.  ( A `
 x ) ) )
1448ad2antrr 706 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  T  e.  LMod )
145 ffvelrn 5663 . . . . . . . . . . . . . 14  |-  ( ( y : I --> ( Base `  R )  /\  x  e.  I )  ->  (
y `  x )  e.  ( Base `  R
) )
146125, 145sylan 457 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
y `  x )  e.  ( Base `  R
) )
14739ad2antrr 706 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  ( Base `  R )  =  ( Base `  (Scalar `  T ) ) )
148146, 147eleqtrd 2359 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
y `  x )  e.  ( Base `  (Scalar `  T ) ) )
149 ffvelrn 5663 . . . . . . . . . . . . . 14  |-  ( ( z : I --> ( Base `  R )  /\  x  e.  I )  ->  (
z `  x )  e.  ( Base `  R
) )
150128, 149sylan 457 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
z `  x )  e.  ( Base `  R
) )
151150, 147eleqtrd 2359 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
z `  x )  e.  ( Base `  (Scalar `  T ) ) )
15249adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  ->  A : I --> C )
153152, 78sylan 457 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  ( A `  x )  e.  C )
154 eqid 2283 . . . . . . . . . . . . 13  |-  ( +g  `  (Scalar `  T )
)  =  ( +g  `  (Scalar `  T )
)
15519, 21, 5, 3, 43, 154lmodvsdir 15652 . . . . . . . . . . . 12  |-  ( ( T  e.  LMod  /\  (
( y `  x
)  e.  ( Base `  (Scalar `  T )
)  /\  ( z `  x )  e.  (
Base `  (Scalar `  T
) )  /\  ( A `  x )  e.  C ) )  -> 
( ( ( y `
 x ) ( +g  `  (Scalar `  T ) ) ( z `  x ) )  .x.  ( A `
 x ) )  =  ( ( ( y `  x ) 
.x.  ( A `  x ) ) ( +g  `  T ) ( ( z `  x )  .x.  ( A `  x )
) ) )
156144, 148, 151, 153, 155syl13anc 1184 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( ( y `  x ) ( +g  `  (Scalar `  T )
) ( z `  x ) )  .x.  ( A `  x ) )  =  ( ( ( y `  x
)  .x.  ( A `  x ) ) ( +g  `  T ) ( ( z `  x )  .x.  ( A `  x )
) ) )
157143, 156eqtrd 2315 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( ( y `  x ) ( +g  `  R ) ( z `
 x ) ) 
.x.  ( A `  x ) )  =  ( ( ( y `
 x )  .x.  ( A `  x ) ) ( +g  `  T
) ( ( z `
 x )  .x.  ( A `  x ) ) ) )
158127adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  y  Fn  I )
159129adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  z  Fn  I )
16012ad2antrr 706 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  I  e.  X )
161 simpr 447 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  x  e.  I )
162 fnfvof 6090 . . . . . . . . . . . 12  |-  ( ( ( y  Fn  I  /\  z  Fn  I
)  /\  ( I  e.  X  /\  x  e.  I ) )  -> 
( ( y  o F ( +g  `  R
) z ) `  x )  =  ( ( y `  x
) ( +g  `  R
) ( z `  x ) ) )
163158, 159, 160, 161, 162syl22anc 1183 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( y  o F ( +g  `  R
) z ) `  x )  =  ( ( y `  x
) ( +g  `  R
) ( z `  x ) ) )
164163oveq1d 5873 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( ( y  o F ( +g  `  R
) z ) `  x )  .x.  ( A `  x )
)  =  ( ( ( y `  x
) ( +g  `  R
) ( z `  x ) )  .x.  ( A `  x ) ) )
16566ad2antrr 706 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  A  Fn  I )
166 fnfvof 6090 . . . . . . . . . . . 12  |-  ( ( ( y  Fn  I  /\  A  Fn  I
)  /\  ( I  e.  X  /\  x  e.  I ) )  -> 
( ( y  o F  .x.  A ) `
 x )  =  ( ( y `  x )  .x.  ( A `  x )
) )
167158, 165, 160, 161, 166syl22anc 1183 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( y  o F 
.x.  A ) `  x )  =  ( ( y `  x
)  .x.  ( A `  x ) ) )
168159, 165, 160, 161, 71syl22anc 1183 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( z  o F 
.x.  A ) `  x )  =  ( ( z `  x
)  .x.  ( A `  x ) ) )
169167, 168oveq12d 5876 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( ( y  o F  .x.  A ) `
 x ) ( +g  `  T ) ( ( z  o F  .x.  A ) `
 x ) )  =  ( ( ( y `  x ) 
.x.  ( A `  x ) ) ( +g  `  T ) ( ( z `  x )  .x.  ( A `  x )
) ) )
170157, 164, 1693eqtr4d 2325 . . . . . . . . 9  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( ( y  o F ( +g  `  R
) z ) `  x )  .x.  ( A `  x )
)  =  ( ( ( y  o F 
.x.  A ) `  x ) ( +g  `  T ) ( ( z  o F  .x.  A ) `  x
) ) )
171130adantr 451 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
y  o F ( +g  `  R ) z )  Fn  I
)
172 fnfvof 6090 . . . . . . . . . 10  |-  ( ( ( ( y  o F ( +g  `  R
) z )  Fn  I  /\  A  Fn  I )  /\  (
I  e.  X  /\  x  e.  I )
)  ->  ( (
( y  o F ( +g  `  R
) z )  o F  .x.  A ) `
 x )  =  ( ( ( y  o F ( +g  `  R ) z ) `
 x )  .x.  ( A `  x ) ) )
173171, 165, 160, 161, 172syl22anc 1183 . . . . . . . . 9  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( ( y  o F ( +g  `  R
) z )  o F  .x.  A ) `
 x )  =  ( ( ( y  o F ( +g  `  R ) z ) `
 x )  .x.  ( A `  x ) ) )
174135adantr 451 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
y  o F  .x.  A )  Fn  I
)
175138adantr 451 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
z  o F  .x.  A )  Fn  I
)
176 fnfvof 6090 . . . . . . . . . 10  |-  ( ( ( ( y  o F  .x.  A )  Fn  I  /\  (
z  o F  .x.  A )  Fn  I
)  /\  ( I  e.  X  /\  x  e.  I ) )  -> 
( ( ( y  o F  .x.  A
)  o F ( +g  `  T ) ( z  o F 
.x.  A ) ) `
 x )  =  ( ( ( y  o F  .x.  A
) `  x )
( +g  `  T ) ( ( z  o F  .x.  A ) `
 x ) ) )
177174, 175, 160, 161, 176syl22anc 1183 . . . . . . . . 9  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( ( y  o F  .x.  A )  o F ( +g  `  T ) ( z  o F  .x.  A
) ) `  x
)  =  ( ( ( y  o F 
.x.  A ) `  x ) ( +g  `  T ) ( ( z  o F  .x.  A ) `  x
) ) )
178170, 173, 1773eqtr4d 2325 . . . . . . . 8  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( ( y  o F ( +g  `  R
) z )  o F  .x.  A ) `
 x )  =  ( ( ( y  o F  .x.  A
)  o F ( +g  `  T ) ( z  o F 
.x.  A ) ) `
 x ) )
179132, 139, 178eqfnfvd 5625 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( ( y  o F ( +g  `  R
) z )  o F  .x.  A )  =  ( ( y  o F  .x.  A
)  o F ( +g  `  T ) ( z  o F 
.x.  A ) ) )
180122, 179eqtrd 2315 . . . . . 6  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( ( y ( +g  `  F ) z )  o F 
.x.  A )  =  ( ( y  o F  .x.  A )  o F ( +g  `  T ) ( z  o F  .x.  A
) ) )
181180oveq2d 5874 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( T  gsumg  ( ( y ( +g  `  F ) z )  o F 
.x.  A ) )  =  ( T  gsumg  ( ( y  o F  .x.  A )  o F ( +g  `  T
) ( z  o F  .x.  A ) ) ) )
182116, 181eqtrd 2315 . . . 4  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( E `  (
y ( +g  `  F
) z ) )  =  ( T  gsumg  ( ( y  o F  .x.  A )  o F ( +g  `  T
) ( z  o F  .x.  A ) ) ) )
183 oveq1 5865 . . . . . . . 8  |-  ( x  =  y  ->  (
x  o F  .x.  A )  =  ( y  o F  .x.  A ) )
184183oveq2d 5874 . . . . . . 7  |-  ( x  =  y  ->  ( T  gsumg  ( x  o F 
.x.  A ) )  =  ( T  gsumg  ( y  o F  .x.  A
) ) )
185 ovex 5883 . . . . . . 7  |-  ( T 
gsumg  ( y  o F 
.x.  A ) )  e.  _V
186184, 89, 185fvmpt 5602 . . . . . 6  |-  ( y  e.  B  ->  ( E `  y )  =  ( T  gsumg  ( y  o F  .x.  A
) ) )
187186ad2antrl 708 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( E `  y
)  =  ( T 
gsumg  ( y  o F 
.x.  A ) ) )
188 oveq1 5865 . . . . . . . 8  |-  ( x  =  z  ->  (
x  o F  .x.  A )  =  ( z  o F  .x.  A ) )
189188oveq2d 5874 . . . . . . 7  |-  ( x  =  z  ->  ( T  gsumg  ( x  o F 
.x.  A ) )  =  ( T  gsumg  ( z  o F  .x.  A
) ) )
190 ovex 5883 . . . . . . 7  |-  ( T 
gsumg  ( z  o F 
.x.  A ) )  e.  _V
191189, 89, 190fvmpt 5602 . . . . . 6  |-  ( z  e.  B  ->  ( E `  z )  =  ( T  gsumg  ( z  o F  .x.  A
) ) )
192191ad2antll 709 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( E `  z
)  =  ( T 
gsumg  ( z  o F 
.x.  A ) ) )
193187, 192oveq12d 5876 . . . 4  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( ( E `  y ) ( +g  `  T ) ( E `
 z ) )  =  ( ( T 
gsumg  ( y  o F 
.x.  A ) ) ( +g  `  T
) ( T  gsumg  ( z  o F  .x.  A
) ) ) )
194108, 182, 1933eqtr4d 2325 . . 3  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( E `  (
y ( +g  `  F
) z ) )  =  ( ( E `
 y ) ( +g  `  T ) ( E `  z
) ) )
1951, 19, 20, 21, 23, 25, 90, 194isghmd 14692 . 2  |-  ( ph  ->  E  e.  ( F 
GrpHom  T ) )
1968adantr 451 . . . . 5  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  T  e.  LMod )
19712adantr 451 . . . . 5  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  I  e.  X )
19818fveq2d 5529 . . . . . . . 8  |-  ( ph  ->  ( Base `  (Scalar `  T ) )  =  ( Base `  (Scalar `  F ) ) )
199198eleq2d 2350 . . . . . . 7  |-  ( ph  ->  ( y  e.  (
Base `  (Scalar `  T
) )  <->  y  e.  ( Base `  (Scalar `  F
) ) ) )
200199biimpar 471 . . . . . 6  |-  ( (
ph  /\  y  e.  ( Base `  (Scalar `  F
) ) )  -> 
y  e.  ( Base `  (Scalar `  T )
) )
201200adantrr 697 . . . . 5  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  y  e.  ( Base `  (Scalar `  T
) ) )
20252adantrl 696 . . . . . 6  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( z  o F  .x.  A ) : I --> C )
203 ffvelrn 5663 . . . . . 6  |-  ( ( ( z  o F 
.x.  A ) : I --> C  /\  x  e.  I )  ->  (
( z  o F 
.x.  A ) `  x )  e.  C
)
204202, 203sylan 457 . . . . 5  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( ( z  o F  .x.  A ) `
 x )  e.  C )
20552feqmptd 5575 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  B )  ->  (
z  o F  .x.  A )  =  ( x  e.  I  |->  ( ( z  o F 
.x.  A ) `  x ) ) )
206205cnveqd 4857 . . . . . . . 8  |-  ( (
ph  /\  z  e.  B )  ->  `' ( z  o F 
.x.  A )  =  `' ( x  e.  I  |->  ( ( z  o F  .x.  A
) `  x )
) )
207206imaeq1d 5011 . . . . . . 7  |-  ( (
ph  /\  z  e.  B )  ->  ( `' ( z  o F  .x.  A )
" ( _V  \  { ( 0g `  T ) } ) )  =  ( `' ( x  e.  I  |->  ( ( z  o F  .x.  A ) `
 x ) )
" ( _V  \  { ( 0g `  T ) } ) ) )
208207, 86eqeltrrd 2358 . . . . . 6  |-  ( (
ph  /\  z  e.  B )  ->  ( `' ( x  e.  I  |->  ( ( z  o F  .x.  A
) `  x )
) " ( _V 
\  { ( 0g
`  T ) } ) )  e.  Fin )
209208adantrl 696 . . . . 5  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( `' ( x  e.  I  |->  ( ( z  o F  .x.  A ) `
 x ) )
" ( _V  \  { ( 0g `  T ) } ) )  e.  Fin )
21019, 5, 43, 32, 21, 3, 196, 197, 201, 204, 209gsumvsmul 26764 . . . 4  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( T  gsumg  ( x  e.  I  |->  ( y  .x.  ( ( z  o F  .x.  A ) `  x
) ) ) )  =  ( y  .x.  ( T  gsumg  ( x  e.  I  |->  ( ( z  o F  .x.  A ) `
 x ) ) ) ) )
21115adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  F  e.  LMod )
212 simprl 732 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  y  e.  ( Base `  (Scalar `  F
) ) )
213 simprr 733 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  z  e.  B )
2141, 4, 2, 6lmodvscl 15644 . . . . . . . . . . . 12  |-  ( ( F  e.  LMod  /\  y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )  ->  ( y ( .s
`  F ) z )  e.  B )
215211, 212, 213, 214syl3anc 1182 . . . . . . . . . . 11  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( y
( .s `  F
) z )  e.  B )
21613, 46, 1frlmbasf 27228 . . . . . . . . . . 11  |-  ( ( I  e.  X  /\  ( y ( .s
`  F ) z )  e.  B )  ->  ( y ( .s `  F ) z ) : I --> ( Base `  R
) )
217197, 215, 216syl2anc 642 . . . . . . . . . 10  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( y
( .s `  F
) z ) : I --> ( Base `  R
) )
218 ffn 5389 . . . . . . . . . 10  |-  ( ( y ( .s `  F ) z ) : I --> ( Base `  R )  ->  (
y ( .s `  F ) z )  Fn  I )
219217, 218syl 15 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( y
( .s `  F
) z )  Fn  I )
22066adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  A  Fn  I )
221219, 220, 197, 197, 51offn 6089 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( (
y ( .s `  F ) z )  o F  .x.  A
)  Fn  I )
222 dffn2 5390 . . . . . . . 8  |-  ( ( ( y ( .s
`  F ) z )  o F  .x.  A )  Fn  I  <->  ( ( y ( .s
`  F ) z )  o F  .x.  A ) : I --> _V )
223221, 222sylib 188 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( (
y ( .s `  F ) z )  o F  .x.  A
) : I --> _V )
224223feqmptd 5575 . . . . . 6  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( (
y ( .s `  F ) z )  o F  .x.  A
)  =  ( x  e.  I  |->  ( ( ( y ( .s
`  F ) z )  o F  .x.  A ) `  x
) ) )
2257fveq2d 5529 . . . . . . . . . . . 12  |-  ( ph  ->  ( .r `  R
)  =  ( .r
`  (Scalar `  T )
) )
226225ad2antrr 706 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( .r `  R
)  =  ( .r
`  (Scalar `  T )
) )
227226oveqd 5875 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( y ( .r
`  R ) ( z `  x ) )  =  ( y ( .r `  (Scalar `  T ) ) ( z `  x ) ) )
228227oveq1d 5873 . . . . . . . . 9  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( ( y ( .r `  R ) ( z `  x
) )  .x.  ( A `  x )
)  =  ( ( y ( .r `  (Scalar `  T ) ) ( z `  x
) )  .x.  ( A `  x )
) )
2298ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  T  e.  LMod )
230 simplrl 736 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  y  e.  ( Base `  (Scalar `  F )
) )
231198ad2antrr 706 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( Base `  (Scalar `  T ) )  =  ( Base `  (Scalar `  F ) ) )
232230, 231eleqtrrd 2360 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  y  e.  ( Base `  (Scalar `  T )
) )
23348, 149sylan 457 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  I )  ->  (
z `  x )  e.  ( Base `  R
) )
23439ad2antrr 706 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  I )  ->  ( Base `  R )  =  ( Base `  (Scalar `  T ) ) )
235233, 234eleqtrd 2359 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  I )  ->  (
z `  x )  e.  ( Base `  (Scalar `  T ) ) )
236235adantlrl 700 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( z `  x
)  e.  ( Base `  (Scalar `  T )
) )
23749, 78sylan 457 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  I )  ->  ( A `  x )  e.  C )
238237adantlr 695 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( A `  x
)  e.  C )
239 eqid 2283 . . . . . . . . . . 11  |-  ( .r
`  (Scalar `  T )
)  =  ( .r
`  (Scalar `  T )
)
24019, 5, 3, 43, 239lmodvsass 15654 . . . . . . . . . 10  |-  ( ( T  e.  LMod  /\  (
y  e.  ( Base `  (Scalar `  T )
)  /\  ( z `  x )  e.  (
Base `  (Scalar `  T
) )  /\  ( A `  x )  e.  C ) )  -> 
( ( y ( .r `  (Scalar `  T ) ) ( z `  x ) )  .x.  ( A `
 x ) )  =  ( y  .x.  ( ( z `  x )  .x.  ( A `  x )
) ) )
241229, 232, 236, 238, 240syl13anc 1184 . . . . . . . . 9  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( ( y ( .r `  (Scalar `  T ) ) ( z `  x ) )  .x.  ( A `
 x ) )  =  ( y  .x.  ( ( z `  x )  .x.  ( A `  x )
) ) )
242228, 241eqtrd 2315 . . . . . . . 8  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( ( y ( .r `  R ) ( z `  x
) )  .x.  ( A `  x )
)  =  ( y 
.x.  ( ( z `
 x )  .x.  ( A `  x ) ) ) )
243219adantr 451 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( y ( .s
`  F ) z )  Fn  I )
24466ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  A  Fn  I )
24512ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  I  e.  X )
246 simpr 447 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  x  e.  I )
247 fnfvof 6090 . . . . . . . . . 10  |-  ( ( ( ( y ( .s `  F ) z )  Fn  I  /\  A  Fn  I
)  /\  ( I  e.  X  /\  x  e.  I ) )  -> 
( ( ( y ( .s `  F
) z )  o F  .x.  A ) `
 x )  =  ( ( ( y ( .s `  F
) z ) `  x )  .x.  ( A `  x )
) )
248243, 244, 245, 246, 247syl22anc 1183 . . . . . . . . 9  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( ( ( y ( .s `  F
) z )  o F  .x.  A ) `
 x )  =  ( ( ( y ( .s `  F
) z ) `  x )  .x.  ( A `  x )
) )
24917fveq2d 5529 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Base `  R
)  =  ( Base `  (Scalar `  F )
) )
250249ad2antrr 706 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( Base `  R
)  =  ( Base `  (Scalar `  F )
) )
251230, 250eleqtrrd 2360 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  y  e.  ( Base `  R ) )
252 simplrr 737 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  z  e.  B )
253 eqid 2283 . . . . . . . . . . 11  |-  ( .r
`  R )  =  ( .r `  R
)
25413, 1, 46, 245, 251, 252, 246, 2, 253frlmvscaval 27231 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( ( y ( .s `  F ) z ) `  x
)  =  ( y ( .r `  R
) ( z `  x ) ) )
255254oveq1d 5873 . . . . . . . . 9  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( ( ( y ( .s `  F
) z ) `  x )  .x.  ( A `  x )
)  =  ( ( y ( .r `  R ) ( z `
 x ) ) 
.x.  ( A `  x ) ) )
256248, 255eqtrd 2315 . . . . . . . 8  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( ( ( y ( .s `  F
) z )  o F  .x.  A ) `
 x )  =  ( ( y ( .r `  R ) ( z `  x
) )  .x.  ( A `  x )
) )
25763adantrl 696 . . . . . . . . . . 11  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  z  Fn  I )
258257adantr 451 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  z  Fn  I )
259258, 244, 245, 246, 71syl22anc 1183 . . . . . . . . 9  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( ( z  o F  .x.  A ) `
 x )  =  ( ( z `  x )  .x.  ( A `  x )
) )
260259oveq2d 5874 . . . . . . . 8  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( y  .x.  (
( z  o F 
.x.  A ) `  x ) )  =  ( y  .x.  (
( z `  x
)  .x.  ( A `  x ) ) ) )
261242, 256, 2603eqtr4d 2325 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( ( ( y ( .s `  F
) z )  o F  .x.  A ) `
 x )  =  ( y  .x.  (
( z  o F 
.x.  A ) `  x ) ) )
262261mpteq2dva 4106 . . . . . 6  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( x  e.  I  |->  ( ( ( y ( .s
`  F ) z )  o F  .x.  A ) `  x
) )  =  ( x  e.  I  |->  ( y  .x.  ( ( z  o F  .x.  A ) `  x
) ) ) )
263224, 262eqtrd 2315 . . . . 5  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( (
y ( .s `  F ) z )  o F  .x.  A
)  =  ( x  e.  I  |->  ( y 
.x.  ( ( z  o F  .x.  A
) `  x )
) ) )
264263oveq2d 5874 . . . 4  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( T  gsumg  ( ( y ( .s
`  F ) z )  o F  .x.  A ) )  =  ( T  gsumg  ( x  e.  I  |->  ( y  .x.  (
( z  o F 
.x.  A ) `  x ) ) ) ) )
265202feqmptd 5575 . . . . . 6  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( z  o F  .x.  A )  =  ( x  e.  I  |->  ( ( z  o F  .x.  A
) `  x )
) )
266265oveq2d 5874 . . . . 5  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( T  gsumg  ( z  o F  .x.  A ) )  =  ( T  gsumg  ( x  e.  I  |->  ( ( z  o F  .x.  A ) `
 x ) ) ) )
267266oveq2d 5874 . . . 4  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( y  .x.  ( T  gsumg  ( z  o F 
.x.  A ) ) )  =  ( y 
.x.  ( T  gsumg  ( x  e.  I  |->  ( ( z  o F  .x.  A ) `  x
) ) ) ) )
268210, 264, 2673eqtr4d 2325 . . 3  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( T  gsumg  ( ( y ( .s
`  F ) z )  o F  .x.  A ) )  =  ( y  .x.  ( T  gsumg  ( z  o F 
.x.  A ) ) ) )
269 oveq1 5865 . . . . . 6  |-  ( x  =  ( y ( .s `  F ) z )  ->  (
x  o F  .x.  A )  =  ( ( y ( .s
`  F ) z )  o F  .x.  A ) )
270269oveq2d 5874 . . . . 5  |-  ( x  =  ( y ( .s `  F ) z )  ->  ( T  gsumg  ( x  o F 
.x.  A ) )  =  ( T  gsumg  ( ( y ( .s `  F ) z )  o F  .x.  A
) ) )
271 ovex 5883 . . . . 5  |-  ( T 
gsumg  ( ( y ( .s `  F ) z )  o F 
.x.  A ) )  e.  _V
272270, 89, 271fvmpt 5602 . . . 4  |-  ( ( y ( .s `  F ) z )  e.  B  ->  ( E `  ( y
( .s `  F
) z ) )  =  ( T  gsumg  ( ( y ( .s `  F ) z )  o F  .x.  A
) ) )
273215, 272syl 15 . . 3  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( E `  ( y ( .s
`  F ) z ) )  =  ( T  gsumg  ( ( y ( .s `  F ) z )  o F 
.x.  A ) ) )
274191oveq2d 5874 . . . 4  |-  ( z  e.  B  ->  (
y  .x.  ( E `  z ) )  =  ( y  .x.  ( T  gsumg  ( z  o F 
.x.  A ) ) ) )
275274ad2antll 709 . . 3  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( y  .x.  ( E `  z
) )  =  ( y  .x.  ( T 
gsumg  ( z  o F 
.x.  A ) ) ) )
276268, 273, 2753eqtr4d 2325 . 2  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( E `  ( y ( .s
`  F ) z ) )  =  ( y  .x.  ( E `
 z ) ) )
2771, 2, 3, 4, 5, 6, 15, 8, 18, 195, 276islmhmd 15796 1  |-  ( ph  ->  E  e.  ( F LMHom 
T ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    e. wcel 1684   _Vcvv 2788    \ cdif 3149    C_ wss 3152   {csn 3640    e. cmpt 4077   `'ccnv 4688   "cima 4692    Fn wfn 5250   -->wf 5251   ` cfv 5255  (class class class)co 5858    o Fcof 6076   Fincfn 6863   Basecbs 13148   +g cplusg 13208   .rcmulr 13209  Scalarcsca 13211   .scvsca 13212   0gc0g 13400    gsumg cgsu 13401   Grpcgrp 14362  CMndccmn 15089   Ringcrg 15337   LModclmod 15627   LMHom clmhm 15776   freeLMod cfrlm 27212
This theorem is referenced by:  frlmup3  27252  frlmup4  27253  islindf5  27309  indlcim  27310  lnrfg  27323
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-se 4353  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-isom 5264  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-of 6078  df-1st 6122  df-2nd 6123  df-riota 6304  df-recs 6388  df-rdg 6423  df-1o 6479  df-oadd 6483  df-er 6660  df-map 6774  df-ixp 6818  df-en 6864  df-dom 6865  df-sdom 6866  df-fin 6867  df-sup 7194  df-oi 7225  df-card 7572  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-nn 9747  df-2 9804  df-3 9805  df-4 9806  df-5 9807  df-6 9808  df-7 9809  df-8 9810  df-9 9811  df-10 9812  df-n0 9966  df-z 10025  df-dec 10125  df-uz 10231  df-fz 10783  df-fzo 10871  df-seq 11047  df-hash 11338  df-struct 13150  df-ndx 13151  df-slot 13152  df-base 13153  df-sets 13154  df-ress 13155  df-plusg 13221  df-mulr 13222  df-sca 13224  df-vsca 13225  df-tset 13227  df-ple 13228  df-ds 13230  df-hom 13232  df-cco 13233  df-prds 13348  df-pws 13350  df-0g 13404  df-gsum 13405  df-mnd 14367  df-mhm 14415  df-submnd 14416  df-grp 14489  df-minusg 14490  df-sbg 14491  df-subg 14618  df-ghm 14681  df-cntz 14793  df-cmn 15091  df-abl 15092  df-mgp 15326  df-rng 15340  df-ur 15342  df-subrg 15543  df-lmod 15629  df-lss 15690  df-lmhm 15779  df-sra 15925  df-rgmod 15926  df-dsmm 27198  df-frlm 27214
  Copyright terms: Public domain W3C validator