Theorem frlmphl 18175

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 2438	. 2 |- ( ph -> ( +g ` Y ) = ( +g ` Y ) )
4		eqidd 2438	. 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 16817	. . . . 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 18147	. . 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 2438	. 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 16815	. . . . 5 |- ( R e. DivRing -> R e. Ring )
27	12, 26	syl 16	. . . 4 |- ( ph -> R e. Ring )
28	14	frlmlmod 18143	. . . 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 2512	. . 3 |- ( ph -> (Scalar ` Y ) e. DivRing )
31		eqid 2437	. . . 4 |- (Scalar ` Y ) = (Scalar ` Y )
32	31	islvec 17159	. . 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 16923	. 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 18173	. . . . 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 18156	. . . . . . . . 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 7226	. . . . . . . 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 5552	. . . . . . 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 18156	. . . . . . . . 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 7226	. . . . . . . 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 5552	. . . . . . 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 3552	. . . . . 6 |- ( I i^i I ) = I
56		eqidd 2438	. . . . . 6 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( g ` x ) = ( g ` x ) )
57		eqidd 2438	. . . . . 6 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( h ` x ) = ( h ` x ) )
58	48, 54, 37, 37, 55, 56, 57	offval 6322	. . . . 5 |- ( ( ph /\ g e. V /\ h e. V ) -> ( g oF .x. h ) = ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) )
59	58	oveq2d 6102	. . . 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 2469	. . 3 |- ( ( ph /\ g e. V /\ h e. V ) -> ( g ., h ) = ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) )
61		rngcmn 16661	. . . . . 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 5836	. . . . . 6 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( g ` x ) e. B )
66	52	ffvelrnda 5836	. . . . . 6 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( h ` x ) e. B )
67	17, 20	rngcl 16644	. . . . . 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 2437	. . . . 5 |- ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) = ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) )
70	68, 69	fmptd 5860	. . . 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 18174	. . . 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 16386	. . 3 |- ( ( ph /\ g e. V /\ h e. V ) -> ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) e. B )
74	60, 73	eqeltrd 2511	. 2 |- ( ( ph /\ g e. V /\ h e. V ) -> ( g ., h ) e. B )
75		eqid 2437	. . . 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 5836	. . . . . 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 18156	. . . . . . . . 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 7226	. . . . . . . 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 5836	. . . . . 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 16644	. . . . . 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 16644	. . . . 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 5836	. . . . 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 16644	. . . . 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 2438	. . . 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 2438	. . . 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 5684	. . . . . . . . 9 |- ( x = y -> ( g ` x ) = ( g ` y ) )
105	104	oveq2d 6102	. . . . . . . 8 |- ( x = y -> ( k .x. ( g ` x ) ) = ( k .x. ( g ` y ) ) )
106	105	cbvmptv 4376	. . . . . . 7 |- ( x e. I |-> ( k .x. ( g ` x ) ) ) = ( y e. I |-> ( k .x. ( g ` y ) ) )
107	106	oveq1i 6096	. . . . . 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 16644	. . . . . . . . . . . 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 2437	. . . . . . . . . . 11 |- ( x e. I |-> ( k .x. ( g ` x ) ) ) = ( x e. I |-> ( k .x. ( g ` x ) ) )
111	109, 110	fmptd 5860	. . . . . . . . . 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 5552	. . . . . . . . . 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 5498	. . . . . . . . 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 5552	. . . . . . . . 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 2438	. . . . . . . . 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 5688	. . . . . . . . . 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 6102	. . . . . . . . 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 6111	. . . . . . . . . 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 5772	. . . . . . . 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 2438	. . . . . . . 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 6322	. . . . . . 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 16647	. . . . . . . . 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 4371	. . . . . . 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 2469	. . . . . 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 2481	. . . . 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 6111	. . . . . . 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 5447	. . . . . . 7 |- Fun ( z e. I |-> ( ( ( x e. I |-> ( k .x. ( g ` x ) ) ) ` z ) .x. ( i ` z ) ) )
136		eqidd 2438	. . . . . . . . 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 2438	. . . . . . . . 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 6322	. . . . . . . 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 5432	. . . . . . 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 18154	. . . . . . 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 16652	. . . . . . . 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 16668	. . . . . . . 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 6722	. . . . . 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 7628	. . . . . 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 4307	. . . 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 2497	. . . . . . . . 9 |- ( g = h -> ( g e. V <-> h e. V ) )
156		id 22	. . . . . . . . . . 11 |- ( g = h -> g = h )
157	156, 156	oveq12d 6104	. . . . . . . . . 10 |- ( g = h -> ( g ., g ) = ( h ., h ) )
158	157	eqeq1d 2445	. . . . . . . . 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 2443	. . . . . . . 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 18174	. . . . 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 16403	. . 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 18172	. . . . . . . . 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 2488	. . . . . . 7 |- ( ph -> ., = ( g e. ( B ^m I ) , h e. ( B ^m I ) |-> ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) ) )
169		fveq1 5683	. . . . . . . . . . 11 |- ( e = g -> ( e ` x ) = ( g ` x ) )
170	169	oveq1d 6101	. . . . . . . . . 10 |- ( e = g -> ( ( e ` x ) .x. ( f ` x ) ) = ( ( g ` x ) .x. ( f ` x ) ) )
171	170	mpteq2dv 4372	. . . . . . . . 9 |- ( e = g -> ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) = ( x e. I |-> ( ( g ` x ) .x. ( f ` x ) ) ) )
172	171	oveq2d 6102	. . . . . . . 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 5683	. . . . . . . . . . 11 |- ( f = h -> ( f ` x ) = ( h ` x ) )
174	173	oveq2d 6102	. . . . . . . . . 10 |- ( f = h -> ( ( g ` x ) .x. ( f ` x ) ) = ( ( g ` x ) .x. ( h ` x ) ) )
175	174	mpteq2dv 4372	. . . . . . . . 9 |- ( f = h -> ( x e. I |-> ( ( g ` x ) .x. ( f ` x ) ) ) = ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) )
176	175	oveq2d 6102	. . . . . . . 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 6161	. . . . . . 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 2487	. . . . . 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 5686	. . . . . . . 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 5686	. . . . . . . 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 6104	. . . . . . 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 4372	. . . . . 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 6102	. . . . 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 5688	. . . . . . . . . 10 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( Base ` R ) = ( Base ` (Scalar ` Y ) ) )
190	17, 189	syl5eq 2481	. . . . . . . . 9 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> B = ( Base ` (Scalar ` Y ) ) )
191	80, 190	eleqtrd 2513	. . . . . . . 8 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> k e. ( Base ` (Scalar ` Y ) ) )
192		eqid 2437	. . . . . . . . 9 |- ( .s ` Y ) = ( .s ` Y )
193		eqid 2437	. . . . . . . . 9 |- ( Base ` (Scalar ` Y ) ) = ( Base ` (Scalar ` Y ) )
194	1, 31, 192, 193	lmodvscl 16941	. . . . . . . 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 2437	. . . . . . . 8 |- ( +g ` Y ) = ( +g ` Y )
197	1, 196	lmodvacl 16938	. . . . . . 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 18156	. . . . . 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 6111	. . . . . 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 6213	. . . 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 18160	. . . . . . . . . 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 18156	. . . . . . . . . . . . 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 7226	. . . . . . . . . . . 12 |- ( ( k ( .s ` Y ) g ) e. ( B ^m I ) -> ( k ( .s ` Y ) g ) : I --> B )
208		ffn 5552	. . . . . . . . . . . 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 18163	. . . . . . . . . . 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 2438	. . . . . . . . . . 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 6322	. . . . . . . . . 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 2469	. . . . . . . . 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 6111	. . . . . . . . . 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 5776	. . . . . . . 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 6101	. . . . . . 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 16650	. . . . . . . 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 6101	. . . . . . 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 2473	. . . . . 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 4371	. . . . 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 6102	. . . 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 2469	. . 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 5686	. . . . . . . . . 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 5686	. . . . . . . . . 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 6104	. . . . . . . . 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 4372	. . . . . . . 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 6102	. . . . . . 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 6111	. . . . . . . 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 6213	. . . . . 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 6102	. . . . 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 18174	. . . . . . 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 16682	. . . . 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 2472	. . . 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 5686	. . . . . . . 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 5686	. . . . . . . 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 6104	. . . . . . 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 4372	. . . . . 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 6102	. . . . 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 6111	. . . . . 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 6213	. . . 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 6104	. . 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 2479	. 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 16645	. . . . . 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 4371	. . . 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 6102	. . 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 5686	. . . . . . 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 5686	. . . . . . 7 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ ( e = h /\ f = g ) ) -> ( f ` x ) = ( g ` x ) )
266	263, 265	oveq12d 6104	. . . . . 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 4372	. . . . 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 6102	. . . 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 6111	. . . . 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 6213	. . 3 |- ( ( ph /\ g e. V /\ h e. V ) -> ( h ., g ) = ( R gsumg ( x e. I |-> ( ( h ` x ) .x. ( g ` x ) ) ) ) )
272	35	ralrimiva 2793	. . . . . 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 5684	. . . . . . 7 |- ( x = ( g ., h ) -> ( .* ` x ) = ( .* ` ( g ., h ) ) )
275		id 22	. . . . . . 7 |- ( x = ( g ., h ) -> x = ( g ., h ) )
276	274, 275	eqeq12d 2451	. . . . . 6 |- ( x = ( g ., h ) -> ( ( .* ` x ) = x <-> ( .* ` ( g ., h ) ) = ( g ., h ) ) )
277	276	rspcv 3062	. . . . 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 2469	. . 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 2480	. 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 18052	1 |- ( ph -> Y e. PreHil )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 965   = wceq 1369   e. wcel 1756   A.wral 2709   _Vcvv 2966   C_ wss 3321   class class class wbr 4285   e. cmpt 4343   Fun wfun 5405   Fn wfn 5406   -->wf 5407   ` cfv 5411  (class class class)co 6086   e. cmpt2 6088   oFcof 6313   supp csupp 6685   ^m cmap 7206   finSupp cfsupp 7612   Basecbs 14166   +g cplusg 14230   .rcmulr 14231   *rcstv 14232  Scalarcsca 14233   .scvsca 14234   .icip 14235   0gc0g 14370   gsum_g cgsu 14371  CMndccmn 16266   Ringcrg 16631   CRingccrg 16632   DivRingcdr 16808  Fieldcfield 16809   LModclmod 16924   LVecclvec 17157   PreHilcphl 18022   freeLMod cfrlm 18140

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 2418  ax-rep 4396  ax-sep 4406  ax-nul 4414  ax-pow 4463  ax-pr 4524  ax-un 6367  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351

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 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3282  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3631  df-if 3785  df-pw 3855  df-sn 3871  df-pr 3873  df-tp 3875  df-op 3877  df-uni 4085  df-int 4122  df-iun 4166  df-br 4286  df-opab 4344  df-mpt 4345  df-tr 4379  df-eprel 4624  df-id 4628  df-po 4633  df-so 4634  df-fr 4671  df-se 4672  df-we 4673  df-ord 4714  df-on 4715  df-lim 4716  df-suc 4717  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5374  df-fun 5413  df-fn 5414  df-f 5415  df-f1 5416  df-fo 5417  df-f1o 5418  df-fv 5419  df-isom 5420  df-riota 6045  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-of 6315  df-om 6472  df-1st 6572  df-2nd 6573  df-supp 6686  df-tpos 6740  df-recs 6824  df-rdg 6858  df-1o 6912  df-oadd 6916  df-er 7093  df-map 7208  df-ixp 7256  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-fsupp 7613  df-sup 7683  df-oi 7716  df-card 8101  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-nn 10315  df-2 10372  df-3 10373  df-4 10374  df-5 10375  df-6 10376  df-7 10377  df-8 10378  df-9 10379  df-10 10380  df-n0 10572  df-z 10639  df-dec 10748  df-uz 10854  df-fz 11430  df-fzo 11541  df-seq 11799  df-hash 12096  df-struct 14168  df-ndx 14169  df-slot 14170  df-base 14171  df-sets 14172  df-ress 14173  df-plusg 14243  df-mulr 14244  df-sca 14246  df-vsca 14247  df-ip 14248  df-tset 14249  df-ple 14250  df-ds 14252  df-hom 14254  df-cco 14255  df-0g 14372  df-gsum 14373  df-prds 14378  df-pws 14380  df-mnd 15407  df-mhm 15456  df-submnd 15457  df-grp 15534  df-minusg 15535  df-sbg 15536  df-subg 15667  df-ghm 15734  df-cntz 15824  df-cmn 16268  df-abl 16269  df-mgp 16578  df-ur 16590  df-rng 16633  df-cring 16634  df-oppr 16701  df-rnghom 16792  df-drng 16810  df-field 16811  df-subrg 16839  df-staf 16906  df-srng 16907  df-lmod 16926  df-lss 16988  df-lmhm 17077  df-lvec 17158  df-sra 17227  df-rgmod 17228  df-phl 18024  df-dsmm 18126  df-frlm 18141

This theorem is referenced by:  rrxcph  20865