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

Theorem frlmup1 18229
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.) (Proof shortened by AV, 21-Jul-2019.)
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  oF  .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  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frlmup.b . 2  |-  B  =  ( Base `  F
)
2 eqid 2443 . 2  |-  ( .s
`  F )  =  ( .s `  F
)
3 frlmup.v . 2  |-  .x.  =  ( .s `  T )
4 eqid 2443 . 2  |-  (Scalar `  F )  =  (Scalar `  F )
5 eqid 2443 . 2  |-  (Scalar `  T )  =  (Scalar `  T )
6 eqid 2443 . 2  |-  ( Base `  (Scalar `  F )
)  =  ( Base `  (Scalar `  F )
)
7 frlmup.r . . . 4  |-  ( ph  ->  R  =  (Scalar `  T ) )
8 frlmup.t . . . . 5  |-  ( ph  ->  T  e.  LMod )
95lmodrng 16959 . . . . 5  |-  ( T  e.  LMod  ->  (Scalar `  T )  e.  Ring )
108, 9syl 16 . . . 4  |-  ( ph  ->  (Scalar `  T )  e.  Ring )
117, 10eqeltrd 2517 . . 3  |-  ( ph  ->  R  e.  Ring )
12 frlmup.i . . 3  |-  ( ph  ->  I  e.  X )
13 frlmup.f . . . 4  |-  F  =  ( R freeLMod  I )
1413frlmlmod 18177 . . 3  |-  ( ( R  e.  Ring  /\  I  e.  X )  ->  F  e.  LMod )
1511, 12, 14syl2anc 661 . 2  |-  ( ph  ->  F  e.  LMod )
1613frlmsca 18181 . . . 4  |-  ( ( R  e.  Ring  /\  I  e.  X )  ->  R  =  (Scalar `  F )
)
1711, 12, 16syl2anc 661 . . 3  |-  ( ph  ->  R  =  (Scalar `  F ) )
187, 17eqtr3d 2477 . 2  |-  ( ph  ->  (Scalar `  T )  =  (Scalar `  F )
)
19 frlmup.c . . 3  |-  C  =  ( Base `  T
)
20 eqid 2443 . . 3  |-  ( +g  `  F )  =  ( +g  `  F )
21 eqid 2443 . . 3  |-  ( +g  `  T )  =  ( +g  `  T )
22 lmodgrp 16958 . . . 4  |-  ( F  e.  LMod  ->  F  e. 
Grp )
2315, 22syl 16 . . 3  |-  ( ph  ->  F  e.  Grp )
24 lmodgrp 16958 . . . 4  |-  ( T  e.  LMod  ->  T  e. 
Grp )
258, 24syl 16 . . 3  |-  ( ph  ->  T  e.  Grp )
26 eleq1 2503 . . . . . . 7  |-  ( z  =  x  ->  (
z  e.  B  <->  x  e.  B ) )
2726anbi2d 703 . . . . . 6  |-  ( z  =  x  ->  (
( ph  /\  z  e.  B )  <->  ( ph  /\  x  e.  B ) ) )
28 oveq1 6101 . . . . . . . 8  |-  ( z  =  x  ->  (
z  oF  .x.  A )  =  ( x  oF  .x.  A ) )
2928oveq2d 6110 . . . . . . 7  |-  ( z  =  x  ->  ( T  gsumg  ( z  oF  .x.  A ) )  =  ( T  gsumg  ( x  oF  .x.  A
) ) )
3029eleq1d 2509 . . . . . 6  |-  ( z  =  x  ->  (
( T  gsumg  ( z  oF  .x.  A ) )  e.  C  <->  ( T  gsumg  ( x  oF  .x.  A ) )  e.  C ) )
3127, 30imbi12d 320 . . . . 5  |-  ( z  =  x  ->  (
( ( ph  /\  z  e.  B )  ->  ( T  gsumg  ( z  oF  .x.  A ) )  e.  C )  <->  ( ( ph  /\  x  e.  B
)  ->  ( T  gsumg  ( x  oF  .x.  A ) )  e.  C ) ) )
32 eqid 2443 . . . . . 6  |-  ( 0g
`  T )  =  ( 0g `  T
)
33 lmodcmn 16996 . . . . . . . 8  |-  ( T  e.  LMod  ->  T  e. CMnd
)
348, 33syl 16 . . . . . . 7  |-  ( ph  ->  T  e. CMnd )
3534adantr 465 . . . . . 6  |-  ( (
ph  /\  z  e.  B )  ->  T  e. CMnd )
3612adantr 465 . . . . . 6  |-  ( (
ph  /\  z  e.  B )  ->  I  e.  X )
378ad2antrr 725 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  B )  /\  (
x  e.  ( Base `  R )  /\  y  e.  C ) )  ->  T  e.  LMod )
38 simprl 755 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  B )  /\  (
x  e.  ( Base `  R )  /\  y  e.  C ) )  ->  x  e.  ( Base `  R ) )
397fveq2d 5698 . . . . . . . . . 10  |-  ( ph  ->  ( Base `  R
)  =  ( Base `  (Scalar `  T )
) )
4039ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  B )  /\  (
x  e.  ( Base `  R )  /\  y  e.  C ) )  -> 
( Base `  R )  =  ( Base `  (Scalar `  T ) ) )
4138, 40eleqtrd 2519 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  B )  /\  (
x  e.  ( Base `  R )  /\  y  e.  C ) )  ->  x  e.  ( Base `  (Scalar `  T )
) )
42 simprr 756 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  B )  /\  (
x  e.  ( Base `  R )  /\  y  e.  C ) )  -> 
y  e.  C )
43 eqid 2443 . . . . . . . . 9  |-  ( Base `  (Scalar `  T )
)  =  ( Base `  (Scalar `  T )
)
4419, 5, 3, 43lmodvscl 16968 . . . . . . . 8  |-  ( ( T  e.  LMod  /\  x  e.  ( Base `  (Scalar `  T ) )  /\  y  e.  C )  ->  ( x  .x.  y
)  e.  C )
4537, 41, 42, 44syl3anc 1218 . . . . . . 7  |-  ( ( ( ph  /\  z  e.  B )  /\  (
x  e.  ( Base `  R )  /\  y  e.  C ) )  -> 
( x  .x.  y
)  e.  C )
46 eqid 2443 . . . . . . . . 9  |-  ( Base `  R )  =  (
Base `  R )
4713, 46, 1frlmbasf 18191 . . . . . . . 8  |-  ( ( I  e.  X  /\  z  e.  B )  ->  z : I --> ( Base `  R ) )
4812, 47sylan 471 . . . . . . 7  |-  ( (
ph  /\  z  e.  B )  ->  z : I --> ( Base `  R ) )
49 frlmup.a . . . . . . . 8  |-  ( ph  ->  A : I --> C )
5049adantr 465 . . . . . . 7  |-  ( (
ph  /\  z  e.  B )  ->  A : I --> C )
51 inidm 3562 . . . . . . 7  |-  ( I  i^i  I )  =  I
5245, 48, 50, 36, 36, 51off 6337 . . . . . 6  |-  ( (
ph  /\  z  e.  B )  ->  (
z  oF  .x.  A ) : I --> C )
53 ovex 6119 . . . . . . . 8  |-  ( z  oF  .x.  A
)  e.  _V
5453a1i 11 . . . . . . 7  |-  ( (
ph  /\  z  e.  B )  ->  (
z  oF  .x.  A )  e.  _V )
55 ffun 5564 . . . . . . . 8  |-  ( ( z  oF  .x.  A ) : I --> C  ->  Fun  ( z  oF  .x.  A
) )
5652, 55syl 16 . . . . . . 7  |-  ( (
ph  /\  z  e.  B )  ->  Fun  ( z  oF  .x.  A ) )
57 fvex 5704 . . . . . . . 8  |-  ( 0g
`  T )  e. 
_V
5857a1i 11 . . . . . . 7  |-  ( (
ph  /\  z  e.  B )  ->  ( 0g `  T )  e. 
_V )
59 eqid 2443 . . . . . . . . . . 11  |-  ( 0g
`  R )  =  ( 0g `  R
)
6013, 59, 1frlmbasfsupp 18188 . . . . . . . . . 10  |-  ( ( I  e.  X  /\  z  e.  B )  ->  z finSupp  ( 0g `  R ) )
6112, 60sylan 471 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  B )  ->  z finSupp  ( 0g `  R ) )
627fveq2d 5698 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0g `  R
)  =  ( 0g
`  (Scalar `  T )
) )
6362eqcomd 2448 . . . . . . . . . . 11  |-  ( ph  ->  ( 0g `  (Scalar `  T ) )  =  ( 0g `  R
) )
6463breq2d 4307 . . . . . . . . . 10  |-  ( ph  ->  ( z finSupp  ( 0g
`  (Scalar `  T )
)  <->  z finSupp  ( 0g `  R ) ) )
6564adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  B )  ->  (
z finSupp  ( 0g `  (Scalar `  T ) )  <->  z finSupp  ( 0g
`  R ) ) )
6661, 65mpbird 232 . . . . . . . 8  |-  ( (
ph  /\  z  e.  B )  ->  z finSupp  ( 0g `  (Scalar `  T ) ) )
6766fsuppimpd 7630 . . . . . . 7  |-  ( (
ph  /\  z  e.  B )  ->  (
z supp  ( 0g `  (Scalar `  T ) ) )  e.  Fin )
68 ssid 3378 . . . . . . . . 9  |-  ( z supp  ( 0g `  (Scalar `  T ) ) ) 
C_  ( z supp  ( 0g `  (Scalar `  T
) ) )
6968a1i 11 . . . . . . . 8  |-  ( (
ph  /\  z  e.  B )  ->  (
z supp  ( 0g `  (Scalar `  T ) ) )  C_  ( z supp  ( 0g `  (Scalar `  T ) ) ) )
708ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  z  e.  B )  /\  w  e.  C )  ->  T  e.  LMod )
71 eqid 2443 . . . . . . . . . 10  |-  ( 0g
`  (Scalar `  T )
)  =  ( 0g
`  (Scalar `  T )
)
7219, 5, 3, 71, 32lmod0vs 16984 . . . . . . . . 9  |-  ( ( T  e.  LMod  /\  w  e.  C )  ->  (
( 0g `  (Scalar `  T ) )  .x.  w )  =  ( 0g `  T ) )
7370, 72sylancom 667 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  B )  /\  w  e.  C )  ->  (
( 0g `  (Scalar `  T ) )  .x.  w )  =  ( 0g `  T ) )
74 fvex 5704 . . . . . . . . 9  |-  ( 0g
`  (Scalar `  T )
)  e.  _V
7574a1i 11 . . . . . . . 8  |-  ( (
ph  /\  z  e.  B )  ->  ( 0g `  (Scalar `  T
) )  e.  _V )
7669, 73, 48, 50, 36, 75suppssof1 6725 . . . . . . 7  |-  ( (
ph  /\  z  e.  B )  ->  (
( z  oF  .x.  A ) supp  ( 0g `  T ) ) 
C_  ( z supp  ( 0g `  (Scalar `  T
) ) ) )
77 suppssfifsupp 7638 . . . . . . 7  |-  ( ( ( ( z  oF  .x.  A )  e.  _V  /\  Fun  ( z  oF  .x.  A )  /\  ( 0g `  T )  e.  _V )  /\  ( ( z supp  ( 0g `  (Scalar `  T
) ) )  e. 
Fin  /\  ( (
z  oF  .x.  A ) supp  ( 0g `  T ) )  C_  ( z supp  ( 0g `  (Scalar `  T )
) ) ) )  ->  ( z  oF  .x.  A ) finSupp 
( 0g `  T
) )
7854, 56, 58, 67, 76, 77syl32anc 1226 . . . . . 6  |-  ( (
ph  /\  z  e.  B )  ->  (
z  oF  .x.  A ) finSupp  ( 0g `  T ) )
7919, 32, 35, 36, 52, 78gsumcl 16400 . . . . 5  |-  ( (
ph  /\  z  e.  B )  ->  ( T  gsumg  ( z  oF  .x.  A ) )  e.  C )
8031, 79chvarv 1958 . . . 4  |-  ( (
ph  /\  x  e.  B )  ->  ( T  gsumg  ( x  oF  .x.  A ) )  e.  C )
81 frlmup.e . . . 4  |-  E  =  ( x  e.  B  |->  ( T  gsumg  ( x  oF  .x.  A ) ) )
8280, 81fmptd 5870 . . 3  |-  ( ph  ->  E : B --> C )
8334adantr 465 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  ->  T  e. CMnd )
8412adantr 465 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  ->  I  e.  X )
85 eleq1 2503 . . . . . . . . 9  |-  ( z  =  y  ->  (
z  e.  B  <->  y  e.  B ) )
8685anbi2d 703 . . . . . . . 8  |-  ( z  =  y  ->  (
( ph  /\  z  e.  B )  <->  ( ph  /\  y  e.  B ) ) )
87 oveq1 6101 . . . . . . . . 9  |-  ( z  =  y  ->  (
z  oF  .x.  A )  =  ( y  oF  .x.  A ) )
8887feq1d 5549 . . . . . . . 8  |-  ( z  =  y  ->  (
( z  oF  .x.  A ) : I --> C  <->  ( y  oF  .x.  A ) : I --> C ) )
8986, 88imbi12d 320 . . . . . . 7  |-  ( z  =  y  ->  (
( ( ph  /\  z  e.  B )  ->  ( z  oF  .x.  A ) : I --> C )  <->  ( ( ph  /\  y  e.  B
)  ->  ( y  oF  .x.  A ) : I --> C ) ) )
9089, 52chvarv 1958 . . . . . 6  |-  ( (
ph  /\  y  e.  B )  ->  (
y  oF  .x.  A ) : I --> C )
9190adantrr 716 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( y  oF  .x.  A ) : I --> C )
9252adantrl 715 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( z  oF  .x.  A ) : I --> C )
9387breq1d 4305 . . . . . . . 8  |-  ( z  =  y  ->  (
( z  oF  .x.  A ) finSupp  ( 0g `  T )  <->  ( y  oF  .x.  A ) finSupp 
( 0g `  T
) ) )
9486, 93imbi12d 320 . . . . . . 7  |-  ( z  =  y  ->  (
( ( ph  /\  z  e.  B )  ->  ( z  oF  .x.  A ) finSupp  ( 0g `  T ) )  <-> 
( ( ph  /\  y  e.  B )  ->  ( y  oF  .x.  A ) finSupp  ( 0g `  T ) ) ) )
9594, 78chvarv 1958 . . . . . 6  |-  ( (
ph  /\  y  e.  B )  ->  (
y  oF  .x.  A ) finSupp  ( 0g `  T ) )
9695adantrr 716 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( y  oF  .x.  A ) finSupp  ( 0g `  T ) )
9778adantrl 715 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( z  oF  .x.  A ) finSupp  ( 0g `  T ) )
9819, 32, 21, 83, 84, 91, 92, 96, 97gsumadd 16415 . . . 4  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( T  gsumg  ( ( y  oF  .x.  A )  oF ( +g  `  T ) ( z  oF  .x.  A
) ) )  =  ( ( T  gsumg  ( y  oF  .x.  A
) ) ( +g  `  T ) ( T 
gsumg  ( z  oF  .x.  A ) ) ) )
991, 20lmodvacl 16965 . . . . . . . 8  |-  ( ( F  e.  LMod  /\  y  e.  B  /\  z  e.  B )  ->  (
y ( +g  `  F
) z )  e.  B )
100993expb 1188 . . . . . . 7  |-  ( ( F  e.  LMod  /\  (
y  e.  B  /\  z  e.  B )
)  ->  ( y
( +g  `  F ) z )  e.  B
)
10115, 100sylan 471 . . . . . 6  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( y ( +g  `  F ) z )  e.  B )
102 oveq1 6101 . . . . . . . 8  |-  ( x  =  ( y ( +g  `  F ) z )  ->  (
x  oF  .x.  A )  =  ( ( y ( +g  `  F ) z )  oF  .x.  A
) )
103102oveq2d 6110 . . . . . . 7  |-  ( x  =  ( y ( +g  `  F ) z )  ->  ( T  gsumg  ( x  oF  .x.  A ) )  =  ( T  gsumg  ( ( y ( +g  `  F
) z )  oF  .x.  A ) ) )
104 ovex 6119 . . . . . . 7  |-  ( T 
gsumg  ( ( y ( +g  `  F ) z )  oF  .x.  A ) )  e.  _V
105103, 81, 104fvmpt 5777 . . . . . 6  |-  ( ( y ( +g  `  F
) z )  e.  B  ->  ( E `  ( y ( +g  `  F ) z ) )  =  ( T 
gsumg  ( ( y ( +g  `  F ) z )  oF  .x.  A ) ) )
106101, 105syl 16 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( E `  (
y ( +g  `  F
) z ) )  =  ( T  gsumg  ( ( y ( +g  `  F
) z )  oF  .x.  A ) ) )
10711adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  ->  R  e.  Ring )
108 simprl 755 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
y  e.  B )
109 simprr 756 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
z  e.  B )
110 eqid 2443 . . . . . . . . 9  |-  ( +g  `  R )  =  ( +g  `  R )
11113, 1, 107, 84, 108, 109, 110, 20frlmplusgval 18194 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( y ( +g  `  F ) z )  =  ( y  oF ( +g  `  R
) z ) )
112111oveq1d 6109 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( ( y ( +g  `  F ) z )  oF  .x.  A )  =  ( ( y  oF ( +g  `  R
) z )  oF  .x.  A ) )
11313, 46, 1frlmbasf 18191 . . . . . . . . . . . . 13  |-  ( ( I  e.  X  /\  y  e.  B )  ->  y : I --> ( Base `  R ) )
11412, 113sylan 471 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  B )  ->  y : I --> ( Base `  R ) )
115114adantrr 716 . . . . . . . . . . 11  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
y : I --> ( Base `  R ) )
116 ffn 5562 . . . . . . . . . . 11  |-  ( y : I --> ( Base `  R )  ->  y  Fn  I )
117115, 116syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
y  Fn  I )
11848adantrl 715 . . . . . . . . . . 11  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
z : I --> ( Base `  R ) )
119 ffn 5562 . . . . . . . . . . 11  |-  ( z : I --> ( Base `  R )  ->  z  Fn  I )
120118, 119syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
z  Fn  I )
121117, 120, 84, 84, 51offn 6334 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( y  oF ( +g  `  R
) z )  Fn  I )
122 ffn 5562 . . . . . . . . . . 11  |-  ( A : I --> C  ->  A  Fn  I )
12349, 122syl 16 . . . . . . . . . 10  |-  ( ph  ->  A  Fn  I )
124123adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  ->  A  Fn  I )
125121, 124, 84, 84, 51offn 6334 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( ( y  oF ( +g  `  R
) z )  oF  .x.  A )  Fn  I )
126 ffn 5562 . . . . . . . . . . 11  |-  ( ( y  oF  .x.  A ) : I --> C  ->  ( y  oF  .x.  A )  Fn  I )
12790, 126syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  B )  ->  (
y  oF  .x.  A )  Fn  I
)
128127adantrr 716 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( y  oF  .x.  A )  Fn  I )
129 ffn 5562 . . . . . . . . . . 11  |-  ( ( z  oF  .x.  A ) : I --> C  ->  ( z  oF  .x.  A )  Fn  I )
13052, 129syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  z  e.  B )  ->  (
z  oF  .x.  A )  Fn  I
)
131130adantrl 715 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( z  oF  .x.  A )  Fn  I )
132128, 131, 84, 84, 51offn 6334 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( ( y  oF  .x.  A )  oF ( +g  `  T ) ( z  oF  .x.  A
) )  Fn  I
)
1337fveq2d 5698 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( +g  `  R
)  =  ( +g  `  (Scalar `  T )
) )
134133ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  ( +g  `  R )  =  ( +g  `  (Scalar `  T ) ) )
135134oveqd 6111 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( y `  x
) ( +g  `  R
) ( z `  x ) )  =  ( ( y `  x ) ( +g  `  (Scalar `  T )
) ( z `  x ) ) )
136135oveq1d 6109 . . . . . . . . . . 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 ) ) )
1378ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  T  e.  LMod )
138115ffvelrnda 5846 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
y `  x )  e.  ( Base `  R
) )
13939ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  ( Base `  R )  =  ( Base `  (Scalar `  T ) ) )
140138, 139eleqtrd 2519 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
y `  x )  e.  ( Base `  (Scalar `  T ) ) )
141118ffvelrnda 5846 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
z `  x )  e.  ( Base `  R
) )
142141, 139eleqtrd 2519 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
z `  x )  e.  ( Base `  (Scalar `  T ) ) )
14349adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  ->  A : I --> C )
144143ffvelrnda 5846 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  ( A `  x )  e.  C )
145 eqid 2443 . . . . . . . . . . . . 13  |-  ( +g  `  (Scalar `  T )
)  =  ( +g  `  (Scalar `  T )
)
14619, 21, 5, 3, 43, 145lmodvsdir 16975 . . . . . . . . . . . 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 )
) ) )
147137, 140, 142, 144, 146syl13anc 1220 . . . . . . . . . . 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 )
) ) )
148136, 147eqtrd 2475 . . . . . . . . . 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 ) ) ) )
149117adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  y  Fn  I )
150120adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  z  Fn  I )
15112ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  I  e.  X )
152 simpr 461 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  x  e.  I )
153 fnfvof 6336 . . . . . . . . . . . 12  |-  ( ( ( y  Fn  I  /\  z  Fn  I
)  /\  ( I  e.  X  /\  x  e.  I ) )  -> 
( ( y  oF ( +g  `  R
) z ) `  x )  =  ( ( y `  x
) ( +g  `  R
) ( z `  x ) ) )
154149, 150, 151, 152, 153syl22anc 1219 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( y  oF ( +g  `  R
) z ) `  x )  =  ( ( y `  x
) ( +g  `  R
) ( z `  x ) ) )
155154oveq1d 6109 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( ( y  oF ( +g  `  R
) z ) `  x )  .x.  ( A `  x )
)  =  ( ( ( y `  x
) ( +g  `  R
) ( z `  x ) )  .x.  ( A `  x ) ) )
156123ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  A  Fn  I )
157 fnfvof 6336 . . . . . . . . . . . 12  |-  ( ( ( y  Fn  I  /\  A  Fn  I
)  /\  ( I  e.  X  /\  x  e.  I ) )  -> 
( ( y  oF  .x.  A ) `
 x )  =  ( ( y `  x )  .x.  ( A `  x )
) )
158149, 156, 151, 152, 157syl22anc 1219 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( y  oF  .x.  A ) `  x )  =  ( ( y `  x
)  .x.  ( A `  x ) ) )
159 fnfvof 6336 . . . . . . . . . . . 12  |-  ( ( ( z  Fn  I  /\  A  Fn  I
)  /\  ( I  e.  X  /\  x  e.  I ) )  -> 
( ( z  oF  .x.  A ) `
 x )  =  ( ( z `  x )  .x.  ( A `  x )
) )
160150, 156, 151, 152, 159syl22anc 1219 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( z  oF  .x.  A ) `  x )  =  ( ( z `  x
)  .x.  ( A `  x ) ) )
161158, 160oveq12d 6112 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( ( y  oF  .x.  A ) `
 x ) ( +g  `  T ) ( ( z  oF  .x.  A ) `
 x ) )  =  ( ( ( y `  x ) 
.x.  ( A `  x ) ) ( +g  `  T ) ( ( z `  x )  .x.  ( A `  x )
) ) )
162148, 155, 1613eqtr4d 2485 . . . . . . . . 9  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( ( y  oF ( +g  `  R
) z ) `  x )  .x.  ( A `  x )
)  =  ( ( ( y  oF  .x.  A ) `  x ) ( +g  `  T ) ( ( z  oF  .x.  A ) `  x
) ) )
163121adantr 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
y  oF ( +g  `  R ) z )  Fn  I
)
164 fnfvof 6336 . . . . . . . . . 10  |-  ( ( ( ( y  oF ( +g  `  R
) z )  Fn  I  /\  A  Fn  I )  /\  (
I  e.  X  /\  x  e.  I )
)  ->  ( (
( y  oF ( +g  `  R
) z )  oF  .x.  A ) `
 x )  =  ( ( ( y  oF ( +g  `  R ) z ) `
 x )  .x.  ( A `  x ) ) )
165163, 156, 151, 152, 164syl22anc 1219 . . . . . . . . 9  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( ( y  oF ( +g  `  R
) z )  oF  .x.  A ) `
 x )  =  ( ( ( y  oF ( +g  `  R ) z ) `
 x )  .x.  ( A `  x ) ) )
166128adantr 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
y  oF  .x.  A )  Fn  I
)
167131adantr 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
z  oF  .x.  A )  Fn  I
)
168 fnfvof 6336 . . . . . . . . . 10  |-  ( ( ( ( y  oF  .x.  A )  Fn  I  /\  (
z  oF  .x.  A )  Fn  I
)  /\  ( I  e.  X  /\  x  e.  I ) )  -> 
( ( ( y  oF  .x.  A
)  oF ( +g  `  T ) ( z  oF  .x.  A ) ) `
 x )  =  ( ( ( y  oF  .x.  A
) `  x )
( +g  `  T ) ( ( z  oF  .x.  A ) `
 x ) ) )
169166, 167, 151, 152, 168syl22anc 1219 . . . . . . . . 9  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( ( y  oF  .x.  A )  oF ( +g  `  T ) ( z  oF  .x.  A
) ) `  x
)  =  ( ( ( y  oF  .x.  A ) `  x ) ( +g  `  T ) ( ( z  oF  .x.  A ) `  x
) ) )
170162, 165, 1693eqtr4d 2485 . . . . . . . 8  |-  ( ( ( ph  /\  (
y  e.  B  /\  z  e.  B )
)  /\  x  e.  I )  ->  (
( ( y  oF ( +g  `  R
) z )  oF  .x.  A ) `
 x )  =  ( ( ( y  oF  .x.  A
)  oF ( +g  `  T ) ( z  oF  .x.  A ) ) `
 x ) )
171125, 132, 170eqfnfvd 5803 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( ( y  oF ( +g  `  R
) z )  oF  .x.  A )  =  ( ( y  oF  .x.  A
)  oF ( +g  `  T ) ( z  oF  .x.  A ) ) )
172112, 171eqtrd 2475 . . . . . 6  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( ( y ( +g  `  F ) z )  oF  .x.  A )  =  ( ( y  oF  .x.  A )  oF ( +g  `  T ) ( z  oF  .x.  A
) ) )
173172oveq2d 6110 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( T  gsumg  ( ( y ( +g  `  F ) z )  oF  .x.  A ) )  =  ( T  gsumg  ( ( y  oF  .x.  A )  oF ( +g  `  T
) ( z  oF  .x.  A ) ) ) )
174106, 173eqtrd 2475 . . . 4  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( E `  (
y ( +g  `  F
) z ) )  =  ( T  gsumg  ( ( y  oF  .x.  A )  oF ( +g  `  T
) ( z  oF  .x.  A ) ) ) )
175 oveq1 6101 . . . . . . . 8  |-  ( x  =  y  ->  (
x  oF  .x.  A )  =  ( y  oF  .x.  A ) )
176175oveq2d 6110 . . . . . . 7  |-  ( x  =  y  ->  ( T  gsumg  ( x  oF  .x.  A ) )  =  ( T  gsumg  ( y  oF  .x.  A
) ) )
177 ovex 6119 . . . . . . 7  |-  ( T 
gsumg  ( y  oF  .x.  A ) )  e.  _V
178176, 81, 177fvmpt 5777 . . . . . 6  |-  ( y  e.  B  ->  ( E `  y )  =  ( T  gsumg  ( y  oF  .x.  A
) ) )
179178ad2antrl 727 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( E `  y
)  =  ( T 
gsumg  ( y  oF  .x.  A ) ) )
180 oveq1 6101 . . . . . . . 8  |-  ( x  =  z  ->  (
x  oF  .x.  A )  =  ( z  oF  .x.  A ) )
181180oveq2d 6110 . . . . . . 7  |-  ( x  =  z  ->  ( T  gsumg  ( x  oF  .x.  A ) )  =  ( T  gsumg  ( z  oF  .x.  A
) ) )
182 ovex 6119 . . . . . . 7  |-  ( T 
gsumg  ( z  oF  .x.  A ) )  e.  _V
183181, 81, 182fvmpt 5777 . . . . . 6  |-  ( z  e.  B  ->  ( E `  z )  =  ( T  gsumg  ( z  oF  .x.  A
) ) )
184183ad2antll 728 . . . . 5  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( E `  z
)  =  ( T 
gsumg  ( z  oF  .x.  A ) ) )
185179, 184oveq12d 6112 . . . 4  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( ( E `  y ) ( +g  `  T ) ( E `
 z ) )  =  ( ( T 
gsumg  ( y  oF  .x.  A ) ) ( +g  `  T
) ( T  gsumg  ( z  oF  .x.  A
) ) ) )
18698, 174, 1853eqtr4d 2485 . . 3  |-  ( (
ph  /\  ( y  e.  B  /\  z  e.  B ) )  -> 
( E `  (
y ( +g  `  F
) z ) )  =  ( ( E `
 y ) ( +g  `  T ) ( E `  z
) ) )
1871, 19, 20, 21, 23, 25, 82, 186isghmd 15759 . 2  |-  ( ph  ->  E  e.  ( F 
GrpHom  T ) )
1888adantr 465 . . . . 5  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  T  e.  LMod )
18912adantr 465 . . . . 5  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  I  e.  X )
19018fveq2d 5698 . . . . . . . 8  |-  ( ph  ->  ( Base `  (Scalar `  T ) )  =  ( Base `  (Scalar `  F ) ) )
191190eleq2d 2510 . . . . . . 7  |-  ( ph  ->  ( y  e.  (
Base `  (Scalar `  T
) )  <->  y  e.  ( Base `  (Scalar `  F
) ) ) )
192191biimpar 485 . . . . . 6  |-  ( (
ph  /\  y  e.  ( Base `  (Scalar `  F
) ) )  -> 
y  e.  ( Base `  (Scalar `  T )
) )
193192adantrr 716 . . . . 5  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  y  e.  ( Base `  (Scalar `  T
) ) )
19452adantrl 715 . . . . . 6  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( z  oF  .x.  A ) : I --> C )
195194ffvelrnda 5846 . . . . 5  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( ( z  oF  .x.  A ) `
 x )  e.  C )
19652feqmptd 5747 . . . . . . 7  |-  ( (
ph  /\  z  e.  B )  ->  (
z  oF  .x.  A )  =  ( x  e.  I  |->  ( ( z  oF  .x.  A ) `  x ) ) )
197196, 78eqbrtrrd 4317 . . . . . 6  |-  ( (
ph  /\  z  e.  B )  ->  (
x  e.  I  |->  ( ( z  oF  .x.  A ) `  x ) ) finSupp  ( 0g `  T ) )
198197adantrl 715 . . . . 5  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( x  e.  I  |->  ( ( z  oF  .x.  A ) `  x
) ) finSupp  ( 0g `  T ) )
19919, 5, 43, 32, 21, 3, 188, 189, 193, 195, 198gsumvsmul 17012 . . . 4  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( T  gsumg  ( x  e.  I  |->  ( y  .x.  ( ( z  oF  .x.  A ) `  x
) ) ) )  =  ( y  .x.  ( T  gsumg  ( x  e.  I  |->  ( ( z  oF  .x.  A ) `
 x ) ) ) ) )
20015adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  F  e.  LMod )
201 simprl 755 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  y  e.  ( Base `  (Scalar `  F
) ) )
202 simprr 756 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  z  e.  B )
2031, 4, 2, 6lmodvscl 16968 . . . . . . . . . . . 12  |-  ( ( F  e.  LMod  /\  y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )  ->  ( y ( .s
`  F ) z )  e.  B )
204200, 201, 202, 203syl3anc 1218 . . . . . . . . . . 11  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( y
( .s `  F
) z )  e.  B )
20513, 46, 1frlmbasf 18191 . . . . . . . . . . 11  |-  ( ( I  e.  X  /\  ( y ( .s
`  F ) z )  e.  B )  ->  ( y ( .s `  F ) z ) : I --> ( Base `  R
) )
206189, 204, 205syl2anc 661 . . . . . . . . . 10  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( y
( .s `  F
) z ) : I --> ( Base `  R
) )
207 ffn 5562 . . . . . . . . . 10  |-  ( ( y ( .s `  F ) z ) : I --> ( Base `  R )  ->  (
y ( .s `  F ) z )  Fn  I )
208206, 207syl 16 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( y
( .s `  F
) z )  Fn  I )
209123adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  A  Fn  I )
210208, 209, 189, 189, 51offn 6334 . . . . . . . 8  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( (
y ( .s `  F ) z )  oF  .x.  A
)  Fn  I )
211 dffn2 5563 . . . . . . . 8  |-  ( ( ( y ( .s
`  F ) z )  oF  .x.  A )  Fn  I  <->  ( ( y ( .s
`  F ) z )  oF  .x.  A ) : I --> _V )
212210, 211sylib 196 . . . . . . 7  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( (
y ( .s `  F ) z )  oF  .x.  A
) : I --> _V )
213212feqmptd 5747 . . . . . 6  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( (
y ( .s `  F ) z )  oF  .x.  A
)  =  ( x  e.  I  |->  ( ( ( y ( .s
`  F ) z )  oF  .x.  A ) `  x
) ) )
2147fveq2d 5698 . . . . . . . . . . . 12  |-  ( ph  ->  ( .r `  R
)  =  ( .r
`  (Scalar `  T )
) )
215214ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( .r `  R
)  =  ( .r
`  (Scalar `  T )
) )
216215oveqd 6111 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( y ( .r
`  R ) ( z `  x ) )  =  ( y ( .r `  (Scalar `  T ) ) ( z `  x ) ) )
217216oveq1d 6109 . . . . . . . . 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 )
) )
2188ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  T  e.  LMod )
219 simplrl 759 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  y  e.  ( Base `  (Scalar `  F )
) )
220190ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( Base `  (Scalar `  T ) )  =  ( Base `  (Scalar `  F ) ) )
221219, 220eleqtrrd 2520 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  y  e.  ( Base `  (Scalar `  T )
) )
22248ffvelrnda 5846 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  I )  ->  (
z `  x )  e.  ( Base `  R
) )
22339ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  I )  ->  ( Base `  R )  =  ( Base `  (Scalar `  T ) ) )
224222, 223eleqtrd 2519 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  B )  /\  x  e.  I )  ->  (
z `  x )  e.  ( Base `  (Scalar `  T ) ) )
225224adantlrl 719 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( z `  x
)  e.  ( Base `  (Scalar `  T )
) )
22649ffvelrnda 5846 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  I )  ->  ( A `  x )  e.  C )
227226adantlr 714 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( A `  x
)  e.  C )
228 eqid 2443 . . . . . . . . . . 11  |-  ( .r
`  (Scalar `  T )
)  =  ( .r
`  (Scalar `  T )
)
22919, 5, 3, 43, 228lmodvsass 16976 . . . . . . . . . 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 )
) ) )
230218, 221, 225, 227, 229syl13anc 1220 . . . . . . . . 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 )
) ) )
231217, 230eqtrd 2475 . . . . . . . 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 ) ) ) )
232208adantr 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( y ( .s
`  F ) z )  Fn  I )
233123ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  A  Fn  I )
23412ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  I  e.  X )
235 simpr 461 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  x  e.  I )
236 fnfvof 6336 . . . . . . . . . 10  |-  ( ( ( ( y ( .s `  F ) z )  Fn  I  /\  A  Fn  I
)  /\  ( I  e.  X  /\  x  e.  I ) )  -> 
( ( ( y ( .s `  F
) z )  oF  .x.  A ) `
 x )  =  ( ( ( y ( .s `  F
) z ) `  x )  .x.  ( A `  x )
) )
237232, 233, 234, 235, 236syl22anc 1219 . . . . . . . . 9  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( ( ( y ( .s `  F
) z )  oF  .x.  A ) `
 x )  =  ( ( ( y ( .s `  F
) z ) `  x )  .x.  ( A `  x )
) )
23817fveq2d 5698 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Base `  R
)  =  ( Base `  (Scalar `  F )
) )
239238ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( Base `  R
)  =  ( Base `  (Scalar `  F )
) )
240219, 239eleqtrrd 2520 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  y  e.  ( Base `  R ) )
241 simplrr 760 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  z  e.  B )
242 eqid 2443 . . . . . . . . . . 11  |-  ( .r
`  R )  =  ( .r `  R
)
24313, 1, 46, 234, 240, 241, 235, 2, 242frlmvscaval 18197 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( ( y ( .s `  F ) z ) `  x
)  =  ( y ( .r `  R
) ( z `  x ) ) )
244243oveq1d 6109 . . . . . . . . 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 ) ) )
245237, 244eqtrd 2475 . . . . . . . 8  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( ( ( y ( .s `  F
) z )  oF  .x.  A ) `
 x )  =  ( ( y ( .r `  R ) ( z `  x
) )  .x.  ( A `  x )
) )
24648, 119syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  z  e.  B )  ->  z  Fn  I )
247246adantrl 715 . . . . . . . . . . 11  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  z  Fn  I )
248247adantr 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  z  Fn  I )
249248, 233, 234, 235, 159syl22anc 1219 . . . . . . . . 9  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( ( z  oF  .x.  A ) `
 x )  =  ( ( z `  x )  .x.  ( A `  x )
) )
250249oveq2d 6110 . . . . . . . 8  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( y  .x.  (
( z  oF  .x.  A ) `  x ) )  =  ( y  .x.  (
( z `  x
)  .x.  ( A `  x ) ) ) )
251231, 245, 2503eqtr4d 2485 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( Base `  (Scalar `  F )
)  /\  z  e.  B ) )  /\  x  e.  I )  ->  ( ( ( y ( .s `  F
) z )  oF  .x.  A ) `
 x )  =  ( y  .x.  (
( z  oF  .x.  A ) `  x ) ) )
252251mpteq2dva 4381 . . . . . 6  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( x  e.  I  |->  ( ( ( y ( .s
`  F ) z )  oF  .x.  A ) `  x
) )  =  ( x  e.  I  |->  ( y  .x.  ( ( z  oF  .x.  A ) `  x
) ) ) )
253213, 252eqtrd 2475 . . . . 5  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( (
y ( .s `  F ) z )  oF  .x.  A
)  =  ( x  e.  I  |->  ( y 
.x.  ( ( z  oF  .x.  A
) `  x )
) ) )
254253oveq2d 6110 . . . 4  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( T  gsumg  ( ( y ( .s
`  F ) z )  oF  .x.  A ) )  =  ( T  gsumg  ( x  e.  I  |->  ( y  .x.  (
( z  oF  .x.  A ) `  x ) ) ) ) )
255194feqmptd 5747 . . . . . 6  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( z  oF  .x.  A )  =  ( x  e.  I  |->  ( ( z  oF  .x.  A
) `  x )
) )
256255oveq2d 6110 . . . . 5  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( T  gsumg  ( z  oF  .x.  A ) )  =  ( T  gsumg  ( x  e.  I  |->  ( ( z  oF  .x.  A ) `
 x ) ) ) )
257256oveq2d 6110 . . . 4  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( y  .x.  ( T  gsumg  ( z  oF  .x.  A ) ) )  =  ( y 
.x.  ( T  gsumg  ( x  e.  I  |->  ( ( z  oF  .x.  A ) `  x
) ) ) ) )
258199, 254, 2573eqtr4d 2485 . . 3  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( T  gsumg  ( ( y ( .s
`  F ) z )  oF  .x.  A ) )  =  ( y  .x.  ( T  gsumg  ( z  oF  .x.  A ) ) ) )
259 oveq1 6101 . . . . . 6  |-  ( x  =  ( y ( .s `  F ) z )  ->  (
x  oF  .x.  A )  =  ( ( y ( .s
`  F ) z )  oF  .x.  A ) )
260259oveq2d 6110 . . . . 5  |-  ( x  =  ( y ( .s `  F ) z )  ->  ( T  gsumg  ( x  oF  .x.  A ) )  =  ( T  gsumg  ( ( y ( .s `  F ) z )  oF  .x.  A
) ) )
261 ovex 6119 . . . . 5  |-  ( T 
gsumg  ( ( y ( .s `  F ) z )  oF  .x.  A ) )  e.  _V
262260, 81, 261fvmpt 5777 . . . 4  |-  ( ( y ( .s `  F ) z )  e.  B  ->  ( E `  ( y
( .s `  F
) z ) )  =  ( T  gsumg  ( ( y ( .s `  F ) z )  oF  .x.  A
) ) )
263204, 262syl 16 . . 3  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( E `  ( y ( .s
`  F ) z ) )  =  ( T  gsumg  ( ( y ( .s `  F ) z )  oF  .x.  A ) ) )
264183oveq2d 6110 . . . 4  |-  ( z  e.  B  ->  (
y  .x.  ( E `  z ) )  =  ( y  .x.  ( T  gsumg  ( z  oF  .x.  A ) ) ) )
265264ad2antll 728 . . 3  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( y  .x.  ( E `  z
) )  =  ( y  .x.  ( T 
gsumg  ( z  oF  .x.  A ) ) ) )
266258, 263, 2653eqtr4d 2485 . 2  |-  ( (
ph  /\  ( y  e.  ( Base `  (Scalar `  F ) )  /\  z  e.  B )
)  ->  ( E `  ( y ( .s
`  F ) z ) )  =  ( y  .x.  ( E `
 z ) ) )
2671, 2, 3, 4, 5, 6, 15, 8, 18, 187, 266islmhmd 17123 1  |-  ( ph  ->  E  e.  ( F LMHom 
T ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369    e. wcel 1756   _Vcvv 2975    C_ wss 3331   class class class wbr 4295    e. cmpt 4353   Fun wfun 5415    Fn wfn 5416   -->wf 5417   ` cfv 5421  (class class class)co 6094    oFcof 6321   supp csupp 6693   Fincfn 7313   finSupp cfsupp 7623   Basecbs 14177   +g cplusg 14241   .rcmulr 14242  Scalarcsca 14244   .scvsca 14245   0gc0g 14381    gsumg cgsu 14382   Grpcgrp 15413  CMndccmn 16280   Ringcrg 16648   LModclmod 16951   LMHom clmhm 17103   freeLMod cfrlm 18174
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4406  ax-sep 4416  ax-nul 4424  ax-pow 4473  ax-pr 4534  ax-un 6375  ax-cnex 9341  ax-resscn 9342  ax-1cn 9343  ax-icn 9344  ax-addcl 9345  ax-addrcl 9346  ax-mulcl 9347  ax-mulrcl 9348  ax-mulcom 9349  ax-addass 9350  ax-mulass 9351  ax-distr 9352  ax-i2m1 9353  ax-1ne0 9354  ax-1rid 9355  ax-rnegex 9356  ax-rrecex 9357  ax-cnre 9358  ax-pre-lttri 9359  ax-pre-lttrn 9360  ax-pre-ltadd 9361  ax-pre-mulgt0 9362
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-nel 2612  df-ral 2723  df-rex 2724  df-reu 2725  df-rmo 2726  df-rab 2727  df-v 2977  df-sbc 3190  df-csb 3292  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-pss 3347  df-nul 3641  df-if 3795  df-pw 3865  df-sn 3881  df-pr 3883  df-tp 3885  df-op 3887  df-uni 4095  df-int 4132  df-iun 4176  df-br 4296  df-opab 4354  df-mpt 4355  df-tr 4389  df-eprel 4635  df-id 4639  df-po 4644  df-so 4645  df-fr 4682  df-se 4683  df-we 4684  df-ord 4725  df-on 4726  df-lim 4727  df-suc 4728  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-res 4855  df-ima 4856  df-iota 5384  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-isom 5430  df-riota 6055  df-ov 6097  df-oprab 6098  df-mpt2 6099  df-of 6323  df-om 6480  df-1st 6580  df-2nd 6581  df-supp 6694  df-recs 6835  df-rdg 6869  df-1o 6923  df-oadd 6927  df-er 7104  df-map 7219  df-ixp 7267  df-en 7314  df-dom 7315  df-sdom 7316  df-fin 7317  df-fsupp 7624  df-sup 7694  df-oi 7727  df-card 8112  df-pnf 9423  df-mnf 9424  df-xr 9425  df-ltxr 9426  df-le 9427  df-sub 9600  df-neg 9601  df-nn 10326  df-2 10383  df-3 10384  df-4 10385  df-5 10386  df-6 10387  df-7 10388  df-8 10389  df-9 10390  df-10 10391  df-n0 10583  df-z 10650  df-dec 10759  df-uz 10865  df-fz 11441  df-fzo 11552  df-seq 11810  df-hash 12107  df-struct 14179  df-ndx 14180  df-slot 14181  df-base 14182  df-sets 14183  df-ress 14184  df-plusg 14254  df-mulr 14255  df-sca 14257  df-vsca 14258  df-ip 14259  df-tset 14260  df-ple 14261  df-ds 14263  df-hom 14265  df-cco 14266  df-0g 14383  df-gsum 14384  df-prds 14389  df-pws 14391  df-mnd 15418  df-mhm 15467  df-submnd 15468  df-grp 15548  df-minusg 15549  df-sbg 15550  df-subg 15681  df-ghm 15748  df-cntz 15838  df-cmn 16282  df-abl 16283  df-mgp 16595  df-ur 16607  df-rng 16650  df-subrg 16866  df-lmod 16953  df-lss 17017  df-lmhm 17106  df-sra 17256  df-rgmod 17257  df-dsmm 18160  df-frlm 18175
This theorem is referenced by:  frlmup3  18231  frlmup4  18232  islindf5  18271  indlcim  18272  lnrfg  29478
  Copyright terms: Public domain W3C validator