Metamath Proof Explorer

Theorem frlmphl

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)

Ref Expression
Hypotheses 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 frlmphl 
|- ( ph -> Y e. PreHil )

Proof

Step Hyp Ref Expression
1 frlmphl.y 
 |-  Y = ( R freeLMod I )
2 frlmphl.b 
 |-  B = ( Base ` R )
3 frlmphl.t 
 |-  .x. = ( .r ` R )
4 frlmphl.v 
 |-  V = ( Base ` Y )
5 frlmphl.j 
 |-  ., = ( .i ` Y )
6 frlmphl.o 
 |-  O = ( 0g ` Y )
7 frlmphl.0 
 |-  .0. = ( 0g ` R )
8 frlmphl.s 
 |-  .* = ( *r ` R )
9 frlmphl.f 
 |-  ( ph -> R e. Field )
10 frlmphl.m 
 |-  ( ( ph /\ g e. V /\ ( g ., g ) = .0. ) -> g = O )
11 frlmphl.u 
 |-  ( ( ph /\ x e. B ) -> ( .* ` x ) = x )
12 frlmphl.i 
 |-  ( ph -> I e. W )
13 4 a1i 
 |-  ( ph -> V = ( Base ` Y ) )
14 eqidd 
 |-  ( ph -> ( +g ` Y ) = ( +g ` Y ) )
15 eqidd 
 |-  ( ph -> ( .s ` Y ) = ( .s ` Y ) )
16 5 a1i 
 |-  ( ph -> ., = ( .i ` Y ) )
17 6 a1i 
 |-  ( ph -> O = ( 0g ` Y ) )
18 isfld 
 |-  ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )
19 9 18 sylib 
 |-  ( ph -> ( R e. DivRing /\ R e. CRing ) )
20 19 simpld 
 |-  ( ph -> R e. DivRing )
21 1 frlmsca 
 |-  ( ( R e. DivRing /\ I e. W ) -> R = ( Scalar ` Y ) )
22 20 12 21 syl2anc 
 |-  ( ph -> R = ( Scalar ` Y ) )
23 2 a1i 
 |-  ( ph -> B = ( Base ` R ) )
24 eqidd 
 |-  ( ph -> ( +g ` R ) = ( +g ` R ) )
25 3 a1i 
 |-  ( ph -> .x. = ( .r ` R ) )
26 8 a1i 
 |-  ( ph -> .* = ( *r ` R ) )
27 7 a1i 
 |-  ( ph -> .0. = ( 0g ` R ) )
28 drngring 
 |-  ( R e. DivRing -> R e. Ring )
29 20 28 syl 
 |-  ( ph -> R e. Ring )
30 1 frlmlmod 
 |-  ( ( R e. Ring /\ I e. W ) -> Y e. LMod )
31 29 12 30 syl2anc 
 |-  ( ph -> Y e. LMod )
32 22 20 eqeltrrd 
 |-  ( ph -> ( Scalar ` Y ) e. DivRing )
33 eqid 
 |-  ( Scalar ` Y ) = ( Scalar ` Y )
34 33 islvec 
 |-  ( Y e. LVec <-> ( Y e. LMod /\ ( Scalar ` Y ) e. DivRing ) )
35 31 32 34 sylanbrc 
 |-  ( ph -> Y e. LVec )
36 19 simprd 
 |-  ( ph -> R e. CRing )
37 2 8 36 11 idsrngd 
 |-  ( ph -> R e. *Ring )
38 12 3ad2ant1 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> I e. W )
39 29 3ad2ant1 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> R e. Ring )
40 simp2 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> g e. V )
41 simp3 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> h e. V )
42 1 2 3 4 5 frlmipval 
 |-  ( ( ( I e. W /\ R e. Ring ) /\ ( g e. V /\ h e. V ) ) -> ( g ., h ) = ( R gsum ( g oF .x. h ) ) )
43 38 39 40 41 42 syl22anc 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( g ., h ) = ( R gsum ( g oF .x. h ) ) )
44 1 2 4 frlmbasmap 
 |-  ( ( I e. W /\ g e. V ) -> g e. ( B ^m I ) )
45 38 40 44 syl2anc 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> g e. ( B ^m I ) )
46 elmapi 
 |-  ( g e. ( B ^m I ) -> g : I --> B )
47 45 46 syl 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> g : I --> B )
48 47 ffnd 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> g Fn I )
49 1 2 4 frlmbasmap 
 |-  ( ( I e. W /\ h e. V ) -> h e. ( B ^m I ) )
50 38 41 49 syl2anc 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> h e. ( B ^m I ) )
51 elmapi 
 |-  ( h e. ( B ^m I ) -> h : I --> B )
52 50 51 syl 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> h : I --> B )
53 52 ffnd 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> h Fn I )
54 inidm 
 |-  ( I i^i I ) = I
55 eqidd 
 |-  ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( g ` x ) = ( g ` x ) )
56 eqidd 
 |-  ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( h ` x ) = ( h ` x ) )
57 48 53 38 38 54 55 56 offval 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( g oF .x. h ) = ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) )
58 57 oveq2d 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( R gsum ( g oF .x. h ) ) = ( R gsum ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) )
59 43 58 eqtrd 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( g ., h ) = ( R gsum ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) )
60 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
61 29 60 syl 
 |-  ( ph -> R e. CMnd )
62 61 3ad2ant1 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> R e. CMnd )
63 39 adantr 
 |-  ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> R e. Ring )
64 47 ffvelrnda 
 |-  ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( g ` x ) e. B )
65 52 ffvelrnda 
 |-  ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( h ` x ) e. B )
66 2 3 ringcl 
 |-  ( ( R e. Ring /\ ( g ` x ) e. B /\ ( h ` x ) e. B ) -> ( ( g ` x ) .x. ( h ` x ) ) e. B )
67 63 64 65 66 syl3anc 
 |-  ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( ( g ` x ) .x. ( h ` x ) ) e. B )
68 67 fmpttd 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) : I --> B )
69 1 2 3 4 5 6 7 8 9 10 11 12 frlmphllem 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) finSupp .0. )
70 2 7 62 38 68 69 gsumcl 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( R gsum ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) e. B )
71 59 70 eqeltrd 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( g ., h ) e. B )
72 eqid 
 |-  ( +g ` R ) = ( +g ` R )
73 61 3ad2ant1 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> R e. CMnd )
74 12 3ad2ant1 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> I e. W )
75 29 3ad2ant1 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> R e. Ring )
76 75 adantr 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> R e. Ring )
77 simp2 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> k e. B )
78 77 adantr 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> k e. B )
79 simp31 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> g e. V )
80 74 79 44 syl2anc 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> g e. ( B ^m I ) )
81 80 46 syl 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> g : I --> B )
82 81 ffvelrnda 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( g ` x ) e. B )
83 simp33 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> i e. V )
84 1 2 4 frlmbasmap 
 |-  ( ( I e. W /\ i e. V ) -> i e. ( B ^m I ) )
85 74 83 84 syl2anc 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> i e. ( B ^m I ) )
86 elmapi 
 |-  ( i e. ( B ^m I ) -> i : I --> B )
87 85 86 syl 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> i : I --> B )
88 87 ffvelrnda 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( i ` x ) e. B )
89 2 3 ringcl 
 |-  ( ( R e. Ring /\ ( g ` x ) e. B /\ ( i ` x ) e. B ) -> ( ( g ` x ) .x. ( i ` x ) ) e. B )
90 76 82 88 89 syl3anc 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( ( g ` x ) .x. ( i ` x ) ) e. B )
91 2 3 ringcl 
 |-  ( ( R e. Ring /\ k e. B /\ ( ( g ` x ) .x. ( i ` x ) ) e. B ) -> ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) e. B )
92 76 78 90 91 syl3anc 
 |-  ( ( ( 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 )
93 simp32 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> h e. V )
94 74 93 49 syl2anc 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> h e. ( B ^m I ) )
95 94 51 syl 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> h : I --> B )
96 95 ffvelrnda 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( h ` x ) e. B )
97 2 3 ringcl 
 |-  ( ( R e. Ring /\ ( h ` x ) e. B /\ ( i ` x ) e. B ) -> ( ( h ` x ) .x. ( i ` x ) ) e. B )
98 76 96 88 97 syl3anc 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( ( h ` x ) .x. ( i ` x ) ) e. B )
99 eqidd 
 |-  ( ( 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 ) ) ) ) )
100 eqidd 
 |-  ( ( 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 ) ) ) )
101 fveq2 
 |-  ( x = y -> ( g ` x ) = ( g ` y ) )
102 101 oveq2d 
 |-  ( x = y -> ( k .x. ( g ` x ) ) = ( k .x. ( g ` y ) ) )
103 102 cbvmptv 
 |-  ( x e. I |-> ( k .x. ( g ` x ) ) ) = ( y e. I |-> ( k .x. ( g ` y ) ) )
104 103 oveq1i 
 |-  ( ( x e. I |-> ( k .x. ( g ` x ) ) ) oF .x. i ) = ( ( y e. I |-> ( k .x. ( g ` y ) ) ) oF .x. i )
105 2 3 ringcl 
 |-  ( ( R e. Ring /\ k e. B /\ ( g ` x ) e. B ) -> ( k .x. ( g ` x ) ) e. B )
106 76 78 82 105 syl3anc 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( k .x. ( g ` x ) ) e. B )
107 106 fmpttd 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( x e. I |-> ( k .x. ( g ` x ) ) ) : I --> B )
108 107 ffnd 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( x e. I |-> ( k .x. ( g ` x ) ) ) Fn I )
109 103 fneq1i 
 |-  ( ( x e. I |-> ( k .x. ( g ` x ) ) ) Fn I <-> ( y e. I |-> ( k .x. ( g ` y ) ) ) Fn I )
110 108 109 sylib 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( y e. I |-> ( k .x. ( g ` y ) ) ) Fn I )
111 87 ffnd 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> i Fn I )
112 eqidd 
 |-  ( ( ( 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 ) ) ) )
113 simpr 
 |-  ( ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) /\ y = x ) -> y = x )
114 113 fveq2d 
 |-  ( ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) /\ y = x ) -> ( g ` y ) = ( g ` x ) )
115 114 oveq2d 
 |-  ( ( ( ( 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 ) ) )
116 simpr 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> x e. I )
117 ovexd 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( k .x. ( g ` x ) ) e. _V )
118 112 115 116 117 fvmptd 
 |-  ( ( ( 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 ) ) )
119 eqidd 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( i ` x ) = ( i ` x ) )
120 110 111 74 74 54 118 119 offval 
 |-  ( ( 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 ) ) ) )
121 2 3 ringass 
 |-  ( ( 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 ) ) ) )
122 76 78 82 88 121 syl13anc 
 |-  ( ( ( 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 ) ) ) )
123 122 mpteq2dva 
 |-  ( ( 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 ) ) ) ) )
124 120 123 eqtrd 
 |-  ( ( 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 ) ) ) ) )
125 104 124 eqtrid 
 |-  ( ( 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 ) ) ) ) )
126 ovexd 
 |-  ( ( 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 )
127 funmpt 
 |-  Fun ( z e. I |-> ( ( ( x e. I |-> ( k .x. ( g ` x ) ) ) ` z ) .x. ( i ` z ) ) )
128 eqidd 
 |-  ( ( ( 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 ) )
129 eqidd 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ z e. I ) -> ( i ` z ) = ( i ` z ) )
130 108 111 74 74 54 128 129 offval 
 |-  ( ( 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 ) ) ) )
131 130 funeqd 
 |-  ( ( 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 ) ) ) ) )
132 127 131 mpbiri 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> Fun ( ( x e. I |-> ( k .x. ( g ` x ) ) ) oF .x. i ) )
133 simp3 
 |-  ( ( g e. V /\ h e. V /\ i e. V ) -> i e. V )
134 12 133 anim12i 
 |-  ( ( ph /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( I e. W /\ i e. V ) )
135 134 3adant2 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( I e. W /\ i e. V ) )
136 1 7 4 frlmbasfsupp 
 |-  ( ( I e. W /\ i e. V ) -> i finSupp .0. )
137 135 136 syl 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> i finSupp .0. )
138 2 7 ring0cl 
 |-  ( R e. Ring -> .0. e. B )
139 75 138 syl 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> .0. e. B )
140 2 3 7 ringrz 
 |-  ( ( R e. Ring /\ y e. B ) -> ( y .x. .0. ) = .0. )
141 75 140 sylan 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ y e. B ) -> ( y .x. .0. ) = .0. )
142 74 139 107 87 141 suppofss2d 
 |-  ( ( 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. ) )
143 fsuppsssupp 
 |-  ( ( ( ( ( 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. )
144 126 132 137 142 143 syl22anc 
 |-  ( ( 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. )
145 125 144 eqbrtrrd 
 |-  ( ( 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. )
146 simp1 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ph )
147 eleq1w 
 |-  ( g = h -> ( g e. V <-> h e. V ) )
148 id 
 |-  ( g = h -> g = h )
149 148 148 oveq12d 
 |-  ( g = h -> ( g ., g ) = ( h ., h ) )
150 149 eqeq1d 
 |-  ( g = h -> ( ( g ., g ) = .0. <-> ( h ., h ) = .0. ) )
151 147 150 3anbi23d 
 |-  ( g = h -> ( ( ph /\ g e. V /\ ( g ., g ) = .0. ) <-> ( ph /\ h e. V /\ ( h ., h ) = .0. ) ) )
152 eqeq1 
 |-  ( g = h -> ( g = O <-> h = O ) )
153 151 152 imbi12d 
 |-  ( g = h -> ( ( ( ph /\ g e. V /\ ( g ., g ) = .0. ) -> g = O ) <-> ( ( ph /\ h e. V /\ ( h ., h ) = .0. ) -> h = O ) ) )
154 153 10 chvarvv 
 |-  ( ( ph /\ h e. V /\ ( h ., h ) = .0. ) -> h = O )
155 1 2 3 4 5 6 7 8 9 154 11 12 frlmphllem 
 |-  ( ( ph /\ h e. V /\ i e. V ) -> ( x e. I |-> ( ( h ` x ) .x. ( i ` x ) ) ) finSupp .0. )
156 146 93 83 155 syl3anc 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( x e. I |-> ( ( h ` x ) .x. ( i ` x ) ) ) finSupp .0. )
157 2 7 72 73 74 92 98 99 100 145 156 gsummptfsadd 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( R gsum ( x e. I |-> ( ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ( +g ` R ) ( ( h ` x ) .x. ( i ` x ) ) ) ) ) = ( ( R gsum ( x e. I |-> ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ) ) ( +g ` R ) ( R gsum ( x e. I |-> ( ( h ` x ) .x. ( i ` x ) ) ) ) ) )
158 1 2 3 frlmip 
 |-  ( ( I e. W /\ R e. DivRing ) -> ( g e. ( B ^m I ) , h e. ( B ^m I ) |-> ( R gsum ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) ) = ( .i ` Y ) )
159 12 20 158 syl2anc 
 |-  ( ph -> ( g e. ( B ^m I ) , h e. ( B ^m I ) |-> ( R gsum ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) ) = ( .i ` Y ) )
160 5 159 eqtr4id 
 |-  ( ph -> ., = ( g e. ( B ^m I ) , h e. ( B ^m I ) |-> ( R gsum ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) ) )
161 fveq1 
 |-  ( e = g -> ( e ` x ) = ( g ` x ) )
162 161 oveq1d 
 |-  ( e = g -> ( ( e ` x ) .x. ( f ` x ) ) = ( ( g ` x ) .x. ( f ` x ) ) )
163 162 mpteq2dv 
 |-  ( e = g -> ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) = ( x e. I |-> ( ( g ` x ) .x. ( f ` x ) ) ) )
164 163 oveq2d 
 |-  ( e = g -> ( R gsum ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) ) = ( R gsum ( x e. I |-> ( ( g ` x ) .x. ( f ` x ) ) ) ) )
165 fveq1 
 |-  ( f = h -> ( f ` x ) = ( h ` x ) )
166 165 oveq2d 
 |-  ( f = h -> ( ( g ` x ) .x. ( f ` x ) ) = ( ( g ` x ) .x. ( h ` x ) ) )
167 166 mpteq2dv 
 |-  ( f = h -> ( x e. I |-> ( ( g ` x ) .x. ( f ` x ) ) ) = ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) )
168 167 oveq2d 
 |-  ( f = h -> ( R gsum ( x e. I |-> ( ( g ` x ) .x. ( f ` x ) ) ) ) = ( R gsum ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) )
169 164 168 cbvmpov 
 |-  ( e e. ( B ^m I ) , f e. ( B ^m I ) |-> ( R gsum ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) ) ) = ( g e. ( B ^m I ) , h e. ( B ^m I ) |-> ( R gsum ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) )
170 160 169 eqtr4di 
 |-  ( ph -> ., = ( e e. ( B ^m I ) , f e. ( B ^m I ) |-> ( R gsum ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) ) ) )
171 170 3ad2ant1 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ., = ( e e. ( B ^m I ) , f e. ( B ^m I ) |-> ( R gsum ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) ) ) )
172 simprl 
 |-  ( ( ( 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 ) )
173 172 fveq1d 
 |-  ( ( ( 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 ) )
174 simprr 
 |-  ( ( ( 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 )
175 174 fveq1d 
 |-  ( ( ( 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 ) )
176 173 175 oveq12d 
 |-  ( ( ( 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 ) ) )
177 176 mpteq2dv 
 |-  ( ( ( 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 ) ) ) )
178 177 oveq2d 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) /\ f = i ) ) -> ( R gsum ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) ) = ( R gsum ( x e. I |-> ( ( ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) ` x ) .x. ( i ` x ) ) ) ) )
179 31 3ad2ant1 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> Y e. LMod )
180 22 3ad2ant1 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> R = ( Scalar ` Y ) )
181 180 fveq2d 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( Base ` R ) = ( Base ` ( Scalar ` Y ) ) )
182 2 181 eqtrid 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> B = ( Base ` ( Scalar ` Y ) ) )
183 77 182 eleqtrd 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> k e. ( Base ` ( Scalar ` Y ) ) )
184 eqid 
 |-  ( .s ` Y ) = ( .s ` Y )
185 eqid 
 |-  ( Base ` ( Scalar ` Y ) ) = ( Base ` ( Scalar ` Y ) )
186 4 33 184 185 lmodvscl 
 |-  ( ( Y e. LMod /\ k e. ( Base ` ( Scalar ` Y ) ) /\ g e. V ) -> ( k ( .s ` Y ) g ) e. V )
187 179 183 79 186 syl3anc 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( k ( .s ` Y ) g ) e. V )
188 eqid 
 |-  ( +g ` Y ) = ( +g ` Y )
189 4 188 lmodvacl 
 |-  ( ( Y e. LMod /\ ( k ( .s ` Y ) g ) e. V /\ h e. V ) -> ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) e. V )
190 179 187 93 189 syl3anc 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) e. V )
191 1 2 4 frlmbasmap 
 |-  ( ( I e. W /\ ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) e. V ) -> ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) e. ( B ^m I ) )
192 74 190 191 syl2anc 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) e. ( B ^m I ) )
193 ovexd 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( R gsum ( x e. I |-> ( ( ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) ` x ) .x. ( i ` x ) ) ) ) e. _V )
194 171 178 192 85 193 ovmpod 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) ., i ) = ( R gsum ( x e. I |-> ( ( ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) ` x ) .x. ( i ` x ) ) ) ) )
195 1 4 75 74 187 93 72 188 frlmplusgval 
 |-  ( ( 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 ) )
196 1 2 4 frlmbasmap 
 |-  ( ( I e. W /\ ( k ( .s ` Y ) g ) e. V ) -> ( k ( .s ` Y ) g ) e. ( B ^m I ) )
197 74 187 196 syl2anc 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( k ( .s ` Y ) g ) e. ( B ^m I ) )
198 elmapi 
 |-  ( ( k ( .s ` Y ) g ) e. ( B ^m I ) -> ( k ( .s ` Y ) g ) : I --> B )
199 ffn 
 |-  ( ( k ( .s ` Y ) g ) : I --> B -> ( k ( .s ` Y ) g ) Fn I )
200 197 198 199 3syl 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( k ( .s ` Y ) g ) Fn I )
201 95 ffnd 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> h Fn I )
202 74 adantr 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> I e. W )
203 79 adantr 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> g e. V )
204 1 4 2 202 78 203 116 184 3 frlmvscaval 
 |-  ( ( ( 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 ) ) )
205 eqidd 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ x e. I ) -> ( h ` x ) = ( h ` x ) )
206 200 201 74 74 54 204 205 offval 
 |-  ( ( 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 ) ) ) )
207 195 206 eqtrd 
 |-  ( ( 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 ) ) ) )
208 ovexd 
 |-  ( ( ( 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 )
209 207 208 fvmpt2d 
 |-  ( ( ( 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 ) ) )
210 209 oveq1d 
 |-  ( ( ( 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 ) ) )
211 2 72 3 ringdir 
 |-  ( ( 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 ) ) ) )
212 76 106 96 88 211 syl13anc 
 |-  ( ( ( 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 ) ) ) )
213 122 oveq1d 
 |-  ( ( ( 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 ) ) ) )
214 210 212 213 3eqtrd 
 |-  ( ( ( 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 ) ) ) )
215 214 mpteq2dva 
 |-  ( ( 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 ) ) ) ) )
216 215 oveq2d 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( R gsum ( x e. I |-> ( ( ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) ` x ) .x. ( i ` x ) ) ) ) = ( R gsum ( x e. I |-> ( ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ( +g ` R ) ( ( h ` x ) .x. ( i ` x ) ) ) ) ) )
217 194 216 eqtrd 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( ( ( k ( .s ` Y ) g ) ( +g ` Y ) h ) ., i ) = ( R gsum ( x e. I |-> ( ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ( +g ` R ) ( ( h ` x ) .x. ( i ` x ) ) ) ) ) )
218 simprl 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = g /\ f = i ) ) -> e = g )
219 218 fveq1d 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = g /\ f = i ) ) -> ( e ` x ) = ( g ` x ) )
220 simprr 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = g /\ f = i ) ) -> f = i )
221 220 fveq1d 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = g /\ f = i ) ) -> ( f ` x ) = ( i ` x ) )
222 219 221 oveq12d 
 |-  ( ( ( 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 ) ) )
223 222 mpteq2dv 
 |-  ( ( ( 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 ) ) ) )
224 223 oveq2d 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = g /\ f = i ) ) -> ( R gsum ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) ) = ( R gsum ( x e. I |-> ( ( g ` x ) .x. ( i ` x ) ) ) ) )
225 ovexd 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( R gsum ( x e. I |-> ( ( g ` x ) .x. ( i ` x ) ) ) ) e. _V )
226 171 224 80 85 225 ovmpod 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( g ., i ) = ( R gsum ( x e. I |-> ( ( g ` x ) .x. ( i ` x ) ) ) ) )
227 226 oveq2d 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( k .x. ( g ., i ) ) = ( k .x. ( R gsum ( x e. I |-> ( ( g ` x ) .x. ( i ` x ) ) ) ) ) )
228 1 2 3 4 5 6 7 8 9 10 11 12 frlmphllem 
 |-  ( ( ph /\ g e. V /\ i e. V ) -> ( x e. I |-> ( ( g ` x ) .x. ( i ` x ) ) ) finSupp .0. )
229 146 79 83 228 syl3anc 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( x e. I |-> ( ( g ` x ) .x. ( i ` x ) ) ) finSupp .0. )
230 2 7 72 3 75 74 77 90 229 gsummulc2 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( R gsum ( x e. I |-> ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ) ) = ( k .x. ( R gsum ( x e. I |-> ( ( g ` x ) .x. ( i ` x ) ) ) ) ) )
231 227 230 eqtr4d 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( k .x. ( g ., i ) ) = ( R gsum ( x e. I |-> ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ) ) )
232 simprl 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = h /\ f = i ) ) -> e = h )
233 232 fveq1d 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = h /\ f = i ) ) -> ( e ` x ) = ( h ` x ) )
234 simprr 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = h /\ f = i ) ) -> f = i )
235 234 fveq1d 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = h /\ f = i ) ) -> ( f ` x ) = ( i ` x ) )
236 233 235 oveq12d 
 |-  ( ( ( 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 ) ) )
237 236 mpteq2dv 
 |-  ( ( ( 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 ) ) ) )
238 237 oveq2d 
 |-  ( ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) /\ ( e = h /\ f = i ) ) -> ( R gsum ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) ) = ( R gsum ( x e. I |-> ( ( h ` x ) .x. ( i ` x ) ) ) ) )
239 ovexd 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( R gsum ( x e. I |-> ( ( h ` x ) .x. ( i ` x ) ) ) ) e. _V )
240 171 238 94 85 239 ovmpod 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( h ., i ) = ( R gsum ( x e. I |-> ( ( h ` x ) .x. ( i ` x ) ) ) ) )
241 231 240 oveq12d 
 |-  ( ( ph /\ k e. B /\ ( g e. V /\ h e. V /\ i e. V ) ) -> ( ( k .x. ( g ., i ) ) ( +g ` R ) ( h ., i ) ) = ( ( R gsum ( x e. I |-> ( k .x. ( ( g ` x ) .x. ( i ` x ) ) ) ) ) ( +g ` R ) ( R gsum ( x e. I |-> ( ( h ` x ) .x. ( i ` x ) ) ) ) ) )
242 157 217 241 3eqtr4d 
 |-  ( ( 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 ) ) )
243 36 3ad2ant1 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> R e. CRing )
244 243 adantr 
 |-  ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> R e. CRing )
245 2 3 crngcom 
 |-  ( ( R e. CRing /\ ( h ` x ) e. B /\ ( g ` x ) e. B ) -> ( ( h ` x ) .x. ( g ` x ) ) = ( ( g ` x ) .x. ( h ` x ) ) )
246 244 65 64 245 syl3anc 
 |-  ( ( ( ph /\ g e. V /\ h e. V ) /\ x e. I ) -> ( ( h ` x ) .x. ( g ` x ) ) = ( ( g ` x ) .x. ( h ` x ) ) )
247 246 mpteq2dva 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( x e. I |-> ( ( h ` x ) .x. ( g ` x ) ) ) = ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) )
248 247 oveq2d 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( R gsum ( x e. I |-> ( ( h ` x ) .x. ( g ` x ) ) ) ) = ( R gsum ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) )
249 170 3ad2ant1 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ., = ( e e. ( B ^m I ) , f e. ( B ^m I ) |-> ( R gsum ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) ) ) )
250 simprl 
 |-  ( ( ( ph /\ g e. V /\ h e. V ) /\ ( e = h /\ f = g ) ) -> e = h )
251 250 fveq1d 
 |-  ( ( ( ph /\ g e. V /\ h e. V ) /\ ( e = h /\ f = g ) ) -> ( e ` x ) = ( h ` x ) )
252 simprr 
 |-  ( ( ( ph /\ g e. V /\ h e. V ) /\ ( e = h /\ f = g ) ) -> f = g )
253 252 fveq1d 
 |-  ( ( ( ph /\ g e. V /\ h e. V ) /\ ( e = h /\ f = g ) ) -> ( f ` x ) = ( g ` x ) )
254 251 253 oveq12d 
 |-  ( ( ( ph /\ g e. V /\ h e. V ) /\ ( e = h /\ f = g ) ) -> ( ( e ` x ) .x. ( f ` x ) ) = ( ( h ` x ) .x. ( g ` x ) ) )
255 254 mpteq2dv 
 |-  ( ( ( 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 ) ) ) )
256 255 oveq2d 
 |-  ( ( ( ph /\ g e. V /\ h e. V ) /\ ( e = h /\ f = g ) ) -> ( R gsum ( x e. I |-> ( ( e ` x ) .x. ( f ` x ) ) ) ) = ( R gsum ( x e. I |-> ( ( h ` x ) .x. ( g ` x ) ) ) ) )
257 ovexd 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( R gsum ( x e. I |-> ( ( h ` x ) .x. ( g ` x ) ) ) ) e. _V )
258 249 256 50 45 257 ovmpod 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( h ., g ) = ( R gsum ( x e. I |-> ( ( h ` x ) .x. ( g ` x ) ) ) ) )
259 fveq2 
 |-  ( x = ( g ., h ) -> ( .* ` x ) = ( .* ` ( g ., h ) ) )
260 id 
 |-  ( x = ( g ., h ) -> x = ( g ., h ) )
261 259 260 eqeq12d 
 |-  ( x = ( g ., h ) -> ( ( .* ` x ) = x <-> ( .* ` ( g ., h ) ) = ( g ., h ) ) )
262 11 ralrimiva 
 |-  ( ph -> A. x e. B ( .* ` x ) = x )
263 262 3ad2ant1 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> A. x e. B ( .* ` x ) = x )
264 261 263 71 rspcdva 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( .* ` ( g ., h ) ) = ( g ., h ) )
265 264 59 eqtrd 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( .* ` ( g ., h ) ) = ( R gsum ( x e. I |-> ( ( g ` x ) .x. ( h ` x ) ) ) ) )
266 248 258 265 3eqtr4rd 
 |-  ( ( ph /\ g e. V /\ h e. V ) -> ( .* ` ( g ., h ) ) = ( h ., g ) )
267 13 14 15 16 17 22 23 24 25 26 27 35 37 71 242 10 266 isphld 
 |-  ( ph -> Y e. PreHil )