let F be commutative Skew-Field; :: thesis: for G being Subgroup of MultGroup F

for n being Nat st 0 < n holds

ex f being Polynomial of F st

( deg f = n & ( for x, xn being Element of F

for xz being Element of G st x = xz & xn = xz |^ n holds

eval (f,x) = xn - (1. F) ) )

let G be Subgroup of MultGroup F; :: thesis: for n being Nat st 0 < n holds

ex f being Polynomial of F st

( deg f = n & ( for x, xn being Element of F

for xz being Element of G st x = xz & xn = xz |^ n holds

eval (f,x) = xn - (1. F) ) )

let n be Nat; :: thesis: ( 0 < n implies ex f being Polynomial of F st

( deg f = n & ( for x, xn being Element of F

for xz being Element of G st x = xz & xn = xz |^ n holds

eval (f,x) = xn - (1. F) ) ) )

reconsider n0 = n as Element of NAT by ORDINAL1:def 12;

set f = (<%(0. F),(1_ F)%> `^ n0) - (1_. F);

( deg f = n & ( for x, xn being Element of F

for xz being Element of G st x = xz & xn = xz |^ n holds

eval (f,x) = xn - (1. F) ) )

then A5: 0 + 1 < n + 1 by XREAL_1:8;

len (1_. F) = 1 by POLYNOM4:4;

then A6: len (- (1_. F)) = 1 by POLYNOM4:8;

len <%(0. F),(1_ F)%> = 2 by POLYNOM5:40;

then len (<%(0. F),(1_ F)%> `^ n0) = ((n * 2) - n) + 1 by POLYNOM5:23

.= n + 1 ;

then len ((<%(0. F),(1_ F)%> `^ n0) - (1_. F)) = max ((n + 1),1) by A5, A6, POLYNOM4:7

.= n + 1 by A5, XXREAL_0:def 10 ;

then deg ((<%(0. F),(1_ F)%> `^ n0) - (1_. F)) = n ;

hence ex f being Polynomial of F st

( deg f = n & ( for x, xn being Element of F

for xz being Element of G st x = xz & xn = xz |^ n holds

eval (f,x) = xn - (1. F) ) ) by A1; :: thesis: verum

for n being Nat st 0 < n holds

ex f being Polynomial of F st

( deg f = n & ( for x, xn being Element of F

for xz being Element of G st x = xz & xn = xz |^ n holds

eval (f,x) = xn - (1. F) ) )

let G be Subgroup of MultGroup F; :: thesis: for n being Nat st 0 < n holds

ex f being Polynomial of F st

( deg f = n & ( for x, xn being Element of F

for xz being Element of G st x = xz & xn = xz |^ n holds

eval (f,x) = xn - (1. F) ) )

let n be Nat; :: thesis: ( 0 < n implies ex f being Polynomial of F st

( deg f = n & ( for x, xn being Element of F

for xz being Element of G st x = xz & xn = xz |^ n holds

eval (f,x) = xn - (1. F) ) ) )

reconsider n0 = n as Element of NAT by ORDINAL1:def 12;

set f = (<%(0. F),(1_ F)%> `^ n0) - (1_. F);

A1: now :: thesis: for x, xn being Element of F

for xz being Element of G st x = xz & xn = xz |^ n holds

eval (((<%(0. F),(1_ F)%> `^ n0) - (1_. F)),x) = xn - (1_ F)

assume
0 < n
; :: thesis: ex f being Polynomial of F st for xz being Element of G st x = xz & xn = xz |^ n holds

eval (((<%(0. F),(1_ F)%> `^ n0) - (1_. F)),x) = xn - (1_ F)

let x, xn be Element of F; :: thesis: for xz being Element of G st x = xz & xn = xz |^ n holds

eval (((<%(0. F),(1_ F)%> `^ n0) - (1_. F)),x) = xn - (1_ F)

let xz be Element of G; :: thesis: ( x = xz & xn = xz |^ n implies eval (((<%(0. F),(1_ F)%> `^ n0) - (1_. F)),x) = xn - (1_ F) )

assume that

A2: x = xz and

A3: xn = xz |^ n ; :: thesis: eval (((<%(0. F),(1_ F)%> `^ n0) - (1_. F)),x) = xn - (1_ F)

the carrier of G c= the carrier of (MultGroup F) by GROUP_2:def 5;

then reconsider xxz = xz as Element of (MultGroup F) ;

A4: xn = xxz |^ n0 by A3, GROUP_4:1

.= (power F) . (x,n0) by A2, UNIROOTS:29 ;

thus eval (((<%(0. F),(1_ F)%> `^ n0) - (1_. F)),x) = (eval ((<%(0. F),(1_ F)%> `^ n0),x)) - (eval ((1_. F),x)) by POLYNOM4:21

.= (eval ((<%(0. F),(1_ F)%> `^ n0),x)) - (1_ F) by POLYNOM4:18

.= ((power F) . ((eval (<%(0. F),(1_ F)%>,x)),n0)) - (1_ F) by POLYNOM5:22

.= xn - (1_ F) by A4, POLYNOM5:48 ; :: thesis: verum

end;eval (((<%(0. F),(1_ F)%> `^ n0) - (1_. F)),x) = xn - (1_ F)

let xz be Element of G; :: thesis: ( x = xz & xn = xz |^ n implies eval (((<%(0. F),(1_ F)%> `^ n0) - (1_. F)),x) = xn - (1_ F) )

assume that

A2: x = xz and

A3: xn = xz |^ n ; :: thesis: eval (((<%(0. F),(1_ F)%> `^ n0) - (1_. F)),x) = xn - (1_ F)

the carrier of G c= the carrier of (MultGroup F) by GROUP_2:def 5;

then reconsider xxz = xz as Element of (MultGroup F) ;

A4: xn = xxz |^ n0 by A3, GROUP_4:1

.= (power F) . (x,n0) by A2, UNIROOTS:29 ;

thus eval (((<%(0. F),(1_ F)%> `^ n0) - (1_. F)),x) = (eval ((<%(0. F),(1_ F)%> `^ n0),x)) - (eval ((1_. F),x)) by POLYNOM4:21

.= (eval ((<%(0. F),(1_ F)%> `^ n0),x)) - (1_ F) by POLYNOM4:18

.= ((power F) . ((eval (<%(0. F),(1_ F)%>,x)),n0)) - (1_ F) by POLYNOM5:22

.= xn - (1_ F) by A4, POLYNOM5:48 ; :: thesis: verum

( deg f = n & ( for x, xn being Element of F

for xz being Element of G st x = xz & xn = xz |^ n holds

eval (f,x) = xn - (1. F) ) )

then A5: 0 + 1 < n + 1 by XREAL_1:8;

len (1_. F) = 1 by POLYNOM4:4;

then A6: len (- (1_. F)) = 1 by POLYNOM4:8;

len <%(0. F),(1_ F)%> = 2 by POLYNOM5:40;

then len (<%(0. F),(1_ F)%> `^ n0) = ((n * 2) - n) + 1 by POLYNOM5:23

.= n + 1 ;

then len ((<%(0. F),(1_ F)%> `^ n0) - (1_. F)) = max ((n + 1),1) by A5, A6, POLYNOM4:7

.= n + 1 by A5, XXREAL_0:def 10 ;

then deg ((<%(0. F),(1_ F)%> `^ n0) - (1_. F)) = n ;

hence ex f being Polynomial of F st

( deg f = n & ( for x, xn being Element of F

for xz being Element of G st x = xz & xn = xz |^ n holds

eval (f,x) = xn - (1. F) ) ) by A1; :: thesis: verum