Theorem frlmphl 19339

Description: Conditions for a free module to be a pre-Hilbert space. (Contributed by Thierry Arnoux, 21-Jun-2019.) (Proof shortened by AV, 21-Jul-2019.)

Hypotheses

Ref	Expression
frlmphl.y	|- Y = ( R freeLMod I )
frlmphl.b	|- B = ( Base ` R )
frlmphl.t	|- .x. = ( .r ` R )
frlmphl.v	|- V = ( Base ` Y )
frlmphl.j	|- ., = ( .i ` Y )
frlmphl.o	|- O = ( 0g ` Y )
frlmphl.0	|- .0. = ( 0g ` R )
frlmphl.s	|- .* = ( *r ` R )
frlmphl.f	|- ( ph -> R e. Field )
frlmphl.m	|- ( ( ph /\ g e. V /\ ( g ., g ) = .0. ) -> g = O )
frlmphl.u	|- ( ( ph /\ x e. B ) -> ( .* ` x ) = x )
frlmphl.i	|- ( ph -> I e. W )

Assertion

Ref	Expression
frlmphl	|- ( ph -> Y e. PreHil )

Distinct variable groups:   B, g, x   g, I, x   R, g, x   g, V, x   g, W, x   .x. , g, x   g, Y, x   .0. , g, x   ph, g, x   ., , g, x   g, O   x, .*

Allowed substitution hints:   .* ( g)   O( x)

Proof of Theorem frlmphl

Dummy variables f e h i y z k are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		frlmphl.v	. . 3 |- V = ( Base ` Y )
2	1	a1i 11	. 2 |- ( ph -> V = ( Base ` Y ) )
3		eqidd 2452	. 2 |- ( ph -> ( +g ` Y ) = ( +g ` Y ) )
4		eqidd 2452	. 2 |- ( ph -> ( .s ` Y ) = ( .s ` Y ) )
5		frlmphl.j	. . 3 |- ., = ( .i ` Y )
6	5	a1i 11	. 2 |- ( ph -> ., = ( .i ` Y ) )
7		frlmphl.o	. . 3 |- O = ( 0g ` Y )
8	7	a1i 11	. 2 |- ( ph -> O = ( 0g ` Y ) )
9		frlmphl.f	. . . . 5 |- ( ph -> R e. Field )
10		isfld 17984	. . . . 5 |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )
11	9, 10	sylib 200	. . . 4 |- ( ph -> ( R e. DivRing /\ R e. CRing ) )
12	11	simpld 461	. . 3 |- ( ph -> R e. DivRing )
13		frlmphl.i	. . 3 |- ( ph -> I e. W )
14		frlmphl.y	. . . 4 |- Y = ( R freeLMod I )
15	14	frlmsca 19316	. . 3 |- ( ( R e. DivRing /\ I e. W ) -> R = (Scalar ` Y ) )
16	12, 13, 15	syl2anc 667	. 2 |- ( ph -> R = (Scalar ` Y ) )
17		frlmphl.b	. . 3 |- B = ( Base ` R )
18	17	a1i 11	. 2 |- ( ph -> B = ( Base ` R ) )
19		eqidd 2452	. 2 |- ( ph -> ( +g ` R ) = ( +g ` R ) )
20		frlmphl.t	. . 3 |- .x. = ( .r ` R )
21	20	a1i 11	. 2 |- ( ph -> .x. = ( .r ` R ) )
22		frlmphl.s	. . 3 |- .* = ( *r ` R )
23	22	a1i 11	. 2 |- ( ph -> .* = ( *r ` R ) )
24		frlmphl.0	. . 3 |- .0. = ( 0g ` R )
25	24	a1i 11	. 2 |- ( ph -> .0. = ( 0g ` R ) )
26		drngring 17982	. . . . 5 |- ( R e. DivRing -> R e. Ring )
27	12, 26	syl 17	. . . 4 |- ( ph -> R e. Ring )
28	14	frlmlmod 19312	. . . 4 |- ( ( R e. Ring /\ I e. W ) -> Y e. LMod )
29	27, 13, 28	syl2anc 667	. . 3 |- ( ph -> Y e. LMod )
30	16, 12	eqeltrrd 2530	. . 3 |- ( ph -> (Scalar ` Y ) e. DivRing )
31		eqid 2451	. . . 4 |- (Scalar ` Y ) = (Scalar ` Y )
32	31	islvec 18327	. . 3 |- ( Y e. LVec <-> ( Y e. LMod /\ (Scalar ` Y ) e. DivRing ) )
33	29, 30, 32	sylanbrc 670	. 2 |- ( ph -> Y e. LVec )
34	11	simprd 465	. . 3 |- ( ph -> R e. CRing )
35		frlmphl.u	. . 3 |- ( ( ph /\ x e. B ) -> ( .* ` x ) = x )
36	17, 22, 34, 35	idsrngd 18090	. 2 |- ( ph -> R e. *Ring )
37	13	3ad2ant1 1029	. . . . 5 |- ( ( ph /\ g e. V /\ h e. V ) -> I e. W )
38	27	3ad2ant1 1029	. . . . 5 |- ( ( ph /\ g e. V /\ h e. V ) -> R e. Ring )
39		simp2 1009	. . . . 5 |- ( ( ph /\ g e. V /\ h e. V ) -> g e. V )
40		simp3 1010	. . . . 5 |- ( ( ph /\ g e. V /\ h e. V ) -> h e. V )
41	14, 17, 20, 1, 5	frlmipval 19337	. . . . 5 |- ( ( ( I e. W /\ R e. Ring ) /\ ( g e. V /\ h e. V ) ) -> ( g ., h ) = ( R gsumg ( g oF .x. h ) ) )
42	37, 38, 39, 40, 41	syl22anc 1269	. . . 4 |- ( ( ph /\ g e. V /\ h e. V ) -> ( g ., h ) = ( R gsumg ( g oF .x. h ) ) )
43	14, 17, 1	frlmbasmap 19322	. . . . . . . . 9 |- ( ( I e. W /\ g e. V ) -> g e. ( B ^m I ) )
44	37, 39, 43	syl2anc 667	. . . . . . . 8 |- ( ( ph /\ g e. V /\ h e. V ) -> g e. ( B ^m I ) )
45		elmapi 7493	. . . . . . . 8 |- ( g e. ( B ^m I ) -> g : I --> B )
46	44, 45	syl 17	. . . . . . 7 |- ( ( ph /\ g e. V /\ h e. V ) -> g : I --> B )
47		ffn 5728	. . . . . . 7 |- ( g : I --> B -> g Fn I )
48	46, 47	syl 17	. . . . . 6 |- ( ( ph /\ g e. V /\ h e. V ) -> g Fn I )
49	14, 17, 1	frlmbasmap 19322	. . . . . . . . 9 |- ( ( I e. W /\ h e. V ) -> h e. ( B ^m I ) )
50	37, 40, 49	syl2anc 667	. . . . . . . 8 |- ( ( ph /\ g e. V /\ h e. V ) -> h e. ( B ^m I ) )
51		elmapi 7493	. . . . . . . 8 |- ( h e. ( B ^m I ) -> h : I --> B )
52	50, 51	syl 17	. . . . . . 7 |- ( ( ph /\ g e. V /\ h e. V ) -> h : I --> B )
53		ffn 5728	. . . . . . 7 |- ( h : I --> B -> h Fn I )
54	52, 53	syl 17	. . . . . 6 |- ( ( ph /\ g e. V /\ h e. V ) -> h Fn I )
55		inidm 3641	. . . . . 6 |- ( I i^i I ) = I
56		eqidd 2452	. . . . . 6 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( g ` x ) = ( g ` x ) )
57		eqidd 2452	. . . . . 6 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( h ` x ) = ( h ` x ) )
58	48, 54, 37, 37, 55, 56, 57	offval 6538	. . . . 5 |- ( ( ph /\ g e. V /\ h e. V ) -> ( g oF .x. h ) = ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) )
59	58	oveq2d 6306	. . . 4 |- ( ( ph /\ g e. V /\ h e. V ) -> ( R gsumg ( g oF .x. h ) ) = ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) )
60	42, 59	eqtrd 2485	. . 3 |- ( ( ph /\ g e. V /\ h e. V ) -> ( g ., h ) = ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) )
61		ringcmn 17811	. . . . . 6 |- ( R e. Ring -> R e. CMnd )
62	27, 61	syl 17	. . . . 5 |- ( ph -> R e. CMnd )
63	62	3ad2ant1 1029	. . . 4 |- ( ( ph /\ g e. V /\ h e. V ) -> R e. CMnd )
64	38	adantr 467	. . . . . 6 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> R e. Ring )
65	46	ffvelrnda 6022	. . . . . 6 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( g ` x ) e. B )
66	52	ffvelrnda 6022	. . . . . 6 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( h ` x ) e. B )
67	17, 20	ringcl 17794	. . . . . 6 |- ( ( R e. Ring /\ ( g ` x ) e. B /\ ( h ` x ) e. B ) -> ( ( g ` x ) .x. ( h ` x ) ) e. B )
68	64, 65, 66, 67	syl3anc 1268	. . . . 5 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( ( g ` x ) .x. ( h ` x ) ) e. B )
69		eqid 2451	. . . . 5 |- ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) = ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) )
70	68, 69	fmptd 6046	. . . 4 |- ( ( ph /\ g e. V /\ h e. V ) -> ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) : I --> B )
71		frlmphl.m	. . . . 5 |- ( ( ph /\ g e. V /\ ( g ., g ) = .0. ) -> g = O )
72	14, 17, 20, 1, 5, 7, 24, 22, 9, 71, 35, 13	frlmphllem 19338	. . . 4 |- ( ( ph /\ g e. V /\ h e. V ) -> ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) finSupp .0. )
73	17, 24, 63, 37, 70, 72	gsumcl 17549	. . 3 |- ( ( ph /\ g e. V /\ h e. V ) -> ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) e. B )
74	60, 73	eqeltrd 2529	. 2 |- ( ( ph /\ g e. V /\ h e. V ) -> ( g ., h ) e. B )
75		eqid 2451	. . . 4 |- ( +g ` R ) = ( +g ` R )
76	62	3ad2ant1 1029	. . . 4 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> R e. CMnd )
77	13	3ad2ant1 1029	. . . 4 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> I e. W )
78	27	3ad2ant1 1029	. . . . . 6 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> R e. Ring )
79	78	adantr 467	. . . . 5 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> R e. Ring )
80		simp2 1009	. . . . . 6 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> k e. B )
81	80	adantr 467	. . . . 5 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> k e. B )
82		simp31 1044	. . . . . . . . 9 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> g e. V )
83	77, 82, 43	syl2anc 667	. . . . . . . 8 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> g e. ( B ^m I ) )
84	83, 45	syl 17	. . . . . . 7 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> g : I --> B )
85	84	ffvelrnda 6022	. . . . . 6 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( g ` x ) e. B )
86		simp33 1046	. . . . . . . . 9 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> i e. V )
87	14, 17, 1	frlmbasmap 19322	. . . . . . . . 9 |- ( ( I e. W /\ i e. V ) -> i e. ( B ^m I ) )
88	77, 86, 87	syl2anc 667	. . . . . . . 8 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> i e. ( B ^m I ) )
89		elmapi 7493	. . . . . . . 8 |- ( i e. ( B ^m I ) -> i : I --> B )
90	88, 89	syl 17	. . . . . . 7 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> i : I --> B )
91	90	ffvelrnda 6022	. . . . . 6 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( i ` x ) e. B )
92	17, 20	ringcl 17794	. . . . . 6 |- ( ( R e. Ring /\ ( g ` x ) e. B /\ ( i ` x ) e. B ) -> ( ( g ` x ) .x. ( i ` x ) ) e. B )
93	79, 85, 91, 92	syl3anc 1268	. . . . 5 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( ( g ` x ) .x. ( i ` x ) ) e. B )
94	17, 20	ringcl 17794	. . . . 5 |- ( ( R e. Ring /\ k e. B /\ ( ( g ` x ) .x. ( i ` x ) ) e. B ) -> ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) e. B )
95	79, 81, 93, 94	syl3anc 1268	. . . 4 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) e. B )
96		simp32 1045	. . . . . . . 8 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> h e. V )
97	77, 96, 49	syl2anc 667	. . . . . . 7 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> h e. ( B ^m I ) )
98	97, 51	syl 17	. . . . . 6 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> h : I --> B )
99	98	ffvelrnda 6022	. . . . 5 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( h ` x ) e. B )
100	17, 20	ringcl 17794	. . . . 5 |- ( ( R e. Ring /\ ( h ` x ) e. B /\ ( i ` x ) e. B ) -> ( ( h ` x ) .x. ( i ` x ) ) e. B )
101	79, 99, 91, 100	syl3anc 1268	. . . 4 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( ( h ` x ) .x. ( i ` x ) ) e. B )
102		eqidd 2452	. . . 4 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( x e. I |-> ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ) = ( x e. I |-> ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ) )
103		eqidd 2452	. . . 4 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( x e. I |-> ( ( h ` x ) .x. ( i ` x ) ) ) = ( x e. I |-> ( ( h ` x ) .x. ( i ` x ) ) ) )
104		fveq2 5865	. . . . . . . . 9 |- ( x = y -> ( g ` x ) = ( g ` y ) )
105	104	oveq2d 6306	. . . . . . . 8 |- ( x = y -> ( k .x. ( g ` x ) ) = ( k .x. ( g ` y ) ) )
106	105	cbvmptv 4495	. . . . . . 7 |- ( x e. I |-> ( k .x. ( g ` x ) ) ) = ( y e. I |-> ( k .x. ( g ` y ) ) )
107	106	oveq1i 6300	. . . . . 6 |- ( ( x e. I |-> ( k .x. ( g ` x ) ) ) oF .x. i ) = ( ( y e. I |-> ( k .x. ( g ` y ) ) ) oF .x. i )
108	17, 20	ringcl 17794	. . . . . . . . . . . 12 |- ( ( R e. Ring /\ k e. B /\ ( g ` x ) e. B ) -> ( k .x. ( g ` x ) ) e. B )
109	79, 81, 85, 108	syl3anc 1268	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( k .x. ( g ` x ) ) e. B )
110		eqid 2451	. . . . . . . . . . 11 |- ( x e. I |-> ( k .x. ( g ` x ) ) ) = ( x e. I |-> ( k .x. ( g ` x ) ) )
111	109, 110	fmptd 6046	. . . . . . . . . 10 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( x e. I |-> ( k .x. ( g ` x ) ) ) : I --> B )
112		ffn 5728	. . . . . . . . . 10 |- ( ( x e. I |-> ( k .x. ( g ` x ) ) ) : I --> B -> ( x e. I |-> ( k .x. ( g ` x ) ) ) Fn I )
113	111, 112	syl 17	. . . . . . . . 9 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( x e. I |-> ( k .x. ( g ` x ) ) ) Fn I )
114	106	fneq1i 5670	. . . . . . . . 9 |- ( ( x e. I |-> ( k .x. ( g ` x ) ) ) Fn I <-> ( y e. I |-> ( k .x. ( g ` y ) ) ) Fn I )
115	113, 114	sylib 200	. . . . . . . 8 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( y e. I |-> ( k .x. ( g ` y ) ) ) Fn I )
116		ffn 5728	. . . . . . . . 9 |- ( i : I --> B -> i Fn I )
117	90, 116	syl 17	. . . . . . . 8 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> i Fn I )
118		eqidd 2452	. . . . . . . . 9 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( y e. I |-> ( k .x. ( g ` y ) ) ) = ( y e. I |-> ( k .x. ( g ` y ) ) ) )
119		simpr 463	. . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) /\ y = x ) -> y = x )
120	119	fveq2d 5869	. . . . . . . . . 10 |- ( ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) /\ y = x ) -> ( g ` y ) = ( g ` x ) )
121	120	oveq2d 6306	. . . . . . . . 9 |- ( ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) /\ y = x ) -> ( k .x. ( g ` y ) ) = ( k .x. ( g ` x ) ) )
122		simpr 463	. . . . . . . . 9 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> x e. I )
123		ovex 6318	. . . . . . . . . 10 |- ( k .x. ( g ` x ) ) e. _V
124	123	a1i 11	. . . . . . . . 9 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( k .x. ( g ` x ) ) e. _V )
125	118, 121, 122, 124	fvmptd 5954	. . . . . . . 8 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( ( y e. I |-> ( k .x. ( g ` y ) ) ) ` x ) = ( k .x. ( g ` x ) ) )
126		eqidd 2452	. . . . . . . 8 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( i ` x ) = ( i ` x ) )
127	115, 117, 77, 77, 55, 125, 126	offval 6538	. . . . . . 7 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( ( y e. I |-> ( k .x. ( g ` y ) ) ) oF .x. i ) = ( x e. I |-> ( ( k .x. ( g ` x ) ) .x. ( i ` x ) ) ) )
128	17, 20	ringass 17797	. . . . . . . . 9 |- ( ( R e. Ring /\ ( k e. B /\ ( g ` x ) e. B /\ ( i ` x ) e. B ) ) -> ( ( k .x. ( g ` x ) ) .x. ( i ` x ) ) = ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) )
129	79, 81, 85, 91, 128	syl13anc 1270	. . . . . . . 8 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( ( k .x. ( g ` x ) ) .x. ( i ` x ) ) = ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) )
130	129	mpteq2dva 4489	. . . . . . 7 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( x e. I |-> ( ( k .x. ( g ` x ) ) .x. ( i ` x ) ) ) = ( x e. I |-> ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ) )
131	127, 130	eqtrd 2485	. . . . . 6 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( ( y e. I |-> ( k .x. ( g ` y ) ) ) oF .x. i ) = ( x e. I |-> ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ) )
132	107, 131	syl5eq 2497	. . . . 5 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( ( x e. I |-> ( k .x. ( g ` x ) ) ) oF .x. i ) = ( x e. I |-> ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ) )
133		ovex 6318	. . . . . . 7 |- ( ( x e. I |-> ( k .x. ( g ` x ) ) ) oF .x. i ) e. _V
134	133	a1i 11	. . . . . 6 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( ( x e. I |-> ( k .x. ( g ` x ) ) ) oF .x. i ) e. _V )
135		funmpt 5618	. . . . . . 7 |- Fun ( z e. I |-> ( ( ( x e. I |-> ( k .x. ( g ` x ) ) ) ` z ) .x. ( i ` z ) ) )
136		eqidd 2452	. . . . . . . . 9 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ z e. I ) -> ( ( x e. I |-> ( k .x. ( g ` x ) ) ) ` z ) = ( ( x e. I |-> ( k .x. ( g ` x ) ) ) ` z ) )
137		eqidd 2452	. . . . . . . . 9 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ z e. I ) -> ( i ` z ) = ( i ` z ) )
138	113, 117, 77, 77, 55, 136, 137	offval 6538	. . . . . . . 8 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( ( x e. I |-> ( k .x. ( g ` x ) ) ) oF .x. i ) = ( z e. I |-> ( ( ( x e. I |-> ( k .x. ( g ` x ) ) ) ` z ) .x. ( i ` z ) ) ) )
139	138	funeqd 5603	. . . . . . 7 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( Fun ( ( x e. I |-> ( k .x. ( g ` x ) ) ) oF .x. i ) <-> Fun ( z e. I |-> ( ( ( x e. I |-> ( k .x. ( g ` x ) ) ) ` z ) .x. ( i ` z ) ) ) ) )
140	135, 139	mpbiri 237	. . . . . 6 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> Fun ( ( x e. I |-> ( k .x. ( g ` x ) ) ) oF .x. i ) )
141		simp3 1010	. . . . . . . . 9 |- ( ( g e. V /\ h e. V /\ i e. V ) -> i e. V )
142	13, 141	anim12i 570	. . . . . . . 8 |- ( ( ph /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( I e. W /\ i e. V ) )
143	142	3adant2 1027	. . . . . . 7 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( I e. W /\ i e. V ) )
144	14, 24, 1	frlmbasfsupp 19321	. . . . . . 7 |- ( ( I e. W /\ i e. V ) -> i finSupp .0. )
145	143, 144	syl 17	. . . . . 6 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> i finSupp .0. )
146	17, 24	ring0cl 17802	. . . . . . . 8 |- ( R e. Ring -> .0. e. B )
147	78, 146	syl 17	. . . . . . 7 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> .0. e. B )
148	17, 20, 24	ringrz 17818	. . . . . . . 8 |- ( ( R e. Ring /\ y e. B ) -> ( y .x. .0. ) = .0. )
149	78, 148	sylan 474	. . . . . . 7 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ y e. B ) -> ( y .x. .0. ) = .0. )
150	77, 147, 111, 90, 149	suppofss2d 6953	. . . . . 6 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( ( ( x e. I |-> ( k .x. ( g ` x ) ) ) oF .x. i ) supp .0. ) C_ ( i supp .0. ) )
151		fsuppsssupp 7899	. . . . . 6 |- ( ( ( ( ( x e. I |-> ( k .x. ( g ` x ) ) ) oF .x. i ) e. _V /\ Fun ( ( x e. I |-> ( k .x. ( g ` x ) ) ) oF .x. i ) ) /\ ( i finSupp .0. /\ ( ( ( x e. I |-> ( k .x. ( g ` x ) ) ) oF .x. i ) supp .0. ) C_ ( i supp .0. ) ) ) -> ( ( x e. I |-> ( k .x. ( g ` x ) ) ) oF .x. i ) finSupp .0. )
152	134, 140, 145, 150, 151	syl22anc 1269	. . . . 5 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( ( x e. I |-> ( k .x. ( g ` x ) ) ) oF .x. i ) finSupp .0. )
153	132, 152	eqbrtrrd 4425	. . . 4 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( x e. I |-> ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ) finSupp .0. )
154		simp1 1008	. . . . 5 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ph )
155		eleq1 2517	. . . . . . . . 9 |- ( g = h -> ( g e. V <-> h e. V ) )
156		id 22	. . . . . . . . . . 11 |- ( g = h -> g = h )
157	156, 156	oveq12d 6308	. . . . . . . . . 10 |- ( g = h -> ( g ., g ) = ( h ., h ) )
158	157	eqeq1d 2453	. . . . . . . . 9 |- ( g = h -> ( ( g ., g ) = .0. <-> ( h ., h ) = .0. ) )
159	155, 158	3anbi23d 1342	. . . . . . . 8 |- ( g = h -> ( ( ph /\ g e. V /\ ( g ., g ) = .0. ) <-> ( ph /\ h e. V /\ ( h ., h ) = .0. ) ) )
160		eqeq1 2455	. . . . . . . 8 |- ( g = h -> ( g = O <-> h = O ) )
161	159, 160	imbi12d 322	. . . . . . 7 |- ( g = h -> ( ( ( ph /\ g e. V /\ ( g ., g ) = .0. ) -> g = O ) <-> ( ( ph /\ h e. V /\ ( h ., h ) = .0. ) -> h = O ) ) )
162	161, 71	chvarv 2107	. . . . . 6 |- ( ( ph /\ h e. V /\ ( h ., h ) = .0. ) -> h = O )
163	14, 17, 20, 1, 5, 7, 24, 22, 9, 162, 35, 13	frlmphllem 19338	. . . . 5 |- ( ( ph /\ h e. V /\ i e. V ) -> ( x e. I |-> ( ( h ` x ) .x. ( i ` x ) ) ) finSupp .0. )
164	154, 96, 86, 163	syl3anc 1268	. . . 4 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( x e. I |-> ( ( h ` x ) .x. ( i ` x ) ) ) finSupp .0. )
165	17, 24, 75, 76, 77, 95, 101, 102, 103, 153, 164	gsummptfsadd 17557	. . 3 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( R gsumg ( x e. I |-> ( ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ( +g ` R ) ( ( h ` x ) .x. ( i ` x ) ) ) ) ) = ( ( R gsumg ( x e. I |-> ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ) ) ( +g ` R ) ( R gsumg ( x e. I |-> ( ( h ` x ) .x. ( i ` x ) ) ) ) ) )
166	14, 17, 20	frlmip 19336	. . . . . . . . 9 |- ( ( I e. W /\ R e. DivRing ) -> ( g e. ( B ^m I ) , h e. ( B ^m I ) |-> ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) ) = ( .i ` Y ) )
167	13, 12, 166	syl2anc 667	. . . . . . . 8 |- ( ph -> ( g e. ( B ^m I ) , h e. ( B ^m I ) |-> ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) ) = ( .i ` Y ) )
168	167, 5	syl6reqr 2504	. . . . . . 7 |- ( ph -> ., = ( g e. ( B ^m I ) , h e. ( B ^m I ) |-> ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) ) )
169		fveq1 5864	. . . . . . . . . . 11 |- ( e = g -> ( e ` x ) = ( g ` x ) )
170	169	oveq1d 6305	. . . . . . . . . 10 |- ( e = g -> ( ( e ` x ) .x. ( f ` x ) ) = ( ( g ` x ) .x. ( f ` x ) ) )
171	170	mpteq2dv 4490	. . . . . . . . 9 |- ( e = g -> ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) = ( x e. I |-> ( ( g ` x ) .x. ( f ` x ) ) ) )
172	171	oveq2d 6306	. . . . . . . 8 |- ( e = g -> ( R gsumg ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) ) = ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( f ` x ) ) ) ) )
173		fveq1 5864	. . . . . . . . . . 11 |- ( f = h -> ( f ` x ) = ( h ` x ) )
174	173	oveq2d 6306	. . . . . . . . . 10 |- ( f = h -> ( ( g ` x ) .x. ( f ` x ) ) = ( ( g ` x ) .x. ( h ` x ) ) )
175	174	mpteq2dv 4490	. . . . . . . . 9 |- ( f = h -> ( x e. I |-> ( ( g ` x ) .x. ( f ` x ) ) ) = ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) )
176	175	oveq2d 6306	. . . . . . . 8 |- ( f = h -> ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( f ` x ) ) ) ) = ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) )
177	172, 176	cbvmpt2v 6371	. . . . . . 7 |- ( e e. ( B ^m I ) , f e. ( B ^m I ) |-> ( R gsumg ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) ) ) = ( g e. ( B ^m I ) , h e. ( B ^m I ) |-> ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) )
178	168, 177	syl6eqr 2503	. . . . . 6 |- ( ph -> ., = ( e e. ( B ^m I ) , f e. ( B ^m I ) |-> ( R gsumg ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) ) ) )
179	178	3ad2ant1 1029	. . . . 5 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ., = ( e e. ( B ^m I ) , f e. ( B ^m I ) |-> ( R gsumg ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) ) ) )
180		simprl 764	. . . . . . . . 9 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) /\ f = i ) ) -> e = ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) )
181	180	fveq1d 5867	. . . . . . . 8 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) /\ f = i ) ) -> ( e ` x ) = ( ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) ` x ) )
182		simprr 766	. . . . . . . . 9 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) /\ f = i ) ) -> f = i )
183	182	fveq1d 5867	. . . . . . . 8 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) /\ f = i ) ) -> ( f ` x ) = ( i ` x ) )
184	181, 183	oveq12d 6308	. . . . . . 7 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) /\ f = i ) ) -> ( ( e ` x ) .x. ( f ` x ) ) = ( ( ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) ` x ) .x. ( i ` x ) ) )
185	184	mpteq2dv 4490	. . . . . 6 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) /\ f = i ) ) -> ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) = ( x e. I |-> ( ( ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) ` x ) .x. ( i ` x ) ) ) )
186	185	oveq2d 6306	. . . . 5 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) /\ f = i ) ) -> ( R gsumg ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) ) = ( R gsumg ( x e. I |-> ( ( ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) ` x ) .x. ( i ` x ) ) ) ) )
187	29	3ad2ant1 1029	. . . . . . 7 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> Y e. LMod )
188	16	3ad2ant1 1029	. . . . . . . . . . 11 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> R = (Scalar ` Y ) )
189	188	fveq2d 5869	. . . . . . . . . 10 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( Base ` R ) = ( Base ` (Scalar ` Y ) ) )
190	17, 189	syl5eq 2497	. . . . . . . . 9 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> B = ( Base ` (Scalar ` Y ) ) )
191	80, 190	eleqtrd 2531	. . . . . . . 8 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> k e. ( Base ` (Scalar ` Y ) ) )
192		eqid 2451	. . . . . . . . 9 |- ( .s ` Y ) = ( .s ` Y )
193		eqid 2451	. . . . . . . . 9 |- ( Base ` (Scalar ` Y ) ) = ( Base ` (Scalar ` Y ) )
194	1, 31, 192, 193	lmodvscl 18108	. . . . . . . 8 |- ( ( Y e. LMod /\ k e. ( Base ` (Scalar ` Y ) ) /\ g e. V ) -> ( k ( .s ` Y ) g ) e. V )
195	187, 191, 82, 194	syl3anc 1268	. . . . . . 7 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( k ( .s ` Y ) g ) e. V )
196		eqid 2451	. . . . . . . 8 |- ( +g ` Y ) = ( +g ` Y )
197	1, 196	lmodvacl 18105	. . . . . . 7 |- ( ( Y e. LMod /\ ( k ( .s ` Y ) g ) e. V /\ h e. V ) -> ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) e. V )
198	187, 195, 96, 197	syl3anc 1268	. . . . . 6 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) e. V )
199	14, 17, 1	frlmbasmap 19322	. . . . . 6 |- ( ( I e. W /\ ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) e. V ) -> ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) e. ( B ^m I ) )
200	77, 198, 199	syl2anc 667	. . . . 5 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) e. ( B ^m I ) )
201		ovex 6318	. . . . . 6 |- ( R gsumg ( x e. I |-> ( ( ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) ` x ) .x. ( i ` x ) ) ) ) e. _V
202	201	a1i 11	. . . . 5 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( R gsumg ( x e. I |-> ( ( ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) ` x ) .x. ( i ` x ) ) ) ) e. _V )
203	179, 186, 200, 88, 202	ovmpt2d 6424	. . . 4 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) ., i ) = ( R gsumg ( x e. I |-> ( ( ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) ` x ) .x. ( i ` x ) ) ) ) )
204	14, 1, 78, 77, 195, 96, 75, 196	frlmplusgval 19326	. . . . . . . . . 10 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) = ( ( k ( .s ` Y ) g ) oF ( +g ` R ) h ) )
205	14, 17, 1	frlmbasmap 19322	. . . . . . . . . . . . 13 |- ( ( I e. W /\ ( k ( .s ` Y ) g ) e. V ) -> ( k ( .s ` Y ) g ) e. ( B ^m I ) )
206	77, 195, 205	syl2anc 667	. . . . . . . . . . . 12 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( k ( .s ` Y ) g ) e. ( B ^m I ) )
207		elmapi 7493	. . . . . . . . . . . 12 |- ( ( k ( .s ` Y ) g ) e. ( B ^m I ) -> ( k ( .s ` Y ) g ) : I --> B )
208		ffn 5728	. . . . . . . . . . . 12 |- ( ( k ( .s ` Y ) g ) : I --> B -> ( k ( .s ` Y ) g ) Fn I )
209	206, 207, 208	3syl 18	. . . . . . . . . . 11 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( k ( .s ` Y ) g ) Fn I )
210	98, 53	syl 17	. . . . . . . . . . 11 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> h Fn I )
211	77	adantr 467	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> I e. W )
212	82	adantr 467	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> g e. V )
213	14, 1, 17, 211, 81, 212, 122, 192, 20	frlmvscaval 19329	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( ( k ( .s ` Y ) g ) ` x ) = ( k .x. ( g ` x ) ) )
214		eqidd 2452	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( h ` x ) = ( h ` x ) )
215	209, 210, 77, 77, 55, 213, 214	offval 6538	. . . . . . . . . 10 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( ( k ( .s ` Y ) g ) oF ( +g ` R ) h ) = ( x e. I |-> ( ( k .x. ( g ` x ) ) ( +g ` R ) ( h ` x ) ) ) )
216	204, 215	eqtrd 2485	. . . . . . . . 9 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) = ( x e. I |-> ( ( k .x. ( g ` x ) ) ( +g ` R ) ( h ` x ) ) ) )
217		ovex 6318	. . . . . . . . . 10 |- ( ( k .x. ( g ` x ) ) ( +g ` R ) ( h ` x ) ) e. _V
218	217	a1i 11	. . . . . . . . 9 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( ( k .x. ( g ` x ) ) ( +g ` R ) ( h ` x ) ) e. _V )
219	216, 218	fvmpt2d 5959	. . . . . . . 8 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) ` x ) = ( ( k .x. ( g ` x ) ) ( +g ` R ) ( h ` x ) ) )
220	219	oveq1d 6305	. . . . . . 7 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( ( ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) ` x ) .x. ( i ` x ) ) = ( ( ( k .x. ( g ` x ) ) ( +g ` R ) ( h ` x ) ) .x. ( i ` x ) ) )
221	17, 75, 20	ringdir 17800	. . . . . . . 8 |- ( ( R e. Ring /\ ( ( k .x. ( g ` x ) ) e. B /\ ( h ` x ) e. B /\ ( i ` x ) e. B ) ) -> ( ( ( k .x. ( g ` x ) ) ( +g ` R ) ( h ` x ) ) .x. ( i ` x ) ) = ( ( ( k .x. ( g ` x ) ) .x. ( i ` x ) ) ( +g ` R ) ( ( h ` x ) .x. ( i ` x ) ) ) )
222	79, 109, 99, 91, 221	syl13anc 1270	. . . . . . 7 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( ( ( k .x. ( g ` x ) ) ( +g ` R ) ( h ` x ) ) .x. ( i ` x ) ) = ( ( ( k .x. ( g ` x ) ) .x. ( i ` x ) ) ( +g ` R ) ( ( h ` x ) .x. ( i ` x ) ) ) )
223	129	oveq1d 6305	. . . . . . 7 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( ( ( k .x. ( g ` x ) ) .x. ( i ` x ) ) ( +g ` R ) ( ( h ` x ) .x. ( i ` x ) ) ) = ( ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ( +g ` R ) ( ( h ` x ) .x. ( i ` x ) ) ) )
224	220, 222, 223	3eqtrd 2489	. . . . . 6 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( ( ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) ` x ) .x. ( i ` x ) ) = ( ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ( +g ` R ) ( ( h ` x ) .x. ( i ` x ) ) ) )
225	224	mpteq2dva 4489	. . . . 5 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( x e. I |-> ( ( ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) ` x ) .x. ( i ` x ) ) ) = ( x e. I |-> ( ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ( +g ` R ) ( ( h ` x ) .x. ( i ` x ) ) ) ) )
226	225	oveq2d 6306	. . . 4 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( R gsumg ( x e. I |-> ( ( ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) ` x ) .x. ( i ` x ) ) ) ) = ( R gsumg ( x e. I |-> ( ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ( +g ` R ) ( ( h ` x ) .x. ( i ` x ) ) ) ) ) )
227	203, 226	eqtrd 2485	. . 3 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) ., i ) = ( R gsumg ( x e. I |-> ( ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ( +g ` R ) ( ( h ` x ) .x. ( i ` x ) ) ) ) ) )
228		simprl 764	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = g /\ f = i ) ) -> e = g )
229	228	fveq1d 5867	. . . . . . . . . 10 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = g /\ f = i ) ) -> ( e ` x ) = ( g ` x ) )
230		simprr 766	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = g /\ f = i ) ) -> f = i )
231	230	fveq1d 5867	. . . . . . . . . 10 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = g /\ f = i ) ) -> ( f ` x ) = ( i ` x ) )
232	229, 231	oveq12d 6308	. . . . . . . . 9 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = g /\ f = i ) ) -> ( ( e ` x ) .x. ( f ` x ) ) = ( ( g ` x ) .x. ( i ` x ) ) )
233	232	mpteq2dv 4490	. . . . . . . 8 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = g /\ f = i ) ) -> ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) = ( x e. I |-> ( ( g ` x ) .x. ( i ` x ) ) ) )
234	233	oveq2d 6306	. . . . . . 7 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = g /\ f = i ) ) -> ( R gsumg ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) ) = ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( i ` x ) ) ) ) )
235		ovex 6318	. . . . . . . 8 |- ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( i ` x ) ) ) ) e. _V
236	235	a1i 11	. . . . . . 7 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( i ` x ) ) ) ) e. _V )
237	179, 234, 83, 88, 236	ovmpt2d 6424	. . . . . 6 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( g ., i ) = ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( i ` x ) ) ) ) )
238	237	oveq2d 6306	. . . . 5 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( k .x. ( g ., i ) ) = ( k .x. ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( i ` x ) ) ) ) ) )
239	14, 17, 20, 1, 5, 7, 24, 22, 9, 71, 35, 13	frlmphllem 19338	. . . . . . 7 |- ( ( ph /\ g e. V /\ i e. V ) -> ( x e. I |-> ( ( g ` x ) .x. ( i ` x ) ) ) finSupp .0. )
240	154, 82, 86, 239	syl3anc 1268	. . . . . 6 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( x e. I |-> ( ( g ` x ) .x. ( i ` x ) ) ) finSupp .0. )
241	17, 24, 75, 20, 78, 77, 80, 93, 240	gsummulc2 17835	. . . . 5 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( R gsumg ( x e. I |-> ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ) ) = ( k .x. ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( i ` x ) ) ) ) ) )
242	238, 241	eqtr4d 2488	. . . 4 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( k .x. ( g ., i ) ) = ( R gsumg ( x e. I |-> ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ) ) )
243		simprl 764	. . . . . . . . 9 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = h /\ f = i ) ) -> e = h )
244	243	fveq1d 5867	. . . . . . . 8 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = h /\ f = i ) ) -> ( e ` x ) = ( h ` x ) )
245		simprr 766	. . . . . . . . 9 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = h /\ f = i ) ) -> f = i )
246	245	fveq1d 5867	. . . . . . . 8 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = h /\ f = i ) ) -> ( f ` x ) = ( i ` x ) )
247	244, 246	oveq12d 6308	. . . . . . 7 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = h /\ f = i ) ) -> ( ( e ` x ) .x. ( f ` x ) ) = ( ( h ` x ) .x. ( i ` x ) ) )
248	247	mpteq2dv 4490	. . . . . 6 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = h /\ f = i ) ) -> ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) = ( x e. I |-> ( ( h ` x ) .x. ( i ` x ) ) ) )
249	248	oveq2d 6306	. . . . 5 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = h /\ f = i ) ) -> ( R gsumg ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) ) = ( R gsumg ( x e. I |-> ( ( h ` x ) .x. ( i ` x ) ) ) ) )
250		ovex 6318	. . . . . 6 |- ( R gsumg ( x e. I |-> ( ( h ` x ) .x. ( i ` x ) ) ) ) e. _V
251	250	a1i 11	. . . . 5 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( R gsumg ( x e. I |-> ( ( h ` x ) .x. ( i ` x ) ) ) ) e. _V )
252	179, 249, 97, 88, 251	ovmpt2d 6424	. . . 4 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( h ., i ) = ( R gsumg ( x e. I |-> ( ( h ` x ) .x. ( i ` x ) ) ) ) )
253	242, 252	oveq12d 6308	. . 3 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( ( k .x. ( g ., i ) ) ( +g ` R ) ( h ., i ) ) = ( ( R gsumg ( x e. I |-> ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ) ) ( +g ` R ) ( R gsumg ( x e. I |-> ( ( h ` x ) .x. ( i ` x ) ) ) ) ) )
254	165, 227, 253	3eqtr4d 2495	. 2 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) ., i ) = ( ( k .x. ( g ., i ) ) ( +g ` R ) ( h ., i ) ) )
255	34	3ad2ant1 1029	. . . . . . 7 |- ( ( ph /\ g e. V /\ h e. V ) -> R e. CRing )
256	255	adantr 467	. . . . . 6 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> R e. CRing )
257	17, 20	crngcom 17795	. . . . . 6 |- ( ( R e. CRing /\ ( h ` x ) e. B /\ ( g ` x ) e. B ) -> ( ( h ` x ) .x. ( g ` x ) ) = ( ( g ` x ) .x. ( h ` x ) ) )
258	256, 66, 65, 257	syl3anc 1268	. . . . 5 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( ( h ` x ) .x. ( g ` x ) ) = ( ( g ` x ) .x. ( h ` x ) ) )
259	258	mpteq2dva 4489	. . . 4 |- ( ( ph /\ g e. V /\ h e. V ) -> ( x e. I |-> ( ( h ` x ) .x. ( g ` x ) ) ) = ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) )
260	259	oveq2d 6306	. . 3 |- ( ( ph /\ g e. V /\ h e. V ) -> ( R gsumg ( x e. I |-> ( ( h ` x ) .x. ( g ` x ) ) ) ) = ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) )
261	178	3ad2ant1 1029	. . . 4 |- ( ( ph /\ g e. V /\ h e. V ) -> ., = ( e e. ( B ^m I ) , f e. ( B ^m I ) |-> ( R gsumg ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) ) ) )
262		simprl 764	. . . . . . . 8 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ ( e = h /\ f = g ) ) -> e = h )
263	262	fveq1d 5867	. . . . . . 7 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ ( e = h /\ f = g ) ) -> ( e ` x ) = ( h ` x ) )
264		simprr 766	. . . . . . . 8 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ ( e = h /\ f = g ) ) -> f = g )
265	264	fveq1d 5867	. . . . . . 7 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ ( e = h /\ f = g ) ) -> ( f ` x ) = ( g ` x ) )
266	263, 265	oveq12d 6308	. . . . . 6 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ ( e = h /\ f = g ) ) -> ( ( e ` x ) .x. ( f ` x ) ) = ( ( h ` x ) .x. ( g ` x ) ) )
267	266	mpteq2dv 4490	. . . . 5 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ ( e = h /\ f = g ) ) -> ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) = ( x e. I |-> ( ( h ` x ) .x. ( g ` x ) ) ) )
268	267	oveq2d 6306	. . . 4 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ ( e = h /\ f = g ) ) -> ( R gsumg ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) ) = ( R gsumg ( x e. I |-> ( ( h ` x ) .x. ( g ` x ) ) ) ) )
269		ovex 6318	. . . . 5 |- ( R gsumg ( x e. I |-> ( ( h ` x ) .x. ( g ` x ) ) ) ) e. _V
270	269	a1i 11	. . . 4 |- ( ( ph /\ g e. V /\ h e. V ) -> ( R gsumg ( x e. I |-> ( ( h ` x ) .x. ( g ` x ) ) ) ) e. _V )
271	261, 268, 50, 44, 270	ovmpt2d 6424	. . 3 |- ( ( ph /\ g e. V /\ h e. V ) -> ( h ., g ) = ( R gsumg ( x e. I |-> ( ( h ` x ) .x. ( g ` x ) ) ) ) )
272	35	ralrimiva 2802	. . . . . 6 |- ( ph -> A. x e. B ( .* ` x ) = x )
273	272	3ad2ant1 1029	. . . . 5 |- ( ( ph /\ g e. V /\ h e. V ) -> A. x e. B ( .* ` x ) = x )
274		fveq2 5865	. . . . . . 7 |- ( x = ( g ., h ) -> ( .* ` x ) = ( .* ` ( g ., h ) ) )
275		id 22	. . . . . . 7 |- ( x = ( g ., h ) -> x = ( g ., h ) )
276	274, 275	eqeq12d 2466	. . . . . 6 |- ( x = ( g ., h ) -> ( ( .* ` x ) = x <-> ( .* ` ( g ., h ) ) = ( g ., h ) ) )
277	276	rspcv 3146	. . . . 5 |- ( ( g ., h ) e. B -> ( A. x e. B ( .* ` x ) = x -> ( .* ` ( g ., h ) ) = ( g ., h ) ) )
278	74, 273, 277	sylc 62	. . . 4 |- ( ( ph /\ g e. V /\ h e. V ) -> ( .* ` ( g ., h ) ) = ( g ., h ) )
279	278, 60	eqtrd 2485	. . 3 |- ( ( ph /\ g e. V /\ h e. V ) -> ( .* ` ( g ., h ) ) = ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) )
280	260, 271, 279	3eqtr4rd 2496	. 2 |- ( ( ph /\ g e. V /\ h e. V ) -> ( .* ` ( g ., h ) ) = ( h ., g ) )
281	2, 3, 4, 6, 8, 16, 18, 19, 21, 23, 25, 33, 36, 74, 254, 71, 280	isphld 19221	1 |- ( ph -> Y e. PreHil )

Syntax hints:   -> wi 4   /\ wa 371   /\ w3a 985   = wceq 1444   e. wcel 1887   A.wral 2737   _Vcvv 3045   C_ wss 3404   class class class wbr 4402   |-> cmpt 4461   Fun wfun 5576   Fn wfn 5577   -->wf 5578   ` cfv 5582  (class class class)co 6290   |-> cmpt2 6292   oFcof 6529   supp csupp 6914   ^m cmap 7472   finSupp cfsupp 7883   Basecbs 15121   +g cplusg 15190   .rcmulr 15191   *rcstv 15192  Scalarcsca 15193   .scvsca 15194   .icip 15195   0gc0g 15338   gsum_g cgsu 15339  CMndccmn 17430   Ringcrg 17780   CRingccrg 17781   DivRingcdr 17975  Fieldcfield 17976   LModclmod 18091   LVecclvec 18325   PreHilcphl 19191   freeLMod cfrlm 19309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-int 4235  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-se 4794  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-isom 5591  df-riota 6252  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-of 6531  df-om 6693  df-1st 6793  df-2nd 6794  df-supp 6915  df-tpos 6973  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-oadd 7186  df-er 7363  df-map 7474  df-ixp 7523  df-en 7570  df-dom 7571  df-sdom 7572  df-fin 7573  df-fsupp 7884  df-sup 7956  df-oi 8025  df-card 8373  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-nn 10610  df-2 10668  df-3 10669  df-4 10670  df-5 10671  df-6 10672  df-7 10673  df-8 10674  df-9 10675  df-10 10676  df-n0 10870  df-z 10938  df-dec 11052  df-uz 11160  df-fz 11785  df-fzo 11916  df-seq 12214  df-hash 12516  df-struct 15123  df-ndx 15124  df-slot 15125  df-base 15126  df-sets 15127  df-ress 15128  df-plusg 15203  df-mulr 15204  df-sca 15206  df-vsca 15207  df-ip 15208  df-tset 15209  df-ple 15210  df-ds 15212  df-hom 15214  df-cco 15215  df-0g 15340  df-gsum 15341  df-prds 15346  df-pws 15348  df-mgm 16488  df-sgrp 16527  df-mnd 16537  df-mhm 16582  df-submnd 16583  df-grp 16673  df-minusg 16674  df-sbg 16675  df-subg 16814  df-ghm 16881  df-cntz 16971  df-cmn 17432  df-abl 17433  df-mgp 17724  df-ur 17736  df-ring 17782  df-cring 17783  df-oppr 17851  df-rnghom 17943  df-drng 17977  df-field 17978  df-subrg 18006  df-staf 18073  df-srng 18074  df-lmod 18093  df-lss 18156  df-lmhm 18245  df-lvec 18326  df-sra 18395  df-rgmod 18396  df-phl 19193  df-dsmm 19295  df-frlm 19310

This theorem is referenced by:  rrxcph  22351