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
|
syl5eq |
|- ( ( 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
|
syl5eq |
|- ( ( 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 ) |