Step |
Hyp |
Ref |
Expression |
1 |
|
subrgply1.s |
|- S = ( Poly1 ` R ) |
2 |
|
subrgply1.h |
|- H = ( R |`s T ) |
3 |
|
subrgply1.u |
|- U = ( Poly1 ` H ) |
4 |
|
subrgply1.b |
|- B = ( Base ` U ) |
5 |
|
gsumply1subr.s |
|- ( ph -> T e. ( SubRing ` R ) ) |
6 |
|
gsumply1subr.a |
|- ( ph -> A e. V ) |
7 |
|
gsumply1subr.f |
|- ( ph -> F : A --> B ) |
8 |
1 2 3 4
|
subrgply1 |
|- ( T e. ( SubRing ` R ) -> B e. ( SubRing ` S ) ) |
9 |
|
subrgsubg |
|- ( B e. ( SubRing ` S ) -> B e. ( SubGrp ` S ) ) |
10 |
|
subgsubm |
|- ( B e. ( SubGrp ` S ) -> B e. ( SubMnd ` S ) ) |
11 |
9 10
|
syl |
|- ( B e. ( SubRing ` S ) -> B e. ( SubMnd ` S ) ) |
12 |
5 8 11
|
3syl |
|- ( ph -> B e. ( SubMnd ` S ) ) |
13 |
|
eqid |
|- ( S |`s B ) = ( S |`s B ) |
14 |
6 12 7 13
|
gsumsubm |
|- ( ph -> ( S gsum F ) = ( ( S |`s B ) gsum F ) ) |
15 |
7 6
|
fexd |
|- ( ph -> F e. _V ) |
16 |
|
ovexd |
|- ( ph -> ( S |`s B ) e. _V ) |
17 |
3
|
fvexi |
|- U e. _V |
18 |
17
|
a1i |
|- ( ph -> U e. _V ) |
19 |
|
eqid |
|- ( Base ` U ) = ( Base ` U ) |
20 |
4
|
oveq2i |
|- ( S |`s B ) = ( S |`s ( Base ` U ) ) |
21 |
1 2 3 19 5 20
|
ressply1bas |
|- ( ph -> ( Base ` U ) = ( Base ` ( S |`s B ) ) ) |
22 |
21
|
eqcomd |
|- ( ph -> ( Base ` ( S |`s B ) ) = ( Base ` U ) ) |
23 |
13
|
subrgring |
|- ( B e. ( SubRing ` S ) -> ( S |`s B ) e. Ring ) |
24 |
8 23
|
syl |
|- ( T e. ( SubRing ` R ) -> ( S |`s B ) e. Ring ) |
25 |
|
ringmgm |
|- ( ( S |`s B ) e. Ring -> ( S |`s B ) e. Mgm ) |
26 |
5 24 25
|
3syl |
|- ( ph -> ( S |`s B ) e. Mgm ) |
27 |
|
simpl |
|- ( ( ph /\ ( s e. ( Base ` ( S |`s B ) ) /\ t e. ( Base ` ( S |`s B ) ) ) ) -> ph ) |
28 |
1 2 3 4 5 13
|
ressply1bas |
|- ( ph -> B = ( Base ` ( S |`s B ) ) ) |
29 |
28
|
eqcomd |
|- ( ph -> ( Base ` ( S |`s B ) ) = B ) |
30 |
29
|
eleq2d |
|- ( ph -> ( s e. ( Base ` ( S |`s B ) ) <-> s e. B ) ) |
31 |
30
|
biimpcd |
|- ( s e. ( Base ` ( S |`s B ) ) -> ( ph -> s e. B ) ) |
32 |
31
|
adantr |
|- ( ( s e. ( Base ` ( S |`s B ) ) /\ t e. ( Base ` ( S |`s B ) ) ) -> ( ph -> s e. B ) ) |
33 |
32
|
impcom |
|- ( ( ph /\ ( s e. ( Base ` ( S |`s B ) ) /\ t e. ( Base ` ( S |`s B ) ) ) ) -> s e. B ) |
34 |
29
|
eleq2d |
|- ( ph -> ( t e. ( Base ` ( S |`s B ) ) <-> t e. B ) ) |
35 |
34
|
biimpcd |
|- ( t e. ( Base ` ( S |`s B ) ) -> ( ph -> t e. B ) ) |
36 |
35
|
adantl |
|- ( ( s e. ( Base ` ( S |`s B ) ) /\ t e. ( Base ` ( S |`s B ) ) ) -> ( ph -> t e. B ) ) |
37 |
36
|
impcom |
|- ( ( ph /\ ( s e. ( Base ` ( S |`s B ) ) /\ t e. ( Base ` ( S |`s B ) ) ) ) -> t e. B ) |
38 |
1 2 3 4 5 13
|
ressply1add |
|- ( ( ph /\ ( s e. B /\ t e. B ) ) -> ( s ( +g ` U ) t ) = ( s ( +g ` ( S |`s B ) ) t ) ) |
39 |
27 33 37 38
|
syl12anc |
|- ( ( ph /\ ( s e. ( Base ` ( S |`s B ) ) /\ t e. ( Base ` ( S |`s B ) ) ) ) -> ( s ( +g ` U ) t ) = ( s ( +g ` ( S |`s B ) ) t ) ) |
40 |
39
|
eqcomd |
|- ( ( ph /\ ( s e. ( Base ` ( S |`s B ) ) /\ t e. ( Base ` ( S |`s B ) ) ) ) -> ( s ( +g ` ( S |`s B ) ) t ) = ( s ( +g ` U ) t ) ) |
41 |
7
|
ffund |
|- ( ph -> Fun F ) |
42 |
7
|
frnd |
|- ( ph -> ran F C_ B ) |
43 |
42 28
|
sseqtrd |
|- ( ph -> ran F C_ ( Base ` ( S |`s B ) ) ) |
44 |
15 16 18 22 26 40 41 43
|
gsummgmpropd |
|- ( ph -> ( ( S |`s B ) gsum F ) = ( U gsum F ) ) |
45 |
14 44
|
eqtrd |
|- ( ph -> ( S gsum F ) = ( U gsum F ) ) |