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 𝑆 = ( Poly1𝑅 )
subrgply1.h 𝐻 = ( 𝑅s 𝑇 )
subrgply1.u 𝑈 = ( Poly1𝐻 )
subrgply1.b 𝐵 = ( Base ‘ 𝑈 )
gsumply1subr.s ( 𝜑𝑇 ∈ ( SubRing ‘ 𝑅 ) )
gsumply1subr.a ( 𝜑𝐴𝑉 )
gsumply1subr.f ( 𝜑𝐹 : 𝐴𝐵 )
Assertion gsumply1subr ( 𝜑 → ( 𝑆 Σg 𝐹 ) = ( 𝑈 Σg 𝐹 ) )

Proof

Step Hyp Ref Expression
1 subrgply1.s 𝑆 = ( Poly1𝑅 )
2 subrgply1.h 𝐻 = ( 𝑅s 𝑇 )
3 subrgply1.u 𝑈 = ( Poly1𝐻 )
4 subrgply1.b 𝐵 = ( Base ‘ 𝑈 )
5 gsumply1subr.s ( 𝜑𝑇 ∈ ( SubRing ‘ 𝑅 ) )
6 gsumply1subr.a ( 𝜑𝐴𝑉 )
7 gsumply1subr.f ( 𝜑𝐹 : 𝐴𝐵 )
8 1 2 3 4 subrgply1 ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )
9 subrgsubg ( 𝐵 ∈ ( SubRing ‘ 𝑆 ) → 𝐵 ∈ ( SubGrp ‘ 𝑆 ) )
10 subgsubm ( 𝐵 ∈ ( SubGrp ‘ 𝑆 ) → 𝐵 ∈ ( SubMnd ‘ 𝑆 ) )
11 5 8 9 10 4syl ( 𝜑𝐵 ∈ ( SubMnd ‘ 𝑆 ) )
12 eqid ( 𝑆s 𝐵 ) = ( 𝑆s 𝐵 )
13 6 11 7 12 gsumsubm ( 𝜑 → ( 𝑆 Σg 𝐹 ) = ( ( 𝑆s 𝐵 ) Σg 𝐹 ) )
14 7 6 fexd ( 𝜑𝐹 ∈ V )
15 ovexd ( 𝜑 → ( 𝑆s 𝐵 ) ∈ V )
16 3 fvexi 𝑈 ∈ V
17 16 a1i ( 𝜑𝑈 ∈ V )
18 eqid ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
19 4 oveq2i ( 𝑆s 𝐵 ) = ( 𝑆s ( Base ‘ 𝑈 ) )
20 1 2 3 18 5 19 ressply1bas ( 𝜑 → ( Base ‘ 𝑈 ) = ( Base ‘ ( 𝑆s 𝐵 ) ) )
21 20 eqcomd ( 𝜑 → ( Base ‘ ( 𝑆s 𝐵 ) ) = ( Base ‘ 𝑈 ) )
22 12 subrgring ( 𝐵 ∈ ( SubRing ‘ 𝑆 ) → ( 𝑆s 𝐵 ) ∈ Ring )
23 ringmgm ( ( 𝑆s 𝐵 ) ∈ Ring → ( 𝑆s 𝐵 ) ∈ Mgm )
24 5 8 22 23 4syl ( 𝜑 → ( 𝑆s 𝐵 ) ∈ Mgm )
25 simpl ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ ( 𝑆s 𝐵 ) ) ∧ 𝑡 ∈ ( Base ‘ ( 𝑆s 𝐵 ) ) ) ) → 𝜑 )
26 1 2 3 4 5 12 ressply1bas ( 𝜑𝐵 = ( Base ‘ ( 𝑆s 𝐵 ) ) )
27 26 eqcomd ( 𝜑 → ( Base ‘ ( 𝑆s 𝐵 ) ) = 𝐵 )
28 27 eleq2d ( 𝜑 → ( 𝑠 ∈ ( Base ‘ ( 𝑆s 𝐵 ) ) ↔ 𝑠𝐵 ) )
29 28 biimpcd ( 𝑠 ∈ ( Base ‘ ( 𝑆s 𝐵 ) ) → ( 𝜑𝑠𝐵 ) )
30 29 adantr ( ( 𝑠 ∈ ( Base ‘ ( 𝑆s 𝐵 ) ) ∧ 𝑡 ∈ ( Base ‘ ( 𝑆s 𝐵 ) ) ) → ( 𝜑𝑠𝐵 ) )
31 30 impcom ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ ( 𝑆s 𝐵 ) ) ∧ 𝑡 ∈ ( Base ‘ ( 𝑆s 𝐵 ) ) ) ) → 𝑠𝐵 )
32 27 eleq2d ( 𝜑 → ( 𝑡 ∈ ( Base ‘ ( 𝑆s 𝐵 ) ) ↔ 𝑡𝐵 ) )
33 32 biimpcd ( 𝑡 ∈ ( Base ‘ ( 𝑆s 𝐵 ) ) → ( 𝜑𝑡𝐵 ) )
34 33 adantl ( ( 𝑠 ∈ ( Base ‘ ( 𝑆s 𝐵 ) ) ∧ 𝑡 ∈ ( Base ‘ ( 𝑆s 𝐵 ) ) ) → ( 𝜑𝑡𝐵 ) )
35 34 impcom ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ ( 𝑆s 𝐵 ) ) ∧ 𝑡 ∈ ( Base ‘ ( 𝑆s 𝐵 ) ) ) ) → 𝑡𝐵 )
36 1 2 3 4 5 12 ressply1add ( ( 𝜑 ∧ ( 𝑠𝐵𝑡𝐵 ) ) → ( 𝑠 ( +g𝑈 ) 𝑡 ) = ( 𝑠 ( +g ‘ ( 𝑆s 𝐵 ) ) 𝑡 ) )
37 25 31 35 36 syl12anc ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ ( 𝑆s 𝐵 ) ) ∧ 𝑡 ∈ ( Base ‘ ( 𝑆s 𝐵 ) ) ) ) → ( 𝑠 ( +g𝑈 ) 𝑡 ) = ( 𝑠 ( +g ‘ ( 𝑆s 𝐵 ) ) 𝑡 ) )
38 37 eqcomd ( ( 𝜑 ∧ ( 𝑠 ∈ ( Base ‘ ( 𝑆s 𝐵 ) ) ∧ 𝑡 ∈ ( Base ‘ ( 𝑆s 𝐵 ) ) ) ) → ( 𝑠 ( +g ‘ ( 𝑆s 𝐵 ) ) 𝑡 ) = ( 𝑠 ( +g𝑈 ) 𝑡 ) )
39 7 ffund ( 𝜑 → Fun 𝐹 )
40 7 frnd ( 𝜑 → ran 𝐹𝐵 )
41 40 26 sseqtrd ( 𝜑 → ran 𝐹 ⊆ ( Base ‘ ( 𝑆s 𝐵 ) ) )
42 14 15 17 21 24 38 39 41 gsummgmpropd ( 𝜑 → ( ( 𝑆s 𝐵 ) Σg 𝐹 ) = ( 𝑈 Σg 𝐹 ) )
43 13 42 eqtrd ( 𝜑 → ( 𝑆 Σg 𝐹 ) = ( 𝑈 Σg 𝐹 ) )