Theorem frlmphl 18619

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 2468	. 2 |- ( ph -> ( +g ` Y ) = ( +g ` Y ) )
4		eqidd 2468	. 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 17217	. . . . 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 18591	. . 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 2468	. 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 17215	. . . . 5 |- ( R e. DivRing -> R e. Ring )
27	12, 26	syl 16	. . . 4 |- ( ph -> R e. Ring )
28	14	frlmlmod 18587	. . . 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 2556	. . 3 |- ( ph -> (Scalar ` Y ) e. DivRing )
31		eqid 2467	. . . 4 |- (Scalar ` Y ) = (Scalar ` Y )
32	31	islvec 17562	. . 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 17323	. 2 |- ( ph -> R e. *Ring )
37	13	3ad2ant1 1017	. . . . 5 |- ( ( ph /\ g e. V /\ h e. V ) -> I e. W )
38	27	3ad2ant1 1017	. . . . 5 |- ( ( ph /\ g e. V /\ h e. V ) -> R e. Ring )
39		simp2 997	. . . . 5 |- ( ( ph /\ g e. V /\ h e. V ) -> g e. V )
40		simp3 998	. . . . 5 |- ( ( ph /\ g e. V /\ h e. V ) -> h e. V )
41	14, 17, 20, 1, 5	frlmipval 18617	. . . . 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 1229	. . . 4 |- ( ( ph /\ g e. V /\ h e. V ) -> ( g ., h ) = ( R gsumg ( g oF .x. h ) ) )
43	14, 17, 1	frlmbasmap 18600	. . . . . . . . 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 7441	. . . . . . . 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 5731	. . . . . . 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 18600	. . . . . . . . 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 7441	. . . . . . . 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 5731	. . . . . . 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 3707	. . . . . 6 |- ( I i^i I ) = I
56		eqidd 2468	. . . . . 6 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( g ` x ) = ( g ` x ) )
57		eqidd 2468	. . . . . 6 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( h ` x ) = ( h ` x ) )
58	48, 54, 37, 37, 55, 56, 57	offval 6532	. . . . 5 |- ( ( ph /\ g e. V /\ h e. V ) -> ( g oF .x. h ) = ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) )
59	58	oveq2d 6301	. . . 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 2508	. . 3 |- ( ( ph /\ g e. V /\ h e. V ) -> ( g ., h ) = ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) )
61		rngcmn 17042	. . . . . 6 |- ( R e. Ring -> R e. CMnd )
62	27, 61	syl 16	. . . . 5 |- ( ph -> R e. CMnd )
63	62	3ad2ant1 1017	. . . 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 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	rngcl 17025	. . . . . 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 1228	. . . . 5 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( ( g ` x ) .x. ( h ` x ) ) e. B )
69		eqid 2467	. . . . 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 18618	. . . 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 16738	. . 3 |- ( ( ph /\ g e. V /\ h e. V ) -> ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) e. B )
74	60, 73	eqeltrd 2555	. 2 |- ( ( ph /\ g e. V /\ h e. V ) -> ( g ., h ) e. B )
75		eqid 2467	. . . 4 |- ( +g ` R ) = ( +g ` R )
76	62	3ad2ant1 1017	. . . 4 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> R e. CMnd )
77	13	3ad2ant1 1017	. . . 4 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> I e. W )
78	27	3ad2ant1 1017	. . . . . 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 997	. . . . . 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 1032	. . . . . . . . 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 6022	. . . . . 6 |- ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( g ` x ) e. B )
86		simp33 1034	. . . . . . . . 9 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> i e. V )
87	14, 17, 1	frlmbasmap 18600	. . . . . . . . 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 7441	. . . . . . . 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 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	rngcl 17025	. . . . . 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 1228	. . . . 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 17025	. . . . 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 1228	. . . 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 1033	. . . . . . . 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 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	rngcl 17025	. . . . 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 1228	. . . 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 2468	. . . 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 2468	. . . 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 5866	. . . . . . . . 9 |- ( x = y -> ( g ` x ) = ( g ` y ) )
105	104	oveq2d 6301	. . . . . . . 8 |- ( x = y -> ( k .x. ( g ` x ) ) = ( k .x. ( g ` y ) ) )
106	105	cbvmptv 4538	. . . . . . 7 |- ( x e. I |-> ( k .x. ( g ` x ) ) ) = ( y e. I |-> ( k .x. ( g ` y ) ) )
107	106	oveq1i 6295	. . . . . 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 17025	. . . . . . . . . . . 12 |- ( ( R e. Ring /\ k e. B /\ ( g ` x ) e. B ) -> ( k .x. ( g ` x ) ) e. B )
109	79, 81, 85, 108	syl3anc 1228	. . . . . . . . . . 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 2467	. . . . . . . . . . 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 5731	. . . . . . . . . 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 5675	. . . . . . . . 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 5731	. . . . . . . . 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 2468	. . . . . . . . 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 5870	. . . . . . . . . 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 6301	. . . . . . . . 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 6310	. . . . . . . . . 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 5956	. . . . . . . 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 2468	. . . . . . . 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 6532	. . . . . . 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 17028	. . . . . . . . 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 1230	. . . . . . . 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 4533	. . . . . . 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 2508	. . . . . 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 2520	. . . . 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 6310	. . . . . . 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 5624	. . . . . . 7 |- Fun ( z e. I |-> ( ( ( x e. I |-> ( k .x. ( g ` x ) ) ) ` z ) .x. ( i ` z ) ) )
136		eqidd 2468	. . . . . . . . 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 2468	. . . . . . . . 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 6532	. . . . . . . 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 5609	. . . . . . 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 998	. . . . . . . . 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 1015	. . . . . . 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 18598	. . . . . . 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 17033	. . . . . . . 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 17049	. . . . . . . 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 6939	. . . . . 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 7846	. . . . . 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 1229	. . . . 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 4469	. . . 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 996	. . . . 5 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ph )
155		eleq1 2539	. . . . . . . . 9 |- ( g = h -> ( g e. V <-> h e. V ) )
156		id 22	. . . . . . . . . . 11 |- ( g = h -> g = h )
157	156, 156	oveq12d 6303	. . . . . . . . . 10 |- ( g = h -> ( g ., g ) = ( h ., h ) )
158	157	eqeq1d 2469	. . . . . . . . 9 |- ( g = h -> ( ( g ., g ) = .0. <-> ( h ., h ) = .0. ) )
159	155, 158	3anbi23d 1302	. . . . . . . 8 |- ( g = h -> ( ( ph /\ g e. V /\ ( g ., g ) = .0. ) <-> ( ph /\ h e. V /\ ( h ., h ) = .0. ) ) )
160		eqeq1 2471	. . . . . . . 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 1983	. . . . . 6 |- ( ( ph /\ h e. V /\ ( h ., h ) = .0. ) -> h = O )
163	14, 17, 20, 1, 5, 7, 24, 22, 9, 162, 35, 13	frlmphllem 18618	. . . . 5 |- ( ( ph /\ h e. V /\ i e. V ) -> ( x e. I |-> ( ( h ` x ) .x. ( i ` x ) ) ) finSupp .0. )
164	154, 96, 86, 163	syl3anc 1228	. . . 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 16755	. . 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 18616	. . . . . . . . 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 2527	. . . . . . 7 |- ( ph -> ., = ( g e. ( B ^m I ) , h e. ( B ^m I ) |-> ( R gsumg ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) ) )
169		fveq1 5865	. . . . . . . . . . 11 |- ( e = g -> ( e ` x ) = ( g ` x ) )
170	169	oveq1d 6300	. . . . . . . . . 10 |- ( e = g -> ( ( e ` x ) .x. ( f ` x ) ) = ( ( g ` x ) .x. ( f ` x ) ) )
171	170	mpteq2dv 4534	. . . . . . . . 9 |- ( e = g -> ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) = ( x e. I |-> ( ( g ` x ) .x. ( f ` x ) ) ) )
172	171	oveq2d 6301	. . . . . . . 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 5865	. . . . . . . . . . 11 |- ( f = h -> ( f ` x ) = ( h ` x ) )
174	173	oveq2d 6301	. . . . . . . . . 10 |- ( f = h -> ( ( g ` x ) .x. ( f ` x ) ) = ( ( g ` x ) .x. ( h ` x ) ) )
175	174	mpteq2dv 4534	. . . . . . . . 9 |- ( f = h -> ( x e. I |-> ( ( g ` x ) .x. ( f ` x ) ) ) = ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) )
176	175	oveq2d 6301	. . . . . . . 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 6362	. . . . . . 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 2526	. . . . . 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 1017	. . . . 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 5868	. . . . . . . 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 5868	. . . . . . . 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 6303	. . . . . . 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 4534	. . . . . 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 6301	. . . . 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 1017	. . . . . . 7 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> Y e. LMod )
188	16	3ad2ant1 1017	. . . . . . . . . . 11 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> R = (Scalar ` Y ) )
189	188	fveq2d 5870	. . . . . . . . . 10 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( Base ` R ) = ( Base ` (Scalar ` Y ) ) )
190	17, 189	syl5eq 2520	. . . . . . . . 9 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> B = ( Base ` (Scalar ` Y ) ) )
191	80, 190	eleqtrd 2557	. . . . . . . 8 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> k e. ( Base ` (Scalar ` Y ) ) )
192		eqid 2467	. . . . . . . . 9 |- ( .s ` Y ) = ( .s ` Y )
193		eqid 2467	. . . . . . . . 9 |- ( Base ` (Scalar ` Y ) ) = ( Base ` (Scalar ` Y ) )
194	1, 31, 192, 193	lmodvscl 17341	. . . . . . . 8 |- ( ( Y e. LMod /\ k e. ( Base ` (Scalar ` Y ) ) /\ g e. V ) -> ( k ( .s ` Y ) g ) e. V )
195	187, 191, 82, 194	syl3anc 1228	. . . . . . 7 |- ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( k ( .s ` Y ) g ) e. V )
196		eqid 2467	. . . . . . . 8 |- ( +g ` Y ) = ( +g ` Y )
197	1, 196	lmodvacl 17338	. . . . . . 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 1228	. . . . . 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 18600	. . . . . 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 6310	. . . . . 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 6415	. . . 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 18604	. . . . . . . . . 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 18600	. . . . . . . . . . . . 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 7441	. . . . . . . . . . . 12 |- ( ( k ( .s ` Y ) g ) e. ( B ^m I ) -> ( k ( .s ` Y ) g ) : I --> B )
208		ffn 5731	. . . . . . . . . . . 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 18607	. . . . . . . . . . 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 2468	. . . . . . . . . . 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 6532	. . . . . . . . . 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 2508	. . . . . . . . 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 6310	. . . . . . . . . 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 5960	. . . . . . . 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 6300	. . . . . . 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 17031	. . . . . . . 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 1230	. . . . . . 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 6300	. . . . . . 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 2512	. . . . . 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 4533	. . . . 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 6301	. . . 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 2508	. . 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 5868	. . . . . . . . . 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 5868	. . . . . . . . . 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 6303	. . . . . . . . 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 4534	. . . . . . . 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 6301	. . . . . . 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 6310	. . . . . . . 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 6415	. . . . . 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 6301	. . . . 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 18618	. . . . . . 7 |- ( ( ph /\ g e. V /\ i e. V ) -> ( x e. I |-> ( ( g ` x ) .x. ( i ` x ) ) ) finSupp .0. )
240	154, 82, 86, 239	syl3anc 1228	. . . . . 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 17066	. . . . 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 2511	. . . 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 5868	. . . . . . . 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 5868	. . . . . . . 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 6303	. . . . . . 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 4534	. . . . . 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 6301	. . . . 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 6310	. . . . . 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 6415	. . . 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 6303	. . 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 2518	. 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 1017	. . . . . . 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 17026	. . . . . 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 1228	. . . . 5 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( ( h ` x ) .x. ( g ` x ) ) = ( ( g ` x ) .x. ( h ` x ) ) )
259	258	mpteq2dva 4533	. . . 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 6301	. . 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 1017	. . . 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 5868	. . . . . . 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 5868	. . . . . . 7 |- ( ( ( ph /\ g e. V /\ h e. V ) /\ ( e = h /\ f = g ) ) -> ( f ` x ) = ( g ` x ) )
266	263, 265	oveq12d 6303	. . . . . 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 4534	. . . . 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 6301	. . . 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 6310	. . . . 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 6415	. . 3 |- ( ( ph /\ g e. V /\ h e. V ) -> ( h ., g ) = ( R gsumg ( x e. I |-> ( ( h ` x ) .x. ( g ` x ) ) ) ) )
272	35	ralrimiva 2878	. . . . . 6 |- ( ph -> A. x e. B ( .* ` x ) = x )
273	272	3ad2ant1 1017	. . . . 5 |- ( ( ph /\ g e. V /\ h e. V ) -> A. x e. B ( .* ` x ) = x )
274		fveq2 5866	. . . . . . 7 |- ( x = ( g ., h ) -> ( .* ` x ) = ( .* ` ( g ., h ) ) )
275		id 22	. . . . . . 7 |- ( x = ( g ., h ) -> x = ( g ., h ) )
276	274, 275	eqeq12d 2489	. . . . . 6 |- ( x = ( g ., h ) -> ( ( .* ` x ) = x <-> ( .* ` ( g ., h ) ) = ( g ., h ) ) )
277	276	rspcv 3210	. . . . 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 2508	. . 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 2519	. 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 18496	1 |- ( ph -> Y e. PreHil )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 973   = wceq 1379   e. wcel 1767   A.wral 2814   _Vcvv 3113   C_ wss 3476   class class class wbr 4447   |-> cmpt 4505   Fun wfun 5582   Fn wfn 5583   -->wf 5584   ` cfv 5588  (class class class)co 6285   |-> cmpt2 6287   oFcof 6523   supp csupp 6902   ^m cmap 7421   finSupp cfsupp 7830   Basecbs 14493   +g cplusg 14558   .rcmulr 14559   *rcstv 14560  Scalarcsca 14561   .scvsca 14562   .icip 14563   0gc0g 14698   gsum_g cgsu 14699  CMndccmn 16613   Ringcrg 17012   CRingccrg 17013   DivRingcdr 17208  Fieldcfield 17209   LModclmod 17324   LVecclvec 17560   PreHilcphl 18466   freeLMod cfrlm 18584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6577  ax-cnex 9549  ax-resscn 9550  ax-1cn 9551  ax-icn 9552  ax-addcl 9553  ax-addrcl 9554  ax-mulcl 9555  ax-mulrcl 9556  ax-mulcom 9557  ax-addass 9558  ax-mulass 9559  ax-distr 9560  ax-i2m1 9561  ax-1ne0 9562  ax-1rid 9563  ax-rnegex 9564  ax-rrecex 9565  ax-cnre 9566  ax-pre-lttri 9567  ax-pre-lttrn 9568  ax-pre-ltadd 9569  ax-pre-mulgt0 9570

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-isom 5597  df-riota 6246  df-ov 6288  df-oprab 6289  df-mpt2 6290  df-of 6525  df-om 6686  df-1st 6785  df-2nd 6786  df-supp 6903  df-tpos 6956  df-recs 7043  df-rdg 7077  df-1o 7131  df-oadd 7135  df-er 7312  df-map 7423  df-ixp 7471  df-en 7518  df-dom 7519  df-sdom 7520  df-fin 7521  df-fsupp 7831  df-sup 7902  df-oi 7936  df-card 8321  df-pnf 9631  df-mnf 9632  df-xr 9633  df-ltxr 9634  df-le 9635  df-sub 9808  df-neg 9809  df-nn 10538  df-2 10595  df-3 10596  df-4 10597  df-5 10598  df-6 10599  df-7 10600  df-8 10601  df-9 10602  df-10 10603  df-n0 10797  df-z 10866  df-dec 10978  df-uz 11084  df-fz 11674  df-fzo 11794  df-seq 12077  df-hash 12375  df-struct 14495  df-ndx 14496  df-slot 14497  df-base 14498  df-sets 14499  df-ress 14500  df-plusg 14571  df-mulr 14572  df-sca 14574  df-vsca 14575  df-ip 14576  df-tset 14577  df-ple 14578  df-ds 14580  df-hom 14582  df-cco 14583  df-0g 14700  df-gsum 14701  df-prds 14706  df-pws 14708  df-mnd 15735  df-mhm 15789  df-submnd 15790  df-grp 15871  df-minusg 15872  df-sbg 15873  df-subg 16012  df-ghm 16079  df-cntz 16169  df-cmn 16615  df-abl 16616  df-mgp 16956  df-ur 16968  df-rng 17014  df-cring 17015  df-oppr 17085  df-rnghom 17177  df-drng 17210  df-field 17211  df-subrg 17239  df-staf 17306  df-srng 17307  df-lmod 17326  df-lss 17391  df-lmhm 17480  df-lvec 17561  df-sra 17630  df-rgmod 17631  df-phl 18468  df-dsmm 18570  df-frlm 18585

This theorem is referenced by:  rrxcph  21651