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 𝐹 ) )