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