This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mplmapghm

Description: The function H mapping polynomials p to their coefficient given a bag of variables F is a group homomorphism. (Contributed by SN, 15-Mar-2025)

Ref Expression
Hypotheses mplmapghm.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mplmapghm.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
mplmapghm.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
mplmapghm.h ⊢ 𝐻 = ( 𝑝 ∈ 𝐵 ↦ ( 𝑝 ‘ 𝐹 ) )
mplmapghm.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
mplmapghm.r ⊢ ( 𝜑 → 𝑅 ∈ Grp )
mplmapghm.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
Assertion mplmapghm ( 𝜑 → 𝐻 ∈ ( 𝑃 GrpHom 𝑅 ) )

Proof

Step Hyp Ref Expression
1 mplmapghm.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 mplmapghm.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 mplmapghm.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
4 mplmapghm.h ⊢ 𝐻 = ( 𝑝 ∈ 𝐵 ↦ ( 𝑝 ‘ 𝐹 ) )
5 mplmapghm.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6 mplmapghm.r ⊢ ( 𝜑 → 𝑅 ∈ Grp )
7 mplmapghm.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
10 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
11 1 mplgrp ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Grp ) → 𝑃 ∈ Grp )
12 5 6 11 syl2anc ⊢ ( 𝜑 → 𝑃 ∈ Grp )
13 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝑝 ∈ 𝐵 )
14 1 8 2 3 13 mplelf ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝑝 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
15 7 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝐹 ∈ 𝐷 )
16 14 15 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 ‘ 𝐹 ) ∈ ( Base ‘ 𝑅 ) )
17 16 4 fmptd ⊢ ( 𝜑 → 𝐻 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
18 simprl ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑞 ∈ 𝐵 )
19 simprr ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑟 ∈ 𝐵 )
20 1 2 10 9 18 19 mpladd ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) = ( 𝑞 ∘f ( +g ‘ 𝑅 ) 𝑟 ) )
21 20 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ‘ 𝐹 ) = ( ( 𝑞 ∘f ( +g ‘ 𝑅 ) 𝑟 ) ‘ 𝐹 ) )
22 1 8 2 3 18 mplelf ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑞 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
23 22 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑞 Fn 𝐷 )
24 1 8 2 3 19 mplelf ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑟 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
25 24 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑟 Fn 𝐷 )
26 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
27 3 26 rabex2 ⊢ 𝐷 ∈ V
28 27 a1i ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝐷 ∈ V )
29 inidm ⊢ ( 𝐷 ∩ 𝐷 ) = 𝐷
30 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ 𝐹 ∈ 𝐷 ) → ( 𝑞 ‘ 𝐹 ) = ( 𝑞 ‘ 𝐹 ) )
31 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ 𝐹 ∈ 𝐷 ) → ( 𝑟 ‘ 𝐹 ) = ( 𝑟 ‘ 𝐹 ) )
32 23 25 28 28 29 30 31 ofval ⊢ ( ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) ∧ 𝐹 ∈ 𝐷 ) → ( ( 𝑞 ∘f ( +g ‘ 𝑅 ) 𝑟 ) ‘ 𝐹 ) = ( ( 𝑞 ‘ 𝐹 ) ( +g ‘ 𝑅 ) ( 𝑟 ‘ 𝐹 ) ) )
33 7 32 mpidan ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝑞 ∘f ( +g ‘ 𝑅 ) 𝑟 ) ‘ 𝐹 ) = ( ( 𝑞 ‘ 𝐹 ) ( +g ‘ 𝑅 ) ( 𝑟 ‘ 𝐹 ) ) )
34 21 33 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ‘ 𝐹 ) = ( ( 𝑞 ‘ 𝐹 ) ( +g ‘ 𝑅 ) ( 𝑟 ‘ 𝐹 ) ) )
35 fveq1 ⊢ ( 𝑝 = ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) → ( 𝑝 ‘ 𝐹 ) = ( ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ‘ 𝐹 ) )
36 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑃 ∈ Grp )
37 2 9 36 18 19 grpcld ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ∈ 𝐵 )
38 fvexd ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ‘ 𝐹 ) ∈ V )
39 4 35 37 38 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝐻 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) = ( ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ‘ 𝐹 ) )
40 fveq1 ⊢ ( 𝑝 = 𝑞 → ( 𝑝 ‘ 𝐹 ) = ( 𝑞 ‘ 𝐹 ) )
41 fvexd ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝑞 ‘ 𝐹 ) ∈ V )
42 4 40 18 41 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝐻 ‘ 𝑞 ) = ( 𝑞 ‘ 𝐹 ) )
43 fveq1 ⊢ ( 𝑝 = 𝑟 → ( 𝑝 ‘ 𝐹 ) = ( 𝑟 ‘ 𝐹 ) )
44 fvexd ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝑟 ‘ 𝐹 ) ∈ V )
45 4 43 19 44 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝐻 ‘ 𝑟 ) = ( 𝑟 ‘ 𝐹 ) )
46 42 45 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝐻 ‘ 𝑞 ) ( +g ‘ 𝑅 ) ( 𝐻 ‘ 𝑟 ) ) = ( ( 𝑞 ‘ 𝐹 ) ( +g ‘ 𝑅 ) ( 𝑟 ‘ 𝐹 ) ) )
47 34 39 46 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝐻 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) = ( ( 𝐻 ‘ 𝑞 ) ( +g ‘ 𝑅 ) ( 𝐻 ‘ 𝑟 ) ) )
48 2 8 9 10 12 6 17 47 isghmd ⊢ ( 𝜑 → 𝐻 ∈ ( 𝑃 GrpHom 𝑅 ) )