Metamath Proof Explorer

Theorem frlmup1

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)

Ref Expression
Hypotheses 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 gsum ( 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 frlmup1 
|- ( ph -> E e. ( F LMHom T ) )

Proof

Step Hyp Ref Expression
1 frlmup.f 
 |-  F = ( R freeLMod I )
2 frlmup.b 
 |-  B = ( Base ` F )
3 frlmup.c 
 |-  C = ( Base ` T )
4 frlmup.v 
 |-  .x. = ( .s ` T )
5 frlmup.e 
 |-  E = ( x e. B |-> ( T gsum ( x oF .x. A ) ) )
6 frlmup.t 
 |-  ( ph -> T e. LMod )
7 frlmup.i 
 |-  ( ph -> I e. X )
8 frlmup.r 
 |-  ( ph -> R = ( Scalar ` T ) )
9 frlmup.a 
 |-  ( ph -> A : I --> C )
10 eqid 
 |-  ( .s ` F ) = ( .s ` F )
11 eqid 
 |-  ( Scalar ` F ) = ( Scalar ` F )
12 eqid 
 |-  ( Scalar ` T ) = ( Scalar ` T )
13 eqid 
 |-  ( Base ` ( Scalar ` F ) ) = ( Base ` ( Scalar ` F ) )
14 12 lmodring 
 |-  ( T e. LMod -> ( Scalar ` T ) e. Ring )
15 6 14 syl 
 |-  ( ph -> ( Scalar ` T ) e. Ring )
16 8 15 eqeltrd 
 |-  ( ph -> R e. Ring )
17 1 frlmlmod 
 |-  ( ( R e. Ring /\ I e. X ) -> F e. LMod )
18 16 7 17 syl2anc 
 |-  ( ph -> F e. LMod )
19 1 frlmsca 
 |-  ( ( R e. Ring /\ I e. X ) -> R = ( Scalar ` F ) )
20 16 7 19 syl2anc 
 |-  ( ph -> R = ( Scalar ` F ) )
21 8 20 eqtr3d 
 |-  ( ph -> ( Scalar ` T ) = ( Scalar ` F ) )
22 eqid 
 |-  ( +g ` F ) = ( +g ` F )
23 eqid 
 |-  ( +g ` T ) = ( +g ` T )
24 lmodgrp 
 |-  ( F e. LMod -> F e. Grp )
25 18 24 syl 
 |-  ( ph -> F e. Grp )
26 lmodgrp 
 |-  ( T e. LMod -> T e. Grp )
27 6 26 syl 
 |-  ( ph -> T e. Grp )
28 eleq1w 
 |-  ( z = x -> ( z e. B <-> x e. B ) )
29 28 anbi2d 
 |-  ( z = x -> ( ( ph /\ z e. B ) <-> ( ph /\ x e. B ) ) )
30 oveq1 
 |-  ( z = x -> ( z oF .x. A ) = ( x oF .x. A ) )
31 30 oveq2d 
 |-  ( z = x -> ( T gsum ( z oF .x. A ) ) = ( T gsum ( x oF .x. A ) ) )
32 31 eleq1d 
 |-  ( z = x -> ( ( T gsum ( z oF .x. A ) ) e. C <-> ( T gsum ( x oF .x. A ) ) e. C ) )
33 29 32 imbi12d 
 |-  ( z = x -> ( ( ( ph /\ z e. B ) -> ( T gsum ( z oF .x. A ) ) e. C ) <-> ( ( ph /\ x e. B ) -> ( T gsum ( x oF .x. A ) ) e. C ) ) )
34 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
35 lmodcmn 
 |-  ( T e. LMod -> T e. CMnd )
36 6 35 syl 
 |-  ( ph -> T e. CMnd )
37 36 adantr 
 |-  ( ( ph /\ z e. B ) -> T e. CMnd )
38 7 adantr 
 |-  ( ( ph /\ z e. B ) -> I e. X )
39 6 ad2antrr 
 |-  ( ( ( ph /\ z e. B ) /\ ( x e. ( Base ` R ) /\ y e. C ) ) -> T e. LMod )
40 simprl 
 |-  ( ( ( ph /\ z e. B ) /\ ( x e. ( Base ` R ) /\ y e. C ) ) -> x e. ( Base ` R ) )
41 8 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` T ) ) )
42 41 ad2antrr 
 |-  ( ( ( ph /\ z e. B ) /\ ( x e. ( Base ` R ) /\ y e. C ) ) -> ( Base ` R ) = ( Base ` ( Scalar ` T ) ) )
43 40 42 eleqtrd 
 |-  ( ( ( ph /\ z e. B ) /\ ( x e. ( Base ` R ) /\ y e. C ) ) -> x e. ( Base ` ( Scalar ` T ) ) )
44 simprr 
 |-  ( ( ( ph /\ z e. B ) /\ ( x e. ( Base ` R ) /\ y e. C ) ) -> y e. C )
45 eqid 
 |-  ( Base ` ( Scalar ` T ) ) = ( Base ` ( Scalar ` T ) )
46 3 12 4 45 lmodvscl 
 |-  ( ( T e. LMod /\ x e. ( Base ` ( Scalar ` T ) ) /\ y e. C ) -> ( x .x. y ) e. C )
47 39 43 44 46 syl3anc 
 |-  ( ( ( ph /\ z e. B ) /\ ( x e. ( Base ` R ) /\ y e. C ) ) -> ( x .x. y ) e. C )
48 eqid 
 |-  ( Base ` R ) = ( Base ` R )
49 1 48 2 frlmbasf 
 |-  ( ( I e. X /\ z e. B ) -> z : I --> ( Base ` R ) )
50 7 49 sylan 
 |-  ( ( ph /\ z e. B ) -> z : I --> ( Base ` R ) )
51 9 adantr 
 |-  ( ( ph /\ z e. B ) -> A : I --> C )
52 inidm 
 |-  ( I i^i I ) = I
53 47 50 51 38 38 52 off 
 |-  ( ( ph /\ z e. B ) -> ( z oF .x. A ) : I --> C )
54 ovexd 
 |-  ( ( ph /\ z e. B ) -> ( z oF .x. A ) e. _V )
55 53 ffund 
 |-  ( ( ph /\ z e. B ) -> Fun ( z oF .x. A ) )
56 fvexd 
 |-  ( ( ph /\ z e. B ) -> ( 0g ` T ) e. _V )
57 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
58 1 57 2 frlmbasfsupp 
 |-  ( ( I e. X /\ z e. B ) -> z finSupp ( 0g ` R ) )
59 7 58 sylan 
 |-  ( ( ph /\ z e. B ) -> z finSupp ( 0g ` R ) )
60 8 fveq2d 
 |-  ( ph -> ( 0g ` R ) = ( 0g ` ( Scalar ` T ) ) )
61 60 eqcomd 
 |-  ( ph -> ( 0g ` ( Scalar ` T ) ) = ( 0g ` R ) )
62 61 breq2d 
 |-  ( ph -> ( z finSupp ( 0g ` ( Scalar ` T ) ) <-> z finSupp ( 0g ` R ) ) )
63 62 adantr 
 |-  ( ( ph /\ z e. B ) -> ( z finSupp ( 0g ` ( Scalar ` T ) ) <-> z finSupp ( 0g ` R ) ) )
64 59 63 mpbird 
 |-  ( ( ph /\ z e. B ) -> z finSupp ( 0g ` ( Scalar ` T ) ) )
65 64 fsuppimpd 
 |-  ( ( ph /\ z e. B ) -> ( z supp ( 0g ` ( Scalar ` T ) ) ) e. Fin )
66 ssidd 
 |-  ( ( ph /\ z e. B ) -> ( z supp ( 0g ` ( Scalar ` T ) ) ) C_ ( z supp ( 0g ` ( Scalar ` T ) ) ) )
67 6 ad2antrr 
 |-  ( ( ( ph /\ z e. B ) /\ w e. C ) -> T e. LMod )
68 eqid 
 |-  ( 0g ` ( Scalar ` T ) ) = ( 0g ` ( Scalar ` T ) )
69 3 12 4 68 34 lmod0vs 
 |-  ( ( T e. LMod /\ w e. C ) -> ( ( 0g ` ( Scalar ` T ) ) .x. w ) = ( 0g ` T ) )
70 67 69 sylancom 
 |-  ( ( ( ph /\ z e. B ) /\ w e. C ) -> ( ( 0g ` ( Scalar ` T ) ) .x. w ) = ( 0g ` T ) )
71 fvexd 
 |-  ( ( ph /\ z e. B ) -> ( 0g ` ( Scalar ` T ) ) e. _V )
72 66 70 50 51 38 71 suppssof1 
 |-  ( ( ph /\ z e. B ) -> ( ( z oF .x. A ) supp ( 0g ` T ) ) C_ ( z supp ( 0g ` ( Scalar ` T ) ) ) )
73 suppssfifsupp 
 |-  ( ( ( ( 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 ) )
74 54 55 56 65 72 73 syl32anc 
 |-  ( ( ph /\ z e. B ) -> ( z oF .x. A ) finSupp ( 0g ` T ) )
75 3 34 37 38 53 74 gsumcl 
 |-  ( ( ph /\ z e. B ) -> ( T gsum ( z oF .x. A ) ) e. C )
76 33 75 chvarvv 
 |-  ( ( ph /\ x e. B ) -> ( T gsum ( x oF .x. A ) ) e. C )
77 76 5 fmptd 
 |-  ( ph -> E : B --> C )
78 36 adantr 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> T e. CMnd )
79 7 adantr 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> I e. X )
80 eleq1w 
 |-  ( z = y -> ( z e. B <-> y e. B ) )
81 80 anbi2d 
 |-  ( z = y -> ( ( ph /\ z e. B ) <-> ( ph /\ y e. B ) ) )
82 oveq1 
 |-  ( z = y -> ( z oF .x. A ) = ( y oF .x. A ) )
83 82 feq1d 
 |-  ( z = y -> ( ( z oF .x. A ) : I --> C <-> ( y oF .x. A ) : I --> C ) )
84 81 83 imbi12d 
 |-  ( z = y -> ( ( ( ph /\ z e. B ) -> ( z oF .x. A ) : I --> C ) <-> ( ( ph /\ y e. B ) -> ( y oF .x. A ) : I --> C ) ) )
85 84 53 chvarvv 
 |-  ( ( ph /\ y e. B ) -> ( y oF .x. A ) : I --> C )
86 85 adantrr 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y oF .x. A ) : I --> C )
87 53 adantrl 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( z oF .x. A ) : I --> C )
88 82 breq1d 
 |-  ( z = y -> ( ( z oF .x. A ) finSupp ( 0g ` T ) <-> ( y oF .x. A ) finSupp ( 0g ` T ) ) )
89 81 88 imbi12d 
 |-  ( z = y -> ( ( ( ph /\ z e. B ) -> ( z oF .x. A ) finSupp ( 0g ` T ) ) <-> ( ( ph /\ y e. B ) -> ( y oF .x. A ) finSupp ( 0g ` T ) ) ) )
90 89 74 chvarvv 
 |-  ( ( ph /\ y e. B ) -> ( y oF .x. A ) finSupp ( 0g ` T ) )
91 90 adantrr 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y oF .x. A ) finSupp ( 0g ` T ) )
92 74 adantrl 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( z oF .x. A ) finSupp ( 0g ` T ) )
93 3 34 23 78 79 86 87 91 92 gsumadd 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( T gsum ( ( y oF .x. A ) oF ( +g ` T ) ( z oF .x. A ) ) ) = ( ( T gsum ( y oF .x. A ) ) ( +g ` T ) ( T gsum ( z oF .x. A ) ) ) )
94 2 22 lmodvacl 
 |-  ( ( F e. LMod /\ y e. B /\ z e. B ) -> ( y ( +g ` F ) z ) e. B )
95 94 3expb 
 |-  ( ( F e. LMod /\ ( y e. B /\ z e. B ) ) -> ( y ( +g ` F ) z ) e. B )
96 18 95 sylan 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y ( +g ` F ) z ) e. B )
97 oveq1 
 |-  ( x = ( y ( +g ` F ) z ) -> ( x oF .x. A ) = ( ( y ( +g ` F ) z ) oF .x. A ) )
98 97 oveq2d 
 |-  ( x = ( y ( +g ` F ) z ) -> ( T gsum ( x oF .x. A ) ) = ( T gsum ( ( y ( +g ` F ) z ) oF .x. A ) ) )
99 ovex 
 |-  ( T gsum ( ( y ( +g ` F ) z ) oF .x. A ) ) e. _V
100 98 5 99 fvmpt 
 |-  ( ( y ( +g ` F ) z ) e. B -> ( E ` ( y ( +g ` F ) z ) ) = ( T gsum ( ( y ( +g ` F ) z ) oF .x. A ) ) )
101 96 100 syl 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( E ` ( y ( +g ` F ) z ) ) = ( T gsum ( ( y ( +g ` F ) z ) oF .x. A ) ) )
102 16 adantr 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> R e. Ring )
103 simprl 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> y e. B )
104 simprr 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> z e. B )
105 eqid 
 |-  ( +g ` R ) = ( +g ` R )
106 1 2 102 79 103 104 105 22 frlmplusgval 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y ( +g ` F ) z ) = ( y oF ( +g ` R ) z ) )
107 106 oveq1d 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( ( y ( +g ` F ) z ) oF .x. A ) = ( ( y oF ( +g ` R ) z ) oF .x. A ) )
108 1 48 2 frlmbasf 
 |-  ( ( I e. X /\ y e. B ) -> y : I --> ( Base ` R ) )
109 7 108 sylan 
 |-  ( ( ph /\ y e. B ) -> y : I --> ( Base ` R ) )
110 109 adantrr 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> y : I --> ( Base ` R ) )
111 110 ffnd 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> y Fn I )
112 50 adantrl 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> z : I --> ( Base ` R ) )
113 112 ffnd 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> z Fn I )
114 111 113 79 79 52 offn 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y oF ( +g ` R ) z ) Fn I )
115 9 ffnd 
 |-  ( ph -> A Fn I )
116 115 adantr 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> A Fn I )
117 114 116 79 79 52 offn 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( ( y oF ( +g ` R ) z ) oF .x. A ) Fn I )
118 85 ffnd 
 |-  ( ( ph /\ y e. B ) -> ( y oF .x. A ) Fn I )
119 118 adantrr 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y oF .x. A ) Fn I )
120 53 ffnd 
 |-  ( ( ph /\ z e. B ) -> ( z oF .x. A ) Fn I )
121 120 adantrl 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( z oF .x. A ) Fn I )
122 119 121 79 79 52 offn 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( ( y oF .x. A ) oF ( +g ` T ) ( z oF .x. A ) ) Fn I )
123 8 fveq2d 
 |-  ( ph -> ( +g ` R ) = ( +g ` ( Scalar ` T ) ) )
124 123 ad2antrr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( +g ` R ) = ( +g ` ( Scalar ` T ) ) )
125 124 oveqd 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( ( y ` x ) ( +g ` R ) ( z ` x ) ) = ( ( y ` x ) ( +g ` ( Scalar ` T ) ) ( z ` x ) ) )
126 125 oveq1d 
 |-  ( ( ( 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 ) ) )
127 6 ad2antrr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> T e. LMod )
128 110 ffvelrnda 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( y ` x ) e. ( Base ` R ) )
129 41 ad2antrr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( Base ` R ) = ( Base ` ( Scalar ` T ) ) )
130 128 129 eleqtrd 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( y ` x ) e. ( Base ` ( Scalar ` T ) ) )
131 112 ffvelrnda 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( z ` x ) e. ( Base ` R ) )
132 131 129 eleqtrd 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( z ` x ) e. ( Base ` ( Scalar ` T ) ) )
133 9 adantr 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> A : I --> C )
134 133 ffvelrnda 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( A ` x ) e. C )
135 eqid 
 |-  ( +g ` ( Scalar ` T ) ) = ( +g ` ( Scalar ` T ) )
136 3 23 12 4 45 135 lmodvsdir 
 |-  ( ( 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 ) ) ) )
137 127 130 132 134 136 syl13anc 
 |-  ( ( ( 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 ) ) ) )
138 126 137 eqtrd 
 |-  ( ( ( 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 ) ) ) )
139 111 adantr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> y Fn I )
140 113 adantr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> z Fn I )
141 7 ad2antrr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> I e. X )
142 simpr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> x e. I )
143 fnfvof 
 |-  ( ( ( y Fn I /\ z Fn I ) /\ ( I e. X /\ x e. I ) ) -> ( ( y oF ( +g ` R ) z ) ` x ) = ( ( y ` x ) ( +g ` R ) ( z ` x ) ) )
144 139 140 141 142 143 syl22anc 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( ( y oF ( +g ` R ) z ) ` x ) = ( ( y ` x ) ( +g ` R ) ( z ` x ) ) )
145 144 oveq1d 
 |-  ( ( ( 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 ) ) )
146 115 ad2antrr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> A Fn I )
147 fnfvof 
 |-  ( ( ( y Fn I /\ A Fn I ) /\ ( I e. X /\ x e. I ) ) -> ( ( y oF .x. A ) ` x ) = ( ( y ` x ) .x. ( A ` x ) ) )
148 139 146 141 142 147 syl22anc 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( ( y oF .x. A ) ` x ) = ( ( y ` x ) .x. ( A ` x ) ) )
149 fnfvof 
 |-  ( ( ( z Fn I /\ A Fn I ) /\ ( I e. X /\ x e. I ) ) -> ( ( z oF .x. A ) ` x ) = ( ( z ` x ) .x. ( A ` x ) ) )
150 140 146 141 142 149 syl22anc 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( ( z oF .x. A ) ` x ) = ( ( z ` x ) .x. ( A ` x ) ) )
151 148 150 oveq12d 
 |-  ( ( ( 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 ) ) ) )
152 138 145 151 3eqtr4d 
 |-  ( ( ( 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 ) ) )
153 114 adantr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( y oF ( +g ` R ) z ) Fn I )
154 fnfvof 
 |-  ( ( ( ( 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 ) ) )
155 153 146 141 142 154 syl22anc 
 |-  ( ( ( 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 ) ) )
156 119 adantr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( y oF .x. A ) Fn I )
157 121 adantr 
 |-  ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( z oF .x. A ) Fn I )
158 fnfvof 
 |-  ( ( ( ( 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 ) ) )
159 156 157 141 142 158 syl22anc 
 |-  ( ( ( 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 ) ) )
160 152 155 159 3eqtr4d 
 |-  ( ( ( 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 ) )
161 117 122 160 eqfnfvd 
 |-  ( ( 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 ) ) )
162 107 161 eqtrd 
 |-  ( ( 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 ) ) )
163 162 oveq2d 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( T gsum ( ( y ( +g ` F ) z ) oF .x. A ) ) = ( T gsum ( ( y oF .x. A ) oF ( +g ` T ) ( z oF .x. A ) ) ) )
164 101 163 eqtrd 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( E ` ( y ( +g ` F ) z ) ) = ( T gsum ( ( y oF .x. A ) oF ( +g ` T ) ( z oF .x. A ) ) ) )
165 oveq1 
 |-  ( x = y -> ( x oF .x. A ) = ( y oF .x. A ) )
166 165 oveq2d 
 |-  ( x = y -> ( T gsum ( x oF .x. A ) ) = ( T gsum ( y oF .x. A ) ) )
167 ovex 
 |-  ( T gsum ( y oF .x. A ) ) e. _V
168 166 5 167 fvmpt 
 |-  ( y e. B -> ( E ` y ) = ( T gsum ( y oF .x. A ) ) )
169 168 ad2antrl 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( E ` y ) = ( T gsum ( y oF .x. A ) ) )
170 oveq1 
 |-  ( x = z -> ( x oF .x. A ) = ( z oF .x. A ) )
171 170 oveq2d 
 |-  ( x = z -> ( T gsum ( x oF .x. A ) ) = ( T gsum ( z oF .x. A ) ) )
172 ovex 
 |-  ( T gsum ( z oF .x. A ) ) e. _V
173 171 5 172 fvmpt 
 |-  ( z e. B -> ( E ` z ) = ( T gsum ( z oF .x. A ) ) )
174 173 ad2antll 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( E ` z ) = ( T gsum ( z oF .x. A ) ) )
175 169 174 oveq12d 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( ( E ` y ) ( +g ` T ) ( E ` z ) ) = ( ( T gsum ( y oF .x. A ) ) ( +g ` T ) ( T gsum ( z oF .x. A ) ) ) )
176 93 164 175 3eqtr4d 
 |-  ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( E ` ( y ( +g ` F ) z ) ) = ( ( E ` y ) ( +g ` T ) ( E ` z ) ) )
177 2 3 22 23 25 27 77 176 isghmd 
 |-  ( ph -> E e. ( F GrpHom T ) )
178 6 adantr 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> T e. LMod )
179 7 adantr 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> I e. X )
180 21 fveq2d 
 |-  ( ph -> ( Base ` ( Scalar ` T ) ) = ( Base ` ( Scalar ` F ) ) )
181 180 eleq2d 
 |-  ( ph -> ( y e. ( Base ` ( Scalar ` T ) ) <-> y e. ( Base ` ( Scalar ` F ) ) ) )
182 181 biimpar 
 |-  ( ( ph /\ y e. ( Base ` ( Scalar ` F ) ) ) -> y e. ( Base ` ( Scalar ` T ) ) )
183 182 adantrr 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> y e. ( Base ` ( Scalar ` T ) ) )
184 53 adantrl 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> ( z oF .x. A ) : I --> C )
185 184 ffvelrnda 
 |-  ( ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> ( ( z oF .x. A ) ` x ) e. C )
186 53 feqmptd 
 |-  ( ( ph /\ z e. B ) -> ( z oF .x. A ) = ( x e. I |-> ( ( z oF .x. A ) ` x ) ) )
187 186 74 eqbrtrrd 
 |-  ( ( ph /\ z e. B ) -> ( x e. I |-> ( ( z oF .x. A ) ` x ) ) finSupp ( 0g ` T ) )
188 187 adantrl 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> ( x e. I |-> ( ( z oF .x. A ) ` x ) ) finSupp ( 0g ` T ) )
189 3 12 45 34 23 4 178 179 183 185 188 gsumvsmul 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> ( T gsum ( x e. I |-> ( y .x. ( ( z oF .x. A ) ` x ) ) ) ) = ( y .x. ( T gsum ( x e. I |-> ( ( z oF .x. A ) ` x ) ) ) ) )
190 18 adantr 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> F e. LMod )
191 simprl 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> y e. ( Base ` ( Scalar ` F ) ) )
192 simprr 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> z e. B )
193 2 11 10 13 lmodvscl 
 |-  ( ( F e. LMod /\ y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) -> ( y ( .s ` F ) z ) e. B )
194 190 191 192 193 syl3anc 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> ( y ( .s ` F ) z ) e. B )
195 1 48 2 frlmbasf 
 |-  ( ( I e. X /\ ( y ( .s ` F ) z ) e. B ) -> ( y ( .s ` F ) z ) : I --> ( Base ` R ) )
196 179 194 195 syl2anc 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> ( y ( .s ` F ) z ) : I --> ( Base ` R ) )
197 196 ffnd 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> ( y ( .s ` F ) z ) Fn I )
198 115 adantr 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> A Fn I )
199 197 198 179 179 52 offn 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> ( ( y ( .s ` F ) z ) oF .x. A ) Fn I )
200 dffn2 
 |-  ( ( ( y ( .s ` F ) z ) oF .x. A ) Fn I <-> ( ( y ( .s ` F ) z ) oF .x. A ) : I --> _V )
201 199 200 sylib 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> ( ( y ( .s ` F ) z ) oF .x. A ) : I --> _V )
202 201 feqmptd 
 |-  ( ( 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 ) ) )
203 8 fveq2d 
 |-  ( ph -> ( .r ` R ) = ( .r ` ( Scalar ` T ) ) )
204 203 ad2antrr 
 |-  ( ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> ( .r ` R ) = ( .r ` ( Scalar ` T ) ) )
205 204 oveqd 
 |-  ( ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> ( y ( .r ` R ) ( z ` x ) ) = ( y ( .r ` ( Scalar ` T ) ) ( z ` x ) ) )
206 205 oveq1d 
 |-  ( ( ( 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 ) ) )
207 6 ad2antrr 
 |-  ( ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> T e. LMod )
208 simplrl 
 |-  ( ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> y e. ( Base ` ( Scalar ` F ) ) )
209 180 ad2antrr 
 |-  ( ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> ( Base ` ( Scalar ` T ) ) = ( Base ` ( Scalar ` F ) ) )
210 208 209 eleqtrrd 
 |-  ( ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> y e. ( Base ` ( Scalar ` T ) ) )
211 50 ffvelrnda 
 |-  ( ( ( ph /\ z e. B ) /\ x e. I ) -> ( z ` x ) e. ( Base ` R ) )
212 41 ad2antrr 
 |-  ( ( ( ph /\ z e. B ) /\ x e. I ) -> ( Base ` R ) = ( Base ` ( Scalar ` T ) ) )
213 211 212 eleqtrd 
 |-  ( ( ( ph /\ z e. B ) /\ x e. I ) -> ( z ` x ) e. ( Base ` ( Scalar ` T ) ) )
214 213 adantlrl 
 |-  ( ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> ( z ` x ) e. ( Base ` ( Scalar ` T ) ) )
215 9 ffvelrnda 
 |-  ( ( ph /\ x e. I ) -> ( A ` x ) e. C )
216 215 adantlr 
 |-  ( ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> ( A ` x ) e. C )
217 eqid 
 |-  ( .r ` ( Scalar ` T ) ) = ( .r ` ( Scalar ` T ) )
218 3 12 4 45 217 lmodvsass 
 |-  ( ( 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 ) ) ) )
219 207 210 214 216 218 syl13anc 
 |-  ( ( ( 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 ) ) ) )
220 206 219 eqtrd 
 |-  ( ( ( 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 ) ) ) )
221 197 adantr 
 |-  ( ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> ( y ( .s ` F ) z ) Fn I )
222 115 ad2antrr 
 |-  ( ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> A Fn I )
223 7 ad2antrr 
 |-  ( ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> I e. X )
224 simpr 
 |-  ( ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> x e. I )
225 fnfvof 
 |-  ( ( ( ( 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 ) ) )
226 221 222 223 224 225 syl22anc 
 |-  ( ( ( 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 ) ) )
227 20 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` F ) ) )
228 227 ad2antrr 
 |-  ( ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> ( Base ` R ) = ( Base ` ( Scalar ` F ) ) )
229 208 228 eleqtrrd 
 |-  ( ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> y e. ( Base ` R ) )
230 simplrr 
 |-  ( ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> z e. B )
231 eqid 
 |-  ( .r ` R ) = ( .r ` R )
232 1 2 48 223 229 230 224 10 231 frlmvscaval 
 |-  ( ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> ( ( y ( .s ` F ) z ) ` x ) = ( y ( .r ` R ) ( z ` x ) ) )
233 232 oveq1d 
 |-  ( ( ( 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 ) ) )
234 226 233 eqtrd 
 |-  ( ( ( 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 ) ) )
235 50 ffnd 
 |-  ( ( ph /\ z e. B ) -> z Fn I )
236 235 adantrl 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> z Fn I )
237 236 adantr 
 |-  ( ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> z Fn I )
238 237 222 223 224 149 syl22anc 
 |-  ( ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> ( ( z oF .x. A ) ` x ) = ( ( z ` x ) .x. ( A ` x ) ) )
239 238 oveq2d 
 |-  ( ( ( 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 ) ) ) )
240 220 234 239 3eqtr4d 
 |-  ( ( ( 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 ) ) )
241 240 mpteq2dva 
 |-  ( ( 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 ) ) ) )
242 202 241 eqtrd 
 |-  ( ( 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 ) ) ) )
243 242 oveq2d 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> ( T gsum ( ( y ( .s ` F ) z ) oF .x. A ) ) = ( T gsum ( x e. I |-> ( y .x. ( ( z oF .x. A ) ` x ) ) ) ) )
244 184 feqmptd 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> ( z oF .x. A ) = ( x e. I |-> ( ( z oF .x. A ) ` x ) ) )
245 244 oveq2d 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> ( T gsum ( z oF .x. A ) ) = ( T gsum ( x e. I |-> ( ( z oF .x. A ) ` x ) ) ) )
246 245 oveq2d 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> ( y .x. ( T gsum ( z oF .x. A ) ) ) = ( y .x. ( T gsum ( x e. I |-> ( ( z oF .x. A ) ` x ) ) ) ) )
247 189 243 246 3eqtr4d 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> ( T gsum ( ( y ( .s ` F ) z ) oF .x. A ) ) = ( y .x. ( T gsum ( z oF .x. A ) ) ) )
248 oveq1 
 |-  ( x = ( y ( .s ` F ) z ) -> ( x oF .x. A ) = ( ( y ( .s ` F ) z ) oF .x. A ) )
249 248 oveq2d 
 |-  ( x = ( y ( .s ` F ) z ) -> ( T gsum ( x oF .x. A ) ) = ( T gsum ( ( y ( .s ` F ) z ) oF .x. A ) ) )
250 ovex 
 |-  ( T gsum ( ( y ( .s ` F ) z ) oF .x. A ) ) e. _V
251 249 5 250 fvmpt 
 |-  ( ( y ( .s ` F ) z ) e. B -> ( E ` ( y ( .s ` F ) z ) ) = ( T gsum ( ( y ( .s ` F ) z ) oF .x. A ) ) )
252 194 251 syl 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> ( E ` ( y ( .s ` F ) z ) ) = ( T gsum ( ( y ( .s ` F ) z ) oF .x. A ) ) )
253 173 oveq2d 
 |-  ( z e. B -> ( y .x. ( E ` z ) ) = ( y .x. ( T gsum ( z oF .x. A ) ) ) )
254 253 ad2antll 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> ( y .x. ( E ` z ) ) = ( y .x. ( T gsum ( z oF .x. A ) ) ) )
255 247 252 254 3eqtr4d 
 |-  ( ( ph /\ ( y e. ( Base ` ( Scalar ` F ) ) /\ z e. B ) ) -> ( E ` ( y ( .s ` F ) z ) ) = ( y .x. ( E ` z ) ) )
256 2 10 4 11 12 13 18 6 21 177 255 islmhmd 
 |-  ( ph -> E e. ( F LMHom T ) )