Theorem frlmphl 18228

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 2444	. 2 |- ( ph -> ( +g ` Y ) = ( +g ` Y ) )
4		eqidd 2444	. 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 16863	. . . . 5 |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )
11	9, 10	sylib 196	. . . 4 |- ( ph -> ( R e. DivRing /\ R e. CRing ) )
12	11	simpld 459	. . 3 |- ( ph -> R e. DivRing )
13		frlmphl.i	. . 3 |- ( ph -> I e. W )
14		frlmphl.y	. . . 4 |- Y = ( R freeLMod I )
15	14	frlmsca 18200	. . 3 |- ( ( R e. DivRing /\ I e. W ) -> R = (Scalar ` Y ) )
16	12, 13, 15	syl2anc 661	. 2 |- ( ph -> R = (Scalar ` Y ) )
17		frlmphl.b	. . 3 |- B = ( Base ` R )
18	17	a1i 11	. 2 |- ( ph -> B = ( Base ` R ) )
19		eqidd 2444	. 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		drngrng 16861	. . . . 5 |- ( R e. DivRing -> R e. Ring )
27	12, 26	syl 16	. . . 4 |- ( ph -> R e. Ring )
28	14	frlmlmod 18196	. . . 4 |- ( ( R e. Ring /\ I e. W ) -> Y e. LMod )
29	27, 13, 28	syl2anc 661	. . 3 |- ( ph -> Y e. LMod )
30	16, 12	eqeltrrd 2518	. . 3 |- ( ph -> (Scalar ` Y ) e. DivRing )
31		eqid 2443	. . . 4 |- (Scalar ` Y ) = (Scalar ` Y )
32	31	islvec 17207	. . 3 |- ( Y e. LVec <-> ( Y e. LMod /\ (Scalar ` Y ) e. DivRing ) )
33	29, 30, 32	sylanbrc 664	. 2 |- ( ph -> Y e. LVec )
34	11	simprd 463	. . 3 |- ( ph -> R e. CRing )
35		frlmphl.u	. . 3 |- ( ( ph /\ x e. B ) -> ( .* ` x ) = x )
36	17, 22, 34, 35	idsrngd 16969	. 2 |- ( ph -> R e. *Ring )
37	13	3ad2ant1 1009	. . . . 5 |- ( ( ph /\ g e. V /\ h e. V ) -> I e. W )
38	27	3ad2ant1 1009	. . . . 5 |- ( ( ph /\ g e. V /\ h e. V ) -> R e. Ring )
39		simp2 989	. . . . 5 |- ( ( ph /\ g e. V /\ h e. V ) -> g e. V )
40		simp3 990	. . . . 5 |- ( ( ph /\ g e. V /\ h e. V ) -> h e. V )
41	14, 17, 20, 1, 5	frlmipval 18226	. . . . 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 1219	. . . 4 |- ( ( ph /\ g e. V /\ h e. V ) -> ( g ., h ) = ( R gsumg ( g oF .x. h ) ) )
43	14, 17, 1	frlmbasmap 18209	. . . . . . . . 9 |- ( ( I e. W /\ g e. V ) -> g e. ( B ^m I ) )
44	37, 39, 43	syl2anc 661	. . . . . . . 8 |- ( ( ph /\ g e. V /\ h e. V ) -> g e. ( B ^m I ) )
45		elmapi 7255	. . . . . . . 8 |- ( g e. ( B ^m I ) -> g : I --> B )
46	44, 45	syl 16	. . . . . . 7 |- ( ( ph /\ g e. V /\ h e. V ) -> g : I --> B )
47		ffn 5580	. . . . . . 7 |- ( g : I --> B -> g Fn I )
48	46, 47	syl 16	. . . . . 6 |- ( ( ph /\ g e. V /\ h e. V ) -> g Fn I )
49	14, 17, 1	frlmbasmap 18209	. . . . . . . . 9 |- ( ( I e. W /\ h e. V ) -> h e. ( B ^m I ) )
50	37, 40, 49	syl2anc 661	. . . . . . . 8 |- ( ( ph /\ g e. V /\ h e. V ) -> h e. ( B ^m I ) )
51		elmapi 7255	. . . . . . . 8 |- ( h e. ( B ^m I ) -> h : I --> B )
52	50, 51	syl 16	. . . . . . 7 |- ( ( ph /\ g e. V /\ h e. V ) -> h : I --> B )
53		ffn 5580	. . . . . . 7 |- ( h : I --> B -> h Fn I )
54	52, 53	syl 16	. . . . . 6 |- ( ( ph /\ g e. V /\ h e. V ) -> h Fn I )
55		inidm 3580	. . . . . 6 |- ( I i^i I ) = I
56		eqidd 2444	. . . . . 6 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( g ` x ) = ( g ` x ) )
57		eqidd 2444	. . . . . 6 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( h ` x ) = ( h ` x ) )
58	48, 54, 37, 37, 55, 56, 57	offval 6348	. . . . 5 |- ( ( ph /\ g e. V /\ h e. V ) -> ( g oF .x. h ) = ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) )
59	58	oveq2d 6128	. . . 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 2475	. . 3 |- ( ( ph /\ g e. V /\ h e. V ) -> ( g ., h ) = ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) )
61		rngcmn 16697	. . . . . 6 |- ( R e. Ring -> R e. CMnd )
62	27, 61	syl 16	. . . . 5 |- ( ph -> R e. CMnd )
63	62	3ad2ant1 1009	. . . 4 |- ( ( ph /\ g e. V /\ h e. V ) -> R e. CMnd )
64	38	adantr 465	. . . . . 6 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> R e. Ring )
65	46	ffvelrnda 5864	. . . . . 6 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( g ` x ) e. B )
66	52	ffvelrnda 5864	. . . . . 6 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( h ` x ) e. B )
67	17, 20	rngcl 16680	. . . . . 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 1218	. . . . 5 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( ( g ` x ) .x. ( h ` x ) ) e. B )
69		eqid 2443	. . . . 5 |- ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) = ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) )
70	68, 69	fmptd 5888	. . . 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 18227	. . . 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 16418	. . 3 |- ( ( ph /\ g e. V /\ h e. V ) -> ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) e. B )
74	60, 73	eqeltrd 2517	. 2 |- ( ( ph /\ g e. V /\ h e. V ) -> ( g ., h ) e. B )
75		eqid 2443	. . . 4 |- ( +g ` R ) = ( +g ` R )
76	62	3ad2ant1 1009	. . . 4 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> R e. CMnd )
77	13	3ad2ant1 1009	. . . 4 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> I e. W )
78	27	3ad2ant1 1009	. . . . . 6 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> R e. Ring )
79	78	adantr 465	. . . . 5 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> R e. Ring )
80		simp2 989	. . . . . 6 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> k e. B )
81	80	adantr 465	. . . . 5 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> k e. B )
82		simp31 1024	. . . . . . . . 9 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> g e. V )
83	77, 82, 43	syl2anc 661	. . . . . . . 8 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> g e. ( B ^m I ) )
84	83, 45	syl 16	. . . . . . 7 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> g : I --> B )
85	84	ffvelrnda 5864	. . . . . 6 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( g ` x ) e. B )
86		simp33 1026	. . . . . . . . 9 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> i e. V )
87	14, 17, 1	frlmbasmap 18209	. . . . . . . . 9 |- ( ( I e. W /\ i e. V ) -> i e. ( B ^m I ) )
88	77, 86, 87	syl2anc 661	. . . . . . . 8 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> i e. ( B ^m I ) )
89		elmapi 7255	. . . . . . . 8 |- ( i e. ( B ^m I ) -> i : I --> B )
90	88, 89	syl 16	. . . . . . 7 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> i : I --> B )
91	90	ffvelrnda 5864	. . . . . 6 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( i ` x ) e. B )
92	17, 20	rngcl 16680	. . . . . 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 1218	. . . . 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	rngcl 16680	. . . . 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 1218	. . . 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 1025	. . . . . . . 8 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> h e. V )
97	77, 96, 49	syl2anc 661	. . . . . . 7 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> h e. ( B ^m I ) )
98	97, 51	syl 16	. . . . . 6 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> h : I --> B )
99	98	ffvelrnda 5864	. . . . 5 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( h ` x ) e. B )
100	17, 20	rngcl 16680	. . . . 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 1218	. . . 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 2444	. . . 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 2444	. . . 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 5712	. . . . . . . . 9 |- ( x = y -> ( g ` x ) = ( g ` y ) )
105	104	oveq2d 6128	. . . . . . . 8 |- ( x = y -> ( k .x. ( g ` x ) ) = ( k .x. ( g ` y ) ) )
106	105	cbvmptv 4404	. . . . . . 7 |- ( x e. I |-> ( k .x. ( g ` x ) ) ) = ( y e. I |-> ( k .x. ( g ` y ) ) )
107	106	oveq1i 6122	. . . . . 6 |- ( ( x e. I |-> ( k .x. ( g ` x ) ) ) oF .x. i ) = ( ( y e. I |-> ( k .x. ( g ` y ) ) ) oF .x. i )
108	17, 20	rngcl 16680	. . . . . . . . . . . 12 |- ( ( R e. Ring /\ k e. B /\ ( g ` x ) e. B ) -> ( k .x. ( g ` x ) ) e. B )
109	79, 81, 85, 108	syl3anc 1218	. . . . . . . . . . 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 2443	. . . . . . . . . . 11 |- ( x e. I |-> ( k .x. ( g ` x ) ) ) = ( x e. I |-> ( k .x. ( g ` x ) ) )
111	109, 110	fmptd 5888	. . . . . . . . . 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 5580	. . . . . . . . . 10 |- ( ( x e. I |-> ( k .x. ( g ` x ) ) ) : I --> B -> ( x e. I |-> ( k .x. ( g ` x ) ) ) Fn I )
113	111, 112	syl 16	. . . . . . . . 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 5526	. . . . . . . . 9 |- ( ( x e. I |-> ( k .x. ( g ` x ) ) ) Fn I <-> ( y e. I |-> ( k .x. ( g ` y ) ) ) Fn I )
115	113, 114	sylib 196	. . . . . . . 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 5580	. . . . . . . . 9 |- ( i : I --> B -> i Fn I )
117	90, 116	syl 16	. . . . . . . 8 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> i Fn I )
118		eqidd 2444	. . . . . . . . 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 461	. . . . . . . . . . 11 |- ( ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) /\ y = x ) -> y = x )
120	119	fveq2d 5716	. . . . . . . . . 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 6128	. . . . . . . . 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 461	. . . . . . . . 9 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> x e. I )
123		ovex 6137	. . . . . . . . . 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 5800	. . . . . . . 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 2444	. . . . . . . 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 6348	. . . . . . 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	rngass 16683	. . . . . . . . 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 1220	. . . . . . . 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 4399	. . . . . . 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 2475	. . . . . 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 2487	. . . . 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 6137	. . . . . . 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 5475	. . . . . . 7 |- Fun ( z e. I |-> ( ( ( x e. I |-> ( k .x. ( g ` x ) ) ) ` z ) .x. ( i ` z ) ) )
136		eqidd 2444	. . . . . . . . 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 2444	. . . . . . . . 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 6348	. . . . . . . 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 5460	. . . . . . 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 233	. . . . . 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 990	. . . . . . . . 9 |- ( ( g e. V /\ h e. V /\ i e. V ) -> i e. V )
142	13, 141	anim12i 566	. . . . . . . 8 |- ( ( ph /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( I e. W /\ i e. V ) )
143	142	3adant2 1007	. . . . . . 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 18207	. . . . . . 7 |- ( ( I e. W /\ i e. V ) -> i finSupp .0. )
145	143, 144	syl 16	. . . . . 6 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> i finSupp .0. )
146	17, 24	rng0cl 16688	. . . . . . . 8 |- ( R e. Ring -> .0. e. B )
147	78, 146	syl 16	. . . . . . 7 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> .0. e. B )
148	17, 20, 24	rngrz 16704	. . . . . . . 8 |- ( ( R e. Ring /\ y e. B ) -> ( y .x. .0. ) = .0. )
149	78, 148	sylan 471	. . . . . . 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 6748	. . . . . 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 7657	. . . . . 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 1219	. . . . 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 4335	. . . 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 988	. . . . 5 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ph )
155		eleq1 2503	. . . . . . . . 9 |- ( g = h -> ( g e. V <-> h e. V ) )
156		id 22	. . . . . . . . . . 11 |- ( g = h -> g = h )
157	156, 156	oveq12d 6130	. . . . . . . . . 10 |- ( g = h -> ( g ., g ) = ( h ., h ) )
158	157	eqeq1d 2451	. . . . . . . . 9 |- ( g = h -> ( ( g ., g ) = .0. <-> ( h ., h ) = .0. ) )
159	155, 158	3anbi23d 1292	. . . . . . . 8 |- ( g = h -> ( ( ph /\ g e. V /\ ( g ., g ) = .0. ) <-> ( ph /\ h e. V /\ ( h ., h ) = .0. ) ) )
160		eqeq1 2449	. . . . . . . 8 |- ( g = h -> ( g = O <-> h = O ) )
161	159, 160	imbi12d 320	. . . . . . 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 1958	. . . . . 6 |- ( ( ph /\ h e. V /\ ( h ., h ) = .0. ) -> h = O )
163	14, 17, 20, 1, 5, 7, 24, 22, 9, 162, 35, 13	frlmphllem 18227	. . . . 5 |- ( ( ph /\ h e. V /\ i e. V ) -> ( x e. I |-> ( ( h ` x ) .x. ( i ` x ) ) ) finSupp .0. )
164	154, 96, 86, 163	syl3anc 1218	. . . 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 16435	. . 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 18225	. . . . . . . . 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 661	. . . . . . . 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 2494	. . . . . . 7 |- ( ph -> ., = ( g e. ( B ^m I ) , h e. ( B ^m I ) |-> ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) ) )
169		fveq1 5711	. . . . . . . . . . 11 |- ( e = g -> ( e ` x ) = ( g ` x ) )
170	169	oveq1d 6127	. . . . . . . . . 10 |- ( e = g -> ( ( e ` x ) .x. ( f ` x ) ) = ( ( g ` x ) .x. ( f ` x ) ) )
171	170	mpteq2dv 4400	. . . . . . . . 9 |- ( e = g -> ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) = ( x e. I |-> ( ( g ` x ) .x. ( f ` x ) ) ) )
172	171	oveq2d 6128	. . . . . . . 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 5711	. . . . . . . . . . 11 |- ( f = h -> ( f ` x ) = ( h ` x ) )
174	173	oveq2d 6128	. . . . . . . . . 10 |- ( f = h -> ( ( g ` x ) .x. ( f ` x ) ) = ( ( g ` x ) .x. ( h ` x ) ) )
175	174	mpteq2dv 4400	. . . . . . . . 9 |- ( f = h -> ( x e. I |-> ( ( g ` x ) .x. ( f ` x ) ) ) = ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) )
176	175	oveq2d 6128	. . . . . . . 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 6187	. . . . . . 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 2493	. . . . . 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 1009	. . . . 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 755	. . . . . . . . 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 5714	. . . . . . . 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 756	. . . . . . . . 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 5714	. . . . . . . 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 6130	. . . . . . 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 4400	. . . . . 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 6128	. . . . 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 1009	. . . . . . 7 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> Y e. LMod )
188	16	3ad2ant1 1009	. . . . . . . . . . 11 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> R = (Scalar ` Y ) )
189	188	fveq2d 5716	. . . . . . . . . 10 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( Base ` R ) = ( Base ` (Scalar ` Y ) ) )
190	17, 189	syl5eq 2487	. . . . . . . . 9 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> B = ( Base ` (Scalar ` Y ) ) )
191	80, 190	eleqtrd 2519	. . . . . . . 8 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> k e. ( Base ` (Scalar ` Y ) ) )
192		eqid 2443	. . . . . . . . 9 |- ( .s ` Y ) = ( .s ` Y )
193		eqid 2443	. . . . . . . . 9 |- ( Base ` (Scalar ` Y ) ) = ( Base ` (Scalar ` Y ) )
194	1, 31, 192, 193	lmodvscl 16987	. . . . . . . 8 |- ( ( Y e. LMod /\ k e. ( Base ` (Scalar ` Y ) ) /\ g e. V ) -> ( k ( .s ` Y ) g ) e. V )
195	187, 191, 82, 194	syl3anc 1218	. . . . . . 7 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( k ( .s ` Y ) g ) e. V )
196		eqid 2443	. . . . . . . 8 |- ( +g ` Y ) = ( +g ` Y )
197	1, 196	lmodvacl 16984	. . . . . . 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 1218	. . . . . 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 18209	. . . . . 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 661	. . . . 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 6137	. . . . . 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 6239	. . . 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 18213	. . . . . . . . . 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 18209	. . . . . . . . . . . . 13 |- ( ( I e. W /\ ( k ( .s ` Y ) g ) e. V ) -> ( k ( .s ` Y ) g ) e. ( B ^m I ) )
206	77, 195, 205	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( k ( .s ` Y ) g ) e. ( B ^m I ) )
207		elmapi 7255	. . . . . . . . . . . 12 |- ( ( k ( .s ` Y ) g ) e. ( B ^m I ) -> ( k ( .s ` Y ) g ) : I --> B )
208		ffn 5580	. . . . . . . . . . . 12 |- ( ( k ( .s ` Y ) g ) : I --> B -> ( k ( .s ` Y ) g ) Fn I )
209	206, 207, 208	3syl 20	. . . . . . . . . . 11 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( k ( .s ` Y ) g ) Fn I )
210	98, 53	syl 16	. . . . . . . . . . 11 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> h Fn I )
211	77	adantr 465	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> I e. W )
212	82	adantr 465	. . . . . . . . . . . 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 18216	. . . . . . . . . . 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 2444	. . . . . . . . . . 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 6348	. . . . . . . . . 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 2475	. . . . . . . . 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 6137	. . . . . . . . . 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 5804	. . . . . . . 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 6127	. . . . . . 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	rngdir 16686	. . . . . . . 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 1220	. . . . . . 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 6127	. . . . . . 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 2479	. . . . . 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 4399	. . . . 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 6128	. . . 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 2475	. . 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 755	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = g /\ f = i ) ) -> e = g )
229	228	fveq1d 5714	. . . . . . . . . 10 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = g /\ f = i ) ) -> ( e ` x ) = ( g ` x ) )
230		simprr 756	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = g /\ f = i ) ) -> f = i )
231	230	fveq1d 5714	. . . . . . . . . 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 6130	. . . . . . . . 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 4400	. . . . . . . 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 6128	. . . . . . 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 6137	. . . . . . . 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 6239	. . . . . 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 6128	. . . . 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 18227	. . . . . . 7 |- ( ( ph /\ g e. V /\ i e. V ) -> ( x e. I |-> ( ( g ` x ) .x. ( i ` x ) ) ) finSupp .0. )
240	154, 82, 86, 239	syl3anc 1218	. . . . . 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 16718	. . . . 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 2478	. . . 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 755	. . . . . . . . 9 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = h /\ f = i ) ) -> e = h )
244	243	fveq1d 5714	. . . . . . . 8 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = h /\ f = i ) ) -> ( e ` x ) = ( h ` x ) )
245		simprr 756	. . . . . . . . 9 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = h /\ f = i ) ) -> f = i )
246	245	fveq1d 5714	. . . . . . . 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 6130	. . . . . . 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 4400	. . . . . 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 6128	. . . . 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 6137	. . . . . 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 6239	. . . 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 6130	. . 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 2485	. 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 1009	. . . . . . 7 |- ( ( ph /\ g e. V /\ h e. V ) -> R e. CRing )
256	255	adantr 465	. . . . . 6 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> R e. CRing )
257	17, 20	crngcom 16681	. . . . . 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 1218	. . . . 5 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( ( h ` x ) .x. ( g ` x ) ) = ( ( g ` x ) .x. ( h ` x ) ) )
259	258	mpteq2dva 4399	. . . 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 6128	. . 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 1009	. . . 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 755	. . . . . . . 8 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ ( e = h /\ f = g ) ) -> e = h )
263	262	fveq1d 5714	. . . . . . 7 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ ( e = h /\ f = g ) ) -> ( e ` x ) = ( h ` x ) )
264		simprr 756	. . . . . . . 8 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ ( e = h /\ f = g ) ) -> f = g )
265	264	fveq1d 5714	. . . . . . 7 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ ( e = h /\ f = g ) ) -> ( f ` x ) = ( g ` x ) )
266	263, 265	oveq12d 6130	. . . . . 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 4400	. . . . 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 6128	. . . 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 6137	. . . . 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 6239	. . 3 |- ( ( ph /\ g e. V /\ h e. V ) -> ( h ., g ) = ( R gsumg ( x e. I |-> ( ( h ` x ) .x. ( g ` x ) ) ) ) )
272	35	ralrimiva 2820	. . . . . 6 |- ( ph -> A. x e. B ( .* ` x ) = x )
273	272	3ad2ant1 1009	. . . . 5 |- ( ( ph /\ g e. V /\ h e. V ) -> A. x e. B ( .* ` x ) = x )
274		fveq2 5712	. . . . . . 7 |- ( x = ( g ., h ) -> ( .* ` x ) = ( .* ` ( g ., h ) ) )
275		id 22	. . . . . . 7 |- ( x = ( g ., h ) -> x = ( g ., h ) )
276	274, 275	eqeq12d 2457	. . . . . 6 |- ( x = ( g ., h ) -> ( ( .* ` x ) = x <-> ( .* ` ( g ., h ) ) = ( g ., h ) ) )
277	276	rspcv 3090	. . . . 5 |- ( ( g ., h ) e. B -> ( A. x e. B ( .* ` x ) = x -> ( .* ` ( g ., h ) ) = ( g ., h ) ) )
278	74, 273, 277	sylc 60	. . . 4 |- ( ( ph /\ g e. V /\ h e. V ) -> ( .* ` ( g ., h ) ) = ( g ., h ) )
279	278, 60	eqtrd 2475	. . 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 2486	. 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 18105	1 |- ( ph -> Y e. PreHil )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 965   = wceq 1369   e. wcel 1756   A.wral 2736   _Vcvv 2993   C_ wss 3349   class class class wbr 4313   e. cmpt 4371   Fun wfun 5433   Fn wfn 5434   -->wf 5435   ` cfv 5439  (class class class)co 6112   e. cmpt2 6114   oFcof 6339   supp csupp 6711   ^m cmap 7235   finSupp cfsupp 7641   Basecbs 14195   +g cplusg 14259   .rcmulr 14260   *rcstv 14261  Scalarcsca 14262   .scvsca 14263   .icip 14264   0gc0g 14399   gsum_g cgsu 14400  CMndccmn 16298   Ringcrg 16667   CRingccrg 16668   DivRingcdr 16854  Fieldcfield 16855   LModclmod 16970   LVecclvec 17205   PreHilcphl 18075   freeLMod cfrlm 18193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4424  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393  ax-cnex 9359  ax-resscn 9360  ax-1cn 9361  ax-icn 9362  ax-addcl 9363  ax-addrcl 9364  ax-mulcl 9365  ax-mulrcl 9366  ax-mulcom 9367  ax-addass 9368  ax-mulass 9369  ax-distr 9370  ax-i2m1 9371  ax-1ne0 9372  ax-1rid 9373  ax-rnegex 9374  ax-rrecex 9375  ax-cnre 9376  ax-pre-lttri 9377  ax-pre-lttrn 9378  ax-pre-ltadd 9379  ax-pre-mulgt0 9380

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-int 4150  df-iun 4194  df-br 4314  df-opab 4372  df-mpt 4373  df-tr 4407  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-se 4701  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-isom 5448  df-riota 6073  df-ov 6115  df-oprab 6116  df-mpt2 6117  df-of 6341  df-om 6498  df-1st 6598  df-2nd 6599  df-supp 6712  df-tpos 6766  df-recs 6853  df-rdg 6887  df-1o 6941  df-oadd 6945  df-er 7122  df-map 7237  df-ixp 7285  df-en 7332  df-dom 7333  df-sdom 7334  df-fin 7335  df-fsupp 7642  df-sup 7712  df-oi 7745  df-card 8130  df-pnf 9441  df-mnf 9442  df-xr 9443  df-ltxr 9444  df-le 9445  df-sub 9618  df-neg 9619  df-nn 10344  df-2 10401  df-3 10402  df-4 10403  df-5 10404  df-6 10405  df-7 10406  df-8 10407  df-9 10408  df-10 10409  df-n0 10601  df-z 10668  df-dec 10777  df-uz 10883  df-fz 11459  df-fzo 11570  df-seq 11828  df-hash 12125  df-struct 14197  df-ndx 14198  df-slot 14199  df-base 14200  df-sets 14201  df-ress 14202  df-plusg 14272  df-mulr 14273  df-sca 14275  df-vsca 14276  df-ip 14277  df-tset 14278  df-ple 14279  df-ds 14281  df-hom 14283  df-cco 14284  df-0g 14401  df-gsum 14402  df-prds 14407  df-pws 14409  df-mnd 15436  df-mhm 15485  df-submnd 15486  df-grp 15566  df-minusg 15567  df-sbg 15568  df-subg 15699  df-ghm 15766  df-cntz 15856  df-cmn 16300  df-abl 16301  df-mgp 16614  df-ur 16626  df-rng 16669  df-cring 16670  df-oppr 16737  df-rnghom 16828  df-drng 16856  df-field 16857  df-subrg 16885  df-staf 16952  df-srng 16953  df-lmod 16972  df-lss 17036  df-lmhm 17125  df-lvec 17206  df-sra 17275  df-rgmod 17276  df-phl 18077  df-dsmm 18179  df-frlm 18194

This theorem is referenced by:  rrxcph  20918