Theorem frlmup1 20137

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.

Step	Hyp	Ref	Expression
1		frlmup.b	. 2 |- B = ( Base ` F )
2		eqid 2622	. 2 |- ( .s ` F ) = ( .s ` F )
3		frlmup.v	. 2 |- .x. = ( .s ` T )
4		eqid 2622	. 2 |- (Scalar ` F ) = (Scalar ` F )
5		eqid 2622	. 2 |- (Scalar ` T ) = (Scalar ` T )
6		eqid 2622	. 2 |- ( Base ` (Scalar ` F ) ) = ( Base ` (Scalar ` F ) )
7		frlmup.r	. . . 4 |- ( ph -> R = (Scalar ` T ) )
8		frlmup.t	. . . . 5 |- ( ph -> T e. LMod )
9	5	lmodring 18871	. . . . 5 |- ( T e. LMod -> (Scalar ` T ) e. Ring )
10	8, 9	syl 17	. . . 4 |- ( ph -> (Scalar ` T ) e. Ring )
11	7, 10	eqeltrd 2701	. . 3 |- ( ph -> R e. Ring )
12		frlmup.i	. . 3 |- ( ph -> I e. X )
13		frlmup.f	. . . 4 |- F = ( R freeLMod I )
14	13	frlmlmod 20093	. . 3 |- ( ( R e. Ring /\ I e. X ) -> F e. LMod )
15	11, 12, 14	syl2anc 693	. 2 |- ( ph -> F e. LMod )
16	13	frlmsca 20097	. . . 4 |- ( ( R e. Ring /\ I e. X ) -> R = (Scalar ` F ) )
17	11, 12, 16	syl2anc 693	. . 3 |- ( ph -> R = (Scalar ` F ) )
18	7, 17	eqtr3d 2658	. 2 |- ( ph -> (Scalar ` T ) = (Scalar ` F ) )
19		frlmup.c	. . 3 |- C = ( Base ` T )
20		eqid 2622	. . 3 |- ( +g ` F ) = ( +g ` F )
21		eqid 2622	. . 3 |- ( +g ` T ) = ( +g ` T )
22		lmodgrp 18870	. . . 4 |- ( F e. LMod -> F e. Grp )
23	15, 22	syl 17	. . 3 |- ( ph -> F e. Grp )
24		lmodgrp 18870	. . . 4 |- ( T e. LMod -> T e. Grp )
25	8, 24	syl 17	. . 3 |- ( ph -> T e. Grp )
26		eleq1 2689	. . . . . . 7 |- ( z = x -> ( z e. B <-> x e. B ) )
27	26	anbi2d 740	. . . . . 6 |- ( z = x -> ( ( ph /\ z e. B ) <-> ( ph /\ x e. B ) ) )
28		oveq1 6657	. . . . . . . 8 |- ( z = x -> ( z oF .x. A ) = ( x oF .x. A ) )
29	28	oveq2d 6666	. . . . . . 7 |- ( z = x -> ( T gsumg ( z oF .x. A ) ) = ( T gsumg ( x oF .x. A ) ) )
30	29	eleq1d 2686	. . . . . 6 |- ( z = x -> ( ( T gsumg ( z oF .x. A ) ) e. C <-> ( T gsumg ( x oF .x. A ) ) e. C ) )
31	27, 30	imbi12d 334	. . . . 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 2622	. . . . . 6 |- ( 0g ` T ) = ( 0g ` T )
33		lmodcmn 18911	. . . . . . . 8 |- ( T e. LMod -> T e. CMnd )
34	8, 33	syl 17	. . . . . . 7 |- ( ph -> T e. CMnd )
35	34	adantr 481	. . . . . 6 |- ( ( ph /\ z e. B ) -> T e. CMnd )
36	12	adantr 481	. . . . . 6 |- ( ( ph /\ z e. B ) -> I e. X )
37	8	ad2antrr 762	. . . . . . . 8 |- ( ( ( ph /\ z e. B ) /\ ( x e. ( Base ` R ) /\ y e. C ) ) -> T e. LMod )
38		simprl 794	. . . . . . . . 9 |- ( ( ( ph /\ z e. B ) /\ ( x e. ( Base ` R ) /\ y e. C ) ) -> x e. ( Base ` R ) )
39	7	fveq2d 6195	. . . . . . . . . 10 |- ( ph -> ( Base ` R ) = ( Base ` (Scalar ` T ) ) )
40	39	ad2antrr 762	. . . . . . . . 9 |- ( ( ( ph /\ z e. B ) /\ ( x e. ( Base ` R ) /\ y e. C ) ) -> ( Base ` R ) = ( Base ` (Scalar ` T ) ) )
41	38, 40	eleqtrd 2703	. . . . . . . 8 |- ( ( ( ph /\ z e. B ) /\ ( x e. ( Base ` R ) /\ y e. C ) ) -> x e. ( Base ` (Scalar ` T ) ) )
42		simprr 796	. . . . . . . 8 |- ( ( ( ph /\ z e. B ) /\ ( x e. ( Base ` R ) /\ y e. C ) ) -> y e. C )
43		eqid 2622	. . . . . . . . 9 |- ( Base ` (Scalar ` T ) ) = ( Base ` (Scalar ` T ) )
44	19, 5, 3, 43	lmodvscl 18880	. . . . . . . 8 |- ( ( T e. LMod /\ x e. ( Base ` (Scalar ` T ) ) /\ y e. C ) -> ( x .x. y ) e. C )
45	37, 41, 42, 44	syl3anc 1326	. . . . . . 7 |- ( ( ( ph /\ z e. B ) /\ ( x e. ( Base ` R ) /\ y e. C ) ) -> ( x .x. y ) e. C )
46		eqid 2622	. . . . . . . . 9 |- ( Base ` R ) = ( Base ` R )
47	13, 46, 1	frlmbasf 20104	. . . . . . . 8 |- ( ( I e. X /\ z e. B ) -> z : I --> ( Base ` R ) )
48	12, 47	sylan 488	. . . . . . 7 |- ( ( ph /\ z e. B ) -> z : I --> ( Base ` R ) )
49		frlmup.a	. . . . . . . 8 |- ( ph -> A : I --> C )
50	49	adantr 481	. . . . . . 7 |- ( ( ph /\ z e. B ) -> A : I --> C )
51		inidm 3822	. . . . . . 7 |- ( I i^i I ) = I
52	45, 48, 50, 36, 36, 51	off 6912	. . . . . 6 |- ( ( ph /\ z e. B ) -> ( z oF .x. A ) : I --> C )
53		ovex 6678	. . . . . . . 8 |- ( z oF .x. A ) e. _V
54	53	a1i 11	. . . . . . 7 |- ( ( ph /\ z e. B ) -> ( z oF .x. A ) e. _V )
55		ffun 6048	. . . . . . . 8 |- ( ( z oF .x. A ) : I --> C -> Fun ( z oF .x. A ) )
56	52, 55	syl 17	. . . . . . 7 |- ( ( ph /\ z e. B ) -> Fun ( z oF .x. A ) )
57		fvexd 6203	. . . . . . 7 |- ( ( ph /\ z e. B ) -> ( 0g ` T ) e. _V )
58		eqid 2622	. . . . . . . . . . 11 |- ( 0g ` R ) = ( 0g ` R )
59	13, 58, 1	frlmbasfsupp 20102	. . . . . . . . . 10 |- ( ( I e. X /\ z e. B ) -> z finSupp ( 0g ` R ) )
60	12, 59	sylan 488	. . . . . . . . 9 |- ( ( ph /\ z e. B ) -> z finSupp ( 0g ` R ) )
61	7	fveq2d 6195	. . . . . . . . . . . 12 |- ( ph -> ( 0g ` R ) = ( 0g ` (Scalar ` T ) ) )
62	61	eqcomd 2628	. . . . . . . . . . 11 |- ( ph -> ( 0g ` (Scalar ` T ) ) = ( 0g ` R ) )
63	62	breq2d 4665	. . . . . . . . . 10 |- ( ph -> ( z finSupp ( 0g ` (Scalar ` T ) ) <-> z finSupp ( 0g ` R ) ) )
64	63	adantr 481	. . . . . . . . 9 |- ( ( ph /\ z e. B ) -> ( z finSupp ( 0g ` (Scalar ` T ) ) <-> z finSupp ( 0g ` R ) ) )
65	60, 64	mpbird 247	. . . . . . . 8 |- ( ( ph /\ z e. B ) -> z finSupp ( 0g ` (Scalar ` T ) ) )
66	65	fsuppimpd 8282	. . . . . . 7 |- ( ( ph /\ z e. B ) -> ( z supp ( 0g ` (Scalar ` T ) ) ) e. Fin )
67		ssid 3624	. . . . . . . . 9 |- ( z supp ( 0g ` (Scalar ` T ) ) ) C_ ( z supp ( 0g ` (Scalar ` T ) ) )
68	67	a1i 11	. . . . . . . 8 |- ( ( ph /\ z e. B ) -> ( z supp ( 0g ` (Scalar ` T ) ) ) C_ ( z supp ( 0g ` (Scalar ` T ) ) ) )
69	8	ad2antrr 762	. . . . . . . . 9 |- ( ( ( ph /\ z e. B ) /\ w e. C ) -> T e. LMod )
70		eqid 2622	. . . . . . . . . 10 |- ( 0g ` (Scalar ` T ) ) = ( 0g ` (Scalar ` T ) )
71	19, 5, 3, 70, 32	lmod0vs 18896	. . . . . . . . 9 |- ( ( T e. LMod /\ w e. C ) -> ( ( 0g ` (Scalar ` T ) ) .x. w ) = ( 0g ` T ) )
72	69, 71	sylancom 701	. . . . . . . 8 |- ( ( ( ph /\ z e. B ) /\ w e. C ) -> ( ( 0g ` (Scalar ` T ) ) .x. w ) = ( 0g ` T ) )
73		fvexd 6203	. . . . . . . 8 |- ( ( ph /\ z e. B ) -> ( 0g ` (Scalar ` T ) ) e. _V )
74	68, 72, 48, 50, 36, 73	suppssof1 7328	. . . . . . 7 |- ( ( ph /\ z e. B ) -> ( ( z oF .x. A ) supp ( 0g ` T ) ) C_ ( z supp ( 0g ` (Scalar ` T ) ) ) )
75		suppssfifsupp 8290	. . . . . . 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 ) )
76	54, 56, 57, 66, 74, 75	syl32anc 1334	. . . . . 6 |- ( ( ph /\ z e. B ) -> ( z oF .x. A ) finSupp ( 0g ` T ) )
77	19, 32, 35, 36, 52, 76	gsumcl 18316	. . . . 5 |- ( ( ph /\ z e. B ) -> ( T gsumg ( z oF .x. A ) ) e. C )
78	31, 77	chvarv 2263	. . . 4 |- ( ( ph /\ x e. B ) -> ( T gsumg ( x oF .x. A ) ) e. C )
79		frlmup.e	. . . 4 |- E = ( x e. B |-> ( T gsumg ( x oF .x. A ) ) )
80	78, 79	fmptd 6385	. . 3 |- ( ph -> E : B --> C )
81	34	adantr 481	. . . . 5 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> T e. CMnd )
82	12	adantr 481	. . . . 5 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> I e. X )
83		eleq1 2689	. . . . . . . . 9 |- ( z = y -> ( z e. B <-> y e. B ) )
84	83	anbi2d 740	. . . . . . . 8 |- ( z = y -> ( ( ph /\ z e. B ) <-> ( ph /\ y e. B ) ) )
85		oveq1 6657	. . . . . . . . 9 |- ( z = y -> ( z oF .x. A ) = ( y oF .x. A ) )
86	85	feq1d 6030	. . . . . . . 8 |- ( z = y -> ( ( z oF .x. A ) : I --> C <-> ( y oF .x. A ) : I --> C ) )
87	84, 86	imbi12d 334	. . . . . . 7 |- ( z = y -> ( ( ( ph /\ z e. B ) -> ( z oF .x. A ) : I --> C ) <-> ( ( ph /\ y e. B ) -> ( y oF .x. A ) : I --> C ) ) )
88	87, 52	chvarv 2263	. . . . . 6 |- ( ( ph /\ y e. B ) -> ( y oF .x. A ) : I --> C )
89	88	adantrr 753	. . . . 5 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y oF .x. A ) : I --> C )
90	52	adantrl 752	. . . . 5 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( z oF .x. A ) : I --> C )
91	85	breq1d 4663	. . . . . . . 8 |- ( z = y -> ( ( z oF .x. A ) finSupp ( 0g ` T ) <-> ( y oF .x. A ) finSupp ( 0g ` T ) ) )
92	84, 91	imbi12d 334	. . . . . . 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 ) ) ) )
93	92, 76	chvarv 2263	. . . . . 6 |- ( ( ph /\ y e. B ) -> ( y oF .x. A ) finSupp ( 0g ` T ) )
94	93	adantrr 753	. . . . 5 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y oF .x. A ) finSupp ( 0g ` T ) )
95	76	adantrl 752	. . . . 5 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( z oF .x. A ) finSupp ( 0g ` T ) )
96	19, 32, 21, 81, 82, 89, 90, 94, 95	gsumadd 18323	. . . 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 ) ) ) )
97	1, 20	lmodvacl 18877	. . . . . . . 8 |- ( ( F e. LMod /\ y e. B /\ z e. B ) -> ( y ( +g ` F ) z ) e. B )
98	97	3expb 1266	. . . . . . 7 |- ( ( F e. LMod /\ ( y e. B /\ z e. B ) ) -> ( y ( +g ` F ) z ) e. B )
99	15, 98	sylan 488	. . . . . 6 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y ( +g ` F ) z ) e. B )
100		oveq1 6657	. . . . . . . 8 |- ( x = ( y ( +g ` F ) z ) -> ( x oF .x. A ) = ( ( y ( +g ` F ) z ) oF .x. A ) )
101	100	oveq2d 6666	. . . . . . 7 |- ( x = ( y ( +g ` F ) z ) -> ( T gsumg ( x oF .x. A ) ) = ( T gsumg ( ( y ( +g ` F ) z ) oF .x. A ) ) )
102		ovex 6678	. . . . . . 7 |- ( T gsumg ( ( y ( +g ` F ) z ) oF .x. A ) ) e. _V
103	101, 79, 102	fvmpt 6282	. . . . . 6 |- ( ( y ( +g ` F ) z ) e. B -> ( E ` ( y ( +g ` F ) z ) ) = ( T gsumg ( ( y ( +g ` F ) z ) oF .x. A ) ) )
104	99, 103	syl 17	. . . . 5 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( E ` ( y ( +g ` F ) z ) ) = ( T gsumg ( ( y ( +g ` F ) z ) oF .x. A ) ) )
105	11	adantr 481	. . . . . . . . 9 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> R e. Ring )
106		simprl 794	. . . . . . . . 9 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> y e. B )
107		simprr 796	. . . . . . . . 9 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> z e. B )
108		eqid 2622	. . . . . . . . 9 |- ( +g ` R ) = ( +g ` R )
109	13, 1, 105, 82, 106, 107, 108, 20	frlmplusgval 20107	. . . . . . . 8 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y ( +g ` F ) z ) = ( y oF ( +g ` R ) z ) )
110	109	oveq1d 6665	. . . . . . 7 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( ( y ( +g ` F ) z ) oF .x. A ) = ( ( y oF ( +g ` R ) z ) oF .x. A ) )
111	13, 46, 1	frlmbasf 20104	. . . . . . . . . . . . 13 |- ( ( I e. X /\ y e. B ) -> y : I --> ( Base ` R ) )
112	12, 111	sylan 488	. . . . . . . . . . . 12 |- ( ( ph /\ y e. B ) -> y : I --> ( Base ` R ) )
113	112	adantrr 753	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> y : I --> ( Base ` R ) )
114		ffn 6045	. . . . . . . . . . 11 |- ( y : I --> ( Base ` R ) -> y Fn I )
115	113, 114	syl 17	. . . . . . . . . 10 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> y Fn I )
116	48	adantrl 752	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> z : I --> ( Base ` R ) )
117		ffn 6045	. . . . . . . . . . 11 |- ( z : I --> ( Base ` R ) -> z Fn I )
118	116, 117	syl 17	. . . . . . . . . 10 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> z Fn I )
119	115, 118, 82, 82, 51	offn 6908	. . . . . . . . 9 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y oF ( +g ` R ) z ) Fn I )
120		ffn 6045	. . . . . . . . . . 11 |- ( A : I --> C -> A Fn I )
121	49, 120	syl 17	. . . . . . . . . 10 |- ( ph -> A Fn I )
122	121	adantr 481	. . . . . . . . 9 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> A Fn I )
123	119, 122, 82, 82, 51	offn 6908	. . . . . . . 8 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( ( y oF ( +g ` R ) z ) oF .x. A ) Fn I )
124		ffn 6045	. . . . . . . . . . 11 |- ( ( y oF .x. A ) : I --> C -> ( y oF .x. A ) Fn I )
125	88, 124	syl 17	. . . . . . . . . 10 |- ( ( ph /\ y e. B ) -> ( y oF .x. A ) Fn I )
126	125	adantrr 753	. . . . . . . . 9 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( y oF .x. A ) Fn I )
127		ffn 6045	. . . . . . . . . . 11 |- ( ( z oF .x. A ) : I --> C -> ( z oF .x. A ) Fn I )
128	52, 127	syl 17	. . . . . . . . . 10 |- ( ( ph /\ z e. B ) -> ( z oF .x. A ) Fn I )
129	128	adantrl 752	. . . . . . . . 9 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( z oF .x. A ) Fn I )
130	126, 129, 82, 82, 51	offn 6908	. . . . . . . 8 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( ( y oF .x. A ) oF ( +g ` T ) ( z oF .x. A ) ) Fn I )
131	7	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( ph -> ( +g ` R ) = ( +g ` (Scalar ` T ) ) )
132	131	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( +g ` R ) = ( +g ` (Scalar ` T ) ) )
133	132	oveqd 6667	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( ( y ` x ) ( +g ` R ) ( z ` x ) ) = ( ( y ` x ) ( +g ` (Scalar ` T ) ) ( z ` x ) ) )
134	133	oveq1d 6665	. . . . . . . . . . 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 ) ) )
135	8	ad2antrr 762	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> T e. LMod )
136	113	ffvelrnda 6359	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( y ` x ) e. ( Base ` R ) )
137	39	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( Base ` R ) = ( Base ` (Scalar ` T ) ) )
138	136, 137	eleqtrd 2703	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( y ` x ) e. ( Base ` (Scalar ` T ) ) )
139	116	ffvelrnda 6359	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( z ` x ) e. ( Base ` R ) )
140	139, 137	eleqtrd 2703	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( z ` x ) e. ( Base ` (Scalar ` T ) ) )
141	49	adantr 481	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> A : I --> C )
142	141	ffvelrnda 6359	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( A ` x ) e. C )
143		eqid 2622	. . . . . . . . . . . . 13 |- ( +g ` (Scalar ` T ) ) = ( +g ` (Scalar ` T ) )
144	19, 21, 5, 3, 43, 143	lmodvsdir 18887	. . . . . . . . . . . 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 ) ) ) )
145	135, 138, 140, 142, 144	syl13anc 1328	. . . . . . . . . . 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 ) ) ) )
146	134, 145	eqtrd 2656	. . . . . . . . . 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 ) ) ) )
147	115	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> y Fn I )
148	118	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> z Fn I )
149	12	ad2antrr 762	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> I e. X )
150		simpr 477	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> x e. I )
151		fnfvof 6911	. . . . . . . . . . . 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 ) ) )
152	147, 148, 149, 150, 151	syl22anc 1327	. . . . . . . . . . 11 |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( ( y oF ( +g ` R ) z ) ` x ) = ( ( y ` x ) ( +g ` R ) ( z ` x ) ) )
153	152	oveq1d 6665	. . . . . . . . . 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 ) ) )
154	121	ad2antrr 762	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> A Fn I )
155		fnfvof 6911	. . . . . . . . . . . 12 |- ( ( ( y Fn I /\ A Fn I ) /\ ( I e. X /\ x e. I ) ) -> ( ( y oF .x. A ) ` x ) = ( ( y ` x ) .x. ( A ` x ) ) )
156	147, 154, 149, 150, 155	syl22anc 1327	. . . . . . . . . . 11 |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( ( y oF .x. A ) ` x ) = ( ( y ` x ) .x. ( A ` x ) ) )
157		fnfvof 6911	. . . . . . . . . . . 12 |- ( ( ( z Fn I /\ A Fn I ) /\ ( I e. X /\ x e. I ) ) -> ( ( z oF .x. A ) ` x ) = ( ( z ` x ) .x. ( A ` x ) ) )
158	148, 154, 149, 150, 157	syl22anc 1327	. . . . . . . . . . 11 |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( ( z oF .x. A ) ` x ) = ( ( z ` x ) .x. ( A ` x ) ) )
159	156, 158	oveq12d 6668	. . . . . . . . . 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 ) ) ) )
160	146, 153, 159	3eqtr4d 2666	. . . . . . . . 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 ) ) )
161	119	adantr 481	. . . . . . . . . 10 |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( y oF ( +g ` R ) z ) Fn I )
162		fnfvof 6911	. . . . . . . . . 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 ) ) )
163	161, 154, 149, 150, 162	syl22anc 1327	. . . . . . . . 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 ) ) )
164	126	adantr 481	. . . . . . . . . 10 |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( y oF .x. A ) Fn I )
165	129	adantr 481	. . . . . . . . . 10 |- ( ( ( ph /\ ( y e. B /\ z e. B ) ) /\ x e. I ) -> ( z oF .x. A ) Fn I )
166		fnfvof 6911	. . . . . . . . . 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 ) ) )
167	164, 165, 149, 150, 166	syl22anc 1327	. . . . . . . . 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 ) ) )
168	160, 163, 167	3eqtr4d 2666	. . . . . . . 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 ) )
169	123, 130, 168	eqfnfvd 6314	. . . . . . 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 ) ) )
170	110, 169	eqtrd 2656	. . . . . 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 ) ) )
171	170	oveq2d 6666	. . . . 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 ) ) ) )
172	104, 171	eqtrd 2656	. . . 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 ) ) ) )
173		oveq1 6657	. . . . . . . 8 |- ( x = y -> ( x oF .x. A ) = ( y oF .x. A ) )
174	173	oveq2d 6666	. . . . . . 7 |- ( x = y -> ( T gsumg ( x oF .x. A ) ) = ( T gsumg ( y oF .x. A ) ) )
175		ovex 6678	. . . . . . 7 |- ( T gsumg ( y oF .x. A ) ) e. _V
176	174, 79, 175	fvmpt 6282	. . . . . 6 |- ( y e. B -> ( E ` y ) = ( T gsumg ( y oF .x. A ) ) )
177	176	ad2antrl 764	. . . . 5 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( E ` y ) = ( T gsumg ( y oF .x. A ) ) )
178		oveq1 6657	. . . . . . . 8 |- ( x = z -> ( x oF .x. A ) = ( z oF .x. A ) )
179	178	oveq2d 6666	. . . . . . 7 |- ( x = z -> ( T gsumg ( x oF .x. A ) ) = ( T gsumg ( z oF .x. A ) ) )
180		ovex 6678	. . . . . . 7 |- ( T gsumg ( z oF .x. A ) ) e. _V
181	179, 79, 180	fvmpt 6282	. . . . . 6 |- ( z e. B -> ( E ` z ) = ( T gsumg ( z oF .x. A ) ) )
182	181	ad2antll 765	. . . . 5 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( E ` z ) = ( T gsumg ( z oF .x. A ) ) )
183	177, 182	oveq12d 6668	. . . 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 ) ) ) )
184	96, 172, 183	3eqtr4d 2666	. . 3 |- ( ( ph /\ ( y e. B /\ z e. B ) ) -> ( E ` ( y ( +g ` F ) z ) ) = ( ( E ` y ) ( +g ` T ) ( E ` z ) ) )
185	1, 19, 20, 21, 23, 25, 80, 184	isghmd 17669	. 2 |- ( ph -> E e. ( F GrpHom T ) )
186	8	adantr 481	. . . . 5 |- ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) -> T e. LMod )
187	12	adantr 481	. . . . 5 |- ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) -> I e. X )
188	18	fveq2d 6195	. . . . . . . 8 |- ( ph -> ( Base ` (Scalar ` T ) ) = ( Base ` (Scalar ` F ) ) )
189	188	eleq2d 2687	. . . . . . 7 |- ( ph -> ( y e. ( Base ` (Scalar ` T ) ) <-> y e. ( Base ` (Scalar ` F ) ) ) )
190	189	biimpar 502	. . . . . 6 |- ( ( ph /\ y e. ( Base ` (Scalar ` F ) ) ) -> y e. ( Base ` (Scalar ` T ) ) )
191	190	adantrr 753	. . . . 5 |- ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) -> y e. ( Base ` (Scalar ` T ) ) )
192	52	adantrl 752	. . . . . 6 |- ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) -> ( z oF .x. A ) : I --> C )
193	192	ffvelrnda 6359	. . . . 5 |- ( ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> ( ( z oF .x. A ) ` x ) e. C )
194	52	feqmptd 6249	. . . . . . 7 |- ( ( ph /\ z e. B ) -> ( z oF .x. A ) = ( x e. I |-> ( ( z oF .x. A ) ` x ) ) )
195	194, 76	eqbrtrrd 4677	. . . . . 6 |- ( ( ph /\ z e. B ) -> ( x e. I |-> ( ( z oF .x. A ) ` x ) ) finSupp ( 0g ` T ) )
196	195	adantrl 752	. . . . 5 |- ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) -> ( x e. I |-> ( ( z oF .x. A ) ` x ) ) finSupp ( 0g ` T ) )
197	19, 5, 43, 32, 21, 3, 186, 187, 191, 193, 196	gsumvsmul 18927	. . . 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 ) ) ) ) )
198	15	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) -> F e. LMod )
199		simprl 794	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) -> y e. ( Base ` (Scalar ` F ) ) )
200		simprr 796	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) -> z e. B )
201	1, 4, 2, 6	lmodvscl 18880	. . . . . . . . . . . 12 |- ( ( F e. LMod /\ y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) -> ( y ( .s ` F ) z ) e. B )
202	198, 199, 200, 201	syl3anc 1326	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) -> ( y ( .s ` F ) z ) e. B )
203	13, 46, 1	frlmbasf 20104	. . . . . . . . . . 11 |- ( ( I e. X /\ ( y ( .s ` F ) z ) e. B ) -> ( y ( .s ` F ) z ) : I --> ( Base ` R ) )
204	187, 202, 203	syl2anc 693	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) -> ( y ( .s ` F ) z ) : I --> ( Base ` R ) )
205		ffn 6045	. . . . . . . . . 10 |- ( ( y ( .s ` F ) z ) : I --> ( Base ` R ) -> ( y ( .s ` F ) z ) Fn I )
206	204, 205	syl 17	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) -> ( y ( .s ` F ) z ) Fn I )
207	121	adantr 481	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) -> A Fn I )
208	206, 207, 187, 187, 51	offn 6908	. . . . . . . 8 |- ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) -> ( ( y ( .s ` F ) z ) oF .x. A ) Fn I )
209		dffn2 6047	. . . . . . . 8 |- ( ( ( y ( .s ` F ) z ) oF .x. A ) Fn I <-> ( ( y ( .s ` F ) z ) oF .x. A ) : I --> _V )
210	208, 209	sylib 208	. . . . . . 7 |- ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) -> ( ( y ( .s ` F ) z ) oF .x. A ) : I --> _V )
211	210	feqmptd 6249	. . . . . 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 ) ) )
212	7	fveq2d 6195	. . . . . . . . . . . 12 |- ( ph -> ( .r ` R ) = ( .r ` (Scalar ` T ) ) )
213	212	ad2antrr 762	. . . . . . . . . . 11 |- ( ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> ( .r ` R ) = ( .r ` (Scalar ` T ) ) )
214	213	oveqd 6667	. . . . . . . . . 10 |- ( ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> ( y ( .r ` R ) ( z ` x ) ) = ( y ( .r ` (Scalar ` T ) ) ( z ` x ) ) )
215	214	oveq1d 6665	. . . . . . . . 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 ) ) )
216	8	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> T e. LMod )
217		simplrl 800	. . . . . . . . . . 11 |- ( ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> y e. ( Base ` (Scalar ` F ) ) )
218	188	ad2antrr 762	. . . . . . . . . . 11 |- ( ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> ( Base ` (Scalar ` T ) ) = ( Base ` (Scalar ` F ) ) )
219	217, 218	eleqtrrd 2704	. . . . . . . . . 10 |- ( ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> y e. ( Base ` (Scalar ` T ) ) )
220	48	ffvelrnda 6359	. . . . . . . . . . . 12 |- ( ( ( ph /\ z e. B ) /\ x e. I ) -> ( z ` x ) e. ( Base ` R ) )
221	39	ad2antrr 762	. . . . . . . . . . . 12 |- ( ( ( ph /\ z e. B ) /\ x e. I ) -> ( Base ` R ) = ( Base ` (Scalar ` T ) ) )
222	220, 221	eleqtrd 2703	. . . . . . . . . . 11 |- ( ( ( ph /\ z e. B ) /\ x e. I ) -> ( z ` x ) e. ( Base ` (Scalar ` T ) ) )
223	222	adantlrl 756	. . . . . . . . . 10 |- ( ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> ( z ` x ) e. ( Base ` (Scalar ` T ) ) )
224	49	ffvelrnda 6359	. . . . . . . . . . 11 |- ( ( ph /\ x e. I ) -> ( A ` x ) e. C )
225	224	adantlr 751	. . . . . . . . . 10 |- ( ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> ( A ` x ) e. C )
226		eqid 2622	. . . . . . . . . . 11 |- ( .r ` (Scalar ` T ) ) = ( .r ` (Scalar ` T ) )
227	19, 5, 3, 43, 226	lmodvsass 18888	. . . . . . . . . 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 ) ) ) )
228	216, 219, 223, 225, 227	syl13anc 1328	. . . . . . . . 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 ) ) ) )
229	215, 228	eqtrd 2656	. . . . . . . 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 ) ) ) )
230	206	adantr 481	. . . . . . . . . 10 |- ( ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> ( y ( .s ` F ) z ) Fn I )
231	121	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> A Fn I )
232	12	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> I e. X )
233		simpr 477	. . . . . . . . . 10 |- ( ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> x e. I )
234		fnfvof 6911	. . . . . . . . . 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 ) ) )
235	230, 231, 232, 233, 234	syl22anc 1327	. . . . . . . . 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 ) ) )
236	17	fveq2d 6195	. . . . . . . . . . . . 13 |- ( ph -> ( Base ` R ) = ( Base ` (Scalar ` F ) ) )
237	236	ad2antrr 762	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> ( Base ` R ) = ( Base ` (Scalar ` F ) ) )
238	217, 237	eleqtrrd 2704	. . . . . . . . . . 11 |- ( ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> y e. ( Base ` R ) )
239		simplrr 801	. . . . . . . . . . 11 |- ( ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> z e. B )
240		eqid 2622	. . . . . . . . . . 11 |- ( .r ` R ) = ( .r ` R )
241	13, 1, 46, 232, 238, 239, 233, 2, 240	frlmvscaval 20110	. . . . . . . . . 10 |- ( ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> ( ( y ( .s ` F ) z ) ` x ) = ( y ( .r ` R ) ( z ` x ) ) )
242	241	oveq1d 6665	. . . . . . . . 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 ) ) )
243	235, 242	eqtrd 2656	. . . . . . . 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 ) ) )
244	48, 117	syl 17	. . . . . . . . . . . 12 |- ( ( ph /\ z e. B ) -> z Fn I )
245	244	adantrl 752	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) -> z Fn I )
246	245	adantr 481	. . . . . . . . . 10 |- ( ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> z Fn I )
247	246, 231, 232, 233, 157	syl22anc 1327	. . . . . . . . 9 |- ( ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) /\ x e. I ) -> ( ( z oF .x. A ) ` x ) = ( ( z ` x ) .x. ( A ` x ) ) )
248	247	oveq2d 6666	. . . . . . . 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 ) ) ) )
249	229, 243, 248	3eqtr4d 2666	. . . . . . 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 ) ) )
250	249	mpteq2dva 4744	. . . . . 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 ) ) ) )
251	211, 250	eqtrd 2656	. . . . 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 ) ) ) )
252	251	oveq2d 6666	. . . 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 ) ) ) ) )
253	192	feqmptd 6249	. . . . . 6 |- ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) -> ( z oF .x. A ) = ( x e. I |-> ( ( z oF .x. A ) ` x ) ) )
254	253	oveq2d 6666	. . . . 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 ) ) ) )
255	254	oveq2d 6666	. . . 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 ) ) ) ) )
256	197, 252, 255	3eqtr4d 2666	. . 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 ) ) ) )
257		oveq1 6657	. . . . . 6 |- ( x = ( y ( .s ` F ) z ) -> ( x oF .x. A ) = ( ( y ( .s ` F ) z ) oF .x. A ) )
258	257	oveq2d 6666	. . . . 5 |- ( x = ( y ( .s ` F ) z ) -> ( T gsumg ( x oF .x. A ) ) = ( T gsumg ( ( y ( .s ` F ) z ) oF .x. A ) ) )
259		ovex 6678	. . . . 5 |- ( T gsumg ( ( y ( .s ` F ) z ) oF .x. A ) ) e. _V
260	258, 79, 259	fvmpt 6282	. . . 4 |- ( ( y ( .s ` F ) z ) e. B -> ( E ` ( y ( .s ` F ) z ) ) = ( T gsumg ( ( y ( .s ` F ) z ) oF .x. A ) ) )
261	202, 260	syl 17	. . 3 |- ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) -> ( E ` ( y ( .s ` F ) z ) ) = ( T gsumg ( ( y ( .s ` F ) z ) oF .x. A ) ) )
262	181	oveq2d 6666	. . . 4 |- ( z e. B -> ( y .x. ( E ` z ) ) = ( y .x. ( T gsumg ( z oF .x. A ) ) ) )
263	262	ad2antll 765	. . 3 |- ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) -> ( y .x. ( E ` z ) ) = ( y .x. ( T gsumg ( z oF .x. A ) ) ) )
264	256, 261, 263	3eqtr4d 2666	. 2 |- ( ( ph /\ ( y e. ( Base ` (Scalar ` F ) ) /\ z e. B ) ) -> ( E ` ( y ( .s ` F ) z ) ) = ( y .x. ( E ` z ) ) )
265	1, 2, 3, 4, 5, 6, 15, 8, 18, 185, 264	islmhmd 19039	1 |- ( ph -> E e. ( F LMHom T ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   _Vcvv 3200   C_ wss 3574   class class class wbr 4653   |-> cmpt 4729   Fun wfun 5882   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   oFcof 6895   supp csupp 7295   Fincfn 7955   finSupp cfsupp 8275   Basecbs 15857   +g cplusg 15941   .rcmulr 15942  Scalarcsca 15944   .scvsca 15945   0gc0g 16100   gsum_g cgsu 16101   Grpcgrp 17422  CMndccmn 18193   Ringcrg 18547   LModclmod 18863   LMHom clmhm 19019   freeLMod cfrlm 20090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-sup 8348  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-fz 12327  df-fzo 12466  df-seq 12802  df-hash 13118  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-hom 15966  df-cco 15967  df-0g 16102  df-gsum 16103  df-prds 16108  df-pws 16110  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-mhm 17335  df-submnd 17336  df-grp 17425  df-minusg 17426  df-sbg 17427  df-subg 17591  df-ghm 17658  df-cntz 17750  df-cmn 18195  df-abl 18196  df-mgp 18490  df-ur 18502  df-ring 18549  df-subrg 18778  df-lmod 18865  df-lss 18933  df-lmhm 19022  df-sra 19172  df-rgmod 19173  df-dsmm 20076  df-frlm 20091

This theorem is referenced by:  frlmup3  20139  frlmup4  20140  islindf5  20178  indlcim  20179  lnrfg  37689