Step |
Hyp |
Ref |
Expression |
1 |
|
evlslem1.p |
|- P = ( I mPoly R ) |
2 |
|
evlslem1.b |
|- B = ( Base ` P ) |
3 |
|
evlslem1.c |
|- C = ( Base ` S ) |
4 |
|
evlslem1.d |
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |
5 |
|
evlslem1.t |
|- T = ( mulGrp ` S ) |
6 |
|
evlslem1.x |
|- .^ = ( .g ` T ) |
7 |
|
evlslem1.m |
|- .x. = ( .r ` S ) |
8 |
|
evlslem1.v |
|- V = ( I mVar R ) |
9 |
|
evlslem1.e |
|- E = ( p e. B |-> ( S gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) |
10 |
|
evlslem1.i |
|- ( ph -> I e. W ) |
11 |
|
evlslem1.r |
|- ( ph -> R e. CRing ) |
12 |
|
evlslem1.s |
|- ( ph -> S e. CRing ) |
13 |
|
evlslem1.f |
|- ( ph -> F e. ( R RingHom S ) ) |
14 |
|
evlslem1.g |
|- ( ph -> G : I --> C ) |
15 |
|
evlslem1.a |
|- A = ( algSc ` P ) |
16 |
|
eqid |
|- ( 1r ` P ) = ( 1r ` P ) |
17 |
|
eqid |
|- ( 1r ` S ) = ( 1r ` S ) |
18 |
|
eqid |
|- ( .r ` P ) = ( .r ` P ) |
19 |
11
|
crngringd |
|- ( ph -> R e. Ring ) |
20 |
1 10 19
|
mplringd |
|- ( ph -> P e. Ring ) |
21 |
12
|
crngringd |
|- ( ph -> S e. Ring ) |
22 |
|
2fveq3 |
|- ( x = ( 1r ` R ) -> ( E ` ( A ` x ) ) = ( E ` ( A ` ( 1r ` R ) ) ) ) |
23 |
|
fveq2 |
|- ( x = ( 1r ` R ) -> ( F ` x ) = ( F ` ( 1r ` R ) ) ) |
24 |
22 23
|
eqeq12d |
|- ( x = ( 1r ` R ) -> ( ( E ` ( A ` x ) ) = ( F ` x ) <-> ( E ` ( A ` ( 1r ` R ) ) ) = ( F ` ( 1r ` R ) ) ) ) |
25 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
26 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
27 |
10
|
adantr |
|- ( ( ph /\ x e. ( Base ` R ) ) -> I e. W ) |
28 |
19
|
adantr |
|- ( ( ph /\ x e. ( Base ` R ) ) -> R e. Ring ) |
29 |
|
simpr |
|- ( ( ph /\ x e. ( Base ` R ) ) -> x e. ( Base ` R ) ) |
30 |
1 4 25 26 15 27 28 29
|
mplascl |
|- ( ( ph /\ x e. ( Base ` R ) ) -> ( A ` x ) = ( y e. D |-> if ( y = ( I X. { 0 } ) , x , ( 0g ` R ) ) ) ) |
31 |
30
|
fveq2d |
|- ( ( ph /\ x e. ( Base ` R ) ) -> ( E ` ( A ` x ) ) = ( E ` ( y e. D |-> if ( y = ( I X. { 0 } ) , x , ( 0g ` R ) ) ) ) ) |
32 |
11
|
adantr |
|- ( ( ph /\ x e. ( Base ` R ) ) -> R e. CRing ) |
33 |
12
|
adantr |
|- ( ( ph /\ x e. ( Base ` R ) ) -> S e. CRing ) |
34 |
13
|
adantr |
|- ( ( ph /\ x e. ( Base ` R ) ) -> F e. ( R RingHom S ) ) |
35 |
14
|
adantr |
|- ( ( ph /\ x e. ( Base ` R ) ) -> G : I --> C ) |
36 |
4
|
psrbag0 |
|- ( I e. W -> ( I X. { 0 } ) e. D ) |
37 |
10 36
|
syl |
|- ( ph -> ( I X. { 0 } ) e. D ) |
38 |
37
|
adantr |
|- ( ( ph /\ x e. ( Base ` R ) ) -> ( I X. { 0 } ) e. D ) |
39 |
1 2 3 26 4 5 6 7 8 9 27 32 33 34 35 25 38 29
|
evlslem3 |
|- ( ( ph /\ x e. ( Base ` R ) ) -> ( E ` ( y e. D |-> if ( y = ( I X. { 0 } ) , x , ( 0g ` R ) ) ) ) = ( ( F ` x ) .x. ( T gsum ( ( I X. { 0 } ) oF .^ G ) ) ) ) |
40 |
|
0zd |
|- ( ( ph /\ x e. I ) -> 0 e. ZZ ) |
41 |
|
fvexd |
|- ( ( ph /\ x e. I ) -> ( G ` x ) e. _V ) |
42 |
|
fconstmpt |
|- ( I X. { 0 } ) = ( x e. I |-> 0 ) |
43 |
42
|
a1i |
|- ( ph -> ( I X. { 0 } ) = ( x e. I |-> 0 ) ) |
44 |
14
|
feqmptd |
|- ( ph -> G = ( x e. I |-> ( G ` x ) ) ) |
45 |
10 40 41 43 44
|
offval2 |
|- ( ph -> ( ( I X. { 0 } ) oF .^ G ) = ( x e. I |-> ( 0 .^ ( G ` x ) ) ) ) |
46 |
14
|
ffvelcdmda |
|- ( ( ph /\ x e. I ) -> ( G ` x ) e. C ) |
47 |
5 3
|
mgpbas |
|- C = ( Base ` T ) |
48 |
5 17
|
ringidval |
|- ( 1r ` S ) = ( 0g ` T ) |
49 |
47 48 6
|
mulg0 |
|- ( ( G ` x ) e. C -> ( 0 .^ ( G ` x ) ) = ( 1r ` S ) ) |
50 |
46 49
|
syl |
|- ( ( ph /\ x e. I ) -> ( 0 .^ ( G ` x ) ) = ( 1r ` S ) ) |
51 |
50
|
mpteq2dva |
|- ( ph -> ( x e. I |-> ( 0 .^ ( G ` x ) ) ) = ( x e. I |-> ( 1r ` S ) ) ) |
52 |
45 51
|
eqtrd |
|- ( ph -> ( ( I X. { 0 } ) oF .^ G ) = ( x e. I |-> ( 1r ` S ) ) ) |
53 |
52
|
oveq2d |
|- ( ph -> ( T gsum ( ( I X. { 0 } ) oF .^ G ) ) = ( T gsum ( x e. I |-> ( 1r ` S ) ) ) ) |
54 |
5
|
crngmgp |
|- ( S e. CRing -> T e. CMnd ) |
55 |
12 54
|
syl |
|- ( ph -> T e. CMnd ) |
56 |
55
|
cmnmndd |
|- ( ph -> T e. Mnd ) |
57 |
48
|
gsumz |
|- ( ( T e. Mnd /\ I e. W ) -> ( T gsum ( x e. I |-> ( 1r ` S ) ) ) = ( 1r ` S ) ) |
58 |
56 10 57
|
syl2anc |
|- ( ph -> ( T gsum ( x e. I |-> ( 1r ` S ) ) ) = ( 1r ` S ) ) |
59 |
53 58
|
eqtrd |
|- ( ph -> ( T gsum ( ( I X. { 0 } ) oF .^ G ) ) = ( 1r ` S ) ) |
60 |
59
|
adantr |
|- ( ( ph /\ x e. ( Base ` R ) ) -> ( T gsum ( ( I X. { 0 } ) oF .^ G ) ) = ( 1r ` S ) ) |
61 |
60
|
oveq2d |
|- ( ( ph /\ x e. ( Base ` R ) ) -> ( ( F ` x ) .x. ( T gsum ( ( I X. { 0 } ) oF .^ G ) ) ) = ( ( F ` x ) .x. ( 1r ` S ) ) ) |
62 |
26 3
|
rhmf |
|- ( F e. ( R RingHom S ) -> F : ( Base ` R ) --> C ) |
63 |
13 62
|
syl |
|- ( ph -> F : ( Base ` R ) --> C ) |
64 |
63
|
ffvelcdmda |
|- ( ( ph /\ x e. ( Base ` R ) ) -> ( F ` x ) e. C ) |
65 |
3 7 17
|
ringridm |
|- ( ( S e. Ring /\ ( F ` x ) e. C ) -> ( ( F ` x ) .x. ( 1r ` S ) ) = ( F ` x ) ) |
66 |
21 64 65
|
syl2an2r |
|- ( ( ph /\ x e. ( Base ` R ) ) -> ( ( F ` x ) .x. ( 1r ` S ) ) = ( F ` x ) ) |
67 |
61 66
|
eqtrd |
|- ( ( ph /\ x e. ( Base ` R ) ) -> ( ( F ` x ) .x. ( T gsum ( ( I X. { 0 } ) oF .^ G ) ) ) = ( F ` x ) ) |
68 |
31 39 67
|
3eqtrd |
|- ( ( ph /\ x e. ( Base ` R ) ) -> ( E ` ( A ` x ) ) = ( F ` x ) ) |
69 |
68
|
ralrimiva |
|- ( ph -> A. x e. ( Base ` R ) ( E ` ( A ` x ) ) = ( F ` x ) ) |
70 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
71 |
26 70
|
ringidcl |
|- ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) ) |
72 |
19 71
|
syl |
|- ( ph -> ( 1r ` R ) e. ( Base ` R ) ) |
73 |
24 69 72
|
rspcdva |
|- ( ph -> ( E ` ( A ` ( 1r ` R ) ) ) = ( F ` ( 1r ` R ) ) ) |
74 |
1
|
mplassa |
|- ( ( I e. W /\ R e. CRing ) -> P e. AssAlg ) |
75 |
10 11 74
|
syl2anc |
|- ( ph -> P e. AssAlg ) |
76 |
|
eqid |
|- ( Scalar ` P ) = ( Scalar ` P ) |
77 |
15 76
|
asclrhm |
|- ( P e. AssAlg -> A e. ( ( Scalar ` P ) RingHom P ) ) |
78 |
75 77
|
syl |
|- ( ph -> A e. ( ( Scalar ` P ) RingHom P ) ) |
79 |
1 10 11
|
mplsca |
|- ( ph -> R = ( Scalar ` P ) ) |
80 |
79
|
oveq1d |
|- ( ph -> ( R RingHom P ) = ( ( Scalar ` P ) RingHom P ) ) |
81 |
78 80
|
eleqtrrd |
|- ( ph -> A e. ( R RingHom P ) ) |
82 |
70 16
|
rhm1 |
|- ( A e. ( R RingHom P ) -> ( A ` ( 1r ` R ) ) = ( 1r ` P ) ) |
83 |
81 82
|
syl |
|- ( ph -> ( A ` ( 1r ` R ) ) = ( 1r ` P ) ) |
84 |
83
|
fveq2d |
|- ( ph -> ( E ` ( A ` ( 1r ` R ) ) ) = ( E ` ( 1r ` P ) ) ) |
85 |
70 17
|
rhm1 |
|- ( F e. ( R RingHom S ) -> ( F ` ( 1r ` R ) ) = ( 1r ` S ) ) |
86 |
13 85
|
syl |
|- ( ph -> ( F ` ( 1r ` R ) ) = ( 1r ` S ) ) |
87 |
73 84 86
|
3eqtr3d |
|- ( ph -> ( E ` ( 1r ` P ) ) = ( 1r ` S ) ) |
88 |
|
eqid |
|- ( +g ` P ) = ( +g ` P ) |
89 |
|
eqid |
|- ( +g ` S ) = ( +g ` S ) |
90 |
20
|
ringgrpd |
|- ( ph -> P e. Grp ) |
91 |
21
|
ringgrpd |
|- ( ph -> S e. Grp ) |
92 |
|
eqid |
|- ( 0g ` S ) = ( 0g ` S ) |
93 |
|
ringcmn |
|- ( S e. Ring -> S e. CMnd ) |
94 |
21 93
|
syl |
|- ( ph -> S e. CMnd ) |
95 |
94
|
adantr |
|- ( ( ph /\ p e. B ) -> S e. CMnd ) |
96 |
|
ovex |
|- ( NN0 ^m I ) e. _V |
97 |
4 96
|
rabex2 |
|- D e. _V |
98 |
97
|
a1i |
|- ( ( ph /\ p e. B ) -> D e. _V ) |
99 |
10
|
adantr |
|- ( ( ph /\ p e. B ) -> I e. W ) |
100 |
11
|
adantr |
|- ( ( ph /\ p e. B ) -> R e. CRing ) |
101 |
12
|
adantr |
|- ( ( ph /\ p e. B ) -> S e. CRing ) |
102 |
13
|
adantr |
|- ( ( ph /\ p e. B ) -> F e. ( R RingHom S ) ) |
103 |
14
|
adantr |
|- ( ( ph /\ p e. B ) -> G : I --> C ) |
104 |
|
simpr |
|- ( ( ph /\ p e. B ) -> p e. B ) |
105 |
1 2 3 4 5 6 7 8 9 99 100 101 102 103 104
|
evlslem6 |
|- ( ( ph /\ p e. B ) -> ( ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) : D --> C /\ ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) finSupp ( 0g ` S ) ) ) |
106 |
105
|
simpld |
|- ( ( ph /\ p e. B ) -> ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) : D --> C ) |
107 |
105
|
simprd |
|- ( ( ph /\ p e. B ) -> ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) finSupp ( 0g ` S ) ) |
108 |
3 92 95 98 106 107
|
gsumcl |
|- ( ( ph /\ p e. B ) -> ( S gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) e. C ) |
109 |
108 9
|
fmptd |
|- ( ph -> E : B --> C ) |
110 |
|
eqid |
|- ( +g ` R ) = ( +g ` R ) |
111 |
|
simplrl |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> x e. B ) |
112 |
|
simplrr |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> y e. B ) |
113 |
1 2 110 88 111 112
|
mpladd |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( x ( +g ` P ) y ) = ( x oF ( +g ` R ) y ) ) |
114 |
113
|
fveq1d |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( x ( +g ` P ) y ) ` b ) = ( ( x oF ( +g ` R ) y ) ` b ) ) |
115 |
|
simprl |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> x e. B ) |
116 |
1 26 2 4 115
|
mplelf |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> x : D --> ( Base ` R ) ) |
117 |
116
|
ffnd |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> x Fn D ) |
118 |
117
|
adantr |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> x Fn D ) |
119 |
|
simprr |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> y e. B ) |
120 |
1 26 2 4 119
|
mplelf |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> y : D --> ( Base ` R ) ) |
121 |
120
|
ffnd |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> y Fn D ) |
122 |
121
|
adantr |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> y Fn D ) |
123 |
97
|
a1i |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> D e. _V ) |
124 |
|
simpr |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> b e. D ) |
125 |
|
fnfvof |
|- ( ( ( x Fn D /\ y Fn D ) /\ ( D e. _V /\ b e. D ) ) -> ( ( x oF ( +g ` R ) y ) ` b ) = ( ( x ` b ) ( +g ` R ) ( y ` b ) ) ) |
126 |
118 122 123 124 125
|
syl22anc |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( x oF ( +g ` R ) y ) ` b ) = ( ( x ` b ) ( +g ` R ) ( y ` b ) ) ) |
127 |
114 126
|
eqtrd |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( x ( +g ` P ) y ) ` b ) = ( ( x ` b ) ( +g ` R ) ( y ` b ) ) ) |
128 |
127
|
fveq2d |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( F ` ( ( x ( +g ` P ) y ) ` b ) ) = ( F ` ( ( x ` b ) ( +g ` R ) ( y ` b ) ) ) ) |
129 |
|
rhmghm |
|- ( F e. ( R RingHom S ) -> F e. ( R GrpHom S ) ) |
130 |
13 129
|
syl |
|- ( ph -> F e. ( R GrpHom S ) ) |
131 |
130
|
ad2antrr |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> F e. ( R GrpHom S ) ) |
132 |
116
|
ffvelcdmda |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( x ` b ) e. ( Base ` R ) ) |
133 |
120
|
ffvelcdmda |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( y ` b ) e. ( Base ` R ) ) |
134 |
26 110 89
|
ghmlin |
|- ( ( F e. ( R GrpHom S ) /\ ( x ` b ) e. ( Base ` R ) /\ ( y ` b ) e. ( Base ` R ) ) -> ( F ` ( ( x ` b ) ( +g ` R ) ( y ` b ) ) ) = ( ( F ` ( x ` b ) ) ( +g ` S ) ( F ` ( y ` b ) ) ) ) |
135 |
131 132 133 134
|
syl3anc |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( F ` ( ( x ` b ) ( +g ` R ) ( y ` b ) ) ) = ( ( F ` ( x ` b ) ) ( +g ` S ) ( F ` ( y ` b ) ) ) ) |
136 |
128 135
|
eqtrd |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( F ` ( ( x ( +g ` P ) y ) ` b ) ) = ( ( F ` ( x ` b ) ) ( +g ` S ) ( F ` ( y ` b ) ) ) ) |
137 |
136
|
oveq1d |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( ( ( F ` ( x ` b ) ) ( +g ` S ) ( F ` ( y ` b ) ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) |
138 |
21
|
ad2antrr |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> S e. Ring ) |
139 |
63
|
ad2antrr |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> F : ( Base ` R ) --> C ) |
140 |
139 132
|
ffvelcdmd |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( F ` ( x ` b ) ) e. C ) |
141 |
139 133
|
ffvelcdmd |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( F ` ( y ` b ) ) e. C ) |
142 |
55
|
ad2antrr |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> T e. CMnd ) |
143 |
14
|
ad2antrr |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> G : I --> C ) |
144 |
4 47 6 142 124 143
|
psrbagev2 |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( T gsum ( b oF .^ G ) ) e. C ) |
145 |
3 89 7
|
ringdir |
|- ( ( S e. Ring /\ ( ( F ` ( x ` b ) ) e. C /\ ( F ` ( y ` b ) ) e. C /\ ( T gsum ( b oF .^ G ) ) e. C ) ) -> ( ( ( F ` ( x ` b ) ) ( +g ` S ) ( F ` ( y ` b ) ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ( +g ` S ) ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) |
146 |
138 140 141 144 145
|
syl13anc |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( ( F ` ( x ` b ) ) ( +g ` S ) ( F ` ( y ` b ) ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ( +g ` S ) ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) |
147 |
137 146
|
eqtrd |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ( +g ` S ) ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) |
148 |
147
|
mpteq2dva |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ( +g ` S ) ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) |
149 |
97
|
a1i |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> D e. _V ) |
150 |
|
ovexd |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) e. _V ) |
151 |
|
ovexd |
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ b e. D ) -> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) e. _V ) |
152 |
|
eqidd |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) |
153 |
|
eqidd |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) |
154 |
149 150 151 152 153
|
offval2 |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) oF ( +g ` S ) ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) = ( b e. D |-> ( ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ( +g ` S ) ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) |
155 |
148 154
|
eqtr4d |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) = ( ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) oF ( +g ` S ) ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) |
156 |
155
|
oveq2d |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( S gsum ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) = ( S gsum ( ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) oF ( +g ` S ) ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) ) |
157 |
94
|
adantr |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> S e. CMnd ) |
158 |
10
|
adantr |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> I e. W ) |
159 |
11
|
adantr |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> R e. CRing ) |
160 |
12
|
adantr |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> S e. CRing ) |
161 |
13
|
adantr |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> F e. ( R RingHom S ) ) |
162 |
14
|
adantr |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> G : I --> C ) |
163 |
1 2 3 4 5 6 7 8 9 158 159 160 161 162 115
|
evlslem6 |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) : D --> C /\ ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) finSupp ( 0g ` S ) ) ) |
164 |
163
|
simpld |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) : D --> C ) |
165 |
1 2 3 4 5 6 7 8 9 158 159 160 161 162 119
|
evlslem6 |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) : D --> C /\ ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) finSupp ( 0g ` S ) ) ) |
166 |
165
|
simpld |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) : D --> C ) |
167 |
163
|
simprd |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) finSupp ( 0g ` S ) ) |
168 |
165
|
simprd |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) finSupp ( 0g ` S ) ) |
169 |
3 92 89 157 149 164 166 167 168
|
gsumadd |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( S gsum ( ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) oF ( +g ` S ) ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) = ( ( S gsum ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ( +g ` S ) ( S gsum ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) ) |
170 |
156 169
|
eqtrd |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( S gsum ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) = ( ( S gsum ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ( +g ` S ) ( S gsum ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) ) |
171 |
90
|
adantr |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> P e. Grp ) |
172 |
2 88
|
grpcl |
|- ( ( P e. Grp /\ x e. B /\ y e. B ) -> ( x ( +g ` P ) y ) e. B ) |
173 |
171 115 119 172
|
syl3anc |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` P ) y ) e. B ) |
174 |
|
fveq1 |
|- ( p = ( x ( +g ` P ) y ) -> ( p ` b ) = ( ( x ( +g ` P ) y ) ` b ) ) |
175 |
174
|
fveq2d |
|- ( p = ( x ( +g ` P ) y ) -> ( F ` ( p ` b ) ) = ( F ` ( ( x ( +g ` P ) y ) ` b ) ) ) |
176 |
175
|
oveq1d |
|- ( p = ( x ( +g ` P ) y ) -> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) |
177 |
176
|
mpteq2dv |
|- ( p = ( x ( +g ` P ) y ) -> ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) |
178 |
177
|
oveq2d |
|- ( p = ( x ( +g ` P ) y ) -> ( S gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) = ( S gsum ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) |
179 |
|
ovex |
|- ( S gsum ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) e. _V |
180 |
178 9 179
|
fvmpt |
|- ( ( x ( +g ` P ) y ) e. B -> ( E ` ( x ( +g ` P ) y ) ) = ( S gsum ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) |
181 |
173 180
|
syl |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` ( x ( +g ` P ) y ) ) = ( S gsum ( b e. D |-> ( ( F ` ( ( x ( +g ` P ) y ) ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) |
182 |
|
fveq1 |
|- ( p = x -> ( p ` b ) = ( x ` b ) ) |
183 |
182
|
fveq2d |
|- ( p = x -> ( F ` ( p ` b ) ) = ( F ` ( x ` b ) ) ) |
184 |
183
|
oveq1d |
|- ( p = x -> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) |
185 |
184
|
mpteq2dv |
|- ( p = x -> ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) |
186 |
185
|
oveq2d |
|- ( p = x -> ( S gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) = ( S gsum ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) |
187 |
|
ovex |
|- ( S gsum ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) e. _V |
188 |
186 9 187
|
fvmpt |
|- ( x e. B -> ( E ` x ) = ( S gsum ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) |
189 |
115 188
|
syl |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` x ) = ( S gsum ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) |
190 |
|
fveq1 |
|- ( p = y -> ( p ` b ) = ( y ` b ) ) |
191 |
190
|
fveq2d |
|- ( p = y -> ( F ` ( p ` b ) ) = ( F ` ( y ` b ) ) ) |
192 |
191
|
oveq1d |
|- ( p = y -> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) = ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) |
193 |
192
|
mpteq2dv |
|- ( p = y -> ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) = ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) |
194 |
193
|
oveq2d |
|- ( p = y -> ( S gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) = ( S gsum ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) |
195 |
|
ovex |
|- ( S gsum ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) e. _V |
196 |
194 9 195
|
fvmpt |
|- ( y e. B -> ( E ` y ) = ( S gsum ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) |
197 |
196
|
ad2antll |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` y ) = ( S gsum ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) |
198 |
189 197
|
oveq12d |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( E ` x ) ( +g ` S ) ( E ` y ) ) = ( ( S gsum ( b e. D |-> ( ( F ` ( x ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ( +g ` S ) ( S gsum ( b e. D |-> ( ( F ` ( y ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) ) ) |
199 |
170 181 198
|
3eqtr4d |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` ( x ( +g ` P ) y ) ) = ( ( E ` x ) ( +g ` S ) ( E ` y ) ) ) |
200 |
2 3 88 89 90 91 109 199
|
isghmd |
|- ( ph -> E e. ( P GrpHom S ) ) |
201 |
|
eqid |
|- ( mulGrp ` R ) = ( mulGrp ` R ) |
202 |
201 5
|
rhmmhm |
|- ( F e. ( R RingHom S ) -> F e. ( ( mulGrp ` R ) MndHom T ) ) |
203 |
13 202
|
syl |
|- ( ph -> F e. ( ( mulGrp ` R ) MndHom T ) ) |
204 |
203
|
adantr |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> F e. ( ( mulGrp ` R ) MndHom T ) ) |
205 |
|
simprll |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> x e. B ) |
206 |
1 26 2 4 205
|
mplelf |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> x : D --> ( Base ` R ) ) |
207 |
|
simprrl |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> z e. D ) |
208 |
206 207
|
ffvelcdmd |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( x ` z ) e. ( Base ` R ) ) |
209 |
|
simprlr |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> y e. B ) |
210 |
1 26 2 4 209
|
mplelf |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> y : D --> ( Base ` R ) ) |
211 |
|
simprrr |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> w e. D ) |
212 |
210 211
|
ffvelcdmd |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( y ` w ) e. ( Base ` R ) ) |
213 |
201 26
|
mgpbas |
|- ( Base ` R ) = ( Base ` ( mulGrp ` R ) ) |
214 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
215 |
201 214
|
mgpplusg |
|- ( .r ` R ) = ( +g ` ( mulGrp ` R ) ) |
216 |
5 7
|
mgpplusg |
|- .x. = ( +g ` T ) |
217 |
213 215 216
|
mhmlin |
|- ( ( F e. ( ( mulGrp ` R ) MndHom T ) /\ ( x ` z ) e. ( Base ` R ) /\ ( y ` w ) e. ( Base ` R ) ) -> ( F ` ( ( x ` z ) ( .r ` R ) ( y ` w ) ) ) = ( ( F ` ( x ` z ) ) .x. ( F ` ( y ` w ) ) ) ) |
218 |
204 208 212 217
|
syl3anc |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( F ` ( ( x ` z ) ( .r ` R ) ( y ` w ) ) ) = ( ( F ` ( x ` z ) ) .x. ( F ` ( y ` w ) ) ) ) |
219 |
56
|
ad2antrr |
|- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> T e. Mnd ) |
220 |
|
simprl |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> z e. D ) |
221 |
4
|
psrbagf |
|- ( z e. D -> z : I --> NN0 ) |
222 |
220 221
|
syl |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> z : I --> NN0 ) |
223 |
222
|
ffvelcdmda |
|- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( z ` v ) e. NN0 ) |
224 |
4
|
psrbagf |
|- ( w e. D -> w : I --> NN0 ) |
225 |
224
|
ad2antll |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> w : I --> NN0 ) |
226 |
225
|
ffvelcdmda |
|- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( w ` v ) e. NN0 ) |
227 |
14
|
adantr |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> G : I --> C ) |
228 |
227
|
ffvelcdmda |
|- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( G ` v ) e. C ) |
229 |
47 6 216
|
mulgnn0dir |
|- ( ( T e. Mnd /\ ( ( z ` v ) e. NN0 /\ ( w ` v ) e. NN0 /\ ( G ` v ) e. C ) ) -> ( ( ( z ` v ) + ( w ` v ) ) .^ ( G ` v ) ) = ( ( ( z ` v ) .^ ( G ` v ) ) .x. ( ( w ` v ) .^ ( G ` v ) ) ) ) |
230 |
219 223 226 228 229
|
syl13anc |
|- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( ( ( z ` v ) + ( w ` v ) ) .^ ( G ` v ) ) = ( ( ( z ` v ) .^ ( G ` v ) ) .x. ( ( w ` v ) .^ ( G ` v ) ) ) ) |
231 |
230
|
mpteq2dva |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( v e. I |-> ( ( ( z ` v ) + ( w ` v ) ) .^ ( G ` v ) ) ) = ( v e. I |-> ( ( ( z ` v ) .^ ( G ` v ) ) .x. ( ( w ` v ) .^ ( G ` v ) ) ) ) ) |
232 |
10
|
adantr |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> I e. W ) |
233 |
|
ovexd |
|- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( ( z ` v ) + ( w ` v ) ) e. _V ) |
234 |
|
fvexd |
|- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( G ` v ) e. _V ) |
235 |
222
|
ffnd |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> z Fn I ) |
236 |
225
|
ffnd |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> w Fn I ) |
237 |
|
inidm |
|- ( I i^i I ) = I |
238 |
|
eqidd |
|- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( z ` v ) = ( z ` v ) ) |
239 |
|
eqidd |
|- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( w ` v ) = ( w ` v ) ) |
240 |
235 236 232 232 237 238 239
|
offval |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( z oF + w ) = ( v e. I |-> ( ( z ` v ) + ( w ` v ) ) ) ) |
241 |
14
|
feqmptd |
|- ( ph -> G = ( v e. I |-> ( G ` v ) ) ) |
242 |
241
|
adantr |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> G = ( v e. I |-> ( G ` v ) ) ) |
243 |
232 233 234 240 242
|
offval2 |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( ( z oF + w ) oF .^ G ) = ( v e. I |-> ( ( ( z ` v ) + ( w ` v ) ) .^ ( G ` v ) ) ) ) |
244 |
|
ovexd |
|- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( ( z ` v ) .^ ( G ` v ) ) e. _V ) |
245 |
|
ovexd |
|- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( ( w ` v ) .^ ( G ` v ) ) e. _V ) |
246 |
14
|
ffnd |
|- ( ph -> G Fn I ) |
247 |
246
|
adantr |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> G Fn I ) |
248 |
|
eqidd |
|- ( ( ( ph /\ ( z e. D /\ w e. D ) ) /\ v e. I ) -> ( G ` v ) = ( G ` v ) ) |
249 |
235 247 232 232 237 238 248
|
offval |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( z oF .^ G ) = ( v e. I |-> ( ( z ` v ) .^ ( G ` v ) ) ) ) |
250 |
236 247 232 232 237 239 248
|
offval |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( w oF .^ G ) = ( v e. I |-> ( ( w ` v ) .^ ( G ` v ) ) ) ) |
251 |
232 244 245 249 250
|
offval2 |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( ( z oF .^ G ) oF .x. ( w oF .^ G ) ) = ( v e. I |-> ( ( ( z ` v ) .^ ( G ` v ) ) .x. ( ( w ` v ) .^ ( G ` v ) ) ) ) ) |
252 |
231 243 251
|
3eqtr4d |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( ( z oF + w ) oF .^ G ) = ( ( z oF .^ G ) oF .x. ( w oF .^ G ) ) ) |
253 |
252
|
oveq2d |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( T gsum ( ( z oF + w ) oF .^ G ) ) = ( T gsum ( ( z oF .^ G ) oF .x. ( w oF .^ G ) ) ) ) |
254 |
55
|
adantr |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> T e. CMnd ) |
255 |
4 47 6 48 254 220 227
|
psrbagev1 |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( ( z oF .^ G ) : I --> C /\ ( z oF .^ G ) finSupp ( 1r ` S ) ) ) |
256 |
255
|
simpld |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( z oF .^ G ) : I --> C ) |
257 |
|
simprr |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> w e. D ) |
258 |
4 47 6 48 254 257 227
|
psrbagev1 |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( ( w oF .^ G ) : I --> C /\ ( w oF .^ G ) finSupp ( 1r ` S ) ) ) |
259 |
258
|
simpld |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( w oF .^ G ) : I --> C ) |
260 |
255
|
simprd |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( z oF .^ G ) finSupp ( 1r ` S ) ) |
261 |
258
|
simprd |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( w oF .^ G ) finSupp ( 1r ` S ) ) |
262 |
47 48 216 254 232 256 259 260 261
|
gsumadd |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( T gsum ( ( z oF .^ G ) oF .x. ( w oF .^ G ) ) ) = ( ( T gsum ( z oF .^ G ) ) .x. ( T gsum ( w oF .^ G ) ) ) ) |
263 |
253 262
|
eqtrd |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( T gsum ( ( z oF + w ) oF .^ G ) ) = ( ( T gsum ( z oF .^ G ) ) .x. ( T gsum ( w oF .^ G ) ) ) ) |
264 |
263
|
adantrl |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( T gsum ( ( z oF + w ) oF .^ G ) ) = ( ( T gsum ( z oF .^ G ) ) .x. ( T gsum ( w oF .^ G ) ) ) ) |
265 |
218 264
|
oveq12d |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( ( F ` ( ( x ` z ) ( .r ` R ) ( y ` w ) ) ) .x. ( T gsum ( ( z oF + w ) oF .^ G ) ) ) = ( ( ( F ` ( x ` z ) ) .x. ( F ` ( y ` w ) ) ) .x. ( ( T gsum ( z oF .^ G ) ) .x. ( T gsum ( w oF .^ G ) ) ) ) ) |
266 |
55
|
adantr |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> T e. CMnd ) |
267 |
63
|
adantr |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> F : ( Base ` R ) --> C ) |
268 |
267 208
|
ffvelcdmd |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( F ` ( x ` z ) ) e. C ) |
269 |
267 212
|
ffvelcdmd |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( F ` ( y ` w ) ) e. C ) |
270 |
4 47 6 254 220 227
|
psrbagev2 |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( T gsum ( z oF .^ G ) ) e. C ) |
271 |
270
|
adantrl |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( T gsum ( z oF .^ G ) ) e. C ) |
272 |
4 47 6 254 257 227
|
psrbagev2 |
|- ( ( ph /\ ( z e. D /\ w e. D ) ) -> ( T gsum ( w oF .^ G ) ) e. C ) |
273 |
272
|
adantrl |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( T gsum ( w oF .^ G ) ) e. C ) |
274 |
47 216
|
cmn4 |
|- ( ( T e. CMnd /\ ( ( F ` ( x ` z ) ) e. C /\ ( F ` ( y ` w ) ) e. C ) /\ ( ( T gsum ( z oF .^ G ) ) e. C /\ ( T gsum ( w oF .^ G ) ) e. C ) ) -> ( ( ( F ` ( x ` z ) ) .x. ( F ` ( y ` w ) ) ) .x. ( ( T gsum ( z oF .^ G ) ) .x. ( T gsum ( w oF .^ G ) ) ) ) = ( ( ( F ` ( x ` z ) ) .x. ( T gsum ( z oF .^ G ) ) ) .x. ( ( F ` ( y ` w ) ) .x. ( T gsum ( w oF .^ G ) ) ) ) ) |
275 |
266 268 269 271 273 274
|
syl122anc |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( ( ( F ` ( x ` z ) ) .x. ( F ` ( y ` w ) ) ) .x. ( ( T gsum ( z oF .^ G ) ) .x. ( T gsum ( w oF .^ G ) ) ) ) = ( ( ( F ` ( x ` z ) ) .x. ( T gsum ( z oF .^ G ) ) ) .x. ( ( F ` ( y ` w ) ) .x. ( T gsum ( w oF .^ G ) ) ) ) ) |
276 |
265 275
|
eqtrd |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( ( F ` ( ( x ` z ) ( .r ` R ) ( y ` w ) ) ) .x. ( T gsum ( ( z oF + w ) oF .^ G ) ) ) = ( ( ( F ` ( x ` z ) ) .x. ( T gsum ( z oF .^ G ) ) ) .x. ( ( F ` ( y ` w ) ) .x. ( T gsum ( w oF .^ G ) ) ) ) ) |
277 |
10
|
adantr |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> I e. W ) |
278 |
11
|
adantr |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> R e. CRing ) |
279 |
12
|
adantr |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> S e. CRing ) |
280 |
13
|
adantr |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> F e. ( R RingHom S ) ) |
281 |
14
|
adantr |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> G : I --> C ) |
282 |
4
|
psrbagaddcl |
|- ( ( z e. D /\ w e. D ) -> ( z oF + w ) e. D ) |
283 |
282
|
ad2antll |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( z oF + w ) e. D ) |
284 |
19
|
adantr |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> R e. Ring ) |
285 |
26 214
|
ringcl |
|- ( ( R e. Ring /\ ( x ` z ) e. ( Base ` R ) /\ ( y ` w ) e. ( Base ` R ) ) -> ( ( x ` z ) ( .r ` R ) ( y ` w ) ) e. ( Base ` R ) ) |
286 |
284 208 212 285
|
syl3anc |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( ( x ` z ) ( .r ` R ) ( y ` w ) ) e. ( Base ` R ) ) |
287 |
1 2 3 26 4 5 6 7 8 9 277 278 279 280 281 25 283 286
|
evlslem3 |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( E ` ( v e. D |-> if ( v = ( z oF + w ) , ( ( x ` z ) ( .r ` R ) ( y ` w ) ) , ( 0g ` R ) ) ) ) = ( ( F ` ( ( x ` z ) ( .r ` R ) ( y ` w ) ) ) .x. ( T gsum ( ( z oF + w ) oF .^ G ) ) ) ) |
288 |
1 2 3 26 4 5 6 7 8 9 277 278 279 280 281 25 207 208
|
evlslem3 |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( E ` ( v e. D |-> if ( v = z , ( x ` z ) , ( 0g ` R ) ) ) ) = ( ( F ` ( x ` z ) ) .x. ( T gsum ( z oF .^ G ) ) ) ) |
289 |
1 2 3 26 4 5 6 7 8 9 277 278 279 280 281 25 211 212
|
evlslem3 |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( E ` ( v e. D |-> if ( v = w , ( y ` w ) , ( 0g ` R ) ) ) ) = ( ( F ` ( y ` w ) ) .x. ( T gsum ( w oF .^ G ) ) ) ) |
290 |
288 289
|
oveq12d |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( ( E ` ( v e. D |-> if ( v = z , ( x ` z ) , ( 0g ` R ) ) ) ) .x. ( E ` ( v e. D |-> if ( v = w , ( y ` w ) , ( 0g ` R ) ) ) ) ) = ( ( ( F ` ( x ` z ) ) .x. ( T gsum ( z oF .^ G ) ) ) .x. ( ( F ` ( y ` w ) ) .x. ( T gsum ( w oF .^ G ) ) ) ) ) |
291 |
276 287 290
|
3eqtr4d |
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. D /\ w e. D ) ) ) -> ( E ` ( v e. D |-> if ( v = ( z oF + w ) , ( ( x ` z ) ( .r ` R ) ( y ` w ) ) , ( 0g ` R ) ) ) ) = ( ( E ` ( v e. D |-> if ( v = z , ( x ` z ) , ( 0g ` R ) ) ) ) .x. ( E ` ( v e. D |-> if ( v = w , ( y ` w ) , ( 0g ` R ) ) ) ) ) ) |
292 |
1 2 7 25 4 10 11 12 200 291
|
evlslem2 |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` ( x ( .r ` P ) y ) ) = ( ( E ` x ) .x. ( E ` y ) ) ) |
293 |
2 16 17 18 7 20 21 87 292 3 88 89 109 199
|
isrhmd |
|- ( ph -> E e. ( P RingHom S ) ) |
294 |
|
ovex |
|- ( S gsum ( b e. D |-> ( ( F ` ( p ` b ) ) .x. ( T gsum ( b oF .^ G ) ) ) ) ) e. _V |
295 |
294 9
|
fnmpti |
|- E Fn B |
296 |
295
|
a1i |
|- ( ph -> E Fn B ) |
297 |
26 2
|
rhmf |
|- ( A e. ( R RingHom P ) -> A : ( Base ` R ) --> B ) |
298 |
81 297
|
syl |
|- ( ph -> A : ( Base ` R ) --> B ) |
299 |
298
|
ffnd |
|- ( ph -> A Fn ( Base ` R ) ) |
300 |
298
|
frnd |
|- ( ph -> ran A C_ B ) |
301 |
|
fnco |
|- ( ( E Fn B /\ A Fn ( Base ` R ) /\ ran A C_ B ) -> ( E o. A ) Fn ( Base ` R ) ) |
302 |
296 299 300 301
|
syl3anc |
|- ( ph -> ( E o. A ) Fn ( Base ` R ) ) |
303 |
63
|
ffnd |
|- ( ph -> F Fn ( Base ` R ) ) |
304 |
|
fvco2 |
|- ( ( A Fn ( Base ` R ) /\ x e. ( Base ` R ) ) -> ( ( E o. A ) ` x ) = ( E ` ( A ` x ) ) ) |
305 |
299 304
|
sylan |
|- ( ( ph /\ x e. ( Base ` R ) ) -> ( ( E o. A ) ` x ) = ( E ` ( A ` x ) ) ) |
306 |
305 68
|
eqtrd |
|- ( ( ph /\ x e. ( Base ` R ) ) -> ( ( E o. A ) ` x ) = ( F ` x ) ) |
307 |
302 303 306
|
eqfnfvd |
|- ( ph -> ( E o. A ) = F ) |
308 |
1 8 2 10 19
|
mvrf2 |
|- ( ph -> V : I --> B ) |
309 |
308
|
ffnd |
|- ( ph -> V Fn I ) |
310 |
308
|
frnd |
|- ( ph -> ran V C_ B ) |
311 |
|
fnco |
|- ( ( E Fn B /\ V Fn I /\ ran V C_ B ) -> ( E o. V ) Fn I ) |
312 |
296 309 310 311
|
syl3anc |
|- ( ph -> ( E o. V ) Fn I ) |
313 |
|
fvco2 |
|- ( ( V Fn I /\ x e. I ) -> ( ( E o. V ) ` x ) = ( E ` ( V ` x ) ) ) |
314 |
309 313
|
sylan |
|- ( ( ph /\ x e. I ) -> ( ( E o. V ) ` x ) = ( E ` ( V ` x ) ) ) |
315 |
10
|
adantr |
|- ( ( ph /\ x e. I ) -> I e. W ) |
316 |
11
|
adantr |
|- ( ( ph /\ x e. I ) -> R e. CRing ) |
317 |
|
simpr |
|- ( ( ph /\ x e. I ) -> x e. I ) |
318 |
8 4 25 70 315 316 317
|
mvrval |
|- ( ( ph /\ x e. I ) -> ( V ` x ) = ( y e. D |-> if ( y = ( z e. I |-> if ( z = x , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) |
319 |
318
|
fveq2d |
|- ( ( ph /\ x e. I ) -> ( E ` ( V ` x ) ) = ( E ` ( y e. D |-> if ( y = ( z e. I |-> if ( z = x , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) ) |
320 |
12
|
adantr |
|- ( ( ph /\ x e. I ) -> S e. CRing ) |
321 |
13
|
adantr |
|- ( ( ph /\ x e. I ) -> F e. ( R RingHom S ) ) |
322 |
14
|
adantr |
|- ( ( ph /\ x e. I ) -> G : I --> C ) |
323 |
4
|
psrbagsn |
|- ( I e. W -> ( z e. I |-> if ( z = x , 1 , 0 ) ) e. D ) |
324 |
10 323
|
syl |
|- ( ph -> ( z e. I |-> if ( z = x , 1 , 0 ) ) e. D ) |
325 |
324
|
adantr |
|- ( ( ph /\ x e. I ) -> ( z e. I |-> if ( z = x , 1 , 0 ) ) e. D ) |
326 |
72
|
adantr |
|- ( ( ph /\ x e. I ) -> ( 1r ` R ) e. ( Base ` R ) ) |
327 |
1 2 3 26 4 5 6 7 8 9 315 316 320 321 322 25 325 326
|
evlslem3 |
|- ( ( ph /\ x e. I ) -> ( E ` ( y e. D |-> if ( y = ( z e. I |-> if ( z = x , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( ( F ` ( 1r ` R ) ) .x. ( T gsum ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) ) ) ) |
328 |
86
|
adantr |
|- ( ( ph /\ x e. I ) -> ( F ` ( 1r ` R ) ) = ( 1r ` S ) ) |
329 |
|
1nn0 |
|- 1 e. NN0 |
330 |
|
0nn0 |
|- 0 e. NN0 |
331 |
329 330
|
ifcli |
|- if ( z = x , 1 , 0 ) e. NN0 |
332 |
331
|
a1i |
|- ( ( ph /\ z e. I ) -> if ( z = x , 1 , 0 ) e. NN0 ) |
333 |
14
|
ffvelcdmda |
|- ( ( ph /\ z e. I ) -> ( G ` z ) e. C ) |
334 |
|
eqidd |
|- ( ph -> ( z e. I |-> if ( z = x , 1 , 0 ) ) = ( z e. I |-> if ( z = x , 1 , 0 ) ) ) |
335 |
14
|
feqmptd |
|- ( ph -> G = ( z e. I |-> ( G ` z ) ) ) |
336 |
10 332 333 334 335
|
offval2 |
|- ( ph -> ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) = ( z e. I |-> ( if ( z = x , 1 , 0 ) .^ ( G ` z ) ) ) ) |
337 |
|
oveq1 |
|- ( 1 = if ( z = x , 1 , 0 ) -> ( 1 .^ ( G ` z ) ) = ( if ( z = x , 1 , 0 ) .^ ( G ` z ) ) ) |
338 |
337
|
eqeq1d |
|- ( 1 = if ( z = x , 1 , 0 ) -> ( ( 1 .^ ( G ` z ) ) = if ( z = x , ( G ` z ) , ( 1r ` S ) ) <-> ( if ( z = x , 1 , 0 ) .^ ( G ` z ) ) = if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) ) |
339 |
|
oveq1 |
|- ( 0 = if ( z = x , 1 , 0 ) -> ( 0 .^ ( G ` z ) ) = ( if ( z = x , 1 , 0 ) .^ ( G ` z ) ) ) |
340 |
339
|
eqeq1d |
|- ( 0 = if ( z = x , 1 , 0 ) -> ( ( 0 .^ ( G ` z ) ) = if ( z = x , ( G ` z ) , ( 1r ` S ) ) <-> ( if ( z = x , 1 , 0 ) .^ ( G ` z ) ) = if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) ) |
341 |
333
|
adantr |
|- ( ( ( ph /\ z e. I ) /\ z = x ) -> ( G ` z ) e. C ) |
342 |
47 6
|
mulg1 |
|- ( ( G ` z ) e. C -> ( 1 .^ ( G ` z ) ) = ( G ` z ) ) |
343 |
341 342
|
syl |
|- ( ( ( ph /\ z e. I ) /\ z = x ) -> ( 1 .^ ( G ` z ) ) = ( G ` z ) ) |
344 |
|
iftrue |
|- ( z = x -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) = ( G ` z ) ) |
345 |
344
|
adantl |
|- ( ( ( ph /\ z e. I ) /\ z = x ) -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) = ( G ` z ) ) |
346 |
343 345
|
eqtr4d |
|- ( ( ( ph /\ z e. I ) /\ z = x ) -> ( 1 .^ ( G ` z ) ) = if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) |
347 |
47 48 6
|
mulg0 |
|- ( ( G ` z ) e. C -> ( 0 .^ ( G ` z ) ) = ( 1r ` S ) ) |
348 |
333 347
|
syl |
|- ( ( ph /\ z e. I ) -> ( 0 .^ ( G ` z ) ) = ( 1r ` S ) ) |
349 |
348
|
adantr |
|- ( ( ( ph /\ z e. I ) /\ -. z = x ) -> ( 0 .^ ( G ` z ) ) = ( 1r ` S ) ) |
350 |
|
iffalse |
|- ( -. z = x -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) = ( 1r ` S ) ) |
351 |
350
|
adantl |
|- ( ( ( ph /\ z e. I ) /\ -. z = x ) -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) = ( 1r ` S ) ) |
352 |
349 351
|
eqtr4d |
|- ( ( ( ph /\ z e. I ) /\ -. z = x ) -> ( 0 .^ ( G ` z ) ) = if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) |
353 |
338 340 346 352
|
ifbothda |
|- ( ( ph /\ z e. I ) -> ( if ( z = x , 1 , 0 ) .^ ( G ` z ) ) = if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) |
354 |
353
|
mpteq2dva |
|- ( ph -> ( z e. I |-> ( if ( z = x , 1 , 0 ) .^ ( G ` z ) ) ) = ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) ) |
355 |
336 354
|
eqtrd |
|- ( ph -> ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) = ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) ) |
356 |
355
|
adantr |
|- ( ( ph /\ x e. I ) -> ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) = ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) ) |
357 |
356
|
oveq2d |
|- ( ( ph /\ x e. I ) -> ( T gsum ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) ) = ( T gsum ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) ) ) |
358 |
56
|
adantr |
|- ( ( ph /\ x e. I ) -> T e. Mnd ) |
359 |
333
|
adantlr |
|- ( ( ( ph /\ x e. I ) /\ z e. I ) -> ( G ` z ) e. C ) |
360 |
3 17
|
ringidcl |
|- ( S e. Ring -> ( 1r ` S ) e. C ) |
361 |
21 360
|
syl |
|- ( ph -> ( 1r ` S ) e. C ) |
362 |
361
|
ad2antrr |
|- ( ( ( ph /\ x e. I ) /\ z e. I ) -> ( 1r ` S ) e. C ) |
363 |
359 362
|
ifcld |
|- ( ( ( ph /\ x e. I ) /\ z e. I ) -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) e. C ) |
364 |
363
|
fmpttd |
|- ( ( ph /\ x e. I ) -> ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) : I --> C ) |
365 |
|
eldifsnneq |
|- ( z e. ( I \ { x } ) -> -. z = x ) |
366 |
365 350
|
syl |
|- ( z e. ( I \ { x } ) -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) = ( 1r ` S ) ) |
367 |
366
|
adantl |
|- ( ( ( ph /\ x e. I ) /\ z e. ( I \ { x } ) ) -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) = ( 1r ` S ) ) |
368 |
367 315
|
suppss2 |
|- ( ( ph /\ x e. I ) -> ( ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) supp ( 1r ` S ) ) C_ { x } ) |
369 |
47 48 358 315 317 364 368
|
gsumpt |
|- ( ( ph /\ x e. I ) -> ( T gsum ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) ) = ( ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) ` x ) ) |
370 |
|
fveq2 |
|- ( z = x -> ( G ` z ) = ( G ` x ) ) |
371 |
344 370
|
eqtrd |
|- ( z = x -> if ( z = x , ( G ` z ) , ( 1r ` S ) ) = ( G ` x ) ) |
372 |
|
eqid |
|- ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) = ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) |
373 |
|
fvex |
|- ( G ` x ) e. _V |
374 |
371 372 373
|
fvmpt |
|- ( x e. I -> ( ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) ` x ) = ( G ` x ) ) |
375 |
374
|
adantl |
|- ( ( ph /\ x e. I ) -> ( ( z e. I |-> if ( z = x , ( G ` z ) , ( 1r ` S ) ) ) ` x ) = ( G ` x ) ) |
376 |
357 369 375
|
3eqtrd |
|- ( ( ph /\ x e. I ) -> ( T gsum ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) ) = ( G ` x ) ) |
377 |
328 376
|
oveq12d |
|- ( ( ph /\ x e. I ) -> ( ( F ` ( 1r ` R ) ) .x. ( T gsum ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) ) ) = ( ( 1r ` S ) .x. ( G ` x ) ) ) |
378 |
3 7 17
|
ringlidm |
|- ( ( S e. Ring /\ ( G ` x ) e. C ) -> ( ( 1r ` S ) .x. ( G ` x ) ) = ( G ` x ) ) |
379 |
21 46 378
|
syl2an2r |
|- ( ( ph /\ x e. I ) -> ( ( 1r ` S ) .x. ( G ` x ) ) = ( G ` x ) ) |
380 |
377 379
|
eqtrd |
|- ( ( ph /\ x e. I ) -> ( ( F ` ( 1r ` R ) ) .x. ( T gsum ( ( z e. I |-> if ( z = x , 1 , 0 ) ) oF .^ G ) ) ) = ( G ` x ) ) |
381 |
319 327 380
|
3eqtrd |
|- ( ( ph /\ x e. I ) -> ( E ` ( V ` x ) ) = ( G ` x ) ) |
382 |
314 381
|
eqtrd |
|- ( ( ph /\ x e. I ) -> ( ( E o. V ) ` x ) = ( G ` x ) ) |
383 |
312 246 382
|
eqfnfvd |
|- ( ph -> ( E o. V ) = G ) |
384 |
293 307 383
|
3jca |
|- ( ph -> ( E e. ( P RingHom S ) /\ ( E o. A ) = F /\ ( E o. V ) = G ) ) |