set R = F;

set RX = Polynom-Ring F;

set f = canHomP p;

set B = Polynom-Ring p;

.= 1_. F by RING_4:14

.= 1_ (Polynom-Ring p) by RING_4:def 8 ; :: according to GROUP_1:def 13 :: thesis: canHomP p is one-to-one

set RX = Polynom-Ring F;

set f = canHomP p;

set B = Polynom-Ring p;

hereby :: according to VECTSP_1:def 19 :: thesis: ( canHomP p is multiplicative & canHomP p is unity-preserving & canHomP p is one-to-one )

let x, y be Element of F; :: thesis: ((canHomP p) . x) + ((canHomP p) . y) = (canHomP p) . (x + y)

B: ( (canHomP p) . x = x | F & (canHomP p) . y = y | F ) by defch;

A: [((canHomP p) . x),((canHomP p) . y)] in [: the carrier of (Polynom-Ring p), the carrier of (Polynom-Ring p):] by ZFMISC_1:def 2;

reconsider fx = (canHomP p) . x, fy = (canHomP p) . y as Element of the carrier of (Polynom-Ring F) by B, POLYNOM3:def 10;

thus ((canHomP p) . x) + ((canHomP p) . y) = ( the addF of (Polynom-Ring F) || the carrier of (Polynom-Ring p)) . (((canHomP p) . x),((canHomP p) . y)) by RING_4:def 8

.= fx + fy by A, FUNCT_1:49

.= (x | F) + (y | F) by B, POLYNOM3:def 10

.= (x + y) | F by RING_4:17

.= (canHomP p) . (x + y) by defch ; :: thesis: verum

end;B: ( (canHomP p) . x = x | F & (canHomP p) . y = y | F ) by defch;

A: [((canHomP p) . x),((canHomP p) . y)] in [: the carrier of (Polynom-Ring p), the carrier of (Polynom-Ring p):] by ZFMISC_1:def 2;

reconsider fx = (canHomP p) . x, fy = (canHomP p) . y as Element of the carrier of (Polynom-Ring F) by B, POLYNOM3:def 10;

thus ((canHomP p) . x) + ((canHomP p) . y) = ( the addF of (Polynom-Ring F) || the carrier of (Polynom-Ring p)) . (((canHomP p) . x),((canHomP p) . y)) by RING_4:def 8

.= fx + fy by A, FUNCT_1:49

.= (x | F) + (y | F) by B, POLYNOM3:def 10

.= (x + y) | F by RING_4:17

.= (canHomP p) . (x + y) by defch ; :: thesis: verum

hereby :: according to GROUP_6:def 6 :: thesis: ( canHomP p is unity-preserving & canHomP p is one-to-one )

thus (canHomP p) . (1_ F) =
(1. F) | F
by defch
let x, y be Element of F; :: thesis: ((canHomP p) . x) * ((canHomP p) . y) = (canHomP p) . (x * y)

B: ( (canHomP p) . x = x | F & (canHomP p) . y = y | F ) by defch;

A: [((canHomP p) . x),((canHomP p) . y)] in [: the carrier of (Polynom-Ring p), the carrier of (Polynom-Ring p):] by ZFMISC_1:def 2;

reconsider fx = (canHomP p) . x, fy = (canHomP p) . y as Element of the carrier of (Polynom-Ring F) by B, POLYNOM3:def 10;

reconsider p1 = p as Polynomial of F ;

C: ( deg ((x * y) | F) <= 0 & deg p > 0 ) by RING_4:def 4, RATFUNC1:def 2;

thus ((canHomP p) . x) * ((canHomP p) . y) = ((poly_mult_mod p) || the carrier of (Polynom-Ring p)) . (((canHomP p) . x),((canHomP p) . y)) by RING_4:def 8

.= (poly_mult_mod p) . (fx,fy) by A, FUNCT_1:49

.= ((x | F) *' (y | F)) mod p by B, RING_4:def 7

.= ((x * y) | F) mod p by RING_4:18

.= (x * y) | F by C, RING_4:2

.= (canHomP p) . (x * y) by defch ; :: thesis: verum

end;B: ( (canHomP p) . x = x | F & (canHomP p) . y = y | F ) by defch;

A: [((canHomP p) . x),((canHomP p) . y)] in [: the carrier of (Polynom-Ring p), the carrier of (Polynom-Ring p):] by ZFMISC_1:def 2;

reconsider fx = (canHomP p) . x, fy = (canHomP p) . y as Element of the carrier of (Polynom-Ring F) by B, POLYNOM3:def 10;

reconsider p1 = p as Polynomial of F ;

C: ( deg ((x * y) | F) <= 0 & deg p > 0 ) by RING_4:def 4, RATFUNC1:def 2;

thus ((canHomP p) . x) * ((canHomP p) . y) = ((poly_mult_mod p) || the carrier of (Polynom-Ring p)) . (((canHomP p) . x),((canHomP p) . y)) by RING_4:def 8

.= (poly_mult_mod p) . (fx,fy) by A, FUNCT_1:49

.= ((x | F) *' (y | F)) mod p by B, RING_4:def 7

.= ((x * y) | F) mod p by RING_4:18

.= (x * y) | F by C, RING_4:2

.= (canHomP p) . (x * y) by defch ; :: thesis: verum

.= 1_. F by RING_4:14

.= 1_ (Polynom-Ring p) by RING_4:def 8 ; :: according to GROUP_1:def 13 :: thesis: canHomP p is one-to-one

now :: thesis: for x1, x2 being object st x1 in the carrier of F & x2 in the carrier of F & (canHomP p) . x1 = (canHomP p) . x2 holds

x1 = x2

hence
canHomP p is one-to-one
by FUNCT_2:19; :: thesis: verumx1 = x2

let x1, x2 be object ; :: thesis: ( x1 in the carrier of F & x2 in the carrier of F & (canHomP p) . x1 = (canHomP p) . x2 implies x1 = x2 )

assume AS: ( x1 in the carrier of F & x2 in the carrier of F & (canHomP p) . x1 = (canHomP p) . x2 ) ; :: thesis: x1 = x2

then reconsider a = x1, b = x2 as Element of F ;

a | F = (canHomP p) . x2 by AS, defch

.= b | F by defch ;

hence x1 = x2 by RING_4:19; :: thesis: verum

end;assume AS: ( x1 in the carrier of F & x2 in the carrier of F & (canHomP p) . x1 = (canHomP p) . x2 ) ; :: thesis: x1 = x2

then reconsider a = x1, b = x2 as Element of F ;

a | F = (canHomP p) . x2 by AS, defch

.= b | F by defch ;

hence x1 = x2 by RING_4:19; :: thesis: verum