:: POLYNOM8 semantic presentation begin Lm1: for j being Integer holds ( j >= 0 or j = - 1 or j < - 1 ) proof let j be Integer; ::_thesis: ( j >= 0 or j = - 1 or j < - 1 ) percases ( j >= 0 or j < 0 ) ; suppose j >= 0 ; ::_thesis: ( j >= 0 or j = - 1 or j < - 1 ) hence ( j >= 0 or j = - 1 or j < - 1 ) ; ::_thesis: verum end; supposeA1: j < 0 ; ::_thesis: ( j >= 0 or j = - 1 or j < - 1 ) then reconsider n = - j as Element of NAT by INT_1:3; n <> - 0 by A1; then n >= 1 by NAT_1:14; then ( n > 1 or n = 1 ) by XXREAL_0:1; then ( - 1 > - (- j) or - 1 = j ) by XREAL_1:24; hence ( j >= 0 or j = - 1 or j < - 1 ) ; ::_thesis: verum end; end; end; Lm2: for j being Integer holds ( j >= 1 or j = 0 or j < 0 ) proof let j be Integer; ::_thesis: ( j >= 1 or j = 0 or j < 0 ) ( j < 0 or ( j is Element of NAT & ( j <> 0 or j = 0 ) ) ) by INT_1:3; hence ( j >= 1 or j = 0 or j < 0 ) by NAT_1:14; ::_thesis: verum end; theorem Th1: :: POLYNOM8:1 for n being Element of NAT for L being non empty non degenerated well-unital domRing-like doubleLoopStr for x being Element of L st x <> 0. L holds x |^ n <> 0. L proof let n be Element of NAT ; ::_thesis: for L being non empty non degenerated well-unital domRing-like doubleLoopStr for x being Element of L st x <> 0. L holds x |^ n <> 0. L let L be non empty non degenerated well-unital domRing-like doubleLoopStr ; ::_thesis: for x being Element of L st x <> 0. L holds x |^ n <> 0. L let x be Element of L; ::_thesis: ( x <> 0. L implies x |^ n <> 0. L ) defpred S1[ Element of NAT ] means x |^ $1 <> 0. L; assume A1: x <> 0. L ; ::_thesis: x |^ n <> 0. L A2: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] then (x |^ n) * x <> 0. L by A1, VECTSP_2:def_1; hence S1[n + 1] by GROUP_1:def_7; ::_thesis: verum end; x |^ 0 = 1_ L by BINOM:8; then A3: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2); hence x |^ n <> 0. L ; ::_thesis: verum end; registration cluster non empty right_complementable almost_left_invertible associative right-distributive well-unital add-associative right_zeroed -> non empty right_complementable associative right-distributive well-unital add-associative right_zeroed domRing-like for doubleLoopStr ; coherence for b1 being non empty right_complementable associative right-distributive well-unital add-associative right_zeroed doubleLoopStr st b1 is almost_left_invertible holds b1 is domRing-like proof let L be non empty right_complementable associative right-distributive well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: ( L is almost_left_invertible implies L is domRing-like ) assume A1: L is almost_left_invertible ; ::_thesis: L is domRing-like for x, y being Element of L holds ( not x * y = 0. L or x = 0. L or y = 0. L ) proof let x, y be Element of L; ::_thesis: ( not x * y = 0. L or x = 0. L or y = 0. L ) assume A2: x * y = 0. L ; ::_thesis: ( x = 0. L or y = 0. L ) now__::_thesis:_(_x_<>_0._L_implies_not_y_<>_0._L_) assume that A3: x <> 0. L and A4: y <> 0. L ; ::_thesis: contradiction consider xx being Element of L such that A5: xx * x = 1. L by A1, A3, VECTSP_1:def_9; y = (1. L) * y by VECTSP_1:def_8 .= xx * (x * y) by A5, GROUP_1:def_3 .= 0. L by A2, VECTSP_1:6 ; hence contradiction by A4; ::_thesis: verum end; hence ( x = 0. L or y = 0. L ) ; ::_thesis: verum end; hence L is domRing-like by VECTSP_2:def_1; ::_thesis: verum end; end; theorem Th2: :: POLYNOM8:2 for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr for x, y being Element of L st x <> 0. L & y <> 0. L holds (x * y) " = (x ") * (y ") proof let L be non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for x, y being Element of L st x <> 0. L & y <> 0. L holds (x * y) " = (x ") * (y ") let x, y be Element of L; ::_thesis: ( x <> 0. L & y <> 0. L implies (x * y) " = (x ") * (y ") ) assume that A1: x <> 0. L and A2: y <> 0. L ; ::_thesis: (x * y) " = (x ") * (y ") A3: ((x ") * (y ")) * (x * y) = (((x ") * (y ")) * y) * x by GROUP_1:def_3 .= ((x ") * ((y ") * y)) * x by GROUP_1:def_3 .= ((x ") * (1. L)) * x by A2, VECTSP_1:def_10 .= (x ") * x by VECTSP_1:def_4 .= 1. L by A1, VECTSP_1:def_10 ; x * y <> 0. L by A1, A2, VECTSP_1:12; hence (x * y) " = (x ") * (y ") by A3, VECTSP_1:def_10; ::_thesis: verum end; theorem Th3: :: POLYNOM8:3 for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr for z, z1 being Element of L st z <> 0. L holds z1 = (z1 * z) / z proof let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for z, z1 being Element of L st z <> 0. L holds z1 = (z1 * z) / z let z, z1 be Element of L; ::_thesis: ( z <> 0. L implies z1 = (z1 * z) / z ) assume A1: z <> 0. L ; ::_thesis: z1 = (z1 * z) / z thus (z1 * z) / z = z1 * (z * (z ")) by GROUP_1:def_3 .= z1 * (1. L) by A1, VECTSP_1:def_10 .= z1 by VECTSP_1:def_8 ; ::_thesis: verum end; theorem Th4: :: POLYNOM8:4 for L being non empty right_complementable add-associative right_zeroed left_zeroed doubleLoopStr for m being Element of NAT for s being FinSequence of L st len s = m & ( for k being Element of NAT st 1 <= k & k <= m holds s /. k = 1. L ) holds Sum s = m * (1. L) proof let L be non empty right_complementable add-associative right_zeroed left_zeroed doubleLoopStr ; ::_thesis: for m being Element of NAT for s being FinSequence of L st len s = m & ( for k being Element of NAT st 1 <= k & k <= m holds s /. k = 1. L ) holds Sum s = m * (1. L) let m be Element of NAT ; ::_thesis: for s being FinSequence of L st len s = m & ( for k being Element of NAT st 1 <= k & k <= m holds s /. k = 1. L ) holds Sum s = m * (1. L) let s be FinSequence of L; ::_thesis: ( len s = m & ( for k being Element of NAT st 1 <= k & k <= m holds s /. k = 1. L ) implies Sum s = m * (1. L) ) assume A1: ( len s = m & ( for k being Element of NAT st 1 <= k & k <= m holds s /. k = 1. L ) ) ; ::_thesis: Sum s = m * (1. L) defpred S1[ Element of NAT ] means for s being FinSequence of L st len s = $1 & ( for k being Element of NAT st 1 <= k & k <= $1 holds s /. k = 1. L ) holds Sum s = $1 * (1. L); A2: for l being Element of NAT st S1[l] holds S1[l + 1] proof let l be Element of NAT ; ::_thesis: ( S1[l] implies S1[l + 1] ) assume A3: for g being FinSequence of L st len g = l & ( for k being Element of NAT st 1 <= k & k <= l holds g /. k = 1. L ) holds Sum g = l * (1. L) ; ::_thesis: S1[l + 1] for s being FinSequence of L st len s = l + 1 & ( for k being Element of NAT st 1 <= k & k <= l + 1 holds s /. k = 1. L ) holds Sum s = (l + 1) * (1. L) proof ex G being FinSequence of L st ( dom G = Seg l & ( for k being Nat st k in Seg l holds G . k = 1. L ) ) proof defpred S2[ Nat, set ] means $2 = 1. L; A4: for n being Nat st n in Seg l holds ex x being Element of L st S2[n,x] ; ex G being FinSequence of L st ( dom G = Seg l & ( for nn being Nat st nn in Seg l holds S2[nn,G . nn] ) ) from FINSEQ_1:sch_5(A4); hence ex G being FinSequence of L st ( dom G = Seg l & ( for k being Nat st k in Seg l holds G . k = 1. L ) ) ; ::_thesis: verum end; then consider g being FinSequence of L such that A5: dom g = Seg l and A6: for k being Nat st k in Seg l holds g . k = 1. L ; A7: len g = l by A5, FINSEQ_1:def_3; A8: for k being Nat st 1 <= k & k <= l holds g /. k = 1. L proof let k be Nat; ::_thesis: ( 1 <= k & k <= l implies g /. k = 1. L ) assume A9: ( 1 <= k & k <= l ) ; ::_thesis: g /. k = 1. L then A10: k in dom g by A5, FINSEQ_1:1; k in Seg l by A9, FINSEQ_1:1; then 1. L = g . k by A6 .= g /. k by A10, PARTFUN1:def_6 ; hence g /. k = 1. L ; ::_thesis: verum end; then A11: for k being Element of NAT st 1 <= k & k <= l holds g /. k = 1. L ; dom <*(1. L)*> = Seg 1 by FINSEQ_1:def_8; then A12: len <*(1. L)*> = 1 by FINSEQ_1:def_3; let s be FinSequence of L; ::_thesis: ( len s = l + 1 & ( for k being Element of NAT st 1 <= k & k <= l + 1 holds s /. k = 1. L ) implies Sum s = (l + 1) * (1. L) ) assume that A13: len s = l + 1 and A14: for k being Element of NAT st 1 <= k & k <= l + 1 holds s /. k = 1. L ; ::_thesis: Sum s = (l + 1) * (1. L) A15: dom s = Seg (l + 1) by A13, FINSEQ_1:def_3; A16: for k being Nat st k in dom s holds s . k = (g ^ <*(1. L)*>) . k proof A17: dom s = Seg (l + 1) by A13, FINSEQ_1:def_3; let k be Nat; ::_thesis: ( k in dom s implies s . k = (g ^ <*(1. L)*>) . k ) A18: k in NAT by ORDINAL1:def_12; assume A19: k in dom s ; ::_thesis: s . k = (g ^ <*(1. L)*>) . k percases ( ( 1 <= k & k <= l ) or ( l < k & k <= l + 1 ) ) by A19, A17, FINSEQ_1:1; supposeA20: ( 1 <= k & k <= l ) ; ::_thesis: s . k = (g ^ <*(1. L)*>) . k then A21: k <= l + 1 by NAT_1:12; A22: k in dom g by A5, A18, A20; then (g ^ <*(1. L)*>) . k = g . k by FINSEQ_1:def_7 .= g /. k by A22, PARTFUN1:def_6 .= 1. L by A8, A20 .= s /. k by A14, A18, A20, A21 .= s . k by A19, PARTFUN1:def_6 ; hence s . k = (g ^ <*(1. L)*>) . k ; ::_thesis: verum end; supposeA23: ( l < k & k <= l + 1 ) ; ::_thesis: s . k = (g ^ <*(1. L)*>) . k then k - k <= (l + 1) - k by XREAL_1:9; then reconsider ii = ((l + 1) - k) + 1 as Element of NAT by INT_1:3; l + 1 <= k by A23, NAT_1:13; then ( dom <*(1. L)*> = Seg 1 & ii = (k - k) + 1 ) by A23, FINSEQ_1:def_8, XXREAL_0:1; then A24: ii in dom <*(1. L)*> ; l + 0 < k + l by A23, XREAL_1:8; then l + 1 <= k + l by NAT_1:13; then A25: (l + 1) - l <= (k + l) - l by XREAL_1:9; l + 1 <= k by A23, NAT_1:13; then A26: ii = (k - k) + 1 by A23, XXREAL_0:1; then (g ^ <*(1. L)*>) . k = (g ^ <*(1. L)*>) . ((len g) + ii) by A5, FINSEQ_1:def_3 .= <*(1. L)*> . 1 by A24, A26, FINSEQ_1:def_7 .= 1. L by FINSEQ_1:def_8 .= s /. k by A14, A18, A23, A25 .= s . k by A19, PARTFUN1:def_6 ; hence s . k = (g ^ <*(1. L)*>) . k ; ::_thesis: verum end; end; end; dom (g ^ <*(1. L)*>) = Seg ((len g) + (len <*(1. L)*>)) by FINSEQ_1:def_7 .= dom s by A5, A12, A15, FINSEQ_1:def_3 ; then s = g ^ <*(1. L)*> by A16, FINSEQ_1:13; then Sum s = (Sum g) + (1. L) by FVSUM_1:71 .= (l * (1. L)) + (1. L) by A3, A7, A11 .= (l * (1. L)) + (1 * (1. L)) by BINOM:13 .= (l + 1) * (1. L) by BINOM:15 ; hence Sum s = (l + 1) * (1. L) ; ::_thesis: verum end; hence S1[l + 1] ; ::_thesis: verum end; for s being FinSequence of L st len s = 0 & ( for k being Element of NAT st 1 <= k & k <= 0 holds s /. k = 1. L ) holds Sum s = 0 * (1. L) proof let s be FinSequence of L; ::_thesis: ( len s = 0 & ( for k being Element of NAT st 1 <= k & k <= 0 holds s /. k = 1. L ) implies Sum s = 0 * (1. L) ) assume that A27: len s = 0 and for k being Element of NAT st 1 <= k & k <= 0 holds s /. k = 1. L ; ::_thesis: Sum s = 0 * (1. L) A28: <*> the carrier of L is Element of 0 -tuples_on the carrier of L by FINSEQ_2:131; s = {} by A27; then Sum s = Sum (<*> the carrier of L) .= 0. L by A28, FVSUM_1:74 .= 0 * (1. L) by BINOM:12 ; hence Sum s = 0 * (1. L) ; ::_thesis: verum end; then A29: S1[ 0 ] ; for l being Element of NAT holds S1[l] from NAT_1:sch_1(A29, A2); hence Sum s = m * (1. L) by A1; ::_thesis: verum end; theorem Th5: :: POLYNOM8:5 for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr for s being FinSequence of L for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds s . i = q |^ (i -' 1) ) holds Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) proof let L be non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for s being FinSequence of L for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds s . i = q |^ (i -' 1) ) holds Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) let s be FinSequence of L; ::_thesis: for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds s . i = q |^ (i -' 1) ) holds Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) let q be Element of L; ::_thesis: ( q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds s . i = q |^ (i -' 1) ) implies Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) ) assume A1: ( q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds s . i = q |^ (i -' 1) ) ) ; ::_thesis: Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) defpred S1[ Nat] means for s being FinSequence of L st len s = $1 holds for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds s . i = q |^ (i -' 1) ) holds Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q); A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_for_s_being_FinSequence_of_L_st_len_s_=_k_+_1_holds_ for_q_being_Element_of_L_st_q_<>_1._L_&_(_for_i_being_Nat_st_1_<=_i_&_i_<=_len_s_holds_ s_._i_=_q_|^_(i_-'_1)_)_holds_ Sum_s_=_((1._L)_-_(q_|^_(len_s)))_/_((1._L)_-_q) let s be FinSequence of L; ::_thesis: ( len s = k + 1 implies for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds s . i = q |^ (i -' 1) ) holds Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) ) set f = s | (Seg k); reconsider f = s | (Seg k) as FinSequence by FINSEQ_1:15; assume A4: len s = k + 1 ; ::_thesis: for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds s . i = q |^ (i -' 1) ) holds Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) then A5: 1 <= len s by NAT_1:12; then len s in dom s by FINSEQ_3:25; then A6: s /. (len s) = s . (len s) by PARTFUN1:def_6; A7: k <= len s by A4, NAT_1:13; then A8: len f = k by FINSEQ_1:17; now__::_thesis:_for_u_being_set_st_u_in_rng_f_holds_ u_in_the_carrier_of_L let u be set ; ::_thesis: ( u in rng f implies u in the carrier of L ) assume u in rng f ; ::_thesis: u in the carrier of L then consider x being set such that A9: x in dom f and A10: f . x = u by FUNCT_1:def_3; reconsider x9 = x as Element of NAT by A9; x9 <= len f by A9, FINSEQ_3:25; then A11: x9 <= len s by A4, A8, NAT_1:12; 1 <= x9 by A9, FINSEQ_3:25; then A12: x in dom s by A11, FINSEQ_3:25; f . x = s . x by A9, FUNCT_1:47 .= s /. x by A12, PARTFUN1:def_6 ; hence u in the carrier of L by A10; ::_thesis: verum end; then rng f c= the carrier of L by TARSKI:def_3; then reconsider f = f as FinSequence of L by FINSEQ_1:def_4; A13: len s = (len f) + 1 by A4, A7, FINSEQ_1:17; let q be Element of L; ::_thesis: ( q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds s . i = q |^ (i -' 1) ) implies Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) ) assume that A14: q <> 1. L and A15: for i being Nat st 1 <= i & i <= len s holds s . i = q |^ (i -' 1) ; ::_thesis: Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) A16: now__::_thesis:_not_(1._L)_-_q_=_0._L assume (1. L) - q = 0. L ; ::_thesis: contradiction then ((1. L) - q) + q = q by ALGSTR_1:def_2; then (1. L) + ((- q) + q) = q by RLVECT_1:def_3; then (1. L) + (0. L) = q by RLVECT_1:5; hence contradiction by A14, RLVECT_1:def_4; ::_thesis: verum end; (len s) - 1 >= 1 - 1 by A5, XREAL_1:9; then A17: (len s) -' 1 = (len s) - 1 by XREAL_0:def_2 .= ((len f) + 1) - 1 by A4, A7, FINSEQ_1:17 ; A18: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_f_holds_ f_._i_=_q_|^_(i_-'_1) let i be Nat; ::_thesis: ( 1 <= i & i <= len f implies f . i = q |^ (i -' 1) ) assume that A19: 1 <= i and A20: i <= len f ; ::_thesis: f . i = q |^ (i -' 1) A21: i <= len s by A4, A8, A20, NAT_1:13; i in dom f by A19, A20, FINSEQ_3:25; hence f . i = s . i by FUNCT_1:47 .= q |^ (i -' 1) by A15, A19, A21 ; ::_thesis: verum end; f = s | (dom f) by A7, FINSEQ_1:17; hence Sum s = (Sum f) + (s /. (len s)) by A13, A6, RLVECT_1:38 .= (((1. L) - (q |^ (len f))) / ((1. L) - q)) + (s /. (len s)) by A3, A14, A7, A18, FINSEQ_1:17 .= (((1. L) - (q |^ (len f))) / ((1. L) - q)) + (q |^ (len f)) by A15, A5, A17, A6 .= (((1. L) - (q |^ (len f))) / ((1. L) - q)) + (((q |^ (len f)) * ((1. L) - q)) / ((1. L) - q)) by A16, Th3 .= (((1. L) - (q |^ (len f))) + ((q |^ (len f)) * ((1. L) - q))) / ((1. L) - q) by VECTSP_1:def_3 .= (((1. L) - (q |^ (len f))) + (((q |^ (len f)) * (1. L)) + ((q |^ (len f)) * (- q)))) / ((1. L) - q) by VECTSP_1:def_2 .= (((1. L) - (q |^ (len f))) + ((q |^ (len f)) + ((q |^ (len f)) * (- q)))) / ((1. L) - q) by VECTSP_1:def_4 .= ((1. L) + ((- (q |^ (len f))) + ((q |^ (len f)) + ((q |^ (len f)) * (- q))))) / ((1. L) - q) by RLVECT_1:def_3 .= ((1. L) + (((- (q |^ (len f))) + (q |^ (len f))) + ((q |^ (len f)) * (- q)))) / ((1. L) - q) by RLVECT_1:def_3 .= ((1. L) + ((0. L) + ((q |^ (len f)) * (- q)))) / ((1. L) - q) by RLVECT_1:5 .= ((1. L) + ((q |^ (len f)) * (- q))) / ((1. L) - q) by ALGSTR_1:def_2 .= ((1. L) + (- ((q |^ (len f)) * q))) / ((1. L) - q) by VECTSP_1:8 .= ((1. L) - (q |^ (len s))) / ((1. L) - q) by A13, GROUP_1:def_7 ; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; now__::_thesis:_for_s_being_FinSequence_of_L_st_len_s_=_0_holds_ for_q_being_Element_of_L_st_q_<>_1._L_&_(_for_i_being_Nat_st_1_<=_i_&_i_<=_len_s_holds_ s_._i_=_q_|^_(i_-'_1)_)_holds_ ((1._L)_-_(q_|^_0))_/_((1._L)_-_q)_=_Sum_s let s be FinSequence of L; ::_thesis: ( len s = 0 implies for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds s . i = q |^ (i -' 1) ) holds ((1. L) - (q |^ 0)) / ((1. L) - q) = Sum s ) assume len s = 0 ; ::_thesis: for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds s . i = q |^ (i -' 1) ) holds ((1. L) - (q |^ 0)) / ((1. L) - q) = Sum s then A22: s = <*> the carrier of L ; let q be Element of L; ::_thesis: ( q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds s . i = q |^ (i -' 1) ) implies ((1. L) - (q |^ 0)) / ((1. L) - q) = Sum s ) assume that q <> 1. L and for i being Nat st 1 <= i & i <= len s holds s . i = q |^ (i -' 1) ; ::_thesis: ((1. L) - (q |^ 0)) / ((1. L) - q) = Sum s thus ((1. L) - (q |^ 0)) / ((1. L) - q) = ((1. L) - (1_ L)) / ((1. L) - q) by BINOM:8 .= (0. L) / ((1. L) - q) by RLVECT_1:15 .= 0. L by VECTSP_1:6 .= Sum s by A22, RLVECT_1:43 ; ::_thesis: verum end; then A23: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A23, A2); hence Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q) by A1; ::_thesis: verum end; definition let L be non empty well-unital doubleLoopStr ; let m be Element of NAT ; func emb (m,L) -> Element of L equals :: POLYNOM8:def 1 m * (1. L); coherence m * (1. L) is Element of L ; end; :: deftheorem defines emb POLYNOM8:def_1_:_ for L being non empty well-unital doubleLoopStr for m being Element of NAT holds emb (m,L) = m * (1. L); theorem Th6: :: POLYNOM8:6 for L being Field for m, n, k being Element of NAT st m > 0 & n > 0 holds for M1 being Matrix of m,n,L for M2 being Matrix of n,k,L holds ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2) proof let L be Field; ::_thesis: for m, n, k being Element of NAT st m > 0 & n > 0 holds for M1 being Matrix of m,n,L for M2 being Matrix of n,k,L holds ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2) let m, n, k be Element of NAT ; ::_thesis: ( m > 0 & n > 0 implies for M1 being Matrix of m,n,L for M2 being Matrix of n,k,L holds ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2) ) assume that A1: m > 0 and A2: n > 0 ; ::_thesis: for M1 being Matrix of m,n,L for M2 being Matrix of n,k,L holds ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2) let M1 be Matrix of m,n,L; ::_thesis: for M2 being Matrix of n,k,L holds ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2) let M2 be Matrix of n,k,L; ::_thesis: ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2) A3: width M1 = n by A1, MATRIX_1:23 .= len M2 by A2, MATRIX_1:23 ; A4: width ((emb (m,L)) * M1) = width M1 by MATRIX_3:def_5 .= n by A1, MATRIX_1:23 .= len M2 by A2, MATRIX_1:23 ; A5: for i, j being Nat st [i,j] in Indices (((emb (m,L)) * M1) * M2) holds (((emb (m,L)) * M1) * M2) * (i,j) = ((emb (m,L)) * (M1 * M2)) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (((emb (m,L)) * M1) * M2) implies (((emb (m,L)) * M1) * M2) * (i,j) = ((emb (m,L)) * (M1 * M2)) * (i,j) ) A6: len M1 = len (M1 * M2) by A3, MATRIX_3:def_4; len (((emb (m,L)) * M1) * M2) = len ((emb (m,L)) * M1) by A4, MATRIX_3:def_4 .= len M1 by MATRIX_3:def_5 ; then A7: dom (((emb (m,L)) * M1) * M2) = Seg (len M1) by FINSEQ_1:def_3 .= dom (M1 * M2) by A6, FINSEQ_1:def_3 ; Seg (len ((emb (m,L)) * (Line (M1,i)))) = dom ((emb (m,L)) * (Line (M1,i))) by FINSEQ_1:def_3 .= dom (Line (M1,i)) by POLYNOM1:def_1 .= Seg (len (Line (M1,i))) by FINSEQ_1:def_3 ; then A8: len ((emb (m,L)) * (Line (M1,i))) = len (Line (M1,i)) by FINSEQ_1:6 .= width M1 by MATRIX_1:def_7 ; A9: len (Line (M1,i)) = len M2 by A3, MATRIX_1:def_7 .= len (Col (M2,j)) by MATRIX_1:def_8 ; assume A10: [i,j] in Indices (((emb (m,L)) * M1) * M2) ; ::_thesis: (((emb (m,L)) * M1) * M2) * (i,j) = ((emb (m,L)) * (M1 * M2)) * (i,j) then A11: (((emb (m,L)) * M1) * M2) * (i,j) = (Line (((emb (m,L)) * M1),i)) "*" (Col (M2,j)) by A4, MATRIX_3:def_4 .= Sum (mlt ((Line (((emb (m,L)) * M1),i)),(Col (M2,j)))) by FVSUM_1:def_9 ; len (Line (((emb (m,L)) * M1),i)) = width ((emb (m,L)) * M1) by MATRIX_1:def_7 .= width M1 by MATRIX_3:def_5 ; then dom (Line (((emb (m,L)) * M1),i)) = Seg (width M1) by FINSEQ_1:def_3; then A12: dom (Line (((emb (m,L)) * M1),i)) = dom ((emb (m,L)) * (Line (M1,i))) by A8, FINSEQ_1:def_3; for k being Nat st k in dom (Line (((emb (m,L)) * M1),i)) holds (Line (((emb (m,L)) * M1),i)) . k = ((emb (m,L)) * (Line (M1,i))) . k proof len (M1 * M2) = len M1 by A3, MATRIX_3:def_4 .= m by A1, MATRIX_1:23 ; then A13: dom (M1 * M2) = Seg m by FINSEQ_1:def_3; A14: ( Indices M1 = [:(Seg m),(Seg n):] & i in dom (M1 * M2) ) by A1, A10, A7, MATRIX_1:23, ZFMISC_1:87; let k be Nat; ::_thesis: ( k in dom (Line (((emb (m,L)) * M1),i)) implies (Line (((emb (m,L)) * M1),i)) . k = ((emb (m,L)) * (Line (M1,i))) . k ) assume A15: k in dom (Line (((emb (m,L)) * M1),i)) ; ::_thesis: (Line (((emb (m,L)) * M1),i)) . k = ((emb (m,L)) * (Line (M1,i))) . k A16: len (Line (((emb (m,L)) * M1),i)) = width ((emb (m,L)) * M1) by MATRIX_1:def_7 .= width M1 by MATRIX_3:def_5 ; then A17: k in Seg (width M1) by A15, FINSEQ_1:def_3; len (Line (M1,i)) = width M1 by MATRIX_1:def_7; then k in dom (Line (M1,i)) by A17, FINSEQ_1:def_3; then (Line (M1,i)) . k = (Line (M1,i)) /. k by PARTFUN1:def_6; then reconsider a = (Line (M1,i)) . k as Element of L ; A18: a = M1 * (i,k) by A17, MATRIX_1:def_7; k in Seg n by A1, A17, MATRIX_1:23; then [i,k] in Indices M1 by A14, A13, ZFMISC_1:87; then A19: (emb (m,L)) * a = ((emb (m,L)) * M1) * (i,k) by A18, MATRIX_3:def_5; dom (Line (((emb (m,L)) * M1),i)) = Seg (width M1) by A16, FINSEQ_1:def_3; then A20: k in Seg (width ((emb (m,L)) * M1)) by A15, MATRIX_3:def_5; ((emb (m,L)) * (Line (M1,i))) . k = (emb (m,L)) * a by A12, A15, FVSUM_1:50; hence (Line (((emb (m,L)) * M1),i)) . k = ((emb (m,L)) * (Line (M1,i))) . k by A20, A19, MATRIX_1:def_7; ::_thesis: verum end; then A21: Line (((emb (m,L)) * M1),i) = (emb (m,L)) * (Line (M1,i)) by A12, FINSEQ_1:13; Seg (len ((emb (m,L)) * (Line (M1,i)))) = dom ((emb (m,L)) * (Line (M1,i))) by FINSEQ_1:def_3 .= dom (Line (M1,i)) by POLYNOM1:def_1 .= Seg (len (Line (M1,i))) by FINSEQ_1:def_3 ; then A22: len ((emb (m,L)) * (Line (M1,i))) = len (Line (M1,i)) by FINSEQ_1:6 .= len M2 by A3, MATRIX_1:def_7 .= len (Col (M2,j)) by MATRIX_1:def_8 ; A23: dom ((emb (m,L)) * (Line (M1,i))) = Seg (len ((emb (m,L)) * (Line (M1,i)))) by FINSEQ_1:def_3 .= Seg (len (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j))))) by A22, MATRIX_3:6 .= dom (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) by FINSEQ_1:def_3 ; A24: dom ((emb (m,L)) * (Line (M1,i))) = dom (Line (M1,i)) by POLYNOM1:def_1 .= Seg (len (Line (M1,i))) by FINSEQ_1:def_3 .= Seg (len (mlt ((Line (M1,i)),(Col (M2,j))))) by A9, MATRIX_3:6 .= dom (mlt ((Line (M1,i)),(Col (M2,j)))) by FINSEQ_1:def_3 ; then A25: dom (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) = dom ((emb (m,L)) * (mlt ((Line (M1,i)),(Col (M2,j))))) by A23, POLYNOM1:def_1; for k being Nat st k in dom (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) holds (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) . k = ((emb (m,L)) * (mlt ((Line (M1,i)),(Col (M2,j))))) . k proof A26: len (Line (M1,i)) = len M2 by A3, MATRIX_1:def_7 .= len (Col (M2,j)) by MATRIX_1:def_8 ; A27: len (Line (M1,i)) = width M1 by MATRIX_1:def_7; let k be Nat; ::_thesis: ( k in dom (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) implies (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) . k = ((emb (m,L)) * (mlt ((Line (M1,i)),(Col (M2,j))))) . k ) assume A28: k in dom (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) ; ::_thesis: (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) . k = ((emb (m,L)) * (mlt ((Line (M1,i)),(Col (M2,j))))) . k dom (Line (M1,i)) = Seg (len (Line (M1,i))) by FINSEQ_1:def_3 .= Seg (len (mlt ((Line (M1,i)),(Col (M2,j))))) by A26, MATRIX_3:6 .= dom (mlt ((Line (M1,i)),(Col (M2,j)))) by FINSEQ_1:def_3 ; then A29: k in Seg (width M1) by A23, A24, A28, A27, FINSEQ_1:def_3; then k in dom M2 by A3, FINSEQ_1:def_3; then A30: (Col (M2,j)) . k = M2 * (k,j) by MATRIX_1:def_8; (Line (M1,i)) . k = M1 * (i,k) by A29, MATRIX_1:def_7; then reconsider c = (Col (M2,j)) . k, d = (Line (M1,i)) . k as Element of L by A30; (mlt ((Line (M1,i)),(Col (M2,j)))) . k = c * d by A23, A24, A28, FVSUM_1:60; then reconsider a = (mlt ((Line (M1,i)),(Col (M2,j)))) . k as Element of L ; A31: ((emb (m,L)) * (mlt ((Line (M1,i)),(Col (M2,j))))) . k = (emb (m,L)) * a by A25, A28, FVSUM_1:50; ((emb (m,L)) * (Line (M1,i))) . k = (emb (m,L)) * d by A23, A28, FVSUM_1:50; then reconsider b = ((emb (m,L)) * (Line (M1,i))) . k as Element of L ; b * c = ((emb (m,L)) * d) * c by A23, A28, FVSUM_1:50 .= (emb (m,L)) * (d * c) by GROUP_1:def_3 .= (emb (m,L)) * a by A23, A24, A28, FVSUM_1:60 ; hence (mlt (((emb (m,L)) * (Line (M1,i))),(Col (M2,j)))) . k = ((emb (m,L)) * (mlt ((Line (M1,i)),(Col (M2,j))))) . k by A28, A31, FVSUM_1:60; ::_thesis: verum end; then A32: (emb (m,L)) * (mlt ((Line (M1,i)),(Col (M2,j)))) = mlt ((Line (((emb (m,L)) * M1),i)),(Col (M2,j))) by A21, A25, FINSEQ_1:13; Seg (width (((emb (m,L)) * M1) * M2)) = Seg (width M2) by A4, MATRIX_3:def_4 .= Seg (width (M1 * M2)) by A3, MATRIX_3:def_4 ; then A33: [i,j] in Indices (M1 * M2) by A10, A7; then ((emb (m,L)) * (M1 * M2)) * (i,j) = (emb (m,L)) * ((M1 * M2) * (i,j)) by MATRIX_3:def_5 .= (emb (m,L)) * ((Line (M1,i)) "*" (Col (M2,j))) by A3, A33, MATRIX_3:def_4 .= (emb (m,L)) * (Sum (mlt ((Line (M1,i)),(Col (M2,j))))) by FVSUM_1:def_9 ; hence (((emb (m,L)) * M1) * M2) * (i,j) = ((emb (m,L)) * (M1 * M2)) * (i,j) by A11, A32, FVSUM_1:73; ::_thesis: verum end; A34: len ((emb (m,L)) * (M1 * M2)) = len (M1 * M2) by MATRIX_3:def_5 .= len M1 by A3, MATRIX_3:def_4 ; width ((emb (m,L)) * (M1 * M2)) = width (M1 * M2) by MATRIX_3:def_5 .= width M2 by A3, MATRIX_3:def_4 ; then A35: width (((emb (m,L)) * M1) * M2) = width ((emb (m,L)) * (M1 * M2)) by A4, MATRIX_3:def_4; len (((emb (m,L)) * M1) * M2) = len ((emb (m,L)) * M1) by A4, MATRIX_3:def_4 .= len M1 by MATRIX_3:def_5 ; hence ((emb (m,L)) * M1) * M2 = (emb (m,L)) * (M1 * M2) by A34, A35, A5, MATRIX_1:21; ::_thesis: verum end; theorem Th7: :: POLYNOM8:7 for L being non empty ZeroStr for p being AlgSequence of L for i being Element of NAT st p . i <> 0. L holds len p >= i + 1 proof let L be non empty ZeroStr ; ::_thesis: for p being AlgSequence of L for i being Element of NAT st p . i <> 0. L holds len p >= i + 1 let p be AlgSequence of L; ::_thesis: for i being Element of NAT st p . i <> 0. L holds len p >= i + 1 let i be Element of NAT ; ::_thesis: ( p . i <> 0. L implies len p >= i + 1 ) A1: len p is_at_least_length_of p by ALGSEQ_1:def_3; assume p . i <> 0. L ; ::_thesis: len p >= i + 1 then len p > i by A1, ALGSEQ_1:def_2; hence len p >= i + 1 by NAT_1:13; ::_thesis: verum end; theorem Th8: :: POLYNOM8:8 for L being non empty ZeroStr for s being AlgSequence of L st len s > 0 holds s . ((len s) - 1) <> 0. L proof let L be non empty ZeroStr ; ::_thesis: for s being AlgSequence of L st len s > 0 holds s . ((len s) - 1) <> 0. L let s be AlgSequence of L; ::_thesis: ( len s > 0 implies s . ((len s) - 1) <> 0. L ) assume len s > 0 ; ::_thesis: s . ((len s) - 1) <> 0. L then len s >= 0 + 1 by NAT_1:13; then (len s) - 1 >= 1 - 1 by XREAL_1:9; then reconsider l = (len s) - 1 as Element of NAT by INT_1:3; assume A1: s . ((len s) - 1) = 0. L ; ::_thesis: contradiction now__::_thesis:_for_i_being_Nat_st_i_>=_l_holds_ s_._i_=_0._L let i be Nat; ::_thesis: ( i >= l implies s . b1 = 0. L ) assume A2: i >= l ; ::_thesis: s . b1 = 0. L percases ( i = l or i > l ) by A2, XXREAL_0:1; suppose i = l ; ::_thesis: s . b1 = 0. L hence s . i = 0. L by A1; ::_thesis: verum end; suppose i > l ; ::_thesis: s . b1 = 0. L then i >= l + 1 by NAT_1:13; hence s . i = 0. L by ALGSEQ_1:8; ::_thesis: verum end; end; end; then A3: l is_at_least_length_of s by ALGSEQ_1:def_2; len s < (len s) + 1 by NAT_1:13; then (len s) - 1 < ((len s) + 1) - 1 by XREAL_1:9; hence contradiction by A3, ALGSEQ_1:def_3; ::_thesis: verum end; theorem Th9: :: POLYNOM8:9 for L being non empty right_complementable associative commutative well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr for p, q being Polynomial of L st len p > 0 & len q > 0 holds len (p *' q) <= (len p) + (len q) proof let L be non empty right_complementable associative commutative well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for p, q being Polynomial of L st len p > 0 & len q > 0 holds len (p *' q) <= (len p) + (len q) let p, q be Polynomial of L; ::_thesis: ( len p > 0 & len q > 0 implies len (p *' q) <= (len p) + (len q) ) assume that A1: len p > 0 and A2: len q > 0 ; ::_thesis: len (p *' q) <= (len p) + (len q) A3: ((len p) + (len q)) - 1 <= ((len p) + (len q)) - 0 by XREAL_1:13; (len q) + 1 > 0 + 1 by A2, XREAL_1:6; then len q >= 1 by NAT_1:13; then A4: (len q) - 1 >= 1 - 1 by XREAL_1:13; q . ((len q) - 1) <> 0. L by A2, Th8; then A5: q . ((len q) -' 1) <> 0. L by A4, XREAL_0:def_2; (len p) + 1 > 0 + 1 by A1, XREAL_1:6; then len p >= 1 by NAT_1:13; then A6: (len p) - 1 >= 1 - 1 by XREAL_1:13; p . ((len p) - 1) <> 0. L by A1, Th8; then p . ((len p) -' 1) <> 0. L by A6, XREAL_0:def_2; then (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L by A5, VECTSP_2:def_1; hence len (p *' q) <= (len p) + (len q) by A3, POLYNOM4:10; ::_thesis: verum end; theorem Th10: :: POLYNOM8:10 for L being non empty associative doubleLoopStr for k, l being Element of L for seq being sequence of L holds k * (l * seq) = (k * l) * seq proof let L be non empty associative doubleLoopStr ; ::_thesis: for k, l being Element of L for seq being sequence of L holds k * (l * seq) = (k * l) * seq let k, l be Element of L; ::_thesis: for seq being sequence of L holds k * (l * seq) = (k * l) * seq let seq be sequence of L; ::_thesis: k * (l * seq) = (k * l) * seq now__::_thesis:_for_i_being_Element_of_NAT_holds_(k_*_(l_*_seq))_._i_=_((k_*_l)_*_seq)_._i let i be Element of NAT ; ::_thesis: (k * (l * seq)) . i = ((k * l) * seq) . i thus (k * (l * seq)) . i = k * ((l * seq) . i) by POLYNOM5:def_3 .= k * (l * (seq . i)) by POLYNOM5:def_3 .= (k * l) * (seq . i) by GROUP_1:def_3 .= ((k * l) * seq) . i by POLYNOM5:def_3 ; ::_thesis: verum end; hence k * (l * seq) = (k * l) * seq by FUNCT_2:63; ::_thesis: verum end; begin definition let L be non empty doubleLoopStr ; let m1, m2 be sequence of L; funcm1 * m2 -> sequence of L means :Def2: :: POLYNOM8:def 2 for i being Nat holds it . i = (m1 . i) * (m2 . i); existence ex b1 being sequence of L st for i being Nat holds b1 . i = (m1 . i) * (m2 . i) proof defpred S1[ set , set ] means $2 = (m1 /. $1) * (m2 /. $1); A1: for x being set st x in NAT holds ex y being set st ( y in the carrier of L & S1[x,y] ) ; consider f being Function of NAT, the carrier of L such that A2: for x being set st x in NAT holds S1[x,f . x] from FUNCT_2:sch_1(A1); reconsider f = f as sequence of L ; take f ; ::_thesis: for i being Nat holds f . i = (m1 . i) * (m2 . i) now__::_thesis:_for_i_being_Nat_holds_f_._i_=_(m1_._i)_*_(m2_._i) let i be Nat; ::_thesis: f . i = (m1 . i) * (m2 . i) A3: i in NAT by ORDINAL1:def_12; dom m2 = NAT by FUNCT_2:def_1; then A4: m2 /. i = m2 . i by A3, PARTFUN1:def_6; dom m1 = NAT by FUNCT_2:def_1; then m1 /. i = m1 . i by A3, PARTFUN1:def_6; hence f . i = (m1 . i) * (m2 . i) by A2, A3, A4; ::_thesis: verum end; hence for i being Nat holds f . i = (m1 . i) * (m2 . i) ; ::_thesis: verum end; uniqueness for b1, b2 being sequence of L st ( for i being Nat holds b1 . i = (m1 . i) * (m2 . i) ) & ( for i being Nat holds b2 . i = (m1 . i) * (m2 . i) ) holds b1 = b2 proof let z1, z2 be sequence of L; ::_thesis: ( ( for i being Nat holds z1 . i = (m1 . i) * (m2 . i) ) & ( for i being Nat holds z2 . i = (m1 . i) * (m2 . i) ) implies z1 = z2 ) assume A5: for i being Nat holds z1 . i = (m1 . i) * (m2 . i) ; ::_thesis: ( ex i being Nat st not z2 . i = (m1 . i) * (m2 . i) or z1 = z2 ) assume A6: for i being Nat holds z2 . i = (m1 . i) * (m2 . i) ; ::_thesis: z1 = z2 A7: now__::_thesis:_for_x_being_set_st_x_in_dom_z1_holds_ z1_._x_=_z2_._x let x be set ; ::_thesis: ( x in dom z1 implies z1 . x = z2 . x ) assume x in dom z1 ; ::_thesis: z1 . x = z2 . x then reconsider x9 = x as Element of NAT by FUNCT_2:def_1; thus z1 . x = (m1 . x9) * (m2 . x9) by A5 .= z2 . x by A6 ; ::_thesis: verum end; dom z1 = NAT by FUNCT_2:def_1 .= dom z2 by FUNCT_2:def_1 ; hence z1 = z2 by A7, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def2 defines * POLYNOM8:def_2_:_ for L being non empty doubleLoopStr for m1, m2, b4 being sequence of L holds ( b4 = m1 * m2 iff for i being Nat holds b4 . i = (m1 . i) * (m2 . i) ); registration let L be non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr ; let m1, m2 be AlgSequence of L; clusterm1 * m2 -> finite-Support ; coherence m1 * m2 is finite-Support proof set f = m1 * m2; ex n being Nat st for i being Nat st i >= n holds (m1 * m2) . i = 0. L proof take (len m1) + 1 ; ::_thesis: for i being Nat st i >= (len m1) + 1 holds (m1 * m2) . i = 0. L now__::_thesis:_for_i_being_Nat_st_i_>=_(len_m1)_+_1_holds_ 0._L_=_(m1_*_m2)_._i let i be Nat; ::_thesis: ( i >= (len m1) + 1 implies 0. L = (m1 * m2) . i ) assume i >= (len m1) + 1 ; ::_thesis: 0. L = (m1 * m2) . i then i > len m1 by NAT_1:13; then m1 . i = 0. L by ALGSEQ_1:8; hence 0. L = (m1 . i) * (m2 . i) by VECTSP_1:7 .= (m1 * m2) . i by Def2 ; ::_thesis: verum end; hence for i being Nat st i >= (len m1) + 1 holds (m1 * m2) . i = 0. L ; ::_thesis: verum end; hence m1 * m2 is finite-Support by ALGSEQ_1:def_1; ::_thesis: verum end; end; theorem Th11: :: POLYNOM8:11 for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr for m1, m2 being AlgSequence of L holds len (m1 * m2) <= min ((len m1),(len m2)) proof let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for m1, m2 being AlgSequence of L holds len (m1 * m2) <= min ((len m1),(len m2)) let m1, m2 be AlgSequence of L; ::_thesis: len (m1 * m2) <= min ((len m1),(len m2)) set p = m1 * m2; set k = min ((len m1),(len m2)); reconsider k = min ((len m1),(len m2)) as Element of NAT ; now__::_thesis:_for_i_being_Nat_st_i_>=_k_holds_ 0._L_=_(m1_*_m2)_._i let i be Nat; ::_thesis: ( i >= k implies 0. L = (m1 * m2) . b1 ) assume A1: i >= k ; ::_thesis: 0. L = (m1 * m2) . b1 percases ( k = len m1 or k = len m2 ) by XXREAL_0:15; suppose k = len m1 ; ::_thesis: 0. L = (m1 * m2) . b1 then m1 . i = 0. L by A1, ALGSEQ_1:8; hence 0. L = (m1 . i) * (m2 . i) by VECTSP_1:7 .= (m1 * m2) . i by Def2 ; ::_thesis: verum end; suppose k = len m2 ; ::_thesis: 0. L = (m1 * m2) . b1 then m2 . i = 0. L by A1, ALGSEQ_1:8; hence 0. L = (m1 . i) * (m2 . i) by VECTSP_1:6 .= (m1 * m2) . i by Def2 ; ::_thesis: verum end; end; end; then k is_at_least_length_of m1 * m2 by ALGSEQ_1:def_2; hence len (m1 * m2) <= min ((len m1),(len m2)) by ALGSEQ_1:def_3; ::_thesis: verum end; theorem :: POLYNOM8:12 for L being non empty right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr for m1, m2 being AlgSequence of L st len m1 = len m2 holds len (m1 * m2) = len m1 proof let L be non empty right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ; ::_thesis: for m1, m2 being AlgSequence of L st len m1 = len m2 holds len (m1 * m2) = len m1 let m1, m2 be AlgSequence of L; ::_thesis: ( len m1 = len m2 implies len (m1 * m2) = len m1 ) set p = m1 * m2; assume A1: len m1 = len m2 ; ::_thesis: len (m1 * m2) = len m1 A2: now__::_thesis:_(_(_len_m1_=_0_&_len_(m1_*_m2)_>=_len_m1_)_or_(_len_m1_<>_0_&_len_(m1_*_m2)_>=_len_m1_)_) percases ( len m1 = 0 or len m1 <> 0 ) ; case len m1 = 0 ; ::_thesis: len (m1 * m2) >= len m1 hence len (m1 * m2) >= len m1 ; ::_thesis: verum end; case len m1 <> 0 ; ::_thesis: len (m1 * m2) >= len m1 then len m1 >= 0 + 1 by NAT_1:13; then (len m1) - 1 >= 1 - 1 by XREAL_1:9; then reconsider l = (len m1) - 1 as Element of NAT by INT_1:3; A3: l + 1 = (len m1) + 0 ; then ( m1 . l <> 0. L & m2 . l <> 0. L ) by A1, ALGSEQ_1:10; then (m1 . l) * (m2 . l) <> 0. L by VECTSP_2:def_1; then (m1 * m2) . l <> 0. L by Def2; hence len (m1 * m2) >= len m1 by A3, Th7; ::_thesis: verum end; end; end; min ((len m1),(len m2)) = len m1 by A1; then len (m1 * m2) <= len m1 by Th11; hence len (m1 * m2) = len m1 by A2, XXREAL_0:1; ::_thesis: verum end; begin definition let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; let a be Element of L; let i be Integer; func pow (a,i) -> Element of L equals :Def3: :: POLYNOM8:def 3 (power L) . (a,i) if 0 <= i otherwise ((power L) . (a,(abs i))) " ; coherence ( ( 0 <= i implies (power L) . (a,i) is Element of L ) & ( not 0 <= i implies ((power L) . (a,(abs i))) " is Element of L ) ) proof ( 0 <= i implies (power L) . (a,i) is Element of L ) proof assume 0 <= i ; ::_thesis: (power L) . (a,i) is Element of L then reconsider i9 = i as Element of NAT by INT_1:3; (power L) . (a,i9) is Element of L ; hence (power L) . (a,i) is Element of L ; ::_thesis: verum end; hence ( ( 0 <= i implies (power L) . (a,i) is Element of L ) & ( not 0 <= i implies ((power L) . (a,(abs i))) " is Element of L ) ) ; ::_thesis: verum end; consistency for b1 being Element of L holds verum ; end; :: deftheorem Def3 defines pow POLYNOM8:def_3_:_ for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr for a being Element of L for i being Integer holds ( ( 0 <= i implies pow (a,i) = (power L) . (a,i) ) & ( not 0 <= i implies pow (a,i) = ((power L) . (a,(abs i))) " ) ); theorem Th13: :: POLYNOM8:13 for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr for x being Element of L holds pow (x,0) = 1. L proof let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for x being Element of L holds pow (x,0) = 1. L let x be Element of L; ::_thesis: pow (x,0) = 1. L pow (x,0) = x |^ 0 by Def3 .= 1_ L by BINOM:8 ; hence pow (x,0) = 1. L ; ::_thesis: verum end; Lm3: for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr for a being Element of L for i being Integer st 0 > i holds pow (a,i) = (pow (a,(abs i))) " proof let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for a being Element of L for i being Integer st 0 > i holds pow (a,i) = (pow (a,(abs i))) " let a be Element of L; ::_thesis: for i being Integer st 0 > i holds pow (a,i) = (pow (a,(abs i))) " let i be Integer; ::_thesis: ( 0 > i implies pow (a,i) = (pow (a,(abs i))) " ) assume A1: 0 > i ; ::_thesis: pow (a,i) = (pow (a,(abs i))) " pow (a,(abs i)) = (power L) . (a,(abs i)) by Def3; hence pow (a,i) = (pow (a,(abs i))) " by A1, Def3; ::_thesis: verum end; Lm4: for L being non empty non degenerated almost_left_invertible associative commutative well-unital distributive doubleLoopStr for i being Integer for x being Element of L st i <= 0 holds pow (x,i) = (pow (x,(abs i))) " proof let L be non empty non degenerated almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for i being Integer for x being Element of L st i <= 0 holds pow (x,i) = (pow (x,(abs i))) " let i be Integer; ::_thesis: for x being Element of L st i <= 0 holds pow (x,i) = (pow (x,(abs i))) " let x be Element of L; ::_thesis: ( i <= 0 implies pow (x,i) = (pow (x,(abs i))) " ) A1: 1. L <> 0. L ; assume A2: i <= 0 ; ::_thesis: pow (x,i) = (pow (x,(abs i))) " percases ( i < 0 or i = 0 ) by A2; suppose i < 0 ; ::_thesis: pow (x,i) = (pow (x,(abs i))) " hence pow (x,i) = (pow (x,(abs i))) " by Lm3; ::_thesis: verum end; supposeA3: i = 0 ; ::_thesis: pow (x,i) = (pow (x,(abs i))) " hence pow (x,i) = 1. L by Th13 .= (1. L) * ((1. L) ") by A1, VECTSP_1:def_10 .= (1_ L) " by VECTSP_1:def_8 .= (x |^ 0) " by BINOM:8 .= (x |^ (abs i)) " by A3, ABSVALUE:def_1 .= (pow (x,(abs i))) " by Def3 ; ::_thesis: verum end; end; end; theorem Th14: :: POLYNOM8:14 for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr for x being Element of L holds pow (x,1) = x proof let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for x being Element of L holds pow (x,1) = x let x be Element of L; ::_thesis: pow (x,1) = x thus pow (x,1) = x |^ 1 by Def3 .= x by BINOM:8 ; ::_thesis: verum end; theorem Th15: :: POLYNOM8:15 for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr for x being Element of L holds pow (x,(- 1)) = x " proof let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for x being Element of L holds pow (x,(- 1)) = x " let x be Element of L; ::_thesis: pow (x,(- 1)) = x " abs (- 1) = - (- 1) by ABSVALUE:def_1; hence pow (x,(- 1)) = (pow (x,1)) " by Lm3 .= x " by Th14 ; ::_thesis: verum end; Lm5: for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr for i being Element of NAT holds pow ((1. L),i) = 1. L proof let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for i being Element of NAT holds pow ((1. L),i) = 1. L let i be Element of NAT ; ::_thesis: pow ((1. L),i) = 1. L defpred S1[ Element of NAT ] means pow ((1. L),$1) = 1. L; A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] pow ((1. L),(k + 1)) = (power L) . ((1. L),(k + 1)) by Def3 .= ((power L) . ((1. L),k)) * (1. L) by GROUP_1:def_7 .= (1. L) * (1. L) by A2, Def3 .= 1. L by VECTSP_1:def_8 ; hence S1[k + 1] ; ::_thesis: verum end; pow ((1_ L),0) = (power L) . ((1. L),0) by Def3; then A3: S1[ 0 ] by GROUP_1:def_7; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A1); hence pow ((1. L),i) = 1. L ; ::_thesis: verum end; theorem Th16: :: POLYNOM8:16 for L being non empty non degenerated almost_left_invertible associative commutative well-unital distributive doubleLoopStr for i being Integer holds pow ((1. L),i) = 1. L proof let L be non empty non degenerated almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for i being Integer holds pow ((1. L),i) = 1. L let i be Integer; ::_thesis: pow ((1. L),i) = 1. L percases ( 0 <= i or 0 > i ) ; suppose 0 <= i ; ::_thesis: pow ((1. L),i) = 1. L then i is Element of NAT by INT_1:3; hence pow ((1. L),i) = 1. L by Lm5; ::_thesis: verum end; supposeA1: 0 > i ; ::_thesis: pow ((1. L),i) = 1. L A2: ( 1. L <> 0. L & (1. L) * (1. L) = 1. L ) by VECTSP_1:def_4; A3: pow ((1. L),(abs i)) = 1. L by Lm5; pow ((1. L),i) = ((power L) . ((1. L),(abs i))) " by A1, Def3 .= (1. L) " by A3, Def3 ; hence pow ((1. L),i) = 1. L by A2, VECTSP_1:def_10; ::_thesis: verum end; end; end; theorem Th17: :: POLYNOM8:17 for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr for x being Element of L for n being Element of NAT holds ( pow (x,(n + 1)) = (pow (x,n)) * x & pow (x,(n + 1)) = x * (pow (x,n)) ) proof let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for x being Element of L for n being Element of NAT holds ( pow (x,(n + 1)) = (pow (x,n)) * x & pow (x,(n + 1)) = x * (pow (x,n)) ) let x be Element of L; ::_thesis: for n being Element of NAT holds ( pow (x,(n + 1)) = (pow (x,n)) * x & pow (x,(n + 1)) = x * (pow (x,n)) ) let n be Element of NAT ; ::_thesis: ( pow (x,(n + 1)) = (pow (x,n)) * x & pow (x,(n + 1)) = x * (pow (x,n)) ) pow (x,(n + 1)) = x |^ (n + 1) by Def3 .= (x |^ n) * x by GROUP_1:def_7 .= (pow (x,n)) * x by Def3 ; hence ( pow (x,(n + 1)) = (pow (x,n)) * x & pow (x,(n + 1)) = x * (pow (x,n)) ) ; ::_thesis: verum end; Lm6: for L being non empty well-unital doubleLoopStr for n being Element of NAT holds (1. L) |^ n = 1. L proof let L be non empty well-unital doubleLoopStr ; ::_thesis: for n being Element of NAT holds (1. L) |^ n = 1. L let n be Element of NAT ; ::_thesis: (1. L) |^ n = 1. L defpred S1[ Element of NAT ] means (1. L) |^ $1 = 1_ L; A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] (1. L) |^ (k + 1) = ((1. L) |^ k) * (1. L) by GROUP_1:def_7 .= 1. L by A2, VECTSP_1:def_8 ; hence S1[k + 1] ; ::_thesis: verum end; A3: S1[ 0 ] by BINOM:8; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A1); hence (1. L) |^ n = 1. L ; ::_thesis: verum end; Lm7: for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr for m being Element of NAT for x being Element of L st x <> 0. L holds (x |^ m) * ((x ") |^ m) = 1. L proof let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for m being Element of NAT for x being Element of L st x <> 0. L holds (x |^ m) * ((x ") |^ m) = 1. L let m be Element of NAT ; ::_thesis: for x being Element of L st x <> 0. L holds (x |^ m) * ((x ") |^ m) = 1. L let x be Element of L; ::_thesis: ( x <> 0. L implies (x |^ m) * ((x ") |^ m) = 1. L ) assume A1: x <> 0. L ; ::_thesis: (x |^ m) * ((x ") |^ m) = 1. L (x |^ m) * ((x ") |^ m) = (x * (x ")) |^ m by BINOM:9 .= (1. L) |^ m by A1, VECTSP_1:def_10 .= 1. L by Lm6 ; hence (x |^ m) * ((x ") |^ m) = 1. L ; ::_thesis: verum end; theorem Th18: :: POLYNOM8:18 for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr for i being Integer for x being Element of L st x <> 0. L holds (pow (x,i)) " = pow (x,(- i)) proof let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for i being Integer for x being Element of L st x <> 0. L holds (pow (x,i)) " = pow (x,(- i)) let i be Integer; ::_thesis: for x being Element of L st x <> 0. L holds (pow (x,i)) " = pow (x,(- i)) let x be Element of L; ::_thesis: ( x <> 0. L implies (pow (x,i)) " = pow (x,(- i)) ) assume A1: x <> 0. L ; ::_thesis: (pow (x,i)) " = pow (x,(- i)) A2: 1. L <> 0. L ; percases ( i >= 0 or i < 0 ) ; supposeA3: i >= 0 ; ::_thesis: (pow (x,i)) " = pow (x,(- i)) percases ( - i < - 0 or i = 0 ) by A3, XREAL_1:24; supposeA4: - i < - 0 ; ::_thesis: (pow (x,i)) " = pow (x,(- i)) hence pow (x,(- i)) = (pow (x,(abs (- i)))) " by Lm3 .= (pow (x,(- (- i)))) " by A4, ABSVALUE:def_1 .= (pow (x,i)) " ; ::_thesis: verum end; supposeA5: i = 0 ; ::_thesis: (pow (x,i)) " = pow (x,(- i)) hence pow (x,(- i)) = 1. L by Th13 .= (1. L) * ((1. L) ") by A2, VECTSP_1:def_10 .= (1. L) " by VECTSP_1:def_8 .= (pow (x,i)) " by A5, Th13 ; ::_thesis: verum end; end; end; supposeA6: i < 0 ; ::_thesis: (pow (x,i)) " = pow (x,(- i)) A7: pow (x,(abs i)) = x |^ (abs i) by Def3; pow (x,i) = (pow (x,(abs i))) " by A6, Lm3; then (pow (x,i)) " = pow (x,(abs i)) by A1, A7, Th1, VECTSP_1:24; hence (pow (x,i)) " = pow (x,(- i)) by A6, ABSVALUE:def_1; ::_thesis: verum end; end; end; theorem Th19: :: POLYNOM8:19 for L being Field for j being Integer for x being Element of L st x <> 0. L holds pow (x,(j + 1)) = (pow (x,j)) * (pow (x,1)) proof let L be Field; ::_thesis: for j being Integer for x being Element of L st x <> 0. L holds pow (x,(j + 1)) = (pow (x,j)) * (pow (x,1)) let j be Integer; ::_thesis: for x being Element of L st x <> 0. L holds pow (x,(j + 1)) = (pow (x,j)) * (pow (x,1)) let x be Element of L; ::_thesis: ( x <> 0. L implies pow (x,(j + 1)) = (pow (x,j)) * (pow (x,1)) ) A1: pow (x,(- 1)) = (x |^ (abs (- 1))) " by Def3; assume A2: x <> 0. L ; ::_thesis: pow (x,(j + 1)) = (pow (x,j)) * (pow (x,1)) then x |^ (abs (- 1)) <> 0. L by Th1; then A3: pow (x,(- 1)) <> 0. L by A1, VECTSP_1:25; A4: pow (x,(- j)) <> 0. L proof percases ( 0 <= - j or - j < 0 ) ; suppose 0 <= - j ; ::_thesis: pow (x,(- j)) <> 0. L then reconsider k = - j as Element of NAT by INT_1:3; pow (x,(- j)) = x |^ k by Def3; hence pow (x,(- j)) <> 0. L by A2, Th1; ::_thesis: verum end; supposeA5: - j < 0 ; ::_thesis: pow (x,(- j)) <> 0. L A6: x |^ (abs (- j)) <> 0. L by A2, Th1; pow (x,(- j)) = (x |^ (abs (- j))) " by A5, Def3; hence pow (x,(- j)) <> 0. L by A6, VECTSP_1:25; ::_thesis: verum end; end; end; A7: pow (x,(j + 1)) <> 0. L proof percases ( 0 <= j + 1 or j + 1 < 0 ) ; suppose 0 <= j + 1 ; ::_thesis: pow (x,(j + 1)) <> 0. L then reconsider k = j + 1 as Element of NAT by INT_1:3; pow (x,(j + 1)) = x |^ k by Def3; hence pow (x,(j + 1)) <> 0. L by A2, Th1; ::_thesis: verum end; supposeA8: j + 1 < 0 ; ::_thesis: pow (x,(j + 1)) <> 0. L A9: x |^ (abs (j + 1)) <> 0. L by A2, Th1; pow (x,(j + 1)) = (x |^ (abs (j + 1))) " by A8, Def3; hence pow (x,(j + 1)) <> 0. L by A9, VECTSP_1:25; ::_thesis: verum end; end; end; A10: now__::_thesis:_(pow_(x,(j_+_1)))_*_((pow_(x,(-_1)))_*_(pow_(x,(-_j))))_=_1._L percases ( j >= 0 or j < - 1 or j = - 1 ) by Lm1; supposeA11: j >= 0 ; ::_thesis: (pow (x,(j + 1))) * ((pow (x,(- 1))) * (pow (x,(- j)))) = 1. L then reconsider n = j as Element of NAT by INT_1:3; A12: n + 1 = abs (j + 1) by ABSVALUE:def_1; pow (x,(abs j)) = x |^ (abs j) by Def3; then A13: pow (x,(abs j)) <> 0. L by A2, Th1; pow (x,(abs (j + 1))) = x |^ (abs (j + 1)) by Def3; then A14: pow (x,(abs (j + 1))) <> 0. L by A2, Th1; n + 1 >= 0 ; hence (pow (x,(j + 1))) * ((pow (x,(- 1))) * (pow (x,(- j)))) = (pow (x,(abs (j + 1)))) * ((pow (x,(- 1))) * (pow (x,(- j)))) by ABSVALUE:def_1 .= (pow (x,(abs (j + 1)))) * ((x ") * (pow (x,(- j)))) by Th15 .= (pow (x,(abs (j + 1)))) * ((x ") * ((pow (x,j)) ")) by A2, Th18 .= (pow (x,(abs (j + 1)))) * ((x ") * ((pow (x,(abs j))) ")) by A11, ABSVALUE:def_1 .= (pow (x,(abs (j + 1)))) * ((x * (pow (x,(abs j)))) ") by A2, A13, Th2 .= (pow (x,(abs (j + 1)))) * ((pow (x,((abs j) + 1))) ") by Th17 .= (pow (x,(abs (j + 1)))) * ((pow (x,(abs (j + 1)))) ") by A12, ABSVALUE:def_1 .= 1. L by A14, VECTSP_1:def_10 ; ::_thesis: verum end; supposeA15: j < - 1 ; ::_thesis: (pow (x,(j + 1))) * ((pow (x,(- 1))) * (pow (x,(- j)))) = 1. L A16: pow (x,(- j)) <> 0. L proof reconsider k = - j as Element of NAT by A15, INT_1:3; pow (x,(- j)) = x |^ k by Def3; hence pow (x,(- j)) <> 0. L by A2, Th1; ::_thesis: verum end; pow (x,(abs (j + 1))) = x |^ (abs (j + 1)) by Def3; then A17: pow (x,(abs (j + 1))) <> 0. L by A2, Th1; A18: j + 1 < (- 1) + 1 by A15, XREAL_1:6; hence (pow (x,(j + 1))) * ((pow (x,(- 1))) * (pow (x,(- j)))) = ((pow (x,(abs (j + 1)))) ") * ((pow (x,(- 1))) * (pow (x,(- j)))) by Lm3 .= ((pow (x,(abs (j + 1)))) ") * ((x ") * (pow (x,(- j)))) by Th15 .= (((pow (x,(abs (j + 1)))) ") * (x ")) * (pow (x,(- j))) by GROUP_1:def_3 .= (((pow (x,(abs (j + 1)))) * x) ") * (pow (x,(- j))) by A2, A17, Th2 .= ((pow (x,((abs (j + 1)) + 1))) ") * (pow (x,(- j))) by Th17 .= ((pow (x,((- (j + 1)) + 1))) ") * (pow (x,(- j))) by A18, ABSVALUE:def_1 .= 1. L by A16, VECTSP_1:def_10 ; ::_thesis: verum end; supposeA19: j = - 1 ; ::_thesis: (pow (x,(j + 1))) * ((pow (x,(- 1))) * (pow (x,(- j)))) = 1. L A20: x " <> 0. L by A2, VECTSP_1:25; thus (pow (x,(j + 1))) * ((pow (x,(- 1))) * (pow (x,(- j)))) = (1. L) * ((pow (x,(- 1))) * (pow (x,(- j)))) by A19, Th13 .= (pow (x,(- 1))) * (pow (x,(- j))) by VECTSP_1:def_8 .= (x ") * (pow (x,(- j))) by Th15 .= (x ") * ((pow (x,j)) ") by A2, Th18 .= (x ") * ((x ") ") by A19, Th15 .= 1. L by A20, VECTSP_1:def_10 ; ::_thesis: verum end; end; end; A21: pow (x,(j + 1)) <> 0. L proof percases ( 0 <= j + 1 or j + 1 < 0 ) ; suppose 0 <= j + 1 ; ::_thesis: pow (x,(j + 1)) <> 0. L then reconsider k = j + 1 as Element of NAT by INT_1:3; pow (x,(j + 1)) = x |^ k by Def3; hence pow (x,(j + 1)) <> 0. L by A2, Th1; ::_thesis: verum end; supposeA22: j + 1 < 0 ; ::_thesis: pow (x,(j + 1)) <> 0. L A23: x |^ (abs (j + 1)) <> 0. L by A2, Th1; pow (x,(j + 1)) = (x |^ (abs (j + 1))) " by A22, Def3; hence pow (x,(j + 1)) <> 0. L by A23, VECTSP_1:25; ::_thesis: verum end; end; end; (pow (x,(j + 1))) * (pow (x,(- (j + 1)))) = (pow (x,(j + 1))) * ((pow (x,(j + 1))) ") by A2, Th18 .= 1. L by A7, VECTSP_1:def_10 ; then A24: pow (x,(- (j + 1))) = (pow (x,(- 1))) * (pow (x,(- j))) by A10, A21, VECTSP_1:5; thus pow (x,(j + 1)) = pow (x,(- (- (j + 1)))) .= ((pow (x,(- 1))) * (pow (x,(- j)))) " by A2, A24, Th18 .= ((pow (x,(- j))) ") * ((pow (x,(- 1))) ") by A4, A3, Th2 .= (pow (x,(- (- j)))) * ((pow (x,(- 1))) ") by A2, Th18 .= (pow (x,j)) * (pow (x,(- (- 1)))) by A2, Th18 .= (pow (x,j)) * (pow (x,1)) ; ::_thesis: verum end; theorem Th20: :: POLYNOM8:20 for L being Field for j being Integer for x being Element of L st x <> 0. L holds pow (x,(j - 1)) = (pow (x,j)) * (pow (x,(- 1))) proof let L be Field; ::_thesis: for j being Integer for x being Element of L st x <> 0. L holds pow (x,(j - 1)) = (pow (x,j)) * (pow (x,(- 1))) let j be Integer; ::_thesis: for x being Element of L st x <> 0. L holds pow (x,(j - 1)) = (pow (x,j)) * (pow (x,(- 1))) let x be Element of L; ::_thesis: ( x <> 0. L implies pow (x,(j - 1)) = (pow (x,j)) * (pow (x,(- 1))) ) assume A1: x <> 0. L ; ::_thesis: pow (x,(j - 1)) = (pow (x,j)) * (pow (x,(- 1))) A2: pow (x,(j - 1)) <> 0. L proof percases ( 0 <= j - 1 or j - 1 < 0 ) ; suppose 0 <= j - 1 ; ::_thesis: pow (x,(j - 1)) <> 0. L then reconsider k = j - 1 as Element of NAT by INT_1:3; pow (x,(j - 1)) = x |^ k by Def3; hence pow (x,(j - 1)) <> 0. L by A1, Th1; ::_thesis: verum end; supposeA3: j - 1 < 0 ; ::_thesis: pow (x,(j - 1)) <> 0. L A4: x |^ (abs (j - 1)) <> 0. L by A1, Th1; pow (x,(j - 1)) = (x |^ (abs (j - 1))) " by A3, Def3; hence pow (x,(j - 1)) <> 0. L by A4, VECTSP_1:25; ::_thesis: verum end; end; end; A5: now__::_thesis:_(pow_(x,(j_-_1)))_*_(x_*_(pow_(x,(-_j))))_=_1._L percases ( j >= 1 or j < 0 or j = 0 ) by Lm2; supposeA6: j >= 1 ; ::_thesis: (pow (x,(j - 1))) * (x * (pow (x,(- j)))) = 1. L then A7: abs j = j by ABSVALUE:def_1; pow (x,(abs (- j))) = x |^ (abs (- j)) by Def3; then A8: pow (x,(abs (- j))) <> 0. L by A1, Th1; A9: abs j = abs (- j) by COMPLEX1:52; j >= 1 + 0 by A6; then A10: j - 1 >= 0 by XREAL_1:19; then A11: (abs (j - 1)) + 1 = (j - 1) + 1 by ABSVALUE:def_1 .= j ; thus (pow (x,(j - 1))) * (x * (pow (x,(- j)))) = ((pow (x,(j - 1))) * x) * (pow (x,(- j))) by GROUP_1:def_3 .= ((pow (x,(abs (j - 1)))) * x) * (pow (x,(- j))) by A10, ABSVALUE:def_1 .= ((pow (x,(abs (j - 1)))) * x) * ((pow (x,(abs (- j)))) ") by A6, Lm4 .= (pow (x,((abs (j - 1)) + 1))) * ((pow (x,(abs (- j)))) ") by Th17 .= 1. L by A8, A11, A7, A9, VECTSP_1:def_10 ; ::_thesis: verum end; supposeA12: j < 0 ; ::_thesis: (pow (x,(j - 1))) * (x * (pow (x,(- j)))) = 1. L pow (x,(abs (j - 1))) = x |^ (abs (j - 1)) by Def3; then A13: pow (x,(abs (j - 1))) <> 0. L by A1, Th1; A14: 1 - j = - (j - 1) ; thus (pow (x,(j - 1))) * (x * (pow (x,(- j)))) = ((pow (x,(abs (j - 1)))) ") * (x * (pow (x,(- j)))) by A12, Lm3 .= ((pow (x,(abs (j - 1)))) ") * (x * (pow (x,(abs (- j))))) by A12, ABSVALUE:def_1 .= ((pow (x,(abs (j - 1)))) ") * (pow (x,(1 + (abs (- j))))) by Th17 .= ((pow (x,(abs (j - 1)))) ") * (pow (x,(1 + (- j)))) by A12, ABSVALUE:def_1 .= ((pow (x,(abs (j - 1)))) ") * (pow (x,(abs (j - 1)))) by A12, A14, ABSVALUE:def_1 .= 1. L by A13, VECTSP_1:def_10 ; ::_thesis: verum end; supposeA15: j = 0 ; ::_thesis: (pow (x,(j - 1))) * (x * (pow (x,(- j)))) = 1. L hence (pow (x,(j - 1))) * (x * (pow (x,(- j)))) = (x ") * (x * (pow (x,(- j)))) by Th15 .= ((x ") * x) * (pow (x,(- j))) by GROUP_1:def_3 .= (1. L) * (pow (x,(- j))) by A1, VECTSP_1:def_10 .= pow (x,0) by A15, VECTSP_1:def_8 .= 1. L by Th13 ; ::_thesis: verum end; end; end; A16: pow (x,(- j)) <> 0. L proof percases ( 0 <= - j or - j < 0 ) ; suppose 0 <= - j ; ::_thesis: pow (x,(- j)) <> 0. L then reconsider k = - j as Element of NAT by INT_1:3; pow (x,(- j)) = x |^ k by Def3; hence pow (x,(- j)) <> 0. L by A1, Th1; ::_thesis: verum end; supposeA17: - j < 0 ; ::_thesis: pow (x,(- j)) <> 0. L A18: x |^ (abs (- j)) <> 0. L by A1, Th1; pow (x,(- j)) = (x |^ (abs (- j))) " by A17, Def3; hence pow (x,(- j)) <> 0. L by A18, VECTSP_1:25; ::_thesis: verum end; end; end; A19: pow (x,(j - 1)) <> 0. L proof percases ( 0 <= j - 1 or j - 1 < 0 ) ; suppose 0 <= j - 1 ; ::_thesis: pow (x,(j - 1)) <> 0. L then reconsider k = j - 1 as Element of NAT by INT_1:3; pow (x,(j - 1)) = x |^ k by Def3; hence pow (x,(j - 1)) <> 0. L by A1, Th1; ::_thesis: verum end; supposeA20: j - 1 < 0 ; ::_thesis: pow (x,(j - 1)) <> 0. L A21: x |^ (abs (j - 1)) <> 0. L by A1, Th1; pow (x,(j - 1)) = (x |^ (abs (j - 1))) " by A20, Def3; hence pow (x,(j - 1)) <> 0. L by A21, VECTSP_1:25; ::_thesis: verum end; end; end; (pow (x,(j - 1))) * (pow (x,(1 - j))) = (pow (x,(j - 1))) * (pow (x,(- (j - 1)))) .= (pow (x,(j - 1))) * ((pow (x,(j - 1))) ") by A1, Th18 .= 1. L by A2, VECTSP_1:def_10 ; then x * (pow (x,(- j))) = pow (x,(1 - j)) by A5, A19, VECTSP_1:5; then (pow (x,(1 - j))) " = ((pow (x,(- j))) ") * (x ") by A1, A16, Th2 .= (pow (x,(- (- j)))) * (x ") by A1, Th18 .= (pow (x,j)) * (pow (x,(- 1))) by Th15 ; then (pow (x,j)) * (pow (x,(- 1))) = pow (x,(- (1 - j))) by A1, Th18; hence pow (x,(j - 1)) = (pow (x,j)) * (pow (x,(- 1))) ; ::_thesis: verum end; theorem Th21: :: POLYNOM8:21 for L being Field for i, j being Integer for x being Element of L st x <> 0. L holds (pow (x,i)) * (pow (x,j)) = pow (x,(i + j)) proof let L be Field; ::_thesis: for i, j being Integer for x being Element of L st x <> 0. L holds (pow (x,i)) * (pow (x,j)) = pow (x,(i + j)) let i, j be Integer; ::_thesis: for x being Element of L st x <> 0. L holds (pow (x,i)) * (pow (x,j)) = pow (x,(i + j)) let x be Element of L; ::_thesis: ( x <> 0. L implies (pow (x,i)) * (pow (x,j)) = pow (x,(i + j)) ) defpred S1[ Integer] means for i being Integer holds pow (x,(i + $1)) = (pow (x,i)) * (pow (x,$1)); assume A1: x <> 0. L ; ::_thesis: (pow (x,i)) * (pow (x,j)) = pow (x,(i + j)) A2: for j being Integer st S1[j] holds ( S1[j - 1] & S1[j + 1] ) proof let j be Integer; ::_thesis: ( S1[j] implies ( S1[j - 1] & S1[j + 1] ) ) assume A3: for i being Integer holds pow (x,(i + j)) = (pow (x,i)) * (pow (x,j)) ; ::_thesis: ( S1[j - 1] & S1[j + 1] ) thus for i being Integer holds pow (x,(i + (j - 1))) = (pow (x,i)) * (pow (x,(j - 1))) ::_thesis: S1[j + 1] proof let i be Integer; ::_thesis: pow (x,(i + (j - 1))) = (pow (x,i)) * (pow (x,(j - 1))) thus pow (x,(i + (j - 1))) = pow (x,((i - 1) + j)) .= (pow (x,(i - 1))) * (pow (x,j)) by A3 .= ((pow (x,i)) * (pow (x,(- 1)))) * (pow (x,j)) by A1, Th20 .= (pow (x,i)) * ((pow (x,(- 1))) * (pow (x,j))) by GROUP_1:def_3 .= (pow (x,i)) * (pow (x,(j + (- 1)))) by A3 .= (pow (x,i)) * (pow (x,(j - 1))) ; ::_thesis: verum end; let i be Integer; ::_thesis: pow (x,(i + (j + 1))) = (pow (x,i)) * (pow (x,(j + 1))) thus pow (x,(i + (j + 1))) = pow (x,((i + 1) + j)) .= (pow (x,(i + 1))) * (pow (x,j)) by A3 .= ((pow (x,i)) * (pow (x,1))) * (pow (x,j)) by A1, Th19 .= (pow (x,i)) * ((pow (x,1)) * (pow (x,j))) by GROUP_1:def_3 .= (pow (x,i)) * (pow (x,(j + 1))) by A3 ; ::_thesis: verum end; A4: S1[ 0 ] proof let i be Integer; ::_thesis: pow (x,(i + 0)) = (pow (x,i)) * (pow (x,0)) thus pow (x,(i + 0)) = (pow (x,i)) * (1. L) by VECTSP_1:def_4 .= (pow (x,i)) * (pow (x,0)) by Th13 ; ::_thesis: verum end; for j being Integer holds S1[j] from INT_1:sch_4(A4, A2); hence (pow (x,i)) * (pow (x,j)) = pow (x,(i + j)) ; ::_thesis: verum end; Lm8: for L being non empty non degenerated right_complementable almost_left_invertible associative commutative left-distributive well-unital add-associative right_zeroed doubleLoopStr for k being Element of NAT for x being Element of L st x <> 0. L holds (x ") |^ k = (x |^ k) " proof let L be non empty non degenerated right_complementable almost_left_invertible associative commutative left-distributive well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for k being Element of NAT for x being Element of L st x <> 0. L holds (x ") |^ k = (x |^ k) " let k be Element of NAT ; ::_thesis: for x being Element of L st x <> 0. L holds (x ") |^ k = (x |^ k) " let x be Element of L; ::_thesis: ( x <> 0. L implies (x ") |^ k = (x |^ k) " ) A1: 1. L <> 0. L ; defpred S1[ Element of NAT ] means (x ") |^ $1 = (x |^ $1) " ; assume A2: x <> 0. L ; ::_thesis: (x ") |^ k = (x |^ k) " A3: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A4: S1[n] ; ::_thesis: S1[n + 1] A5: x |^ n <> 0. L by A2, Th1; (x ") |^ (n + 1) = ((x ") |^ n) * (x ") by GROUP_1:def_7 .= (x * (x |^ n)) " by A2, A4, A5, Th2 .= ((x |^ 1) * (x |^ n)) " by BINOM:8 .= (x |^ (n + 1)) " by BINOM:10 ; hence S1[n + 1] ; ::_thesis: verum end; (x ") |^ 0 = 1_ L by BINOM:8 .= (1. L) * ((1. L) ") by A1, VECTSP_1:def_10 .= (1_ L) " by VECTSP_1:def_8 .= (x |^ 0) " by BINOM:8 ; then A6: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A3); hence (x ") |^ k = (x |^ k) " ; ::_thesis: verum end; theorem Th22: :: POLYNOM8:22 for L being non empty non degenerated right_complementable almost_left_invertible associative commutative left-distributive well-unital add-associative right_zeroed doubleLoopStr for k being Element of NAT for x being Element of L st x <> 0. L holds pow ((x "),k) = pow (x,(- k)) proof let L be non empty non degenerated right_complementable almost_left_invertible associative commutative left-distributive well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for k being Element of NAT for x being Element of L st x <> 0. L holds pow ((x "),k) = pow (x,(- k)) let k be Element of NAT ; ::_thesis: for x being Element of L st x <> 0. L holds pow ((x "),k) = pow (x,(- k)) let x be Element of L; ::_thesis: ( x <> 0. L implies pow ((x "),k) = pow (x,(- k)) ) assume A1: x <> 0. L ; ::_thesis: pow ((x "),k) = pow (x,(- k)) pow ((x "),k) = (x ") |^ k by Def3 .= (x |^ k) " by A1, Lm8 .= (pow (x,k)) " by Def3 .= pow (x,(- k)) by A1, Th18 ; hence pow ((x "),k) = pow (x,(- k)) ; ::_thesis: verum end; theorem Th23: :: POLYNOM8:23 for L being Field for x being Element of L st x <> 0. L holds for i, j, k being Nat holds (pow (x,((i - 1) * (k - 1)))) * (pow (x,(- ((j - 1) * (k - 1))))) = pow (x,((i - j) * (k - 1))) proof let L be Field; ::_thesis: for x being Element of L st x <> 0. L holds for i, j, k being Nat holds (pow (x,((i - 1) * (k - 1)))) * (pow (x,(- ((j - 1) * (k - 1))))) = pow (x,((i - j) * (k - 1))) let x be Element of L; ::_thesis: ( x <> 0. L implies for i, j, k being Nat holds (pow (x,((i - 1) * (k - 1)))) * (pow (x,(- ((j - 1) * (k - 1))))) = pow (x,((i - j) * (k - 1))) ) assume A1: x <> 0. L ; ::_thesis: for i, j, k being Nat holds (pow (x,((i - 1) * (k - 1)))) * (pow (x,(- ((j - 1) * (k - 1))))) = pow (x,((i - j) * (k - 1))) let i, j, k be Nat; ::_thesis: (pow (x,((i - 1) * (k - 1)))) * (pow (x,(- ((j - 1) * (k - 1))))) = pow (x,((i - j) * (k - 1))) (pow (x,((i - 1) * (k - 1)))) * (pow (x,(- ((j - 1) * (k - 1))))) = pow (x,(((i - 1) * (k - 1)) + (- ((j - 1) * (k - 1))))) by A1, Th21 .= pow (x,((i - j) * (k - 1))) ; hence (pow (x,((i - 1) * (k - 1)))) * (pow (x,(- ((j - 1) * (k - 1))))) = pow (x,((i - j) * (k - 1))) ; ::_thesis: verum end; theorem Th24: :: POLYNOM8:24 for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr for x being Element of L for n, m being Element of NAT holds pow (x,(n * m)) = pow ((pow (x,n)),m) proof let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for x being Element of L for n, m being Element of NAT holds pow (x,(n * m)) = pow ((pow (x,n)),m) let x be Element of L; ::_thesis: for n, m being Element of NAT holds pow (x,(n * m)) = pow ((pow (x,n)),m) let n, m be Element of NAT ; ::_thesis: pow (x,(n * m)) = pow ((pow (x,n)),m) pow (x,(n * m)) = x |^ (n * m) by Def3 .= (x |^ n) |^ m by BINOM:11 .= pow ((x |^ n),m) by Def3 .= pow ((pow (x,n)),m) by Def3 ; hence pow (x,(n * m)) = pow ((pow (x,n)),m) ; ::_thesis: verum end; Lm9: for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr for x being Element of L st x <> 0. L holds for n being Element of NAT holds pow ((x "),n) = (pow (x,n)) " proof let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for x being Element of L st x <> 0. L holds for n being Element of NAT holds pow ((x "),n) = (pow (x,n)) " let x be Element of L; ::_thesis: ( x <> 0. L implies for n being Element of NAT holds pow ((x "),n) = (pow (x,n)) " ) A1: 1. L <> 0. L ; defpred S1[ Nat] means pow ((x "),$1) = (pow (x,$1)) " ; assume A2: x <> 0. L ; ::_thesis: for n being Element of NAT holds pow ((x "),n) = (pow (x,n)) " now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ (_pow_((x_"),(n_+_1))_=_(pow_(x,(n_+_1)))_"_&_S1[n_+_1]_) let n be Element of NAT ; ::_thesis: ( S1[n] implies ( pow ((x "),(n + 1)) = (pow (x,(n + 1))) " & S1[n + 1] ) ) assume A3: S1[n] ; ::_thesis: ( pow ((x "),(n + 1)) = (pow (x,(n + 1))) " & S1[n + 1] ) A4: x |^ n <> 0. L by A2, Th1; thus pow ((x "),(n + 1)) = (x ") |^ (n + 1) by Def3 .= ((x ") |^ n) * (x ") by GROUP_1:def_7 .= (pow ((x "),n)) * (x ") by Def3 .= (((power L) . (x,n)) ") * (x ") by A3, Def3 .= (x * (x |^ n)) " by A2, A4, Th2 .= ((x |^ 1) * (x |^ n)) " by BINOM:8 .= (x |^ (n + 1)) " by BINOM:10 .= (pow (x,(n + 1))) " by Def3 ; ::_thesis: S1[n + 1] hence S1[n + 1] ; ::_thesis: verum end; then A5: for n being Element of NAT st S1[n] holds S1[n + 1] ; let n be Element of NAT ; ::_thesis: pow ((x "),n) = (pow (x,n)) " pow ((x "),0) = 1. L by Th13 .= (1. L) * ((1. L) ") by A1, VECTSP_1:def_10 .= (1. L) " by VECTSP_1:def_8 .= (pow (x,0)) " by Th13 ; then A6: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A5); hence pow ((x "),n) = (pow (x,n)) " ; ::_thesis: verum end; theorem Th25: :: POLYNOM8:25 for L being Field for x being Element of L st x <> 0. L holds for i being Integer holds pow ((x "),i) = (pow (x,i)) " proof let L be Field; ::_thesis: for x being Element of L st x <> 0. L holds for i being Integer holds pow ((x "),i) = (pow (x,i)) " let x be Element of L; ::_thesis: ( x <> 0. L implies for i being Integer holds pow ((x "),i) = (pow (x,i)) " ) assume A1: x <> 0. L ; ::_thesis: for i being Integer holds pow ((x "),i) = (pow (x,i)) " let i be Integer; ::_thesis: pow ((x "),i) = (pow (x,i)) " percases ( i >= 0 or i < 0 ) ; suppose i >= 0 ; ::_thesis: pow ((x "),i) = (pow (x,i)) " then reconsider n = i as Element of NAT by INT_1:3; thus pow ((x "),i) = (pow (x,n)) " by A1, Lm9 .= (pow (x,i)) " ; ::_thesis: verum end; supposeA2: i < 0 ; ::_thesis: pow ((x "),i) = (pow (x,i)) " A3: pow (x,(abs i)) = x |^ (abs i) by Def3; thus pow ((x "),i) = (pow ((x "),(abs i))) " by A2, Lm3 .= pow (((x ") "),(abs i)) by A1, Lm9, VECTSP_1:25 .= pow (x,(abs i)) by A1, VECTSP_1:24 .= ((pow (x,(abs i))) ") " by A1, A3, Th1, VECTSP_1:24 .= (pow (x,i)) " by A2, Lm3 ; ::_thesis: verum end; end; end; theorem Th26: :: POLYNOM8:26 for L being Field for x being Element of L st x <> 0. L holds for i, j being Integer holds pow (x,(i * j)) = pow ((pow (x,i)),j) proof let L be Field; ::_thesis: for x being Element of L st x <> 0. L holds for i, j being Integer holds pow (x,(i * j)) = pow ((pow (x,i)),j) let x be Element of L; ::_thesis: ( x <> 0. L implies for i, j being Integer holds pow (x,(i * j)) = pow ((pow (x,i)),j) ) assume A1: x <> 0. L ; ::_thesis: for i, j being Integer holds pow (x,(i * j)) = pow ((pow (x,i)),j) let i, j be Integer; ::_thesis: pow (x,(i * j)) = pow ((pow (x,i)),j) percases ( ( i >= 0 & j >= 0 ) or ( i >= 0 & j < 0 ) or ( i < 0 & j >= 0 ) or ( j < 0 & i < 0 ) ) ; suppose ( i >= 0 & j >= 0 ) ; ::_thesis: pow (x,(i * j)) = pow ((pow (x,i)),j) then reconsider m = i, n = j as Element of NAT by INT_1:3; thus pow (x,(i * j)) = pow ((pow (x,m)),n) by Th24 .= pow ((pow (x,i)),j) ; ::_thesis: verum end; supposeA2: ( i >= 0 & j < 0 ) ; ::_thesis: pow (x,(i * j)) = pow ((pow (x,i)),j) then reconsider m = i, n = - j as Element of NAT by INT_1:3; A3: pow (x,i) = x |^ m by Def3; then A4: pow (x,i) <> 0. L by A1, Th1; A5: pow ((pow (x,i)),j) = ((pow (x,i)) |^ (abs j)) " by A2, Def3; i * j = - (i * n) ; hence pow (x,(i * j)) = (pow (x,(i * n))) " by A1, Th18 .= pow ((x "),(i * n)) by A1, Th25 .= pow ((pow ((x "),m)),n) by Th24 .= pow (((pow (x,i)) "),n) by A1, Th25 .= (pow (((pow (x,i)) "),j)) " by A4, Th18, VECTSP_1:25 .= ((pow ((pow (x,i)),j)) ") " by A1, A3, Th1, Th25 .= pow ((pow (x,i)),j) by A4, A5, Th1, VECTSP_1:24 ; ::_thesis: verum end; supposeA6: ( i < 0 & j >= 0 ) ; ::_thesis: pow (x,(i * j)) = pow ((pow (x,i)),j) then reconsider m = - i, n = j as Element of NAT by INT_1:3; A7: pow (x,i) = (x |^ (abs i)) " by A6, Def3; i * j = - (m * j) ; hence pow (x,(i * j)) = (pow (x,(m * j))) " by A1, Th18 .= pow ((x "),(m * j)) by A1, Th25 .= pow ((pow ((x "),m)),n) by Th24 .= pow (((pow ((x "),i)) "),n) by A1, Th18, VECTSP_1:25 .= pow ((((pow (x,i)) ") "),j) by A1, Th25 .= pow ((pow (x,i)),j) by A1, A7, Th1, VECTSP_1:24 ; ::_thesis: verum end; supposeA8: ( j < 0 & i < 0 ) ; ::_thesis: pow (x,(i * j)) = pow ((pow (x,i)),j) then reconsider m = - i, n = - j as Element of NAT by INT_1:3; A9: pow (x,(- i)) = x |^ m by Def3; x " <> 0. L by A1, VECTSP_1:25; then A10: (x ") |^ (abs i) <> 0. L by Th1; A11: pow ((x "),i) = ((x ") |^ (abs i)) " by A8, Def3; (i * j) * ((- 1) * (- 1)) = m * n ; hence pow (x,(i * j)) = pow ((pow (x,m)),n) by Th24 .= (pow ((pow (x,(- i))),j)) " by A1, A9, Th1, Th18 .= (pow (((pow (x,i)) "),j)) " by A1, Th18 .= (pow ((pow ((x "),i)),j)) " by A1, Th25 .= pow (((pow ((x "),i)) "),j) by A11, A10, Th25, VECTSP_1:25 .= pow ((pow (((x ") "),i)),j) by A1, Th25, VECTSP_1:25 .= pow ((pow (x,i)),j) by A1, VECTSP_1:24 ; ::_thesis: verum end; end; end; theorem Th27: :: POLYNOM8:27 for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr for x being Element of L for i, k being Element of NAT st 1 <= k holds pow (x,(i * (k - 1))) = pow ((x |^ i),(k - 1)) proof let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for x being Element of L for i, k being Element of NAT st 1 <= k holds pow (x,(i * (k - 1))) = pow ((x |^ i),(k - 1)) let x be Element of L; ::_thesis: for i, k being Element of NAT st 1 <= k holds pow (x,(i * (k - 1))) = pow ((x |^ i),(k - 1)) let i, k be Element of NAT ; ::_thesis: ( 1 <= k implies pow (x,(i * (k - 1))) = pow ((x |^ i),(k - 1)) ) assume 1 <= k ; ::_thesis: pow (x,(i * (k - 1))) = pow ((x |^ i),(k - 1)) then 0 < k ; then reconsider m = k - 1 as Element of NAT by NAT_1:20; pow (x,(i * (k - 1))) = x |^ (i * m) by Def3 .= (x |^ i) |^ m by BINOM:11 .= pow ((x |^ i),m) by Def3 ; hence pow (x,(i * (k - 1))) = pow ((x |^ i),(k - 1)) ; ::_thesis: verum end; Lm10: for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr for x being Element of L for m being Element of NAT st x <> 0. L & x |^ m = 1. L holds (x ") |^ m = 1. L proof let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for x being Element of L for m being Element of NAT st x <> 0. L & x |^ m = 1. L holds (x ") |^ m = 1. L let x be Element of L; ::_thesis: for m being Element of NAT st x <> 0. L & x |^ m = 1. L holds (x ") |^ m = 1. L let m be Element of NAT ; ::_thesis: ( x <> 0. L & x |^ m = 1. L implies (x ") |^ m = 1. L ) assume ( x <> 0. L & x |^ m = 1. L ) ; ::_thesis: (x ") |^ m = 1. L then (1. L) * ((x ") |^ m) = 1. L by Lm7; hence (x ") |^ m = 1. L by VECTSP_1:def_4; ::_thesis: verum end; Lm11: for L being non empty non degenerated almost_left_invertible associative commutative well-unital distributive doubleLoopStr for x being Element of L for i being Element of NAT st x <> 0. L & (x ") |^ i = 1. L holds x |^ i = 1. L proof let L be non empty non degenerated almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for x being Element of L for i being Element of NAT st x <> 0. L & (x ") |^ i = 1. L holds x |^ i = 1. L let x be Element of L; ::_thesis: for i being Element of NAT st x <> 0. L & (x ") |^ i = 1. L holds x |^ i = 1. L let i be Element of NAT ; ::_thesis: ( x <> 0. L & (x ") |^ i = 1. L implies x |^ i = 1. L ) assume that A1: x <> 0. L and A2: (x ") |^ i = 1. L ; ::_thesis: x |^ i = 1. L A3: 1_ L = x |^ 0 by BINOM:8; ((x ") |^ i) * (1. L) = 1. L by A2, VECTSP_1:def_4; then ((x ") |^ i) * (x |^ 0) = ((x ") |^ i) * (x |^ i) by A1, A3, Lm7; hence x |^ i = 1. L by A1, A2, A3, VECTSP_1:5; ::_thesis: verum end; begin definition let m be Nat; let L be non empty ZeroStr ; let p be AlgSequence of L; func mConv (p,m) -> Matrix of m,1,L means :Def4: :: POLYNOM8:def 4 for i being Nat st 1 <= i & i <= m holds it * (i,1) = p . (i - 1); existence ex b1 being Matrix of m,1,L st for i being Nat st 1 <= i & i <= m holds b1 * (i,1) = p . (i - 1) proof defpred S1[ Nat, set , set ] means $3 = p . ($1 - 1); reconsider m9 = m as Element of NAT by ORDINAL1:def_12; A1: for i, j being Nat st [i,j] in [:(Seg m9),(Seg 1):] holds ex x being Element of L st S1[i,j,x] proof let i, j be Nat; ::_thesis: ( [i,j] in [:(Seg m9),(Seg 1):] implies ex x being Element of L st S1[i,j,x] ) assume A2: [i,j] in [:(Seg m9),(Seg 1):] ; ::_thesis: ex x being Element of L st S1[i,j,x] take p /. (i - 1) ; ::_thesis: S1[i,j,p /. (i - 1)] [i,j] `1 in Seg m by A2, MCART_1:10; then i in Seg m ; then 1 <= i by FINSEQ_1:1; then ( dom p = NAT & 1 - 1 <= i - 1 ) by FUNCT_2:def_1, XREAL_1:9; hence S1[i,j,p /. (i - 1)] by INT_1:3, PARTFUN1:def_6; ::_thesis: verum end; consider M being Matrix of m9,1,L such that A3: for i, j being Nat st [i,j] in Indices M holds S1[i,j,M * (i,j)] from MATRIX_1:sch_2(A1); reconsider M = M as Matrix of m,1,L ; take M ; ::_thesis: for i being Nat st 1 <= i & i <= m holds M * (i,1) = p . (i - 1) now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_m_holds_ M_*_(i,1)_=_p_._(i_-_1) let i be Nat; ::_thesis: ( 1 <= i & i <= m implies M * (i,1) = p . (i - 1) ) assume ( 1 <= i & i <= m ) ; ::_thesis: M * (i,1) = p . (i - 1) then A4: ( i in Seg m & Indices M = [:(Seg m),(Seg 1):] ) by FINSEQ_1:1, MATRIX_1:23; 1 in Seg 1 ; then [i,1] in Indices M by A4, ZFMISC_1:def_2; hence M * (i,1) = p . (i - 1) by A3; ::_thesis: verum end; hence for i being Nat st 1 <= i & i <= m holds M * (i,1) = p . (i - 1) ; ::_thesis: verum end; uniqueness for b1, b2 being Matrix of m,1,L st ( for i being Nat st 1 <= i & i <= m holds b1 * (i,1) = p . (i - 1) ) & ( for i being Nat st 1 <= i & i <= m holds b2 * (i,1) = p . (i - 1) ) holds b1 = b2 proof let M1, M2 be Matrix of m,1,L; ::_thesis: ( ( for i being Nat st 1 <= i & i <= m holds M1 * (i,1) = p . (i - 1) ) & ( for i being Nat st 1 <= i & i <= m holds M2 * (i,1) = p . (i - 1) ) implies M1 = M2 ) assume that A5: for i being Nat st 1 <= i & i <= m holds M1 * (i,1) = p . (i - 1) and A6: for i being Nat st 1 <= i & i <= m holds M2 * (i,1) = p . (i - 1) ; ::_thesis: M1 = M2 percases ( m = 0 or m > 0 ) ; supposeA7: m = 0 ; ::_thesis: M1 = M2 then A8: for i, j being Nat st [i,j] in Indices M1 holds M1 * (i,j) = M2 * (i,j) by MATRIX_1:22; A9: width M1 = 0 by A7, MATRIX_1:22 .= width M2 by A7, MATRIX_1:22 ; len M1 = 0 by A7, MATRIX_1:22 .= len M2 by A7, MATRIX_1:22 ; hence M1 = M2 by A9, A8, MATRIX_1:21; ::_thesis: verum end; supposeA10: m > 0 ; ::_thesis: M1 = M2 A11: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_M1_holds_ M1_*_(i,j)_=_M2_*_(i,j) let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) ) assume [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j) then A12: [i,j] in [:(Seg m),(Seg 1):] by A10, MATRIX_1:23; then [i,j] `2 in Seg 1 by MCART_1:10; then j in Seg 1 ; then ( 1 <= j & j <= 1 ) by FINSEQ_1:1; then A13: j = 1 by XXREAL_0:1; [i,j] `1 in Seg m by A12, MCART_1:10; then i in Seg m ; then A14: ( 1 <= i & i <= m ) by FINSEQ_1:1; hence M1 * (i,j) = p . (i - 1) by A5, A13 .= M2 * (i,j) by A6, A14, A13 ; ::_thesis: verum end; A15: width M1 = 1 by A10, MATRIX_1:23 .= width M2 by A10, MATRIX_1:23 ; len M1 = m by A10, MATRIX_1:23 .= len M2 by A10, MATRIX_1:23 ; hence M1 = M2 by A15, A11, MATRIX_1:21; ::_thesis: verum end; end; end; end; :: deftheorem Def4 defines mConv POLYNOM8:def_4_:_ for m being Nat for L being non empty ZeroStr for p being AlgSequence of L for b4 being Matrix of m,1,L holds ( b4 = mConv (p,m) iff for i being Nat st 1 <= i & i <= m holds b4 * (i,1) = p . (i - 1) ); theorem Th28: :: POLYNOM8:28 for m being Nat st m > 0 holds for L being non empty ZeroStr for p being AlgSequence of L holds ( len (mConv (p,m)) = m & width (mConv (p,m)) = 1 & ( for i being Nat st i < m holds (mConv (p,m)) * ((i + 1),1) = p . i ) ) proof let m be Nat; ::_thesis: ( m > 0 implies for L being non empty ZeroStr for p being AlgSequence of L holds ( len (mConv (p,m)) = m & width (mConv (p,m)) = 1 & ( for i being Nat st i < m holds (mConv (p,m)) * ((i + 1),1) = p . i ) ) ) assume A1: m > 0 ; ::_thesis: for L being non empty ZeroStr for p being AlgSequence of L holds ( len (mConv (p,m)) = m & width (mConv (p,m)) = 1 & ( for i being Nat st i < m holds (mConv (p,m)) * ((i + 1),1) = p . i ) ) let L be non empty ZeroStr ; ::_thesis: for p being AlgSequence of L holds ( len (mConv (p,m)) = m & width (mConv (p,m)) = 1 & ( for i being Nat st i < m holds (mConv (p,m)) * ((i + 1),1) = p . i ) ) let p be AlgSequence of L; ::_thesis: ( len (mConv (p,m)) = m & width (mConv (p,m)) = 1 & ( for i being Nat st i < m holds (mConv (p,m)) * ((i + 1),1) = p . i ) ) set q = mConv (p,m); thus len (mConv (p,m)) = m by A1, MATRIX_1:23; ::_thesis: ( width (mConv (p,m)) = 1 & ( for i being Nat st i < m holds (mConv (p,m)) * ((i + 1),1) = p . i ) ) thus width (mConv (p,m)) = 1 by A1, MATRIX_1:23; ::_thesis: for i being Nat st i < m holds (mConv (p,m)) * ((i + 1),1) = p . i now__::_thesis:_for_i_being_Nat_st_i_<_m_holds_ (mConv_(p,m))_*_((i_+_1),1)_=_p_._i let i be Nat; ::_thesis: ( i < m implies (mConv (p,m)) * ((i + 1),1) = p . i ) assume i < m ; ::_thesis: (mConv (p,m)) * ((i + 1),1) = p . i then ( 0 + 1 <= i + 1 & i + 1 <= m ) by NAT_1:13; then (mConv (p,m)) * ((i + 1),1) = p . ((i + 1) - 1) by Def4; hence (mConv (p,m)) * ((i + 1),1) = p . i ; ::_thesis: verum end; hence for i being Nat st i < m holds (mConv (p,m)) * ((i + 1),1) = p . i ; ::_thesis: verum end; theorem Th29: :: POLYNOM8:29 for m being Nat st m > 0 holds for L being non empty ZeroStr for a being AlgSequence of L for M being Matrix of m,1,L st ( for i being Nat st i < m holds M * ((i + 1),1) = a . i ) holds mConv (a,m) = M proof let m be Nat; ::_thesis: ( m > 0 implies for L being non empty ZeroStr for a being AlgSequence of L for M being Matrix of m,1,L st ( for i being Nat st i < m holds M * ((i + 1),1) = a . i ) holds mConv (a,m) = M ) assume A1: m > 0 ; ::_thesis: for L being non empty ZeroStr for a being AlgSequence of L for M being Matrix of m,1,L st ( for i being Nat st i < m holds M * ((i + 1),1) = a . i ) holds mConv (a,m) = M let L be non empty ZeroStr ; ::_thesis: for a being AlgSequence of L for M being Matrix of m,1,L st ( for i being Nat st i < m holds M * ((i + 1),1) = a . i ) holds mConv (a,m) = M let a be AlgSequence of L; ::_thesis: for M being Matrix of m,1,L st ( for i being Nat st i < m holds M * ((i + 1),1) = a . i ) holds mConv (a,m) = M let M be Matrix of m,1,L; ::_thesis: ( ( for i being Nat st i < m holds M * ((i + 1),1) = a . i ) implies mConv (a,m) = M ) A2: width (mConv (a,m)) = 1 by A1, Th28 .= width M by A1, MATRIX_1:23 ; assume A3: for i being Nat st i < m holds M * ((i + 1),1) = a . i ; ::_thesis: mConv (a,m) = M A4: for i, j being Nat st [i,j] in Indices (mConv (a,m)) holds (mConv (a,m)) * (i,j) = M * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (mConv (a,m)) implies (mConv (a,m)) * (i,j) = M * (i,j) ) assume A5: [i,j] in Indices (mConv (a,m)) ; ::_thesis: (mConv (a,m)) * (i,j) = M * (i,j) then A6: i in dom (mConv (a,m)) by ZFMISC_1:87; len (mConv (a,m)) = m by A1, Th28; then A7: i in Seg m by A6, FINSEQ_1:def_3; then 0 < i by FINSEQ_1:1; then reconsider k = i - 1 as Nat by NAT_1:20; A8: j in Seg (width (mConv (a,m))) by A5, ZFMISC_1:87; then A9: 1 <= j by FINSEQ_1:1; j in Seg 1 by A1, A8, Th28; then A10: j <= 1 by FINSEQ_1:1; k + 1 <= m by A7, FINSEQ_1:1; then A11: k < m by NAT_1:13; then M * ((k + 1),1) = a . k by A3 .= (mConv (a,m)) * ((k + 1),1) by A11, Th28 .= (mConv (a,m)) * (i,j) by A9, A10, XXREAL_0:1 ; hence (mConv (a,m)) * (i,j) = M * (i,j) by A9, A10, XXREAL_0:1; ::_thesis: verum end; len (mConv (a,m)) = m by A1, Th28 .= len M by A1, MATRIX_1:23 ; hence mConv (a,m) = M by A2, A4, MATRIX_1:21; ::_thesis: verum end; definition let L be non empty ZeroStr ; let M be Matrix of L; func aConv M -> AlgSequence of L means :Def5: :: POLYNOM8:def 5 ( ( for i being Nat st i < len M holds it . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds it . i = 0. L ) ); existence ex b1 being AlgSequence of L st ( ( for i being Nat st i < len M holds b1 . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds b1 . i = 0. L ) ) proof defpred S1[ set , set ] means ex k being Element of NAT st ( k = $1 & ( ( k < len M & $2 = M * ((k + 1),1) ) or ( len M <= k & $2 = 0. L ) ) ); A1: for x being set st x in NAT holds ex y being set st ( y in the carrier of L & S1[x,y] ) proof let u be set ; ::_thesis: ( u in NAT implies ex y being set st ( y in the carrier of L & S1[u,y] ) ) assume u in NAT ; ::_thesis: ex y being set st ( y in the carrier of L & S1[u,y] ) then reconsider u9 = u as Element of NAT ; thus ex y being set st ( y in the carrier of L & S1[u,y] ) ::_thesis: verum proof percases ( u9 < len M or u9 >= len M ) ; supposeA2: u9 < len M ; ::_thesis: ex y being set st ( y in the carrier of L & S1[u,y] ) take M * ((u9 + 1),1) ; ::_thesis: ( M * ((u9 + 1),1) in the carrier of L & S1[u,M * ((u9 + 1),1)] ) thus ( M * ((u9 + 1),1) in the carrier of L & S1[u,M * ((u9 + 1),1)] ) by A2; ::_thesis: verum end; supposeA3: u9 >= len M ; ::_thesis: ex y being set st ( y in the carrier of L & S1[u,y] ) take 0. L ; ::_thesis: ( 0. L in the carrier of L & S1[u, 0. L] ) thus ( 0. L in the carrier of L & S1[u, 0. L] ) by A3; ::_thesis: verum end; end; end; end; consider f being Function of NAT, the carrier of L such that A4: for x being set st x in NAT holds S1[x,f . x] from FUNCT_2:sch_1(A1); reconsider f = f as sequence of L ; ex n being Nat st for i being Nat st i >= n holds f . i = 0. L proof take len M ; ::_thesis: for i being Nat st i >= len M holds f . i = 0. L now__::_thesis:_for_i_being_Nat_st_i_>=_len_M_holds_ f_._i_=_0._L let i be Nat; ::_thesis: ( i >= len M implies f . i = 0. L ) i in NAT by ORDINAL1:def_12; then A5: ex k being Element of NAT st ( k = i & ( ( k < len M & f . i = M * ((k + 1),1) ) or ( len M <= k & f . i = 0. L ) ) ) by A4; assume i >= len M ; ::_thesis: f . i = 0. L hence f . i = 0. L by A5; ::_thesis: verum end; hence for i being Nat st i >= len M holds f . i = 0. L ; ::_thesis: verum end; then reconsider q = f as AlgSequence of L by ALGSEQ_1:def_1; A6: now__::_thesis:_for_i_being_Nat_st_i_>=_len_M_holds_ q_._i_=_0._L let i be Nat; ::_thesis: ( i >= len M implies q . i = 0. L ) i in NAT by ORDINAL1:def_12; then A7: ex k being Element of NAT st ( k = i & ( ( k < len M & q . i = M * ((k + 1),1) ) or ( len M <= k & q . i = 0. L ) ) ) by A4; assume i >= len M ; ::_thesis: q . i = 0. L hence q . i = 0. L by A7; ::_thesis: verum end; take q ; ::_thesis: ( ( for i being Nat st i < len M holds q . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds q . i = 0. L ) ) now__::_thesis:_for_i_being_Nat_st_i_<_len_M_holds_ q_._i_=_M_*_((i_+_1),1) let i be Nat; ::_thesis: ( i < len M implies q . i = M * ((i + 1),1) ) i in NAT by ORDINAL1:def_12; then A8: ex k being Element of NAT st ( k = i & ( ( k < len M & q . i = M * ((k + 1),1) ) or ( len M <= k & q . i = 0. L ) ) ) by A4; assume i < len M ; ::_thesis: q . i = M * ((i + 1),1) hence q . i = M * ((i + 1),1) by A8; ::_thesis: verum end; hence ( ( for i being Nat st i < len M holds q . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds q . i = 0. L ) ) by A6; ::_thesis: verum end; uniqueness for b1, b2 being AlgSequence of L st ( for i being Nat st i < len M holds b1 . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds b1 . i = 0. L ) & ( for i being Nat st i < len M holds b2 . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds b2 . i = 0. L ) holds b1 = b2 proof let z1, z2 be AlgSequence of L; ::_thesis: ( ( for i being Nat st i < len M holds z1 . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds z1 . i = 0. L ) & ( for i being Nat st i < len M holds z2 . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds z2 . i = 0. L ) implies z1 = z2 ) assume that A9: for i being Nat st i < len M holds z1 . i = M * ((i + 1),1) and A10: for i being Nat st i >= len M holds z1 . i = 0. L ; ::_thesis: ( ex i being Nat st ( i < len M & not z2 . i = M * ((i + 1),1) ) or ex i being Nat st ( i >= len M & not z2 . i = 0. L ) or z1 = z2 ) assume that A11: for i being Nat st i < len M holds z2 . i = M * ((i + 1),1) and A12: for i being Nat st i >= len M holds z2 . i = 0. L ; ::_thesis: z1 = z2 A13: now__::_thesis:_for_u_being_set_st_u_in_dom_z1_holds_ z1_._u_=_z2_._u let u be set ; ::_thesis: ( u in dom z1 implies z1 . b1 = z2 . b1 ) assume u in dom z1 ; ::_thesis: z1 . b1 = z2 . b1 then reconsider u9 = u as Element of NAT by FUNCT_2:def_1; percases ( u9 < len M or len M <= u9 ) ; supposeA14: u9 < len M ; ::_thesis: z1 . b1 = z2 . b1 hence z1 . u = M * ((u9 + 1),1) by A9 .= z2 . u by A11, A14 ; ::_thesis: verum end; supposeA15: len M <= u9 ; ::_thesis: z1 . b1 = z2 . b1 hence z1 . u = 0. L by A10 .= z2 . u by A12, A15 ; ::_thesis: verum end; end; end; dom z1 = NAT by FUNCT_2:def_1 .= dom z2 by FUNCT_2:def_1 ; hence z1 = z2 by A13, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def5 defines aConv POLYNOM8:def_5_:_ for L being non empty ZeroStr for M being Matrix of L for b3 being AlgSequence of L holds ( b3 = aConv M iff ( ( for i being Nat st i < len M holds b3 . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds b3 . i = 0. L ) ) ); begin definition let L be non empty well-unital doubleLoopStr ; let x be Element of L; let n be Element of NAT ; predx is_primitive_root_of_degree n means :Def6: :: POLYNOM8:def 6 ( n <> 0 & x |^ n = 1. L & ( for i being Element of NAT st 0 < i & i < n holds x |^ i <> 1. L ) ); end; :: deftheorem Def6 defines is_primitive_root_of_degree POLYNOM8:def_6_:_ for L being non empty well-unital doubleLoopStr for x being Element of L for n being Element of NAT holds ( x is_primitive_root_of_degree n iff ( n <> 0 & x |^ n = 1. L & ( for i being Element of NAT st 0 < i & i < n holds x |^ i <> 1. L ) ) ); theorem Th30: :: POLYNOM8:30 for L being non empty non degenerated right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr for n being Element of NAT holds not 0. L is_primitive_root_of_degree n proof let L be non empty non degenerated right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr ; ::_thesis: for n being Element of NAT holds not 0. L is_primitive_root_of_degree n let n be Element of NAT ; ::_thesis: not 0. L is_primitive_root_of_degree n defpred S1[ Nat] means (0. L) |^ $1 = 0. L; A1: for j being Nat st 1 <= j & S1[j] holds S1[j + 1] proof let j be Nat; ::_thesis: ( 1 <= j & S1[j] implies S1[j + 1] ) assume 1 <= j ; ::_thesis: ( not S1[j] or S1[j + 1] ) assume S1[j] ; ::_thesis: S1[j + 1] j in NAT by ORDINAL1:def_12; then (0. L) |^ (j + 1) = ((0. L) |^ j) * (0. L) by GROUP_1:def_7 .= 0. L by VECTSP_1:6 ; hence S1[j + 1] ; ::_thesis: verum end; A2: S1[1] by BINOM:8; A3: for m being Nat st 1 <= m holds S1[m] from NAT_1:sch_8(A2, A1); assume A4: 0. L is_primitive_root_of_degree n ; ::_thesis: contradiction then n <> 0 by Def6; then 0 + 1 < n + 1 by XREAL_1:8; then 1 <= n by NAT_1:13; then (0. L) |^ n <> 1. L by A3; hence contradiction by A4, Def6; ::_thesis: verum end; theorem Th31: :: POLYNOM8:31 for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr for m being Element of NAT for x being Element of L st x is_primitive_root_of_degree m holds x " is_primitive_root_of_degree m proof let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for m being Element of NAT for x being Element of L st x is_primitive_root_of_degree m holds x " is_primitive_root_of_degree m let m be Element of NAT ; ::_thesis: for x being Element of L st x is_primitive_root_of_degree m holds x " is_primitive_root_of_degree m let x be Element of L; ::_thesis: ( x is_primitive_root_of_degree m implies x " is_primitive_root_of_degree m ) assume A1: x is_primitive_root_of_degree m ; ::_thesis: x " is_primitive_root_of_degree m then A2: x <> 0. L by Th30; A3: for i being Element of NAT st 0 < i & i < m holds (x ") |^ i <> 1. L proof let i be Element of NAT ; ::_thesis: ( 0 < i & i < m implies (x ") |^ i <> 1. L ) assume ( 0 < i & i < m ) ; ::_thesis: (x ") |^ i <> 1. L then x |^ i <> 1. L by A1, Def6; hence (x ") |^ i <> 1. L by A2, Lm11; ::_thesis: verum end; x |^ m = 1. L by A1, Def6; then A4: (x ") |^ m = 1. L by A2, Lm10; m <> 0 by A1, Def6; hence x " is_primitive_root_of_degree m by A4, A3, Def6; ::_thesis: verum end; theorem Th32: :: POLYNOM8:32 for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr for m being Element of NAT for x being Element of L st x is_primitive_root_of_degree m holds for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m & i <> j holds pow (x,(i - j)) <> 1. L proof let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for m being Element of NAT for x being Element of L st x is_primitive_root_of_degree m holds for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m & i <> j holds pow (x,(i - j)) <> 1. L let m be Element of NAT ; ::_thesis: for x being Element of L st x is_primitive_root_of_degree m holds for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m & i <> j holds pow (x,(i - j)) <> 1. L let x be Element of L; ::_thesis: ( x is_primitive_root_of_degree m implies for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m & i <> j holds pow (x,(i - j)) <> 1. L ) assume A1: x is_primitive_root_of_degree m ; ::_thesis: for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m & i <> j holds pow (x,(i - j)) <> 1. L then A2: x <> 0. L by Th30; let i, j be Nat; ::_thesis: ( 1 <= i & i <= m & 1 <= j & j <= m & i <> j implies pow (x,(i - j)) <> 1. L ) assume that A3: 1 <= i and A4: i <= m and A5: 1 <= j and A6: j <= m and A7: i <> j ; ::_thesis: pow (x,(i - j)) <> 1. L percases ( i > j or i <= j ) ; supposeA8: i > j ; ::_thesis: pow (x,(i - j)) <> 1. L then reconsider k = i - j as Element of NAT by INT_1:5; k <= i - 1 by A5, XREAL_1:13; then k + 1 <= (i - 1) + 1 by XREAL_1:6; then k < i by NAT_1:13; then A9: k < m by A4, XXREAL_0:2; i - j > j - j by A8, XREAL_1:14; then x |^ k <> 1. L by A1, A9, Def6; hence pow (x,(i - j)) <> 1. L by Def3; ::_thesis: verum end; suppose i <= j ; ::_thesis: pow (x,(i - j)) <> 1. L then A10: i < j by A7, XXREAL_0:1; then A11: j - i > i - i by XREAL_1:14; A12: i - j < j - j by A10, XREAL_1:14; then A13: abs (i - j) = - (i - j) by ABSVALUE:def_1; then reconsider k = - (i - j) as Element of NAT ; j - i <= j - 1 by A3, XREAL_1:13; then k + 1 <= (j - 1) + 1 by XREAL_1:6; then k < j by NAT_1:13; then A14: k < m by A6, XXREAL_0:2; A15: x |^ k <> 0. L by A2, Th1; now__::_thesis:_not_(x_|^_k)_"_=_1._L assume (x |^ k) " = 1. L ; ::_thesis: contradiction then 1. L = (x |^ k) * (1. L) by A15, VECTSP_1:def_10 .= x |^ k by VECTSP_1:def_4 ; hence contradiction by A1, A11, A14, Def6; ::_thesis: verum end; hence pow (x,(i - j)) <> 1. L by A12, A13, Def3; ::_thesis: verum end; end; end; definition let m be Nat; let L be non empty well-unital doubleLoopStr ; let p be Polynomial of L; let x be Element of L; func DFT (p,x,m) -> AlgSequence of L means :Def7: :: POLYNOM8:def 7 ( ( for i being Nat st i < m holds it . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds it . i = 0. L ) ); existence ex b1 being AlgSequence of L st ( ( for i being Nat st i < m holds b1 . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds b1 . i = 0. L ) ) proof defpred S1[ set , set ] means ex k being Element of NAT st ( k = $1 & ( ( k < m & $2 = eval (p,(x |^ k)) ) or ( m <= k & $2 = 0. L ) ) ); A1: for x being set st x in NAT holds ex y being set st ( y in the carrier of L & S1[x,y] ) proof let u be set ; ::_thesis: ( u in NAT implies ex y being set st ( y in the carrier of L & S1[u,y] ) ) assume u in NAT ; ::_thesis: ex y being set st ( y in the carrier of L & S1[u,y] ) then reconsider u9 = u as Element of NAT ; thus ex y being set st ( y in the carrier of L & S1[u,y] ) ::_thesis: verum proof percases ( u9 < m or u9 >= m ) ; supposeA2: u9 < m ; ::_thesis: ex y being set st ( y in the carrier of L & S1[u,y] ) take eval (p,(x |^ u9)) ; ::_thesis: ( eval (p,(x |^ u9)) in the carrier of L & S1[u, eval (p,(x |^ u9))] ) thus ( eval (p,(x |^ u9)) in the carrier of L & S1[u, eval (p,(x |^ u9))] ) by A2; ::_thesis: verum end; supposeA3: u9 >= m ; ::_thesis: ex y being set st ( y in the carrier of L & S1[u,y] ) take 0. L ; ::_thesis: ( 0. L in the carrier of L & S1[u, 0. L] ) thus ( 0. L in the carrier of L & S1[u, 0. L] ) by A3; ::_thesis: verum end; end; end; end; consider f being Function of NAT, the carrier of L such that A4: for x being set st x in NAT holds S1[x,f . x] from FUNCT_2:sch_1(A1); reconsider f = f as sequence of L ; ex n being Nat st for i being Nat st i >= n holds f . i = 0. L proof reconsider m = m as Element of NAT by ORDINAL1:def_12; take m ; ::_thesis: for i being Nat st i >= m holds f . i = 0. L now__::_thesis:_for_i_being_Nat_st_i_>=_m_holds_ f_._i_=_0._L let i be Nat; ::_thesis: ( i >= m implies f . i = 0. L ) i in NAT by ORDINAL1:def_12; then A5: ex k being Element of NAT st ( k = i & ( ( k < m & f . i = eval (p,(x |^ k)) ) or ( m <= k & f . i = 0. L ) ) ) by A4; assume i >= m ; ::_thesis: f . i = 0. L hence f . i = 0. L by A5; ::_thesis: verum end; hence for i being Nat st i >= m holds f . i = 0. L ; ::_thesis: verum end; then reconsider q = f as AlgSequence of L by ALGSEQ_1:def_1; A6: now__::_thesis:_for_i_being_Nat_st_i_>=_m_holds_ q_._i_=_0._L let i be Nat; ::_thesis: ( i >= m implies q . i = 0. L ) i in NAT by ORDINAL1:def_12; then A7: ex k being Element of NAT st ( k = i & ( ( k < m & q . i = eval (p,(x |^ k)) ) or ( m <= k & q . i = 0. L ) ) ) by A4; assume i >= m ; ::_thesis: q . i = 0. L hence q . i = 0. L by A7; ::_thesis: verum end; take q ; ::_thesis: ( ( for i being Nat st i < m holds q . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds q . i = 0. L ) ) now__::_thesis:_for_i_being_Nat_st_i_<_m_holds_ q_._i_=_eval_(p,(x_|^_i)) let i be Nat; ::_thesis: ( i < m implies q . i = eval (p,(x |^ i)) ) i in NAT by ORDINAL1:def_12; then A8: ex k being Element of NAT st ( k = i & ( ( k < m & q . i = eval (p,(x |^ k)) ) or ( m <= k & q . i = 0. L ) ) ) by A4; assume i < m ; ::_thesis: q . i = eval (p,(x |^ i)) hence q . i = eval (p,(x |^ i)) by A8; ::_thesis: verum end; hence ( ( for i being Nat st i < m holds q . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds q . i = 0. L ) ) by A6; ::_thesis: verum end; uniqueness for b1, b2 being AlgSequence of L st ( for i being Nat st i < m holds b1 . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds b1 . i = 0. L ) & ( for i being Nat st i < m holds b2 . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds b2 . i = 0. L ) holds b1 = b2 proof let z1, z2 be AlgSequence of L; ::_thesis: ( ( for i being Nat st i < m holds z1 . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds z1 . i = 0. L ) & ( for i being Nat st i < m holds z2 . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds z2 . i = 0. L ) implies z1 = z2 ) assume that A9: for i being Nat st i < m holds z1 . i = eval (p,(x |^ i)) and A10: for i being Nat st i >= m holds z1 . i = 0. L ; ::_thesis: ( ex i being Nat st ( i < m & not z2 . i = eval (p,(x |^ i)) ) or ex i being Nat st ( i >= m & not z2 . i = 0. L ) or z1 = z2 ) assume that A11: for i being Nat st i < m holds z2 . i = eval (p,(x |^ i)) and A12: for i being Nat st i >= m holds z2 . i = 0. L ; ::_thesis: z1 = z2 A13: now__::_thesis:_for_u_being_set_st_u_in_dom_z1_holds_ z1_._u_=_z2_._u let u be set ; ::_thesis: ( u in dom z1 implies z1 . b1 = z2 . b1 ) assume u in dom z1 ; ::_thesis: z1 . b1 = z2 . b1 then reconsider u9 = u as Element of NAT by FUNCT_2:def_1; percases ( u9 < m or m <= u9 ) ; supposeA14: u9 < m ; ::_thesis: z1 . b1 = z2 . b1 hence z1 . u = eval (p,(x |^ u9)) by A9 .= z2 . u by A11, A14 ; ::_thesis: verum end; supposeA15: m <= u9 ; ::_thesis: z1 . b1 = z2 . b1 hence z1 . u = 0. L by A10 .= z2 . u by A12, A15 ; ::_thesis: verum end; end; end; dom z1 = NAT by FUNCT_2:def_1 .= dom z2 by FUNCT_2:def_1 ; hence z1 = z2 by A13, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def7 defines DFT POLYNOM8:def_7_:_ for m being Nat for L being non empty well-unital doubleLoopStr for p being Polynomial of L for x being Element of L for b5 being AlgSequence of L holds ( b5 = DFT (p,x,m) iff ( ( for i being Nat st i < m holds b5 . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds b5 . i = 0. L ) ) ); theorem Th33: :: POLYNOM8:33 for m being Nat for L being non empty well-unital doubleLoopStr for x being Element of L holds DFT ((0_. L),x,m) = 0_. L proof let m be Nat; ::_thesis: for L being non empty well-unital doubleLoopStr for x being Element of L holds DFT ((0_. L),x,m) = 0_. L let L be non empty well-unital doubleLoopStr ; ::_thesis: for x being Element of L holds DFT ((0_. L),x,m) = 0_. L let x be Element of L; ::_thesis: DFT ((0_. L),x,m) = 0_. L set q = DFT ((0_. L),x,m); A1: now__::_thesis:_for_u_being_set_st_u_in_dom_(DFT_((0_._L),x,m))_holds_ (DFT_((0_._L),x,m))_._u_=_(0_._L)_._u let u be set ; ::_thesis: ( u in dom (DFT ((0_. L),x,m)) implies (DFT ((0_. L),x,m)) . b1 = (0_. L) . b1 ) assume u in dom (DFT ((0_. L),x,m)) ; ::_thesis: (DFT ((0_. L),x,m)) . b1 = (0_. L) . b1 then reconsider n = u as Element of NAT by FUNCT_2:def_1; percases ( n < m or n >= m ) ; suppose n < m ; ::_thesis: (DFT ((0_. L),x,m)) . b1 = (0_. L) . b1 hence (DFT ((0_. L),x,m)) . u = eval ((0_. L),(x |^ n)) by Def7 .= 0. L by POLYNOM4:17 .= (0_. L) . n by FUNCOP_1:7 .= (0_. L) . u ; ::_thesis: verum end; suppose n >= m ; ::_thesis: (DFT ((0_. L),x,m)) . b1 = (0_. L) . b1 hence (DFT ((0_. L),x,m)) . u = 0. L by Def7 .= (0_. L) . n by FUNCOP_1:7 .= (0_. L) . u ; ::_thesis: verum end; end; end; dom (DFT ((0_. L),x,m)) = NAT by FUNCT_2:def_1 .= dom (0_. L) by FUNCT_2:def_1 ; hence DFT ((0_. L),x,m) = 0_. L by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th34: :: POLYNOM8:34 for m being Nat for L being Field for p, q being Polynomial of L for x being Element of L holds (DFT (p,x,m)) * (DFT (q,x,m)) = DFT ((p *' q),x,m) proof let m be Nat; ::_thesis: for L being Field for p, q being Polynomial of L for x being Element of L holds (DFT (p,x,m)) * (DFT (q,x,m)) = DFT ((p *' q),x,m) let L be Field; ::_thesis: for p, q being Polynomial of L for x being Element of L holds (DFT (p,x,m)) * (DFT (q,x,m)) = DFT ((p *' q),x,m) let p, q be Polynomial of L; ::_thesis: for x being Element of L holds (DFT (p,x,m)) * (DFT (q,x,m)) = DFT ((p *' q),x,m) let x be Element of L; ::_thesis: (DFT (p,x,m)) * (DFT (q,x,m)) = DFT ((p *' q),x,m) set ep = DFT (p,x,m); set eq = DFT (q,x,m); set epq = DFT ((p *' q),x,m); A1: now__::_thesis:_for_u9_being_set_st_u9_in_dom_((DFT_(p,x,m))_*_(DFT_(q,x,m)))_holds_ (DFT_((p_*'_q),x,m))_._u9_=_((DFT_(p,x,m))_*_(DFT_(q,x,m)))_._u9 let u9 be set ; ::_thesis: ( u9 in dom ((DFT (p,x,m)) * (DFT (q,x,m))) implies (DFT ((p *' q),x,m)) . b1 = ((DFT (p,x,m)) * (DFT (q,x,m))) . b1 ) assume u9 in dom ((DFT (p,x,m)) * (DFT (q,x,m))) ; ::_thesis: (DFT ((p *' q),x,m)) . b1 = ((DFT (p,x,m)) * (DFT (q,x,m))) . b1 then reconsider u = u9 as Element of NAT by FUNCT_2:def_1; percases ( u < m or m <= u ) ; supposeA2: u < m ; ::_thesis: (DFT ((p *' q),x,m)) . b1 = ((DFT (p,x,m)) * (DFT (q,x,m))) . b1 hence (DFT ((p *' q),x,m)) . u9 = eval ((p *' q),(x |^ u)) by Def7 .= (eval (p,(x |^ u))) * (eval (q,(x |^ u))) by POLYNOM4:24 .= ((DFT (p,x,m)) . u) * (eval (q,(x |^ u))) by A2, Def7 .= ((DFT (p,x,m)) . u) * ((DFT (q,x,m)) . u) by A2, Def7 .= ((DFT (p,x,m)) * (DFT (q,x,m))) . u9 by Def2 ; ::_thesis: verum end; supposeA3: m <= u ; ::_thesis: ((DFT (p,x,m)) * (DFT (q,x,m))) . b1 = (DFT ((p *' q),x,m)) . b1 thus ((DFT (p,x,m)) * (DFT (q,x,m))) . u9 = ((DFT (p,x,m)) . u) * ((DFT (q,x,m)) . u) by Def2 .= (0. L) * ((DFT (q,x,m)) . u) by A3, Def7 .= 0. L by VECTSP_1:6 .= (DFT ((p *' q),x,m)) . u9 by A3, Def7 ; ::_thesis: verum end; end; end; dom ((DFT (p,x,m)) * (DFT (q,x,m))) = NAT by FUNCT_2:def_1 .= dom (DFT ((p *' q),x,m)) by FUNCT_2:def_1 ; hence (DFT (p,x,m)) * (DFT (q,x,m)) = DFT ((p *' q),x,m) by A1, FUNCT_1:2; ::_thesis: verum end; definition let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; let m be Nat; let x be Element of L; func Vandermonde (x,m) -> Matrix of m,L means :Def8: :: POLYNOM8:def 8 for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds it * (i,j) = pow (x,((i - 1) * (j - 1))); existence ex b1 being Matrix of m,L st for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds b1 * (i,j) = pow (x,((i - 1) * (j - 1))) proof defpred S1[ Nat, Nat, set ] means $3 = pow (x,(($1 - 1) * ($2 - 1))); reconsider m9 = m as Element of NAT by ORDINAL1:def_12; A1: for i, j being Nat st [i,j] in [:(Seg m9),(Seg m9):] holds ex x being Element of L st S1[i,j,x] ; consider M being Matrix of m9,m9,L such that A2: for i, j being Nat st [i,j] in Indices M holds S1[i,j,M * (i,j)] from MATRIX_1:sch_2(A1); reconsider M = M as Matrix of m,m,L ; take M ; ::_thesis: for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds M * (i,j) = pow (x,((i - 1) * (j - 1))) now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_m_holds_ for_j_being_Nat_st_1_<=_j_&_j_<=_m_holds_ M_*_(i,j)_=_pow_(x,((i_-_1)_*_(j_-_1))) let i be Nat; ::_thesis: ( 1 <= i & i <= m implies for j being Nat st 1 <= j & j <= m holds M * (i,j) = pow (x,((i - 1) * (j - 1))) ) assume ( 1 <= i & i <= m ) ; ::_thesis: for j being Nat st 1 <= j & j <= m holds M * (i,j) = pow (x,((i - 1) * (j - 1))) then A3: ( Indices M = [:(Seg m),(Seg m):] & i in Seg m ) by FINSEQ_1:1, MATRIX_1:24; let j be Nat; ::_thesis: ( 1 <= j & j <= m implies M * (i,j) = pow (x,((i - 1) * (j - 1))) ) assume ( 1 <= j & j <= m ) ; ::_thesis: M * (i,j) = pow (x,((i - 1) * (j - 1))) then j in Seg m by FINSEQ_1:1; then [i,j] in Indices M by A3, ZFMISC_1:def_2; hence M * (i,j) = pow (x,((i - 1) * (j - 1))) by A2; ::_thesis: verum end; hence for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds M * (i,j) = pow (x,((i - 1) * (j - 1))) ; ::_thesis: verum end; uniqueness for b1, b2 being Matrix of m,L st ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds b1 * (i,j) = pow (x,((i - 1) * (j - 1))) ) & ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds b2 * (i,j) = pow (x,((i - 1) * (j - 1))) ) holds b1 = b2 proof let M1, M2 be Matrix of m,L; ::_thesis: ( ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds M1 * (i,j) = pow (x,((i - 1) * (j - 1))) ) & ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds M2 * (i,j) = pow (x,((i - 1) * (j - 1))) ) implies M1 = M2 ) assume A4: for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds M1 * (i,j) = pow (x,((i - 1) * (j - 1))) ; ::_thesis: ( ex i, j being Nat st ( 1 <= i & i <= m & 1 <= j & j <= m & not M2 * (i,j) = pow (x,((i - 1) * (j - 1))) ) or M1 = M2 ) assume A5: for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds M2 * (i,j) = pow (x,((i - 1) * (j - 1))) ; ::_thesis: M1 = M2 now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_M1_holds_ M1_*_(i,j)_=_M2_*_(i,j) let i, j be Nat; ::_thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) ) A6: Indices M1 = [:(Seg m),(Seg m):] by MATRIX_1:24; assume [i,j] in Indices M1 ; ::_thesis: M1 * (i,j) = M2 * (i,j) then ex x, y being set st ( x in Seg m & y in Seg m & [x,y] = [i,j] ) by A6, ZFMISC_1:def_2; then consider z, y being set such that A7: [i,j] = [z,y] and A8: z in Seg m and A9: y in Seg m ; j = y by A7, XTUPLE_0:1; then A10: ( 1 <= j & j <= m ) by A9, FINSEQ_1:1; i = z by A7, XTUPLE_0:1; then A11: ( 1 <= i & i <= m ) by A8, FINSEQ_1:1; hence M1 * (i,j) = pow (x,((i - 1) * (j - 1))) by A4, A10 .= M2 * (i,j) by A5, A11, A10 ; ::_thesis: verum end; hence M1 = M2 by MATRIX_1:27; ::_thesis: verum end; end; :: deftheorem Def8 defines Vandermonde POLYNOM8:def_8_:_ for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr for m being Nat for x being Element of L for b4 being Matrix of m,L holds ( b4 = Vandermonde (x,m) iff for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds b4 * (i,j) = pow (x,((i - 1) * (j - 1))) ); notation let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; let m be Nat; let x be Element of L; synonym VM (x,m) for Vandermonde (x,m); end; theorem Th35: :: POLYNOM8:35 for L being Field for m, n being Nat st m > 0 holds for M being Matrix of m,n,L holds (1. (L,m)) * M = M proof let L be Field; ::_thesis: for m, n being Nat st m > 0 holds for M being Matrix of m,n,L holds (1. (L,m)) * M = M let m, n be Nat; ::_thesis: ( m > 0 implies for M being Matrix of m,n,L holds (1. (L,m)) * M = M ) assume A1: m > 0 ; ::_thesis: for M being Matrix of m,n,L holds (1. (L,m)) * M = M let M be Matrix of m,n,L; ::_thesis: (1. (L,m)) * M = M A2: width (1. (L,m)) = m by A1, MATRIX_1:23 .= len M by A1, MATRIX_1:23 ; set M2 = (1. (L,m)) * M; A3: len M = m by A1, MATRIX_1:23; len (1. (L,m)) = m by A1, MATRIX_1:23; then A4: m = len ((1. (L,m)) * M) by A2, MATRIX_3:def_4; A5: now__::_thesis:_for_i,_j_being_Nat_st_[i,j]_in_Indices_M_holds_ M_*_(i,j)_=_((1._(L,m))_*_M)_*_(i,j) let i, j be Nat; ::_thesis: ( [i,j] in Indices M implies M * (i,j) = ((1. (L,m)) * M) * (i,j) ) assume A6: [i,j] in Indices M ; ::_thesis: M * (i,j) = ((1. (L,m)) * M) * (i,j) then A7: i in dom M by ZFMISC_1:87; dom M = Seg (len M) by FINSEQ_1:def_3 .= dom ((1. (L,m)) * M) by A3, A4, FINSEQ_1:def_3 ; then Indices M = Indices ((1. (L,m)) * M) by A2, MATRIX_3:def_4; then A8: ((1. (L,m)) * M) * (i,j) = (Line ((1. (L,m)),i)) "*" (Col (M,j)) by A2, A6, MATRIX_3:def_4 .= Sum (mlt ((Line ((1. (L,m)),i)),(Col (M,j)))) by FVSUM_1:def_9 ; len (Line ((1. (L,m)),i)) = width (1. (L,m)) by MATRIX_1:def_7 .= m by MATRIX_1:24 ; then A9: dom (Line ((1. (L,m)),i)) = Seg m by FINSEQ_1:def_3; A10: len M = m by A1, MATRIX_1:23; then A11: i in dom (Line ((1. (L,m)),i)) by A7, A9, FINSEQ_1:def_3; A12: Indices (1. (L,m)) = [:(Seg m),(Seg m):] by A1, MATRIX_1:23; then A13: [i,i] in Indices (1. (L,m)) by A9, A11, ZFMISC_1:87; A14: for k being Nat st k in dom (Line ((1. (L,m)),i)) & k <> i holds (Line ((1. (L,m)),i)) . k = 0. L proof let k be Nat; ::_thesis: ( k in dom (Line ((1. (L,m)),i)) & k <> i implies (Line ((1. (L,m)),i)) . k = 0. L ) assume that A15: k in dom (Line ((1. (L,m)),i)) and A16: k <> i ; ::_thesis: (Line ((1. (L,m)),i)) . k = 0. L A17: [i,k] in Indices (1. (L,m)) by A9, A11, A12, A15, ZFMISC_1:87; k in Seg (width (1. (L,m))) by A9, A15, MATRIX_1:24; then (Line ((1. (L,m)),i)) . k = (1. (L,m)) * (i,k) by MATRIX_1:def_7 .= 0. L by A16, A17, MATRIX_1:def_11 ; hence (Line ((1. (L,m)),i)) . k = 0. L ; ::_thesis: verum end; len (Col (M,j)) = len M by MATRIX_1:def_8 .= m by A1, MATRIX_1:23 ; then dom (Col (M,j)) = Seg m by FINSEQ_1:def_3; then A18: i in dom (Col (M,j)) by A7, A10, FINSEQ_1:def_3; i in Seg (width (1. (L,m))) by A9, A11, MATRIX_1:24; then A19: (Line ((1. (L,m)),i)) . i = (1. (L,m)) * (i,i) by MATRIX_1:def_7 .= 1. L by A13, MATRIX_1:def_11 ; i in dom (Line ((1. (L,m)),i)) by A7, A10, A9, FINSEQ_1:def_3; then Sum (mlt ((Line ((1. (L,m)),i)),(Col (M,j)))) = (Col (M,j)) . i by A19, A14, A18, MATRIX_3:17; hence M * (i,j) = ((1. (L,m)) * M) * (i,j) by A8, A7, MATRIX_1:def_8; ::_thesis: verum end; width M = width ((1. (L,m)) * M) by A2, MATRIX_3:def_4; hence (1. (L,m)) * M = M by A3, A4, A5, MATRIX_1:21; ::_thesis: verum end; theorem Th36: :: POLYNOM8:36 for L being Field for m being Element of NAT st 0 < m holds for u, v, u1 being Matrix of m,L st ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds (u * v) * (i,j) = (emb (m,L)) * (u1 * (i,j)) ) holds u * v = (emb (m,L)) * u1 proof let L be Field; ::_thesis: for m being Element of NAT st 0 < m holds for u, v, u1 being Matrix of m,L st ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds (u * v) * (i,j) = (emb (m,L)) * (u1 * (i,j)) ) holds u * v = (emb (m,L)) * u1 let m be Element of NAT ; ::_thesis: ( 0 < m implies for u, v, u1 being Matrix of m,L st ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds (u * v) * (i,j) = (emb (m,L)) * (u1 * (i,j)) ) holds u * v = (emb (m,L)) * u1 ) assume A1: m > 0 ; ::_thesis: for u, v, u1 being Matrix of m,L st ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds (u * v) * (i,j) = (emb (m,L)) * (u1 * (i,j)) ) holds u * v = (emb (m,L)) * u1 let u, v, u1 be Matrix of m,L; ::_thesis: ( ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds (u * v) * (i,j) = (emb (m,L)) * (u1 * (i,j)) ) implies u * v = (emb (m,L)) * u1 ) assume A2: for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds (u * v) * (i,j) = (emb (m,L)) * (u1 * (i,j)) ; ::_thesis: u * v = (emb (m,L)) * u1 A3: for i, j being Nat st [i,j] in Indices (u * v) holds (u * v) * (i,j) = ((emb (m,L)) * u1) * (i,j) proof let i, j be Nat; ::_thesis: ( [i,j] in Indices (u * v) implies (u * v) * (i,j) = ((emb (m,L)) * u1) * (i,j) ) A4: ( [i,j] in Indices (u * v) implies ( 1 <= i & i <= m & 1 <= j & j <= m ) ) proof width u = m by MATRIX_1:24 .= len v by MATRIX_1:24 ; then A5: width (u * v) = width v by MATRIX_3:def_4 .= m by MATRIX_1:24 ; assume A6: [i,j] in Indices (u * v) ; ::_thesis: ( 1 <= i & i <= m & 1 <= j & j <= m ) then A7: j in Seg m by A5, ZFMISC_1:87; width u = m by MATRIX_1:24 .= len v by MATRIX_1:24 ; then len (u * v) = len u by MATRIX_3:def_4 .= m by MATRIX_1:24 ; then u * v is Matrix of m,m,L by A1, A5, MATRIX_1:20; then Indices (u * v) = [:(Seg m),(Seg m):] by A5, MATRIX_1:25; then i in Seg m by A6, ZFMISC_1:87; hence ( 1 <= i & i <= m & 1 <= j & j <= m ) by A7, FINSEQ_1:1; ::_thesis: verum end; assume A8: [i,j] in Indices (u * v) ; ::_thesis: (u * v) * (i,j) = ((emb (m,L)) * u1) * (i,j) then ( i in Seg m & j in Seg m ) by A4, FINSEQ_1:1; then [i,j] in [:(Seg m),(Seg m):] by ZFMISC_1:87; then [i,j] in Indices u1 by MATRIX_1:24; then ((emb (m,L)) * u1) * (i,j) = (emb (m,L)) * (u1 * (i,j)) by MATRIX_3:def_5; hence (u * v) * (i,j) = ((emb (m,L)) * u1) * (i,j) by A2, A8, A4; ::_thesis: verum end; A9: width ((emb (m,L)) * u1) = width u1 by MATRIX_3:def_5 .= m by MATRIX_1:24 ; width u = m by MATRIX_1:24 .= len v by MATRIX_1:24 ; then A10: width (u * v) = width v by MATRIX_3:def_4 .= m by MATRIX_1:24 ; width u = m by MATRIX_1:24 .= len v by MATRIX_1:24 ; then A11: len (u * v) = len u by MATRIX_3:def_4 .= m by MATRIX_1:24 ; len ((emb (m,L)) * u1) = len u1 by MATRIX_3:def_5 .= m by MATRIX_1:24 ; hence u * v = (emb (m,L)) * u1 by A11, A9, A10, A3, MATRIX_1:21; ::_thesis: verum end; Lm12: for L being Field for m being Element of NAT st m > 0 holds for p, q being Polynomial of L holds (emb ((2 * m),L)) * ((1. (L,(2 * m))) * (mConv ((p *' q),(2 * m)))) = (emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))) proof let L be Field; ::_thesis: for m being Element of NAT st m > 0 holds for p, q being Polynomial of L holds (emb ((2 * m),L)) * ((1. (L,(2 * m))) * (mConv ((p *' q),(2 * m)))) = (emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))) let m be Element of NAT ; ::_thesis: ( m > 0 implies for p, q being Polynomial of L holds (emb ((2 * m),L)) * ((1. (L,(2 * m))) * (mConv ((p *' q),(2 * m)))) = (emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))) ) assume A1: m > 0 ; ::_thesis: for p, q being Polynomial of L holds (emb ((2 * m),L)) * ((1. (L,(2 * m))) * (mConv ((p *' q),(2 * m)))) = (emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))) let p, q be Polynomial of L; ::_thesis: (emb ((2 * m),L)) * ((1. (L,(2 * m))) * (mConv ((p *' q),(2 * m)))) = (emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))) 2 * m > 2 * 0 by A1, XREAL_1:68; hence (emb ((2 * m),L)) * ((1. (L,(2 * m))) * (mConv ((p *' q),(2 * m)))) = (emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))) by Th35; ::_thesis: verum end; theorem Th37: :: POLYNOM8:37 for L being Field for x being Element of L for s being FinSequence of L for i, j, m being Element of NAT st x is_primitive_root_of_degree m & 1 <= i & i <= m & 1 <= j & j <= m & len s = m & ( for k being Nat st 1 <= k & k <= m holds s /. k = pow (x,((i - j) * (k - 1))) ) holds ((VM (x,m)) * (VM ((x "),m))) * (i,j) = Sum s proof let L be Field; ::_thesis: for x being Element of L for s being FinSequence of L for i, j, m being Element of NAT st x is_primitive_root_of_degree m & 1 <= i & i <= m & 1 <= j & j <= m & len s = m & ( for k being Nat st 1 <= k & k <= m holds s /. k = pow (x,((i - j) * (k - 1))) ) holds ((VM (x,m)) * (VM ((x "),m))) * (i,j) = Sum s let x be Element of L; ::_thesis: for s being FinSequence of L for i, j, m being Element of NAT st x is_primitive_root_of_degree m & 1 <= i & i <= m & 1 <= j & j <= m & len s = m & ( for k being Nat st 1 <= k & k <= m holds s /. k = pow (x,((i - j) * (k - 1))) ) holds ((VM (x,m)) * (VM ((x "),m))) * (i,j) = Sum s let s be FinSequence of L; ::_thesis: for i, j, m being Element of NAT st x is_primitive_root_of_degree m & 1 <= i & i <= m & 1 <= j & j <= m & len s = m & ( for k being Nat st 1 <= k & k <= m holds s /. k = pow (x,((i - j) * (k - 1))) ) holds ((VM (x,m)) * (VM ((x "),m))) * (i,j) = Sum s let i, j, m be Element of NAT ; ::_thesis: ( x is_primitive_root_of_degree m & 1 <= i & i <= m & 1 <= j & j <= m & len s = m & ( for k being Nat st 1 <= k & k <= m holds s /. k = pow (x,((i - j) * (k - 1))) ) implies ((VM (x,m)) * (VM ((x "),m))) * (i,j) = Sum s ) assume that A1: x is_primitive_root_of_degree m and A2: ( 1 <= i & i <= m ) and A3: 1 <= j and A4: j <= m and A5: len s = m and A6: for k being Nat st 1 <= k & k <= m holds s /. k = pow (x,((i - j) * (k - 1))) ; ::_thesis: ((VM (x,m)) * (VM ((x "),m))) * (i,j) = Sum s len (Line ((VM (x,m)),i)) = width (VM (x,m)) by MATRIX_1:def_7 .= m by MATRIX_1:24 .= len (VM ((x "),m)) by MATRIX_1:24 .= len (Col ((VM ((x "),m)),j)) by MATRIX_1:def_8 ; then A7: len (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) = len (Line ((VM (x,m)),i)) by MATRIX_3:6 .= width (VM (x,m)) by MATRIX_1:def_7 .= m by MATRIX_1:24 ; A8: x <> 0. L by A1, Th30; A9: for k being Nat st 1 <= k & k <= m holds ((Line ((VM (x,m)),i)) /. k) * ((Col ((VM ((x "),m)),j)) /. k) = pow (x,((i - j) * (k - 1))) proof len (Col ((VM ((x "),m)),j)) = len (VM ((x "),m)) by MATRIX_1:def_8 .= m by MATRIX_1:24 ; then A10: Seg m = dom (Col ((VM ((x "),m)),j)) by FINSEQ_1:def_3; len (Line ((VM (x,m)),i)) = width (VM (x,m)) by MATRIX_1:def_7 .= m by MATRIX_1:24 ; then A11: Seg m = dom (Line ((VM (x,m)),i)) by FINSEQ_1:def_3; A12: 1 - 1 <= j - 1 by A3, XREAL_1:9; let k be Nat; ::_thesis: ( 1 <= k & k <= m implies ((Line ((VM (x,m)),i)) /. k) * ((Col ((VM ((x "),m)),j)) /. k) = pow (x,((i - j) * (k - 1))) ) assume that A13: 1 <= k and A14: k <= m ; ::_thesis: ((Line ((VM (x,m)),i)) /. k) * ((Col ((VM ((x "),m)),j)) /. k) = pow (x,((i - j) * (k - 1))) ( len (VM ((x "),m)) = m & k in Seg m ) by A13, A14, FINSEQ_1:1, MATRIX_1:24; then A15: k in dom (VM ((x "),m)) by FINSEQ_1:def_3; k in Seg m by A13, A14, FINSEQ_1:1; then A16: (Line ((VM (x,m)),i)) /. k = (Line ((VM (x,m)),i)) . k by A11, PARTFUN1:def_6; 1 - 1 <= k - 1 by A13, XREAL_1:9; then A17: (j - 1) * (k - 1) in NAT by A12, INT_1:3; width (VM (x,m)) = m by MATRIX_1:24; then k in Seg (width (VM (x,m))) by A13, A14, FINSEQ_1:1; then A18: (Line ((VM (x,m)),i)) . k = (VM (x,m)) * (i,k) by MATRIX_1:def_7; k in Seg m by A13, A14, FINSEQ_1:1; then A19: (Col ((VM ((x "),m)),j)) /. k = (Col ((VM ((x "),m)),j)) . k by A10, PARTFUN1:def_6; (VM ((x "),m)) * (k,j) = pow ((x "),((j - 1) * (k - 1))) by A3, A4, A13, A14, Def8 .= pow (x,(- ((j - 1) * (k - 1)))) by A8, A17, Th22 ; then (Col ((VM ((x "),m)),j)) . k = pow (x,(- ((j - 1) * (k - 1)))) by A15, MATRIX_1:def_8; then ((Line ((VM (x,m)),i)) /. k) * ((Col ((VM ((x "),m)),j)) /. k) = (pow (x,((i - 1) * (k - 1)))) * (pow (x,(- ((j - 1) * (k - 1))))) by A2, A13, A14, A16, A18, A19, Def8 .= pow (x,((i - j) * (k - 1))) by A8, Th23 ; hence ((Line ((VM (x,m)),i)) /. k) * ((Col ((VM ((x "),m)),j)) /. k) = pow (x,((i - j) * (k - 1))) ; ::_thesis: verum end; A20: for k being Nat st 1 <= k & k <= m holds (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) /. k = s /. k proof len (Col ((VM ((x "),m)),j)) = len (VM ((x "),m)) by MATRIX_1:def_8 .= m by MATRIX_1:24 ; then A21: Seg m = dom (Col ((VM ((x "),m)),j)) by FINSEQ_1:def_3; let k be Nat; ::_thesis: ( 1 <= k & k <= m implies (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) /. k = s /. k ) len (Line ((VM (x,m)),i)) = width (VM (x,m)) by MATRIX_1:def_7 .= m by MATRIX_1:24 ; then A22: Seg m = dom (Line ((VM (x,m)),i)) by FINSEQ_1:def_3; assume A23: ( 1 <= k & k <= m ) ; ::_thesis: (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) /. k = s /. k then A24: ((Line ((VM (x,m)),i)) /. k) * ((Col ((VM ((x "),m)),j)) /. k) = pow (x,((i - j) * (k - 1))) by A9 .= s /. k by A6, A23 ; k in Seg m by A23, FINSEQ_1:1; then A25: (Col ((VM ((x "),m)),j)) . k = (Col ((VM ((x "),m)),j)) /. k by A21, PARTFUN1:def_6; Seg m = dom (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) by A7, FINSEQ_1:def_3; then A26: k in dom (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) by A23, FINSEQ_1:1; k in Seg m by A23, FINSEQ_1:1; then (Line ((VM (x,m)),i)) . k = (Line ((VM (x,m)),i)) /. k by A22, PARTFUN1:def_6; then (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) . k = ((Line ((VM (x,m)),i)) /. k) * ((Col ((VM ((x "),m)),j)) /. k) by A26, A25, FVSUM_1:60; hence (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) /. k = s /. k by A26, A24, PARTFUN1:def_6; ::_thesis: verum end; A27: for k being Nat st k in dom (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) holds (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) . k = s . k proof let k be Nat; ::_thesis: ( k in dom (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) implies (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) . k = s . k ) assume A28: k in dom (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) ; ::_thesis: (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) . k = s . k A29: Seg m = dom (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) by A7, FINSEQ_1:def_3; then A30: ( 1 <= k & k <= m ) by A28, FINSEQ_1:1; A31: k in dom s by A5, A28, A29, FINSEQ_1:def_3; (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) . k = (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) /. k by A28, PARTFUN1:def_6 .= s /. k by A20, A30 .= s . k by A31, PARTFUN1:def_6 ; hence (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) . k = s . k ; ::_thesis: verum end; dom (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) = Seg m by A7, FINSEQ_1:def_3 .= dom s by A5, FINSEQ_1:def_3 ; then A32: Sum (mlt ((Line ((VM (x,m)),i)),(Col ((VM ((x "),m)),j)))) = Sum s by A27, FINSEQ_1:13; width (VM (x,m)) = m by MATRIX_1:24; then A33: width (VM (x,m)) = len (VM ((x "),m)) by MATRIX_1:24; A34: ( width (VM (x,m)) = m & len (VM ((x "),m)) = m ) by MATRIX_1:24; len (VM (x,m)) = m by MATRIX_1:24; then A35: len ((VM (x,m)) * (VM ((x "),m))) = m by A34, MATRIX_3:def_4; width (VM ((x "),m)) = m by MATRIX_1:24; then width ((VM (x,m)) * (VM ((x "),m))) = m by A34, MATRIX_3:def_4; then (VM (x,m)) * (VM ((x "),m)) is Matrix of m,L by A2, A35, MATRIX_1:20; then A36: Indices ((VM (x,m)) * (VM ((x "),m))) = [:(Seg m),(Seg m):] by MATRIX_1:24; ( i in Seg m & j in Seg m ) by A2, A3, A4; then [i,j] in Indices ((VM (x,m)) * (VM ((x "),m))) by A36, ZFMISC_1:def_2; then ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (Line ((VM (x,m)),i)) "*" (Col ((VM ((x "),m)),j)) by A33, MATRIX_3:def_4; hence ((VM (x,m)) * (VM ((x "),m))) * (i,j) = Sum s by A32, FVSUM_1:def_9; ::_thesis: verum end; theorem Th38: :: POLYNOM8:38 for L being Field for m, i, j being Element of NAT for x being Element of L st i <> j & 1 <= i & i <= m & 1 <= j & j <= m & x is_primitive_root_of_degree m holds ((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L proof let L be Field; ::_thesis: for m, i, j being Element of NAT for x being Element of L st i <> j & 1 <= i & i <= m & 1 <= j & j <= m & x is_primitive_root_of_degree m holds ((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L let m, i, j be Element of NAT ; ::_thesis: for x being Element of L st i <> j & 1 <= i & i <= m & 1 <= j & j <= m & x is_primitive_root_of_degree m holds ((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L let x be Element of L; ::_thesis: ( i <> j & 1 <= i & i <= m & 1 <= j & j <= m & x is_primitive_root_of_degree m implies ((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L ) assume that A1: i <> j and A2: ( 1 <= i & i <= m & 1 <= j & j <= m ) and A3: x is_primitive_root_of_degree m ; ::_thesis: ((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L A4: x <> 0. L by A3, Th30; then A5: pow (x,(m * (i - j))) = pow ((pow (x,m)),(i - j)) by Th26 .= pow ((x |^ m),(i - j)) by Def3 .= pow ((1. L),(i - j)) by A3, Def6 .= 1. L by Th16 ; ex G being FinSequence of L st ( dom G = Seg m & ( for k being Nat st k in Seg m holds G . k = pow (x,((i - j) * (k - 1))) ) ) proof defpred S1[ Nat, set ] means $2 = pow (x,((i - j) * ($1 - 1))); A6: for n being Nat st n in Seg m holds ex x being Element of L st S1[n,x] ; ex G being FinSequence of L st ( dom G = Seg m & ( for nn being Nat st nn in Seg m holds S1[nn,G . nn] ) ) from FINSEQ_1:sch_5(A6); hence ex G being FinSequence of L st ( dom G = Seg m & ( for k being Nat st k in Seg m holds G . k = pow (x,((i - j) * (k - 1))) ) ) ; ::_thesis: verum end; then consider s being FinSequence of L such that A7: dom s = Seg m and A8: for k being Nat st k in Seg m holds s . k = pow (x,((i - j) * (k - 1))) ; A9: for k being Nat st 1 <= k & k <= m holds s /. k = pow (x,((i - j) * (k - 1))) proof let k be Nat; ::_thesis: ( 1 <= k & k <= m implies s /. k = pow (x,((i - j) * (k - 1))) ) assume A10: ( 1 <= k & k <= m ) ; ::_thesis: s /. k = pow (x,((i - j) * (k - 1))) then A11: k in dom s by A7, FINSEQ_1:1; k in Seg m by A10, FINSEQ_1:1; then pow (x,((i - j) * (k - 1))) = s . k by A8 .= s /. k by A11, PARTFUN1:def_6 ; hence s /. k = pow (x,((i - j) * (k - 1))) ; ::_thesis: verum end; consider r being Element of L such that A12: r = pow (x,(i - j)) ; A13: len s = m by A7, FINSEQ_1:def_3; for k being Nat st 1 <= k & k <= len s holds s . k = (pow (x,(i - j))) |^ (k -' 1) proof let k be Nat; ::_thesis: ( 1 <= k & k <= len s implies s . k = (pow (x,(i - j))) |^ (k -' 1) ) assume that A14: 1 <= k and A15: k <= len s ; ::_thesis: s . k = (pow (x,(i - j))) |^ (k -' 1) A16: 1 - 1 <= k - 1 by A14, XREAL_1:9; s . k = s /. k by A14, A15, FINSEQ_4:15 .= pow (x,((i - j) * (k - 1))) by A9, A13, A14, A15 .= pow (x,((i - j) * (k -' 1))) by A16, XREAL_0:def_2 .= pow ((pow (x,(i - j))),(k -' 1)) by A4, Th26 .= (pow (x,(i - j))) |^ (k -' 1) by Def3 ; hence s . k = (pow (x,(i - j))) |^ (k -' 1) ; ::_thesis: verum end; then Sum s = ((1. L) - ((pow (x,(i - j))) |^ (len s))) / ((1. L) - (pow (x,(i - j)))) by A1, A2, A3, Th5, Th32 .= ((1. L) - ((pow (x,(i - j))) |^ m)) / ((1. L) - (pow (x,(i - j)))) by A7, FINSEQ_1:def_3 .= ((1. L) - (pow ((pow (x,(i - j))),m))) / ((1. L) - (pow (x,(i - j)))) by Def3 .= ((1. L) - (pow (x,((i - j) * m)))) / ((1. L) - (pow (x,(i - j)))) by A4, Th26 .= (0. L) / ((1. L) - r) by A5, A12, VECTSP_1:19 .= 0. L by VECTSP_1:7 ; hence ((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L by A2, A3, A9, A13, Th37; ::_thesis: verum end; theorem Th39: :: POLYNOM8:39 for L being Field for m being Element of NAT st m > 0 holds for x being Element of L st x is_primitive_root_of_degree m holds (VM (x,m)) * (VM ((x "),m)) = (emb (m,L)) * (1. (L,m)) proof let L be Field; ::_thesis: for m being Element of NAT st m > 0 holds for x being Element of L st x is_primitive_root_of_degree m holds (VM (x,m)) * (VM ((x "),m)) = (emb (m,L)) * (1. (L,m)) let m be Element of NAT ; ::_thesis: ( m > 0 implies for x being Element of L st x is_primitive_root_of_degree m holds (VM (x,m)) * (VM ((x "),m)) = (emb (m,L)) * (1. (L,m)) ) assume A1: m > 0 ; ::_thesis: for x being Element of L st x is_primitive_root_of_degree m holds (VM (x,m)) * (VM ((x "),m)) = (emb (m,L)) * (1. (L,m)) let x be Element of L; ::_thesis: ( x is_primitive_root_of_degree m implies (VM (x,m)) * (VM ((x "),m)) = (emb (m,L)) * (1. (L,m)) ) assume A2: x is_primitive_root_of_degree m ; ::_thesis: (VM (x,m)) * (VM ((x "),m)) = (emb (m,L)) * (1. (L,m)) for i, j being Nat st i >= 1 & i <= m & j >= 1 & j <= m holds ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j)) proof let i, j be Nat; ::_thesis: ( i >= 1 & i <= m & j >= 1 & j <= m implies ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j)) ) A3: ( i in NAT & j in NAT ) by ORDINAL1:def_12; ex G being FinSequence of L st ( dom G = Seg m & ( for k being Nat st k in Seg m holds G . k = pow (x,((i - j) * (k - 1))) ) ) proof defpred S1[ Nat, set ] means $2 = pow (x,((i - j) * ($1 - 1))); A4: for n being Nat st n in Seg m holds ex x being Element of L st S1[n,x] ; ex G being FinSequence of L st ( dom G = Seg m & ( for nn being Nat st nn in Seg m holds S1[nn,G . nn] ) ) from FINSEQ_1:sch_5(A4); hence ex G being FinSequence of L st ( dom G = Seg m & ( for k being Nat st k in Seg m holds G . k = pow (x,((i - j) * (k - 1))) ) ) ; ::_thesis: verum end; then consider s being FinSequence of L such that A5: dom s = Seg m and A6: for k being Nat st k in Seg m holds s . k = pow (x,((i - j) * (k - 1))) ; A7: len s = m by A5, FINSEQ_1:def_3; A8: for k being Nat st 1 <= k & k <= m holds s /. k = pow (x,((i - j) * (k - 1))) proof let k be Nat; ::_thesis: ( 1 <= k & k <= m implies s /. k = pow (x,((i - j) * (k - 1))) ) assume A9: ( 1 <= k & k <= m ) ; ::_thesis: s /. k = pow (x,((i - j) * (k - 1))) then A10: k in dom s by A5, FINSEQ_1:1; k in Seg m by A9, FINSEQ_1:1; then pow (x,((i - j) * (k - 1))) = s . k by A6 .= s /. k by A10, PARTFUN1:def_6 ; hence s /. k = pow (x,((i - j) * (k - 1))) ; ::_thesis: verum end; A11: Indices (1. (L,m)) = [:(Seg m),(Seg m):] by MATRIX_1:24; assume that A12: ( 1 <= i & i <= m ) and A13: ( 1 <= j & j <= m ) ; ::_thesis: ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j)) percases ( i = j or i <> j ) ; supposeA14: i = j ; ::_thesis: ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j)) A15: for k being Element of NAT st 1 <= k & k <= m holds s /. k = 1. L proof let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= m implies s /. k = 1. L ) assume ( 1 <= k & k <= m ) ; ::_thesis: s /. k = 1. L then s /. k = pow (x,((i - j) * (k - 1))) by A8 .= 1. L by A14, Th13 ; hence s /. k = 1. L ; ::_thesis: verum end; i in Seg m by A12, FINSEQ_1:1; then A16: [i,i] in Indices (1. (L,m)) by A11, ZFMISC_1:87; ((VM (x,m)) * (VM ((x "),m))) * (i,j) = Sum s by A2, A3, A12, A13, A7, A8, Th37 .= m * (1. L) by A7, A15, Th4 .= (emb (m,L)) * (1. L) by VECTSP_1:def_8 ; hence ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j)) by A14, A16, MATRIX_1:def_11; ::_thesis: verum end; supposeA17: i <> j ; ::_thesis: ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j)) ( i in Seg m & j in Seg m ) by A12, A13, FINSEQ_1:1; then A18: [i,j] in Indices (1. (L,m)) by A11, ZFMISC_1:87; ((VM (x,m)) * (VM ((x "),m))) * (i,j) = 0. L by A2, A3, A12, A13, A17, Th38 .= (emb (m,L)) * (0. L) by VECTSP_1:6 ; hence ((VM (x,m)) * (VM ((x "),m))) * (i,j) = (emb (m,L)) * ((1. (L,m)) * (i,j)) by A17, A18, MATRIX_1:def_11; ::_thesis: verum end; end; end; hence (VM (x,m)) * (VM ((x "),m)) = (emb (m,L)) * (1. (L,m)) by A1, Th36; ::_thesis: verum end; theorem Th40: :: POLYNOM8:40 for L being Field for m being Element of NAT for x being Element of L st m > 0 & x is_primitive_root_of_degree m holds (VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m)) proof let L be Field; ::_thesis: for m being Element of NAT for x being Element of L st m > 0 & x is_primitive_root_of_degree m holds (VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m)) let m be Element of NAT ; ::_thesis: for x being Element of L st m > 0 & x is_primitive_root_of_degree m holds (VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m)) let x be Element of L; ::_thesis: ( m > 0 & x is_primitive_root_of_degree m implies (VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m)) ) assume that A1: 0 < m and A2: x is_primitive_root_of_degree m ; ::_thesis: (VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m)) x <> 0. L by A2, Th30; then (VM ((x "),m)) * (VM (x,m)) = (VM ((x "),m)) * (VM (((x ") "),m)) by VECTSP_1:24 .= (emb (m,L)) * (1. (L,m)) by A1, A2, Th31, Th39 ; hence (VM (x,m)) * (VM ((x "),m)) = (VM ((x "),m)) * (VM (x,m)) by A1, A2, Th39; ::_thesis: verum end; begin theorem Th41: :: POLYNOM8:41 for L being Field for p being Polynomial of L for m being Element of NAT st m > 0 & len p <= m holds for x being Element of L for i being Element of NAT st i < m holds (DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) proof let L be Field; ::_thesis: for p being Polynomial of L for m being Element of NAT st m > 0 & len p <= m holds for x being Element of L for i being Element of NAT st i < m holds (DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) let p be Polynomial of L; ::_thesis: for m being Element of NAT st m > 0 & len p <= m holds for x being Element of L for i being Element of NAT st i < m holds (DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) let m be Element of NAT ; ::_thesis: ( m > 0 & len p <= m implies for x being Element of L for i being Element of NAT st i < m holds (DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) ) assume that A1: m > 0 and A2: len p <= m ; ::_thesis: for x being Element of L for i being Element of NAT st i < m holds (DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) let x be Element of L; ::_thesis: for i being Element of NAT st i < m holds (DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) set v = VM (x,m); for i being Element of NAT st i < m holds (DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) proof A3: for k being Nat st k < m holds (Col ((mConv (p,m)),1)) . (k + 1) = p . k proof let k be Nat; ::_thesis: ( k < m implies (Col ((mConv (p,m)),1)) . (k + 1) = p . k ) assume A4: k < m ; ::_thesis: (Col ((mConv (p,m)),1)) . (k + 1) = p . k then ( 1 <= k + 1 & k + 1 <= m ) by NAT_1:11, NAT_1:13; then A5: k + 1 in Seg m ; len (mConv (p,m)) = m by A1, Th28; then k + 1 in dom (mConv (p,m)) by A5, FINSEQ_1:def_3; then (Col ((mConv (p,m)),1)) . (k + 1) = (mConv (p,m)) * ((k + 1),1) by MATRIX_1:def_8; hence (Col ((mConv (p,m)),1)) . (k + 1) = p . k by A4, Th28; ::_thesis: verum end; A6: width (VM (x,m)) = m by MATRIX_1:24 .= len (mConv (p,m)) by A1, Th28 ; then A7: len ((VM (x,m)) * (mConv (p,m))) = len (VM (x,m)) by MATRIX_3:def_4 .= m by MATRIX_1:24 ; width ((VM (x,m)) * (mConv (p,m))) = width (mConv (p,m)) by A6, MATRIX_3:def_4 .= 1 by A1, Th28 ; then (VM (x,m)) * (mConv (p,m)) is Matrix of m,1,L by A1, A7, MATRIX_1:20; then A8: Indices ((VM (x,m)) * (mConv (p,m))) = [:(Seg m),(Seg (width ((VM (x,m)) * (mConv (p,m))))):] by MATRIX_1:25; A9: len (mConv (p,m)) = m by A1, Th28 .= width (VM (x,m)) by MATRIX_1:24 ; width ((VM (x,m)) * (mConv (p,m))) = width (mConv (p,m)) by A6, MATRIX_3:def_4 .= 1 by A1, Th28 ; then A10: 1 in Seg (width ((VM (x,m)) * (mConv (p,m)))) ; let i be Element of NAT ; ::_thesis: ( i < m implies (DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) ) assume A11: i < m ; ::_thesis: (DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) A12: for k being Nat st k < m holds (Line ((VM (x,m)),(i + 1))) . (k + 1) = (VM (x,m)) * ((i + 1),(k + 1)) proof let k be Nat; ::_thesis: ( k < m implies (Line ((VM (x,m)),(i + 1))) . (k + 1) = (VM (x,m)) * ((i + 1),(k + 1)) ) assume k < m ; ::_thesis: (Line ((VM (x,m)),(i + 1))) . (k + 1) = (VM (x,m)) * ((i + 1),(k + 1)) then ( 1 <= k + 1 & k + 1 <= m ) by NAT_1:11, NAT_1:13; then k + 1 in Seg m ; then k + 1 in Seg (width (VM (x,m))) by MATRIX_1:24; hence (Line ((VM (x,m)),(i + 1))) . (k + 1) = (VM (x,m)) * ((i + 1),(k + 1)) by MATRIX_1:def_7; ::_thesis: verum end; A13: for k being Nat st k < m holds (Line ((VM (x,m)),(i + 1))) . (k + 1) = pow (x,(i * k)) proof let k be Nat; ::_thesis: ( k < m implies (Line ((VM (x,m)),(i + 1))) . (k + 1) = pow (x,(i * k)) ) assume A14: k < m ; ::_thesis: (Line ((VM (x,m)),(i + 1))) . (k + 1) = pow (x,(i * k)) then A15: ( 1 <= k + 1 & k + 1 <= m ) by NAT_1:11, NAT_1:13; A16: ( 1 <= i + 1 & i + 1 <= m ) by A11, NAT_1:11, NAT_1:13; (Line ((VM (x,m)),(i + 1))) . (k + 1) = (VM (x,m)) * ((i + 1),(k + 1)) by A12, A14 .= pow (x,(((i + 1) - 1) * ((k + 1) - 1))) by A16, A15, Def8 .= pow (x,(i * k)) ; hence (Line ((VM (x,m)),(i + 1))) . (k + 1) = pow (x,(i * k)) ; ::_thesis: verum end; A17: for k being Nat for a, b, c being Element of L st a = (Line ((VM (x,m)),(i + 1))) . (k + 1) & b = (Col ((mConv (p,m)),1)) . (k + 1) & c = p . k & k < m holds a * b = (pow (x,(i * k))) * c proof let k be Nat; ::_thesis: for a, b, c being Element of L st a = (Line ((VM (x,m)),(i + 1))) . (k + 1) & b = (Col ((mConv (p,m)),1)) . (k + 1) & c = p . k & k < m holds a * b = (pow (x,(i * k))) * c let a, b, c be Element of L; ::_thesis: ( a = (Line ((VM (x,m)),(i + 1))) . (k + 1) & b = (Col ((mConv (p,m)),1)) . (k + 1) & c = p . k & k < m implies a * b = (pow (x,(i * k))) * c ) assume that A18: a = (Line ((VM (x,m)),(i + 1))) . (k + 1) and A19: ( b = (Col ((mConv (p,m)),1)) . (k + 1) & c = p . k ) and A20: k < m ; ::_thesis: a * b = (pow (x,(i * k))) * c a = pow (x,(i * k)) by A13, A18, A20; hence a * b = (pow (x,(i * k))) * c by A3, A19, A20; ::_thesis: verum end; A21: for k being Element of NAT st 1 <= k & k <= m holds (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1))) proof A22: len (mConv (p,m)) = m by A1, Th28; let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= m implies (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1))) ) assume that A23: 1 <= k and A24: k <= m ; ::_thesis: (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1))) k in Seg m by A23, A24; then k in dom (mConv (p,m)) by A22, FINSEQ_1:def_3; then A25: (Col ((mConv (p,m)),1)) . k = (mConv (p,m)) * (k,1) by MATRIX_1:def_8; 0 < k by A23; then ( dom p = NAT & k - 1 is Element of NAT ) by FUNCT_2:def_1, NAT_1:20; then A26: p . (k - 1) = p /. (k - 1) by PARTFUN1:def_6; Seg (width (VM (x,m))) = Seg m by MATRIX_1:24; then k in Seg (width (VM (x,m))) by A23, A24; then (Line ((VM (x,m)),(i + 1))) . k = (VM (x,m)) * ((i + 1),k) by MATRIX_1:def_7; then reconsider a = (Line ((VM (x,m)),(i + 1))) . k, b = (Col ((mConv (p,m)),1)) . k, c = p . (k - 1) as Element of L by A25, A26; len (Line ((VM (x,m)),(i + 1))) = width (VM (x,m)) by MATRIX_1:def_7 .= m by MATRIX_1:24 .= len (mConv (p,m)) by A1, Th28 .= len (Col ((mConv (p,m)),1)) by MATRIX_1:def_8 ; then len (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) = len (Line ((VM (x,m)),(i + 1))) by MATRIX_3:6 .= width (VM (x,m)) by MATRIX_1:def_7 .= m by MATRIX_1:24 ; then dom (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) = Seg m by FINSEQ_1:def_3; then k in dom (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) by A23, A24; then A27: (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = a * b by FVSUM_1:60; A28: a * b = (pow (x,(i * (k - 1)))) * c proof A29: 0 < k by A23; then A30: k - 1 is Nat by NAT_1:20; ( k - 1 <= m - 1 & m - 1 is Nat ) by A1, A24, NAT_1:20, XREAL_1:9; then A31: k - 1 < (m - 1) + 1 by A30, NAT_1:13; reconsider l = k - 1 as Nat by A29, NAT_1:20; a = (Line ((VM (x,m)),(i + 1))) . (l + 1) ; hence a * b = (pow (x,(i * (k - 1)))) * c by A17, A31; ::_thesis: verum end; reconsider d = pow (x,(i * (k - 1))) as Element of L ; A32: k - 1 >= 0 by A23, NAT_1:20; d = pow ((x |^ i),(k - 1)) by A23, Th27 .= (power L) . ((x |^ i),(k - 1)) by A32, Def3 .= (power L) . ((x |^ i),(k -' 1)) by A32, XREAL_0:def_2 ; hence (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1))) by A28, A27, A32, XREAL_0:def_2; ::_thesis: verum end; A33: Sum (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) = eval (p,(x |^ i)) proof A34: for k being Nat st len p < k & k <= m holds (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = 0. L proof A35: 1 <= 1 + (len p) by NAT_1:11; let k be Nat; ::_thesis: ( len p < k & k <= m implies (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = 0. L ) assume that A36: len p < k and A37: k <= m ; ::_thesis: (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = 0. L A38: len p < (k - 1) + 1 by A36; (len p) + 1 <= k by A36, NAT_1:13; then A39: 1 <= k by A35, XXREAL_0:2; then 1 - 1 <= k - 1 by XREAL_1:9; then k -' 1 = k - 1 by XREAL_0:def_2; then A40: k -' 1 >= len p by A38, NAT_1:13; k in NAT by ORDINAL1:def_12; then (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1))) by A21, A37, A39 .= (0. L) * ((power L) . ((x |^ i),(k -' 1))) by A40, ALGSEQ_1:8 .= 0. L by VECTSP_1:7 ; hence (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = 0. L ; ::_thesis: verum end; len (Line ((VM (x,m)),(i + 1))) = width (VM (x,m)) by MATRIX_1:def_7 .= m by MATRIX_1:24 .= len (mConv (p,m)) by A1, Th28 .= len (Col ((mConv (p,m)),1)) by MATRIX_1:def_8 ; then A41: len (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) = len (Line ((VM (x,m)),(i + 1))) by MATRIX_3:6 .= width (VM (x,m)) by MATRIX_1:def_7 .= m by MATRIX_1:24 ; (len p) - (len p) <= m - (len p) by A2, XREAL_1:9; then reconsider lengthG = m - (len p) as Element of NAT by INT_1:3; consider F being FinSequence of L such that A42: eval (p,(x |^ i)) = Sum F and A43: len F = len p and A44: for k being Element of NAT st k in dom F holds F . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1))) by POLYNOM4:def_2; ex G being FinSequence of L st ( dom G = Seg lengthG & ( for k being Nat st k in Seg lengthG holds G . k = 0. L ) ) proof defpred S1[ set , set ] means $2 = 0. L; A45: for n being Nat st n in Seg lengthG holds ex x being Element of L st S1[n,x] ; ex G being FinSequence of L st ( dom G = Seg lengthG & ( for nn being Nat st nn in Seg lengthG holds S1[nn,G . nn] ) ) from FINSEQ_1:sch_5(A45); hence ex G being FinSequence of L st ( dom G = Seg lengthG & ( for k being Nat st k in Seg lengthG holds G . k = 0. L ) ) ; ::_thesis: verum end; then consider G being FinSequence of L such that A46: dom G = Seg lengthG and A47: for k being Nat st k in Seg lengthG holds G . k = 0. L ; A48: for k being Element of NAT st k in Seg lengthG holds G . k = 0. L by A47; A49: len G = m - (len p) by A46, FINSEQ_1:def_3; then (len F) + (len G) = m by A43; then dom (F ^ G) = Seg m by FINSEQ_1:def_7; then A50: dom (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) = dom (F ^ G) by A41, FINSEQ_1:def_3; A51: for k being Element of NAT st 1 <= k & k <= len p holds F . k = (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k proof let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= len p implies F . k = (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k ) assume that A52: 1 <= k and A53: k <= len p ; ::_thesis: F . k = (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k A54: k <= m by A2, A53, XXREAL_0:2; dom F = Seg (len p) by A43, FINSEQ_1:def_3; then k in dom F by A52, A53; then F . k = (p . (k -' 1)) * ((power L) . ((x |^ i),(k -' 1))) by A44 .= (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k by A21, A52, A54 ; hence F . k = (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k ; ::_thesis: verum end; for k being Nat st k in dom (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) holds (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k proof let k be Nat; ::_thesis: ( k in dom (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) implies (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k ) (len F) + (len G) = m by A43, A49; then A55: dom (F ^ G) = Seg m by FINSEQ_1:def_7; assume A56: k in dom (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) ; ::_thesis: (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k percases ( ( 1 <= k & k <= len F ) or ( len F < k & k <= m ) ) by A50, A56, A55, FINSEQ_1:1; supposeA57: ( 1 <= k & k <= len F ) ; ::_thesis: (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k then k in dom F by FINSEQ_3:25; then (F ^ G) . k = F . k by FINSEQ_1:def_7 .= (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k by A43, A51, A56, A57 ; hence (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k ; ::_thesis: verum end; supposeA58: ( len F < k & k <= m ) ; ::_thesis: (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k then (len F) + 1 <= k by NAT_1:13; then ((len F) + 1) - (len F) <= k - (len F) by XREAL_1:9; then reconsider l = k - (len F) as Element of NAT by INT_1:3; (len p) - m <= m - m by A2, XREAL_1:9; then - ((len p) - m) >= 0 ; then reconsider lengthG = m - (len p) as Element of NAT by INT_1:3; (len F) + 1 <= k by A58, NAT_1:13; then A59: ((len F) + 1) - (len F) <= k - (len F) by XREAL_1:9; l <= lengthG by A43, A58, XREAL_1:9; then A60: l in dom G by A46, A59; (len F) + (len G) = m by A43, A49; then dom (F ^ G) = Seg m by FINSEQ_1:def_7; then len (F ^ G) = m by FINSEQ_1:def_3; then (F ^ G) . k = G . (k - (len F)) by A58, FINSEQ_1:24 .= 0. L by A46, A47, A60 .= (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k by A43, A34, A58 ; hence (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) . k = (F ^ G) . k ; ::_thesis: verum end; end; end; then mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1))) = F ^ G by A50, FINSEQ_1:13; then Sum (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) = (Sum F) + (Sum G) by RLVECT_1:41 .= (Sum F) + (0. L) by A46, A48, POLYNOM3:1 .= eval (p,(x |^ i)) by A42, RLVECT_1:def_4 ; hence Sum (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) = eval (p,(x |^ i)) ; ::_thesis: verum end; A61: (Line ((VM (x,m)),(i + 1))) "*" (Col ((mConv (p,m)),1)) = Sum (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) by FVSUM_1:def_9; ( 1 <= i + 1 & i + 1 <= m ) by A11, NAT_1:11, NAT_1:13; then i + 1 in Seg m ; then [(i + 1),1] in Indices ((VM (x,m)) * (mConv (p,m))) by A8, A10, ZFMISC_1:def_2; then ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) = eval (p,(x |^ i)) by A9, A61, A33, MATRIX_3:def_4; hence (DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) by A11, Def7; ::_thesis: verum end; hence for i being Element of NAT st i < m holds (DFT (p,x,m)) . i = ((VM (x,m)) * (mConv (p,m))) * ((i + 1),1) ; ::_thesis: verum end; theorem Th42: :: POLYNOM8:42 for L being Field for p being Polynomial of L for m being Nat st 0 < m & len p <= m holds for x being Element of L holds DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m))) proof let L be Field; ::_thesis: for p being Polynomial of L for m being Nat st 0 < m & len p <= m holds for x being Element of L holds DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m))) let p be Polynomial of L; ::_thesis: for m being Nat st 0 < m & len p <= m holds for x being Element of L holds DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m))) let m be Nat; ::_thesis: ( 0 < m & len p <= m implies for x being Element of L holds DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m))) ) assume that A1: 0 < m and A2: len p <= m ; ::_thesis: for x being Element of L holds DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m))) let x be Element of L; ::_thesis: DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m))) A3: m in NAT by ORDINAL1:def_12; A4: now__::_thesis:_for_u9_being_set_st_u9_in_dom_(DFT_(p,x,m))_holds_ (DFT_(p,x,m))_._u9_=_(aConv_((VM_(x,m))_*_(mConv_(p,m))))_._u9 let u9 be set ; ::_thesis: ( u9 in dom (DFT (p,x,m)) implies (DFT (p,x,m)) . b1 = (aConv ((VM (x,m)) * (mConv (p,m)))) . b1 ) assume u9 in dom (DFT (p,x,m)) ; ::_thesis: (DFT (p,x,m)) . b1 = (aConv ((VM (x,m)) * (mConv (p,m)))) . b1 then reconsider u = u9 as Element of NAT by FUNCT_2:def_1; percases ( u < m or m <= u ) ; supposeA5: u < m ; ::_thesis: (DFT (p,x,m)) . b1 = (aConv ((VM (x,m)) * (mConv (p,m)))) . b1 width (VM (x,m)) = m by MATRIX_1:24 .= len (mConv (p,m)) by A1, Th28 ; then A6: len ((VM (x,m)) * (mConv (p,m))) = len (VM (x,m)) by MATRIX_3:def_4 .= m by MATRIX_1:24 ; thus (DFT (p,x,m)) . u9 = ((VM (x,m)) * (mConv (p,m))) * ((u + 1),1) by A3, A2, A5, Th41 .= (aConv ((VM (x,m)) * (mConv (p,m)))) . u9 by A5, A6, Def5 ; ::_thesis: verum end; supposeA7: m <= u ; ::_thesis: (DFT (p,x,m)) . b1 = (aConv ((VM (x,m)) * (mConv (p,m)))) . b1 width (VM (x,m)) = m by MATRIX_1:24 .= len (mConv (p,m)) by A1, Th28 ; then A8: len ((VM (x,m)) * (mConv (p,m))) = len (VM (x,m)) by MATRIX_3:def_4 .= m by MATRIX_1:24 ; thus (DFT (p,x,m)) . u9 = 0. L by A7, Def7 .= (aConv ((VM (x,m)) * (mConv (p,m)))) . u9 by A7, A8, Def5 ; ::_thesis: verum end; end; end; dom (DFT (p,x,m)) = NAT by FUNCT_2:def_1 .= dom (aConv ((VM (x,m)) * (mConv (p,m)))) by FUNCT_2:def_1 ; hence DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m))) by A4, FUNCT_1:2; ::_thesis: verum end; theorem Th43: :: POLYNOM8:43 for L being Field for p, q being Polynomial of L for m being Element of NAT st m > 0 & len p <= m & len q <= m holds for x being Element of L st x is_primitive_root_of_degree 2 * m holds DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) proof let L be Field; ::_thesis: for p, q being Polynomial of L for m being Element of NAT st m > 0 & len p <= m & len q <= m holds for x being Element of L st x is_primitive_root_of_degree 2 * m holds DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) let p, q be Polynomial of L; ::_thesis: for m being Element of NAT st m > 0 & len p <= m & len q <= m holds for x being Element of L st x is_primitive_root_of_degree 2 * m holds DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) let m be Element of NAT ; ::_thesis: ( m > 0 & len p <= m & len q <= m implies for x being Element of L st x is_primitive_root_of_degree 2 * m holds DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) ) assume that A1: m > 0 and A2: ( len p <= m & len q <= m ) ; ::_thesis: for x being Element of L st x is_primitive_root_of_degree 2 * m holds DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) let x be Element of L; ::_thesis: ( x is_primitive_root_of_degree 2 * m implies DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) ) assume A3: x is_primitive_root_of_degree 2 * m ; ::_thesis: DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) percases ( len p = 0 or len q = 0 or ( len p <> 0 & len q <> 0 ) ) ; supposeA4: ( len p = 0 or len q = 0 ) ; ::_thesis: DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) percases ( len p = 0 or len q = 0 ) by A4; suppose len p = 0 ; ::_thesis: DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) then p = 0_. L by POLYNOM4:5; then p *' q = 0_. L by POLYNOM3:34; then ( (emb ((2 * m),L)) * (p *' q) = 0_. L & DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = DFT ((0_. L),(x "),(2 * m)) ) by Th33, POLYNOM5:28; hence DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) by Th33; ::_thesis: verum end; suppose len q = 0 ; ::_thesis: DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) then q = 0_. L by POLYNOM4:5; then p *' q = 0_. L by POLYNOM3:34; then ( (emb ((2 * m),L)) * (p *' q) = 0_. L & DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = DFT ((0_. L),(x "),(2 * m)) ) by Th33, POLYNOM5:28; hence DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) by Th33; ::_thesis: verum end; end; end; supposeA5: ( len p <> 0 & len q <> 0 ) ; ::_thesis: DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) set v1 = VM (x,(2 * m)); set v2 = VM ((x "),(2 * m)); A6: (len p) + (len q) <= m + m by A2, XREAL_1:7; len (p *' q) <= (len p) + (len q) by A5, Th9; then A7: len (p *' q) <= 2 * m by A6, XXREAL_0:2; A8: for i being Nat st i < 2 * m holds ((VM (x,(2 * m))) * (mConv ((p *' q),(2 * m)))) * ((i + 1),1) = (DFT ((p *' q),x,(2 * m))) . i proof let i be Nat; ::_thesis: ( i < 2 * m implies ((VM (x,(2 * m))) * (mConv ((p *' q),(2 * m)))) * ((i + 1),1) = (DFT ((p *' q),x,(2 * m))) . i ) i in NAT by ORDINAL1:def_12; hence ( i < 2 * m implies ((VM (x,(2 * m))) * (mConv ((p *' q),(2 * m)))) * ((i + 1),1) = (DFT ((p *' q),x,(2 * m))) . i ) by A7, Th41; ::_thesis: verum end; for i being Nat st i >= 2 * m holds (DFT ((p *' q),x,(2 * m))) . i = 0. L by Def7; then 2 * m is_at_least_length_of DFT ((p *' q),x,(2 * m)) by ALGSEQ_1:def_2; then A9: len (DFT ((p *' q),x,(2 * m))) <= 2 * m by ALGSEQ_1:def_3; A10: width (VM ((x "),(2 * m))) = 2 * m by MATRIX_1:24 .= len (VM (x,(2 * m))) by MATRIX_1:24 ; A11: m + m <> 0 by A1; then A12: (VM ((x "),(2 * m))) * (VM (x,(2 * m))) = (VM (x,(2 * m))) * (VM ((x "),(2 * m))) by A3, Th40 .= (emb ((2 * m),L)) * (1. (L,(2 * m))) by A3, A11, Th39 ; A13: now__::_thesis:_for_u9_being_set_st_u9_in_dom_(aConv_((emb_((2_*_m),L))_*_(mConv_((p_*'_q),(2_*_m)))))_holds_ (aConv_((emb_((2_*_m),L))_*_(mConv_((p_*'_q),(2_*_m)))))_._u9_=_((emb_((2_*_m),L))_*_(p_*'_q))_._u9 let u9 be set ; ::_thesis: ( u9 in dom (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) implies (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) . b1 = ((emb ((2 * m),L)) * (p *' q)) . b1 ) assume u9 in dom (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) ; ::_thesis: (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) . b1 = ((emb ((2 * m),L)) * (p *' q)) . b1 then reconsider u = u9 as Element of NAT by FUNCT_2:def_1; percases ( u < 2 * m or 2 * m <= u ) ; supposeA14: u < 2 * m ; ::_thesis: (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) . b1 = ((emb ((2 * m),L)) * (p *' q)) . b1 then ( 0 + 1 <= u + 1 & u + 1 <= 2 * m ) by NAT_1:13; then A15: u + 1 in Seg (2 * m) ; len (mConv ((p *' q),(2 * m))) = 2 * m by A11, Th28; then A16: dom (mConv ((p *' q),(2 * m))) = Seg (2 * m) by FINSEQ_1:def_3; ( Seg (width (mConv ((p *' q),(2 * m)))) = Seg 1 & 1 in Seg 1 ) by A11, Th28; then A17: [(u + 1),1] in Indices (mConv ((p *' q),(2 * m))) by A16, A15, ZFMISC_1:87; len ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m)))) = len (mConv ((p *' q),(2 * m))) by MATRIX_3:def_5 .= 2 * m by A11, Th28 ; hence (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) . u9 = ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m)))) * ((u + 1),1) by A14, Def5 .= (emb ((2 * m),L)) * ((mConv ((p *' q),(2 * m))) * ((u + 1),1)) by A17, MATRIX_3:def_5 .= (emb ((2 * m),L)) * ((p *' q) . u) by A14, Th28 .= ((emb ((2 * m),L)) * (p *' q)) . u9 by POLYNOM5:def_3 ; ::_thesis: verum end; supposeA18: 2 * m <= u ; ::_thesis: (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) . b1 = ((emb ((2 * m),L)) * (p *' q)) . b1 len ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m)))) = len (mConv ((p *' q),(2 * m))) by MATRIX_3:def_5 .= 2 * m by A11, Th28 ; hence (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) . u9 = 0. L by A18, Def5 .= (emb ((2 * m),L)) * (0. L) by VECTSP_1:6 .= (emb ((2 * m),L)) * ((p *' q) . u) by A7, A18, ALGSEQ_1:8, XXREAL_0:2 .= ((emb ((2 * m),L)) * (p *' q)) . u9 by POLYNOM5:def_3 ; ::_thesis: verum end; end; end; dom (aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m))))) = NAT by FUNCT_2:def_1 .= dom ((emb ((2 * m),L)) * (p *' q)) by FUNCT_2:def_1 ; then A19: aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m)))) = (emb ((2 * m),L)) * (p *' q) by A13, FUNCT_1:2; A20: len (mConv ((p *' q),(2 * m))) = 2 * m by A11, Th28 .= width (VM (x,(2 * m))) by MATRIX_1:24 ; then A21: len ((VM (x,(2 * m))) * (mConv ((p *' q),(2 * m)))) = len (VM (x,(2 * m))) by MATRIX_3:def_4 .= 2 * m by MATRIX_1:24 ; width ((VM (x,(2 * m))) * (mConv ((p *' q),(2 * m)))) = width (mConv ((p *' q),(2 * m))) by A20, MATRIX_3:def_4 .= 1 by A11, Th28 ; then (VM (x,(2 * m))) * (mConv ((p *' q),(2 * m))) is Matrix of 2 * m,1,L by A11, A21, MATRIX_1:20; then aConv ((VM ((x "),(2 * m))) * (mConv ((DFT ((p *' q),x,(2 * m))),(2 * m)))) = aConv ((VM ((x "),(2 * m))) * ((VM (x,(2 * m))) * (mConv ((p *' q),(2 * m))))) by A11, A8, Th29 .= aConv (((VM ((x "),(2 * m))) * (VM (x,(2 * m)))) * (mConv ((p *' q),(2 * m)))) by A10, A20, MATRIX_3:33 .= aConv ((emb ((2 * m),L)) * ((1. (L,(2 * m))) * (mConv ((p *' q),(2 * m))))) by A11, A12, Th6 .= aConv ((emb ((2 * m),L)) * (mConv ((p *' q),(2 * m)))) by A1, Lm12 ; hence DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m)) = (emb ((2 * m),L)) * (p *' q) by A11, A9, A19, Th42; ::_thesis: verum end; end; end; theorem :: POLYNOM8:44 for L being Field for p, q being Polynomial of L for m being Element of NAT st m > 0 & len p <= m & len q <= m holds for x being Element of L st x is_primitive_root_of_degree 2 * m & emb ((2 * m),L) <> 0. L holds ((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q proof let L be Field; ::_thesis: for p, q being Polynomial of L for m being Element of NAT st m > 0 & len p <= m & len q <= m holds for x being Element of L st x is_primitive_root_of_degree 2 * m & emb ((2 * m),L) <> 0. L holds ((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q let p, q be Polynomial of L; ::_thesis: for m being Element of NAT st m > 0 & len p <= m & len q <= m holds for x being Element of L st x is_primitive_root_of_degree 2 * m & emb ((2 * m),L) <> 0. L holds ((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q let m be Element of NAT ; ::_thesis: ( m > 0 & len p <= m & len q <= m implies for x being Element of L st x is_primitive_root_of_degree 2 * m & emb ((2 * m),L) <> 0. L holds ((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q ) assume A1: ( m > 0 & len p <= m & len q <= m ) ; ::_thesis: for x being Element of L st x is_primitive_root_of_degree 2 * m & emb ((2 * m),L) <> 0. L holds ((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q let x be Element of L; ::_thesis: ( x is_primitive_root_of_degree 2 * m & emb ((2 * m),L) <> 0. L implies ((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q ) assume A2: x is_primitive_root_of_degree 2 * m ; ::_thesis: ( not emb ((2 * m),L) <> 0. L or ((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q ) assume A3: emb ((2 * m),L) <> 0. L ; ::_thesis: ((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q ((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = ((emb ((2 * m),L)) ") * (DFT ((DFT ((p *' q),x,(2 * m))),(x "),(2 * m))) by Th34 .= ((emb ((2 * m),L)) ") * ((emb ((2 * m),L)) * (p *' q)) by A1, A2, Th43 .= (((emb ((2 * m),L)) ") * (emb ((2 * m),L))) * (p *' q) by Th10 .= (1. L) * (p *' q) by A3, VECTSP_1:def_10 .= p *' q by POLYNOM5:27 ; hence ((emb ((2 * m),L)) ") * (DFT (((DFT (p,x,(2 * m))) * (DFT (q,x,(2 * m)))),(x "),(2 * m))) = p *' q ; ::_thesis: verum end;