Metamath Proof Explorer

Theorem gsumply1subr

Description: Evaluate a group sum in a polynomial ring over a subring. (Contributed by AV, 22-Sep-2019) (Proof shortened by AV, 31-Jan-2020)

Ref Expression
Hypotheses subrgply1.s 
|- S = ( Poly1 ` R )
subrgply1.h 
|- H = ( R |`s T )
subrgply1.u 
|- U = ( Poly1 ` H )
subrgply1.b 
|- B = ( Base ` U )
gsumply1subr.s 
|- ( ph -> T e. ( SubRing ` R ) )
gsumply1subr.a 
|- ( ph -> A e. V )
gsumply1subr.f 
|- ( ph -> F : A --> B )
Assertion gsumply1subr 
|- ( ph -> ( S gsum F ) = ( U gsum F ) )

Proof

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 fex 
 |-  ( ( F : A --> B /\ A e. V ) -> F e. _V )
16 7 6 15 syl2anc 
 |-  ( ph -> F e. _V )
17 ovexd 
 |-  ( ph -> ( S |`s B ) e. _V )
18 3 fvexi 
 |-  U e. _V
19 18 a1i 
 |-  ( ph -> U e. _V )
20 eqid 
 |-  ( Base ` U ) = ( Base ` U )
21 4 oveq2i 
 |-  ( S |`s B ) = ( S |`s ( Base ` U ) )
22 1 2 3 20 5 21 ressply1bas 
 |-  ( ph -> ( Base ` U ) = ( Base ` ( S |`s B ) ) )
23 22 eqcomd 
 |-  ( ph -> ( Base ` ( S |`s B ) ) = ( Base ` U ) )
24 13 subrgring 
 |-  ( B e. ( SubRing ` S ) -> ( S |`s B ) e. Ring )
25 8 24 syl 
 |-  ( T e. ( SubRing ` R ) -> ( S |`s B ) e. Ring )
26 ringmgm 
 |-  ( ( S |`s B ) e. Ring -> ( S |`s B ) e. Mgm )
27 5 25 26 3syl 
 |-  ( ph -> ( S |`s B ) e. Mgm )
28 simpl 
 |-  ( ( ph /\ ( s e. ( Base ` ( S |`s B ) ) /\ t e. ( Base ` ( S |`s B ) ) ) ) -> ph )
29 1 2 3 4 5 13 ressply1bas 
 |-  ( ph -> B = ( Base ` ( S |`s B ) ) )
30 29 eqcomd 
 |-  ( ph -> ( Base ` ( S |`s B ) ) = B )
31 30 eleq2d 
 |-  ( ph -> ( s e. ( Base ` ( S |`s B ) ) <-> s e. B ) )
32 31 biimpcd 
 |-  ( s e. ( Base ` ( S |`s B ) ) -> ( ph -> s e. B ) )
33 32 adantr 
 |-  ( ( s e. ( Base ` ( S |`s B ) ) /\ t e. ( Base ` ( S |`s B ) ) ) -> ( ph -> s e. B ) )
34 33 impcom 
 |-  ( ( ph /\ ( s e. ( Base ` ( S |`s B ) ) /\ t e. ( Base ` ( S |`s B ) ) ) ) -> s e. B )
35 30 eleq2d 
 |-  ( ph -> ( t e. ( Base ` ( S |`s B ) ) <-> t e. B ) )
36 35 biimpcd 
 |-  ( t e. ( Base ` ( S |`s B ) ) -> ( ph -> t e. B ) )
37 36 adantl 
 |-  ( ( s e. ( Base ` ( S |`s B ) ) /\ t e. ( Base ` ( S |`s B ) ) ) -> ( ph -> t e. B ) )
38 37 impcom 
 |-  ( ( ph /\ ( s e. ( Base ` ( S |`s B ) ) /\ t e. ( Base ` ( S |`s B ) ) ) ) -> t e. B )
39 1 2 3 4 5 13 ressply1add 
 |-  ( ( ph /\ ( s e. B /\ t e. B ) ) -> ( s ( +g ` U ) t ) = ( s ( +g ` ( S |`s B ) ) t ) )
40 28 34 38 39 syl12anc 
 |-  ( ( ph /\ ( s e. ( Base ` ( S |`s B ) ) /\ t e. ( Base ` ( S |`s B ) ) ) ) -> ( s ( +g ` U ) t ) = ( s ( +g ` ( S |`s B ) ) t ) )
41 40 eqcomd 
 |-  ( ( ph /\ ( s e. ( Base ` ( S |`s B ) ) /\ t e. ( Base ` ( S |`s B ) ) ) ) -> ( s ( +g ` ( S |`s B ) ) t ) = ( s ( +g ` U ) t ) )
42 7 ffund 
 |-  ( ph -> Fun F )
43 7 frnd 
 |-  ( ph -> ran F C_ B )
44 43 29 sseqtrd 
 |-  ( ph -> ran F C_ ( Base ` ( S |`s B ) ) )
45 16 17 19 23 27 41 42 44 gsummgmpropd 
 |-  ( ph -> ( ( S |`s B ) gsum F ) = ( U gsum F ) )
46 14 45 eqtrd 
 |-  ( ph -> ( S gsum F ) = ( U gsum F ) )