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

Metamath Proof Explorer

Theorem rhmply1mon

Description: Apply a ring homomorphism between two univariate polynomial algebras to a scaled monomial, as in ply1coe . (Contributed by SN, 20-May-2025)

Ref Expression
Hypotheses rhmply1mon.p 
|- P = ( Poly1 ` R )
rhmply1mon.q 
|- Q = ( Poly1 ` S )
rhmply1mon.b 
|- B = ( Base ` P )
rhmply1mon.k 
|- K = ( Base ` R )
rhmply1mon.f 
|- F = ( p e. B |-> ( H o. p ) )
rhmply1mon.x 
|- X = ( var1 ` R )
rhmply1mon.y 
|- Y = ( var1 ` S )
rhmply1mon.t 
|- .x. = ( .s ` P )
rhmply1mon.u 
|- .xb = ( .s ` Q )
rhmply1mon.m 
|- M = ( mulGrp ` P )
rhmply1mon.n 
|- N = ( mulGrp ` Q )
rhmply1mon.l 
|- .^ = ( .g ` M )
rhmply1mon.w 
|- ./\ = ( .g ` N )
rhmply1mon.h 
|- ( ph -> H e. ( R RingHom S ) )
rhmply1mon.c 
|- ( ph -> C e. K )
rhmply1mon.e 
|- ( ph -> E e. NN0 )
Assertion rhmply1mon 
|- ( ph -> ( F ` ( C .x. ( E .^ X ) ) ) = ( ( H ` C ) .xb ( E ./\ Y ) ) )

Proof

Step Hyp Ref Expression
1 rhmply1mon.p 
 |-  P = ( Poly1 ` R )
2 rhmply1mon.q 
 |-  Q = ( Poly1 ` S )
3 rhmply1mon.b 
 |-  B = ( Base ` P )
4 rhmply1mon.k 
 |-  K = ( Base ` R )
5 rhmply1mon.f 
 |-  F = ( p e. B |-> ( H o. p ) )
6 rhmply1mon.x 
 |-  X = ( var1 ` R )
7 rhmply1mon.y 
 |-  Y = ( var1 ` S )
8 rhmply1mon.t 
 |-  .x. = ( .s ` P )
9 rhmply1mon.u 
 |-  .xb = ( .s ` Q )
10 rhmply1mon.m 
 |-  M = ( mulGrp ` P )
11 rhmply1mon.n 
 |-  N = ( mulGrp ` Q )
12 rhmply1mon.l 
 |-  .^ = ( .g ` M )
13 rhmply1mon.w 
 |-  ./\ = ( .g ` N )
14 rhmply1mon.h 
 |-  ( ph -> H e. ( R RingHom S ) )
15 rhmply1mon.c 
 |-  ( ph -> C e. K )
16 rhmply1mon.e 
 |-  ( ph -> E e. NN0 )
17 10 3 mgpbas 
 |-  B = ( Base ` M )
18 rhmrcl1 
 |-  ( H e. ( R RingHom S ) -> R e. Ring )
19 14 18 syl 
 |-  ( ph -> R e. Ring )
20 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
21 19 20 syl 
 |-  ( ph -> P e. Ring )
22 10 ringmgp 
 |-  ( P e. Ring -> M e. Mnd )
23 21 22 syl 
 |-  ( ph -> M e. Mnd )
24 6 1 3 vr1cl 
 |-  ( R e. Ring -> X e. B )
25 19 24 syl 
 |-  ( ph -> X e. B )
26 17 12 23 16 25 mulgnn0cld 
 |-  ( ph -> ( E .^ X ) e. B )
27 1 2 3 4 5 8 9 14 15 26 rhmply1vsca 
 |-  ( ph -> ( F ` ( C .x. ( E .^ X ) ) ) = ( ( H ` C ) .xb ( F ` ( E .^ X ) ) ) )
28 1 2 3 5 14 rhmply1 
 |-  ( ph -> F e. ( P RingHom Q ) )
29 10 11 rhmmhm 
 |-  ( F e. ( P RingHom Q ) -> F e. ( M MndHom N ) )
30 28 29 syl 
 |-  ( ph -> F e. ( M MndHom N ) )
31 17 12 13 mhmmulg 
 |-  ( ( F e. ( M MndHom N ) /\ E e. NN0 /\ X e. B ) -> ( F ` ( E .^ X ) ) = ( E ./\ ( F ` X ) ) )
32 30 16 25 31 syl3anc 
 |-  ( ph -> ( F ` ( E .^ X ) ) = ( E ./\ ( F ` X ) ) )
33 1 2 3 5 6 7 14 rhmply1vr1 
 |-  ( ph -> ( F ` X ) = Y )
34 33 oveq2d 
 |-  ( ph -> ( E ./\ ( F ` X ) ) = ( E ./\ Y ) )
35 32 34 eqtrd 
 |-  ( ph -> ( F ` ( E .^ X ) ) = ( E ./\ Y ) )
36 35 oveq2d 
 |-  ( ph -> ( ( H ` C ) .xb ( F ` ( E .^ X ) ) ) = ( ( H ` C ) .xb ( E ./\ Y ) ) )
37 27 36 eqtrd 
 |-  ( ph -> ( F ` ( C .x. ( E .^ X ) ) ) = ( ( H ` C ) .xb ( E ./\ Y ) ) )