let F be Field; :: thesis: for p, r being Polynomial of F
for q being non zero Polynomial of F holds (p *' r) mod q = ((p mod q) *' (r mod q)) mod q
let p, r be Polynomial of F; :: thesis: for q being non zero Polynomial of F holds (p *' r) mod q = ((p mod q) *' (r mod q)) mod q
let q be non zero Polynomial of F; :: thesis: (p *' r) mod q = ((p mod q) *' (r mod q)) mod q
H1: (((p div q) *' q) *' ((r div q) *' q)) + (((p div q) *' q) *' (r mod q)) = ((((p div q) *' q) *' (r div q)) *' q) + (((p div q) *' q) *' (r mod q)) by POLYNOM3:33
.= (q *' (((p div q) *' q) *' (r div q))) + (q *' ((p div q) *' (r mod q))) by POLYNOM3:33
.= q *' ((((p div q) *' q) *' (r div q)) + ((p div q) *' (r mod q))) by POLYNOM3:31 ;
H2: (p mod q) *' ((r div q) *' q) = q *' ((p mod q) *' (r div q)) by POLYNOM3:33;
p *' r = (((p div q) *' q) + (p mod q)) *' r by div5
.= (((p div q) *' q) + (p mod q)) *' (((r div q) *' q) + (r mod q)) by div5
.= (((p div q) *' q) *' (((r div q) *' q) + (r mod q))) + ((p mod q) *' (((r div q) *' q) + (r mod q))) by POLYNOM3:31
.= ((((p div q) *' q) *' ((r div q) *' q)) + (((p div q) *' q) *' (r mod q))) + ((p mod q) *' (((r div q) *' q) + (r mod q))) by POLYNOM3:31
.= ((((p div q) *' q) *' ((r div q) *' q)) + (((p div q) *' q) *' (r mod q))) + (((p mod q) *' ((r div q) *' q)) + ((p mod q) *' (r mod q))) by POLYNOM3:31 ;
hence (p *' r) mod q = (((((p div q) *' q) *' ((r div q) *' q)) + (((p div q) *' q) *' (r mod q))) mod q) + ((((p mod q) *' ((r div q) *' q)) + ((p mod q) *' (r mod q))) mod q) by div4
.= (0_. F) + ((((p mod q) *' ((r div q) *' q)) + ((p mod q) *' (r mod q))) mod q) by div2, H1, T2
.= (((p mod q) *' ((r div q) *' q)) + ((p mod q) *' (r mod q))) mod q by POLYNOM3:28
.= (((p mod q) *' ((r div q) *' q)) mod q) + (((p mod q) *' (r mod q)) mod q) by div4
.= (0_. F) + (((p mod q) *' (r mod q)) mod q) by div2, H2, T2
.= ((p mod q) *' (r mod q)) mod q by POLYNOM3:28 ;
:: thesis: verum