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

Theorem frlmup1 27118
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 2404 . 2  |-  ( .s
`  F )  =  ( .s `  F
)
3 frlmup.v . 2  |-  .x.  =  ( .s `  T )
4 eqid 2404 . 2  |-  (Scalar `  F )  =  (Scalar `  F )
5 eqid 2404 . 2  |-  (Scalar `  T )  =  (Scalar `  T )
6 eqid 2404 . 2  |-  ( Base `  (Scalar `  F )
)  =  ( Base `  (Scalar `  F )
)
7 frlmup.r . . . 4  |-  ( ph  ->  R  =  (Scalar `  T ) )
8 frlmup.t . . . . 5  |-  ( ph  ->  T  e.  LMod )
95lmodrng 15913 . . . . 5  |-  ( T  e.  LMod  ->  (Scalar `  T )  e.  Ring )
108, 9syl 16 . . . 4  |-  ( ph  ->  (Scalar `  T )  e.  Ring )
117, 10eqeltrd 2478 . . 3  |-  ( ph  ->  R  e.  Ring )
12 frlmup.i . . 3  |-  ( ph  ->  I  e.  X )
13 frlmup.f . . . 4  |-  F  =  ( R freeLMod  I )
1413frlmlmod 27085 . . 3  |-  ( ( R  e.  Ring  /\  I  e.  X )  ->  F  e.  LMod )
1511, 12, 14syl2anc 643 . 2  |-  ( ph  ->  F  e.  LMod )
1613frlmsca 27089 . . . 4  |-  ( ( R  e.  Ring  /\  I  e.  X )  ->  R  =  (Scalar `  F )
)
1711, 12, 16syl2anc 643 . . 3  |-  ( ph  ->  R  =  (Scalar `  F ) )
187, 17eqtr3d 2438 . 2  |-  ( ph  ->  (Scalar `  T )  =  (Scalar `  F )
)
19 frlmup.c . . 3  |-  C  =  ( Base `  T
)
20 eqid 2404 . . 3  |-  ( +g  `  F )  =  ( +g  `  F )
21 eqid 2404 . . 3  |-  ( +g  `  T )  =  ( +g  `  T )
22 lmodgrp 15912 . . . 4  |-  ( F  e.  LMod  ->  F  e. 
Grp )
2315, 22syl 16 . . 3  |-  ( ph  ->  F  e.  Grp )
24 lmodgrp 15912 . . . 4  |-  ( T  e.  LMod  ->  T  e. 
Grp )
258, 24syl 16 . . 3  |-  ( ph  ->  T  e.  Grp )
26 eleq1 2464 . . . . . . 7  |-  ( z  =  x  ->  (
z  e.  B  <->  x  e.  B ) )
2726anbi2d 685 . . . . . 6  |-  ( z  =  x  ->  (
( ph  /\  z  e.  B )  <->  ( ph  /\  x  e.  B ) ) )
28 oveq1 6047 . . . . . . . 8  |-  ( z  =  x  ->  (
z  o F  .x.  A )  =  ( x  o F  .x.  A ) )
2928oveq2d 6056 . . . . . . 7  |-  ( z  =  x  ->  ( T  gsumg  ( z  o F 
.x.  A ) )  =  ( T  gsumg  ( x  o F  .x.  A
) ) )
3029eleq1d 2470 . . . . . 6  |-  ( z  =  x  ->  (
( T  gsumg  ( z  o F 
.x.  A ) )  e.  C  <->  ( T  gsumg  ( x  o F  .x.  A ) )  e.  C ) )
3127, 30imbi12d 312 . . . . 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 2404 . . . . . 6  |-  ( 0g
`  T )  =  ( 0g `  T
)
33 lmodcmn 15947 . . . . . . . 8  |-  ( T  e.  LMod  ->  T  e. CMnd
)
348, 33syl 16 . . . . . . 7  |-  ( ph  ->  T  e. CMnd )
3534adantr 452 . . . . . 6  |-  ( (
ph  /\  z  e.  B )  ->  T  e. CMnd )
3612adantr 452 . . . . . 6  |-  ( (
ph  /\  z  e.  B )  ->  I  e.  X )
378ad2antrr 707 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  B )  /\  (
x  e.  ( Base `  R )  /\  y  e.  C ) )  ->  T  e.  LMod )
38 simprl 733 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  B )  /\  (
x  e.  ( Base `  R )  /\  y  e.  C ) )  ->  x  e.  ( Base `  R ) )
397fveq2d 5691 . . . . . . . . . 10  |-  ( ph  ->  ( Base `  R
)  =  ( Base `  (Scalar `  T )
) )
4039ad2antrr 707 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  B )  /\  (
x  e.  ( Base `  R )  /\  y  e.  C ) )  -> 
( Base `  R )  =  ( Base `  (Scalar `  T ) ) )
4138, 40eleqtrd 2480 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  B )  /\  (
x  e.  ( Base `  R )  /\  y  e.  C ) )  ->  x  e.  ( Base `  (Scalar `  T )
) )
42 simprr 734 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  B )  /\  (
x  e.  ( Base `  R )  /\  y  e.  C ) )  -> 
y  e.  C )
43 eqid 2404 . . . . . . . . 9  |-  ( Base `  (Scalar `  T )
)  =  ( Base `  (Scalar `  T )
)
4419, 5, 3, 43lmodvscl 15922 . . . . . . . 8  |-  ( ( T  e.  LMod  /\  x  e.  ( Base `  (Scalar `  T ) )  /\  y  e.  C )  ->  ( x  .x.  y
)  e.  C )
4537, 41, 42, 44syl3anc 1184 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  B )  /\  (
x  e.  ( Base `  R )  /\  y  e.  C ) )  -> 
( x  .x.  y
)  e.  C )
46 eqid 2404 . . . . . . . . 9  |-  ( Base `  R )  =  (
Base `  R )
4713, 46, 1frlmbasf 27096 . . . . . . . 8  |-  ( ( I  e.  X  /\  z  e.  B )  ->  z : I --> ( Base `  R ) )
4812, 47sylan 458 . . . . . . 7  |-  ( (
ph  /\  z  e.  B )  ->  z : I --> ( Base `  R ) )
49 frlmup.a . . . . . . . 8  |-  ( ph  ->  A : I --> C )
5049adantr 452 . . . . . . 7  |-  ( (
ph  /\  z  e.  B )  ->  A : I --> C )
51 inidm 3510 . . . . . . 7  |-  ( I  i^i  I )  =  I
5245, 48, 50, 36, 36, 51off 6279 . . . . . 6  |-  ( (
ph  /\  z  e.  B )  ->  (
z  o F  .x.  A ) : I --> C )
537fveq2d 5691 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0g `  R
)  =  ( 0g
`  (Scalar `  T )
) )
5453sneqd 3787 . . . . . . . . . . 11  |-  ( ph  ->  { ( 0g `  R ) }  =  { ( 0g `  (Scalar `  T ) ) } )
5554difeq2d 3425 . . . . . . . . . 10  |-  ( ph  ->  ( _V  \  {
( 0g `  R
) } )  =  ( _V  \  {
( 0g `  (Scalar `  T ) ) } ) )
5655imaeq2d 5162 . . . . . . . . 9  |-  ( ph  ->  ( `' z "
( _V  \  {
( 0g `  R
) } ) )  =  ( `' z
" ( _V  \  { ( 0g `  (Scalar `  T ) ) } ) ) )
5756adantr 452 . . . . . . . 8  |-  ( (
ph  /\  z  e.  B )  ->  ( `' z " ( _V  \  { ( 0g
`  R ) } ) )  =  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) )
58 eqid 2404 . . . . . . . . . 10  |-  ( 0g
`  R )  =  ( 0g `  R
)
5913, 58, 1frlmbassup 27094 . . . . . . . . 9  |-  ( ( I  e.  X  /\  z  e.  B )  ->  ( `' z "
( _V  \  {
( 0g `  R
) } ) )  e.  Fin )
6012, 59sylan 458 . . . . . . . 8  |-  ( (
ph  /\  z  e.  B )  ->  ( `' z " ( _V  \  { ( 0g
`  R ) } ) )  e.  Fin )
6157, 60eqeltrrd 2479 . . . . . . 7  |-  ( (
ph  /\  z  e.  B )  ->  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) )  e.  Fin )
62 ffn 5550 . . . . . . . . . . . 12  |-  ( z : I --> ( Base `  R )  ->  z  Fn  I )
6348, 62syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  B )  ->  z  Fn  I )
6463adantr 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  ( I  \  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) ) )  ->  z  Fn  I )
65 ffn 5550 . . . . . . . . . . . 12  |-  ( A : I --> C  ->  A  Fn  I )
6649, 65syl 16 . . . . . . . . . . 11  |-  ( ph  ->  A  Fn  I )
6766ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  ( I  \  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) ) )  ->  A  Fn  I )
6812ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  ( I  \  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) ) )  ->  I  e.  X )
69 eldifi 3429 . . . . . . . . . . 11  |-  ( x  e.  ( I  \ 
( `' z "
( _V  \  {
( 0g `  (Scalar `  T ) ) } ) ) )  ->  x  e.  I )
7069adantl 453 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  ( I  \  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) ) )  ->  x  e.  I )
71 fnfvof 6276 . . . . . . . . . 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 1185 . . . . . . . . 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 3327 . . . . . . . . . . . 12  |-  ( `' z " ( _V 
\  { ( 0g
`  (Scalar `  T )
) } ) ) 
C_  ( `' z
" ( _V  \  { ( 0g `  (Scalar `  T ) ) } ) )
7473a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  z  e.  B )  ->  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) 
C_  ( `' z
" ( _V  \  { ( 0g `  (Scalar `  T ) ) } ) ) )
7548, 74suppssr 5823 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  ( I  \  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) ) )  ->  (
z `  x )  =  ( 0g `  (Scalar `  T ) ) )
7675oveq1d 6055 . . . . . . . . 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 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  ( I  \  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) ) )  ->  T  e.  LMod )
78 ffvelrn 5827 . . . . . . . . . . 11  |-  ( ( A : I --> C  /\  x  e.  I )  ->  ( A `  x
)  e.  C )
7950, 69, 78syl2an 464 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  ( I  \  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) ) )  ->  ( A `  x )  e.  C )
80 eqid 2404 . . . . . . . . . . 11  |-  ( 0g
`  (Scalar `  T )
)  =  ( 0g
`  (Scalar `  T )
)
8119, 5, 3, 80, 32lmod0vs 15938 . . . . . . . . . 10  |-  ( ( T  e.  LMod  /\  ( A `  x )  e.  C )  ->  (
( 0g `  (Scalar `  T ) )  .x.  ( A `  x ) )  =  ( 0g
`  T ) )
8277, 79, 81syl2anc 643 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  ( I  \  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) ) )  ->  (
( 0g `  (Scalar `  T ) )  .x.  ( A `  x ) )  =  ( 0g
`  T ) )
8372, 76, 823eqtrd 2440 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  ( I  \  ( `' z " ( _V  \  { ( 0g
`  (Scalar `  T )
) } ) ) ) )  ->  (
( z  o F 
.x.  A ) `  x )  =  ( 0g `  T ) )
8452, 83suppss 5822 . . . . . . 7  |-  ( (
ph  /\  z  e.  B )  ->  ( `' ( z  o F  .x.  A )
" ( _V  \  { ( 0g `  T ) } ) )  C_  ( `' z " ( _V  \  { ( 0g `  (Scalar `  T ) ) } ) ) )
85 ssfi 7288 . . . . . . 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 643 . . . . . 6  |-  ( (
ph  /\  z  e.  B )  ->  ( `' ( z  o F  .x.  A )
" ( _V  \  { ( 0g `  T ) } ) )  e.  Fin )
8719, 32, 35, 36, 52, 86gsumcl 15476 . . . . 5  |-  ( (
ph  /\  z  e.  B )  ->  ( T  gsumg  ( z  o F 
.x.  A ) )  e.  C )
8831, 87chvarv 2063 . . . 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 5852 . . 3  |-  ( ph  ->  E : B --> C )
9134adantr 452 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  ->  T  e. CMnd )
9212adantr 452 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  ->  I  e.  X )
93 eleq1 2464 . . . . . . . . 9  |-  ( z  =  y  ->  (
z  e.  B  <->  y  e.  B ) )
9493anbi2d 685 . . . . . . . 8  |-  ( z  =  y  ->  (
( ph  /\  z  e.  B )  <->  ( ph  /\  y  e.  B ) ) )
95 oveq1 6047 . . . . . . . . 9  |-  ( z  =  y  ->  (
z  o F  .x.  A )  =  ( y  o F  .x.  A ) )
9695feq1d 5539 . . . . . . . 8  |-  ( z  =  y  ->  (
( z  o F 
.x.  A ) : I --> C  <->  ( y  o F  .x.  A ) : I --> C ) )
9794, 96imbi12d 312 . . . . . . 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 2063 . . . . . 6  |-  ( (
ph  /\  y  e.  B )  ->  (
y  o F  .x.  A ) : I --> C )
9998adantrr 698 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( y  o F 
.x.  A ) : I --> C )
10052adantrl 697 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( z  o F 
.x.  A ) : I --> C )
10195cnveqd 5007 . . . . . . . . . 10  |-  ( z  =  y  ->  `' ( z  o F 
.x.  A )  =  `' ( y  o F  .x.  A ) )
102101imaeq1d 5161 . . . . . . . . 9  |-  ( z  =  y  ->  ( `' ( z  o F  .x.  A )
" ( _V  \  { ( 0g `  T ) } ) )  =  ( `' ( y  o F 
.x.  A ) "
( _V  \  {
( 0g `  T
) } ) ) )
103102eleq1d 2470 . . . . . . . 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 312 . . . . . . 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 2063 . . . . . 6  |-  ( (
ph  /\  y  e.  B )  ->  ( `' ( y  o F  .x.  A )
" ( _V  \  { ( 0g `  T ) } ) )  e.  Fin )
106105adantrr 698 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( `' ( y  o F  .x.  A
) " ( _V 
\  { ( 0g
`  T ) } ) )  e.  Fin )
10786adantrl 697 . . . . 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 15483 . . . 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 15919 . . . . . . . 8  |-  ( ( F  e.  LMod  /\  y  e.  B  /\  z  e.  B )  ->  (
y ( +g  `  F
) z )  e.  B )
1101093expb 1154 . . . . . . 7  |-  ( ( F  e.  LMod  /\  (
y  e.  B  /\  z  e.  B )
)  ->  ( y
( +g  `  F ) z )  e.  B
)
11115, 110sylan 458 . . . . . 6  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( y ( +g  `  F ) z )  e.  B )
112 oveq1 6047 . . . . . . . 8  |-  ( x  =  ( y ( +g  `  F ) z )  ->  (
x  o F  .x.  A )  =  ( ( y ( +g  `  F ) z )  o F  .x.  A
) )
113112oveq2d 6056 . . . . . . 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 6065 . . . . . . 7  |-  ( T 
gsumg  ( ( y ( +g  `  F ) z )  o F 
.x.  A ) )  e.  _V
115113, 89, 114fvmpt 5765 . . . . . 6  |-  ( ( y ( +g  `  F
) z )  e.  B  ->  ( E `  ( y ( +g  `  F ) z ) )  =  ( T 
gsumg  ( ( y ( +g  `  F ) z )  o F 
.x.  A ) ) )
116111, 115syl 16 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( E `  (
y ( +g  `  F
) z ) )  =  ( T  gsumg  ( ( y ( +g  `  F
) z )  o F  .x.  A ) ) )
11711adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  ->  R  e.  Ring )
118 simprl 733 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
y  e.  B )
119 simprr 734 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
z  e.  B )
120 eqid 2404 . . . . . . . . 9  |-  ( +g  `  R )  =  ( +g  `  R )
12113, 1, 117, 92, 118, 119, 120, 20frlmplusgval 27097 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( y ( +g  `  F ) z )  =  ( y  o F ( +g  `  R
) z ) )
122121oveq1d 6055 . . . . . . 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 27096 . . . . . . . . . . . . 13  |-  ( ( I  e.  X  /\  y  e.  B )  ->  y : I --> ( Base `  R ) )
12412, 123sylan 458 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  B )  ->  y : I --> ( Base `  R ) )
125124adantrr 698 . . . . . . . . . . 11  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
y : I --> ( Base `  R ) )
126 ffn 5550 . . . . . . . . . . 11  |-  ( y : I --> ( Base `  R )  ->  y  Fn  I )
127125, 126syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
y  Fn  I )
12848adantrl 697 . . . . . . . . . . 11  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
z : I --> ( Base `  R ) )
129128, 62syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
z  Fn  I )
130127, 129, 92, 92, 51offn 6275 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( y  o F ( +g  `  R
) z )  Fn  I )
13166adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  ->  A  Fn  I )
132130, 131, 92, 92, 51offn 6275 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( ( y  o F ( +g  `  R
) z )  o F  .x.  A )  Fn  I )
133 ffn 5550 . . . . . . . . . . 11  |-  ( ( y  o F  .x.  A ) : I --> C  ->  ( y  o F  .x.  A )  Fn  I )
13498, 133syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  B )  ->  (
y  o F  .x.  A )  Fn  I
)
135134adantrr 698 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( y  o F 
.x.  A )  Fn  I )
136 ffn 5550 . . . . . . . . . . 11  |-  ( ( z  o F  .x.  A ) : I --> C  ->  ( z  o F  .x.  A )  Fn  I )
13752, 136syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  B )  ->  (
z  o F  .x.  A )  Fn  I
)
138137adantrl 697 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( z  o F 
.x.  A )  Fn  I )
139135, 138, 92, 92, 51offn 6275 . . . . . . . 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 5691 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( +g  `  R
)  =  ( +g  `  (Scalar `  T )
) )
141140ad2antrr 707 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  ( +g  `  R )  =  ( +g  `  (Scalar `  T ) ) )
142141oveqd 6057 . . . . . . . . . . . 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 6055 . . . . . . . . . . 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 707 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  T  e.  LMod )
145125ffvelrnda 5829 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
y `  x )  e.  ( Base `  R
) )
14639ad2antrr 707 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  ( Base `  R )  =  ( Base `  (Scalar `  T ) ) )
147145, 146eleqtrd 2480 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
y `  x )  e.  ( Base `  (Scalar `  T ) ) )
148128ffvelrnda 5829 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
z `  x )  e.  ( Base `  R
) )
149148, 146eleqtrd 2480 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
z `  x )  e.  ( Base `  (Scalar `  T ) ) )
15049adantr 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  ->  A : I --> C )
151150ffvelrnda 5829 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  ( A `  x )  e.  C )
152 eqid 2404 . . . . . . . . . . . . 13  |-  ( +g  `  (Scalar `  T )
)  =  ( +g  `  (Scalar `  T )
)
15319, 21, 5, 3, 43, 152lmodvsdir 15929 . . . . . . . . . . . 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 )
) ) )
154144, 147, 149, 151, 153syl13anc 1186 . . . . . . . . . . 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 )
) ) )
155143, 154eqtrd 2436 . . . . . . . . . 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 ) ) ) )
156127adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  y  Fn  I )
157129adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  z  Fn  I )
15812ad2antrr 707 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  I  e.  X )
159 simpr 448 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  x  e.  I )
160 fnfvof 6276 . . . . . . . . . . . 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 ) ) )
161156, 157, 158, 159, 160syl22anc 1185 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( y  o F ( +g  `  R
) z ) `  x )  =  ( ( y `  x
) ( +g  `  R
) ( z `  x ) ) )
162161oveq1d 6055 . . . . . . . . . 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 ) ) )
16366ad2antrr 707 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  A  Fn  I )
164 fnfvof 6276 . . . . . . . . . . . 12  |-  ( ( ( y  Fn  I  /\  A  Fn  I
)  /\  ( I  e.  X  /\  x  e.  I ) )  -> 
( ( y  o F  .x.  A ) `
 x )  =  ( ( y `  x )  .x.  ( A `  x )
) )
165156, 163, 158, 159, 164syl22anc 1185 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( y  o F 
.x.  A ) `  x )  =  ( ( y `  x
)  .x.  ( A `  x ) ) )
166157, 163, 158, 159, 71syl22anc 1185 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( z  o F 
.x.  A ) `  x )  =  ( ( z `  x
)  .x.  ( A `  x ) ) )
167165, 166oveq12d 6058 . . . . . . . . . 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 )
) ) )
168155, 162, 1673eqtr4d 2446 . . . . . . . . 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
) ) )
169130adantr 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
y  o F ( +g  `  R ) z )  Fn  I
)
170 fnfvof 6276 . . . . . . . . . 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 ) ) )
171169, 163, 158, 159, 170syl22anc 1185 . . . . . . . . 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 ) ) )
172135adantr 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
y  o F  .x.  A )  Fn  I
)
173138adantr 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
z  o F  .x.  A )  Fn  I
)
174 fnfvof 6276 . . . . . . . . . 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 ) ) )
175172, 173, 158, 159, 174syl22anc 1185 . . . . . . . . 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
) ) )
176168, 171, 1753eqtr4d 2446 . . . . . . . 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 ) )
177132, 139, 176eqfnfvd 5789 . . . . . . 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 ) ) )
178122, 177eqtrd 2436 . . . . . 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
) ) )
179178oveq2d 6056 . . . . 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 ) ) ) )
180116, 179eqtrd 2436 . . . 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 ) ) ) )
181 oveq1 6047 . . . . . . . 8  |-  ( x  =  y  ->  (
x  o F  .x.  A )  =  ( y  o F  .x.  A ) )
182181oveq2d 6056 . . . . . . 7  |-  ( x  =  y  ->  ( T  gsumg  ( x  o F 
.x.  A ) )  =  ( T  gsumg  ( y  o F  .x.  A
) ) )
183 ovex 6065 . . . . . . 7  |-  ( T 
gsumg  ( y  o F 
.x.  A ) )  e.  _V
184182, 89, 183fvmpt 5765 . . . . . 6  |-  ( y  e.  B  ->  ( E `  y )  =  ( T  gsumg  ( y  o F  .x.  A
) ) )
185184ad2antrl 709 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( E `  y
)  =  ( T 
gsumg  ( y  o F 
.x.  A ) ) )
186 oveq1 6047 . . . . . . . 8  |-  ( x  =  z  ->  (
x  o F  .x.  A )  =  ( z  o F  .x.  A ) )
187186oveq2d 6056 . . . . . . 7  |-  ( x  =  z  ->  ( T  gsumg  ( x  o F 
.x.  A ) )  =  ( T  gsumg  ( z  o F  .x.  A
) ) )
188 ovex 6065 . . . . . . 7  |-  ( T 
gsumg  ( z  o F 
.x.  A ) )  e.  _V
189187, 89, 188fvmpt 5765 . . . . . 6  |-  ( z  e.  B  ->  ( E `  z )  =  ( T  gsumg  ( z  o F  .x.  A
) ) )
190189ad2antll 710 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( E `  z
)  =  ( T 
gsumg  ( z  o F 
.x.  A ) ) )
191185, 190oveq12d 6058 . . . 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
) ) ) )
192108, 180, 1913eqtr4d 2446 . . 3  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( E `  (
y ( +g  `  F
) z ) )  =  ( ( E `
 y ) ( +g  `  T ) ( E `  z
) ) )
1931, 19, 20, 21, 23, 25, 90, 192isghmd 14970 . 2  |-  ( ph  ->  E  e.  ( F 
GrpHom  T ) )
1948adantr 452 . . . . 5  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  T  e.  LMod )
19512adantr 452 . . . . 5  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  I  e.  X )
19618fveq2d 5691 . . . . . . . 8  |-  ( ph  ->  ( Base `  (Scalar `  T ) )  =  ( Base `  (Scalar `  F ) ) )
197196eleq2d 2471 . . . . . . 7  |-  ( ph  ->  ( y  e.  (
Base `  (Scalar `  T
) )  <->  y  e.  ( Base `  (Scalar `  F
) ) ) )
198197biimpar 472 . . . . . 6  |-  ( (
ph  /\  y  e.  ( Base `  (Scalar `  F
) ) )  -> 
y  e.  ( Base `  (Scalar `  T )
) )
199198adantrr 698 . . . . 5  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  y  e.  ( Base `  (Scalar `  T
) ) )
20052adantrl 697 . . . . . 6  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( z  o F  .x.  A ) : I --> C )
201200ffvelrnda 5829 . . . . 5  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( ( z  o F  .x.  A ) `
 x )  e.  C )
20252feqmptd 5738 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  B )  ->  (
z  o F  .x.  A )  =  ( x  e.  I  |->  ( ( z  o F 
.x.  A ) `  x ) ) )
203202cnveqd 5007 . . . . . . . 8  |-  ( (
ph  /\  z  e.  B )  ->  `' ( z  o F 
.x.  A )  =  `' ( x  e.  I  |->  ( ( z  o F  .x.  A
) `  x )
) )
204203imaeq1d 5161 . . . . . . 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 ) } ) ) )
205204, 86eqeltrrd 2479 . . . . . 6  |-  ( (
ph  /\  z  e.  B )  ->  ( `' ( x  e.  I  |->  ( ( z  o F  .x.  A
) `  x )
) " ( _V 
\  { ( 0g
`  T ) } ) )  e.  Fin )
206205adantrl 697 . . . . 5  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( `' ( x  e.  I  |->  ( ( z  o F  .x.  A ) `
 x ) )
" ( _V  \  { ( 0g `  T ) } ) )  e.  Fin )
20719, 5, 43, 32, 21, 3, 194, 195, 199, 201, 206gsumvsmul 26635 . . . 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 ) ) ) ) )
20815adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  F  e.  LMod )
209 simprl 733 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  y  e.  ( Base `  (Scalar `  F
) ) )
210 simprr 734 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  z  e.  B )
2111, 4, 2, 6lmodvscl 15922 . . . . . . . . . . . 12  |-  ( ( F  e.  LMod  /\  y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )  ->  ( y ( .s
`  F ) z )  e.  B )
212208, 209, 210, 211syl3anc 1184 . . . . . . . . . . 11  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( y
( .s `  F
) z )  e.  B )
21313, 46, 1frlmbasf 27096 . . . . . . . . . . 11  |-  ( ( I  e.  X  /\  ( y ( .s
`  F ) z )  e.  B )  ->  ( y ( .s `  F ) z ) : I --> ( Base `  R
) )
214195, 212, 213syl2anc 643 . . . . . . . . . 10  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( y
( .s `  F
) z ) : I --> ( Base `  R
) )
215 ffn 5550 . . . . . . . . . 10  |-  ( ( y ( .s `  F ) z ) : I --> ( Base `  R )  ->  (
y ( .s `  F ) z )  Fn  I )
216214, 215syl 16 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( y
( .s `  F
) z )  Fn  I )
21766adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  A  Fn  I )
218216, 217, 195, 195, 51offn 6275 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( (
y ( .s `  F ) z )  o F  .x.  A
)  Fn  I )
219 dffn2 5551 . . . . . . . 8  |-  ( ( ( y ( .s
`  F ) z )  o F  .x.  A )  Fn  I  <->  ( ( y ( .s
`  F ) z )  o F  .x.  A ) : I --> _V )
220218, 219sylib 189 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( (
y ( .s `  F ) z )  o F  .x.  A
) : I --> _V )
221220feqmptd 5738 . . . . . 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
) ) )
2227fveq2d 5691 . . . . . . . . . . . 12  |-  ( ph  ->  ( .r `  R
)  =  ( .r
`  (Scalar `  T )
) )
223222ad2antrr 707 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( .r `  R
)  =  ( .r
`  (Scalar `  T )
) )
224223oveqd 6057 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( y ( .r
`  R ) ( z `  x ) )  =  ( y ( .r `  (Scalar `  T ) ) ( z `  x ) ) )
225224oveq1d 6055 . . . . . . . . 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 )
) )
2268ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  T  e.  LMod )
227 simplrl 737 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  y  e.  ( Base `  (Scalar `  F )
) )
228196ad2antrr 707 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( Base `  (Scalar `  T ) )  =  ( Base `  (Scalar `  F ) ) )
229227, 228eleqtrrd 2481 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  y  e.  ( Base `  (Scalar `  T )
) )
23048ffvelrnda 5829 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  I )  ->  (
z `  x )  e.  ( Base `  R
) )
23139ad2antrr 707 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  I )  ->  ( Base `  R )  =  ( Base `  (Scalar `  T ) ) )
232230, 231eleqtrd 2480 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  I )  ->  (
z `  x )  e.  ( Base `  (Scalar `  T ) ) )
233232adantlrl 701 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( z `  x
)  e.  ( Base `  (Scalar `  T )
) )
23449ffvelrnda 5829 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  I )  ->  ( A `  x )  e.  C )
235234adantlr 696 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( A `  x
)  e.  C )
236 eqid 2404 . . . . . . . . . . 11  |-  ( .r
`  (Scalar `  T )
)  =  ( .r
`  (Scalar `  T )
)
23719, 5, 3, 43, 236lmodvsass 15930 . . . . . . . . . 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 )
) ) )
238226, 229, 233, 235, 237syl13anc 1186 . . . . . . . . 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 )
) ) )
239225, 238eqtrd 2436 . . . . . . . 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 ) ) ) )
240216adantr 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( y ( .s
`  F ) z )  Fn  I )
24166ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  A  Fn  I )
24212ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  I  e.  X )
243 simpr 448 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  x  e.  I )
244 fnfvof 6276 . . . . . . . . . 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 )
) )
245240, 241, 242, 243, 244syl22anc 1185 . . . . . . . . 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 )
) )
24617fveq2d 5691 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Base `  R
)  =  ( Base `  (Scalar `  F )
) )
247246ad2antrr 707 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( Base `  R
)  =  ( Base `  (Scalar `  F )
) )
248227, 247eleqtrrd 2481 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  y  e.  ( Base `  R ) )
249 simplrr 738 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  z  e.  B )
250 eqid 2404 . . . . . . . . . . 11  |-  ( .r
`  R )  =  ( .r `  R
)
25113, 1, 46, 242, 248, 249, 243, 2, 250frlmvscaval 27099 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( ( y ( .s `  F ) z ) `  x
)  =  ( y ( .r `  R
) ( z `  x ) ) )
252251oveq1d 6055 . . . . . . . . 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 ) ) )
253245, 252eqtrd 2436 . . . . . . . 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 )
) )
25463adantrl 697 . . . . . . . . . . 11  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  z  Fn  I )
255254adantr 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  z  Fn  I )
256255, 241, 242, 243, 71syl22anc 1185 . . . . . . . . 9  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( ( z  o F  .x.  A ) `
 x )  =  ( ( z `  x )  .x.  ( A `  x )
) )
257256oveq2d 6056 . . . . . . . 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 ) ) ) )
258239, 253, 2573eqtr4d 2446 . . . . . . 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 ) ) )
259258mpteq2dva 4255 . . . . . 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
) ) ) )
260221, 259eqtrd 2436 . . . . 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 )
) ) )
261260oveq2d 6056 . . . 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 ) ) ) ) )
262200feqmptd 5738 . . . . . 6  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( z  o F  .x.  A )  =  ( x  e.  I  |->  ( ( z  o F  .x.  A
) `  x )
) )
263262oveq2d 6056 . . . . 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 ) ) ) )
264263oveq2d 6056 . . . 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
) ) ) ) )
265207, 261, 2643eqtr4d 2446 . . 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 ) ) ) )
266 oveq1 6047 . . . . . 6  |-  ( x  =  ( y ( .s `  F ) z )  ->  (
x  o F  .x.  A )  =  ( ( y ( .s
`  F ) z )  o F  .x.  A ) )
267266oveq2d 6056 . . . . 5  |-  ( x  =  ( y ( .s `  F ) z )  ->  ( T  gsumg  ( x  o F 
.x.  A ) )  =  ( T  gsumg  ( ( y ( .s `  F ) z )  o F  .x.  A
) ) )
268 ovex 6065 . . . . 5  |-  ( T 
gsumg  ( ( y ( .s `  F ) z )  o F 
.x.  A ) )  e.  _V
269267, 89, 268fvmpt 5765 . . . 4  |-  ( ( y ( .s `  F ) z )  e.  B  ->  ( E `  ( y
( .s `  F
) z ) )  =  ( T  gsumg  ( ( y ( .s `  F ) z )  o F  .x.  A
) ) )
270212, 269syl 16 . . 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 ) ) )
271189oveq2d 6056 . . . 4  |-  ( z  e.  B  ->  (
y  .x.  ( E `  z ) )  =  ( y  .x.  ( T  gsumg  ( z  o F 
.x.  A ) ) ) )
272271ad2antll 710 . . 3  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( y  .x.  ( E `  z
) )  =  ( y  .x.  ( T 
gsumg  ( z  o F 
.x.  A ) ) ) )
273265, 270, 2723eqtr4d 2446 . 2  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( E `  ( y ( .s
`  F ) z ) )  =  ( y  .x.  ( E `
 z ) ) )
2741, 2, 3, 4, 5, 6, 15, 8, 18, 193, 273islmhmd 16070 1  |-  ( ph  ->  E  e.  ( F LMHom 
T ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1721   _Vcvv 2916    \ cdif 3277    C_ wss 3280   {csn 3774    e. cmpt 4226   `'ccnv 4836   "cima 4840    Fn wfn 5408   -->wf 5409   ` cfv 5413  (class class class)co 6040    o Fcof 6262   Fincfn 7068   Basecbs 13424   +g cplusg 13484   .rcmulr 13485  Scalarcsca 13487   .scvsca 13488   0gc0g 13678    gsumg cgsu 13679   Grpcgrp 14640  CMndccmn 15367   Ringcrg 15615   LModclmod 15905   LMHom clmhm 16050   freeLMod cfrlm 27080
This theorem is referenced by:  frlmup3  27120  frlmup4  27121  islindf5  27177  indlcim  27178  lnrfg  27191
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-of 6264  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-map 6979  df-ixp 7023  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-sup 7404  df-oi 7435  df-card 7782  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-nn 9957  df-2 10014  df-3 10015  df-4 10016  df-5 10017  df-6 10018  df-7 10019  df-8 10020  df-9 10021  df-10 10022  df-n0 10178  df-z 10239  df-dec 10339  df-uz 10445  df-fz 11000  df-fzo 11091  df-seq 11279  df-hash 11574  df-struct 13426  df-ndx 13427  df-slot 13428  df-base 13429  df-sets 13430  df-ress 13431  df-plusg 13497  df-mulr 13498  df-sca 13500  df-vsca 13501  df-tset 13503  df-ple 13504  df-ds 13506  df-hom 13508  df-cco 13509  df-prds 13626  df-pws 13628  df-0g 13682  df-gsum 13683  df-mnd 14645  df-mhm 14693  df-submnd 14694  df-grp 14767  df-minusg 14768  df-sbg 14769  df-subg 14896  df-ghm 14959  df-cntz 15071  df-cmn 15369  df-abl 15370  df-mgp 15604  df-rng 15618  df-ur 15620  df-subrg 15821  df-lmod 15907  df-lss 15964  df-lmhm 16053  df-sra 16199  df-rgmod 16200  df-dsmm 27066  df-frlm 27082
  Copyright terms: Public domain W3C validator