let R, S be non degenerated comRing; :: thesis: for n being Ordinal
for p, q being Polynomial of n,R
for x being Function of n,S st R is Subring of S holds
Ext_eval ((p *' q),x) = (Ext_eval (p,x)) * (Ext_eval (q,x))
let n be Ordinal; :: thesis: for p, q being Polynomial of n,R
for x being Function of n,S st R is Subring of S holds
Ext_eval ((p *' q),x) = (Ext_eval (p,x)) * (Ext_eval (q,x))
let p, q be Polynomial of n,R; :: thesis: for x being Function of n,S st R is Subring of S holds
Ext_eval ((p *' q),x) = (Ext_eval (p,x)) * (Ext_eval (q,x))
let x be Function of n,S; :: thesis: ( R is Subring of S implies Ext_eval ((p *' q),x) = (Ext_eval (p,x)) * (Ext_eval (q,x)) )
assume A0: R is Subring of S ; :: thesis: Ext_eval ((p *' q),x) = (Ext_eval (p,x)) * (Ext_eval (q,x))
defpred S₁[ Nat] means for p being Polynomial of n,R st card (Support p) = $1 holds
Ext_eval ((p *' q),x) = (Ext_eval (p,x)) * (Ext_eval (q,x));
A1: ex k being Element of NAT st card (Support p) = k ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
let p be Polynomial of n,R; :: thesis: ( card (Support p) = k + 1 implies Ext_eval ((p *' q),x) = (Ext_eval (p,x)) * (Ext_eval (q,x)) )
assume A4: card (Support p) = k + 1 ; :: thesis: Ext_eval ((p *' q),x) = (Ext_eval (p,x)) * (Ext_eval (q,x))
set sgp = SgmX ((BagOrder n),(Support p));
set bg = (SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p))));
A5: BagOrder n linearly_orders Support p by POLYNOM2:18;
then SgmX ((BagOrder n),(Support p)) <> {} by A4, PRE_POLY:def 2, RELAT_1:38;
then 1 <= len (SgmX ((BagOrder n),(Support p))) by NAT_1:14;
then len (SgmX ((BagOrder n),(Support p))) in Seg (len (SgmX ((BagOrder n),(Support p)))) ;
then A6: len (SgmX ((BagOrder n),(Support p))) in dom (SgmX ((BagOrder n),(Support p))) by FINSEQ_1:def 3;
then (SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p)))) = (SgmX ((BagOrder n),(Support p))) . (len (SgmX ((BagOrder n),(Support p)))) by PARTFUN1:def 6;
then (SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p)))) in rng (SgmX ((BagOrder n),(Support p))) by A6, FUNCT_1:def 3;
then A7: (SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p)))) in Support p by A5, PRE_POLY:def 2;
then A8: p . ((SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p))))) <> 0. R by POLYNOM1:def 4;
set m = (0_ (n,R)) +* (((SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p))))),(p . ((SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p)))))));
set p9 = p +* (((SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p))))),(0. R));
reconsider bg = (SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p)))) as bag of n ;
dom p = Bags n by FUNCT_2:def 1;
then A9: p +* (((SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p))))),(0. R)) = p +* (bg .--> (0. R)) by FUNCT_7:def 3;
reconsider p9 = p +* (((SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p))))),(0. R)) as Function of (Bags n),R ;
for u being object st u in Support p9 holds
u in Support p

proof

let u be object ; :: thesis: ( u in Support p9 implies u in Support p )
assume A10: u in Support p9 ; :: thesis: u in Support p
then reconsider u = u as Element of Bags n ;
reconsider u = u as bag of n ;

now :: thesis: not u = bg

assume A11: u = bg ; :: thesis: contradiction
then u in dom (bg .--> (0. R)) by TARSKI:def 1;
then p9 . u = (bg .--> (0. R)) . bg by A9, A11, FUNCT_4:13;
then p9 . u = 0. R by FUNCOP_1:72;
hence contradiction by A10, POLYNOM1:def 4; :: thesis: verum

end;

then not u in dom (bg .--> (0. R)) by TARSKI:def 1;
then p . u = p9 . u by A9, FUNCT_4:11;
then p . u <> 0. R by A10, POLYNOM1:def 4;
hence u in Support p by POLYNOM1:def 4; :: thesis: verum

end;

then Support p9 c= Support p ;
then reconsider p9 = p9 as Polynomial of n,R by POLYNOM1:def 5;
A12: dom p = Bags n by FUNCT_2:def 1;
A13: for u being object st u in Support p holds
u in (Support p9) \/ {bg}

proof

let u be object ; :: thesis: ( u in Support p implies u in (Support p9) \/ {bg} )
assume A14: u in Support p ; :: thesis: u in (Support p9) \/ {bg}
then reconsider u = u as Element of Bags n ;
A15: p . u <> 0. R by A14, POLYNOM1:def 4;

per cases ( u = bg or u <> bg ) ;

suppose u = bg ; :: thesis: u in (Support p9) \/ {bg}

then u in {bg} by TARSKI:def 1;
hence u in (Support p9) \/ {bg} by XBOOLE_0:def 3; :: thesis: verum

end;

suppose u <> bg ; :: thesis: u in (Support p9) \/ {bg}

then not u in dom (bg .--> (0. R)) by TARSKI:def 1;
then p9 . u = p . u by A9, FUNCT_4:11;
then u in Support p9 by A15, POLYNOM1:def 4;
hence u in (Support p9) \/ {bg} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

bg in dom (bg .--> (0. R)) by TARSKI:def 1;
then p9 . bg = (bg .--> (0. R)) . bg by A9, FUNCT_4:13;
then A16: p9 . bg = 0. R by FUNCOP_1:72;
then A17: not bg in Support p9 by POLYNOM1:def 4;
for u being object st u in (Support p9) \/ {bg} holds
u in Support p

proof

let u be object ; :: thesis: ( u in (Support p9) \/ {bg} implies u in Support p )
assume A18: u in (Support p9) \/ {bg} ; :: thesis: u in Support p

per cases ( u in Support p9 or u in {bg} ) by A18, XBOOLE_0:def 3;

suppose A19: u in Support p9 ; :: thesis: u in Support p

then reconsider u = u as Element of Bags n ;
u <> bg by A16, A19, POLYNOM1:def 4;
then not u in dom (bg .--> (0. R)) by TARSKI:def 1;
then A20: p9 . u = p . u by A9, FUNCT_4:11;
p9 . u <> 0. R by A19, POLYNOM1:def 4;
hence u in Support p by A20, POLYNOM1:def 4; :: thesis: verum

end;

suppose u in {bg} ; :: thesis: u in Support p

hence u in Support p by A7, TARSKI:def 1; :: thesis: verum

end;

end;

end;

then Support p = (Support p9) \/ {bg} by A13, TARSKI:2;
then A21: k + 1 = (card (Support p9)) + 1 by A4, A17, CARD_2:41;
dom (0_ (n,R)) = Bags n by FUNCT_2:def 1;
then A22: (0_ (n,R)) +* (((SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p))))),(p . ((SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p))))))) = (0_ (n,R)) +* (bg .--> (p . bg)) by FUNCT_7:def 3;
reconsider m = (0_ (n,R)) +* (((SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p))))),(p . ((SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p))))))) as Function of (Bags n), the carrier of R ;
reconsider m = m as Function of (Bags n),R ;
A23: for u being object st u in Support m holds
u in {bg}

proof

let u be object ; :: thesis: ( u in Support m implies u in {bg} )
assume A24: u in Support m ; :: thesis: u in {bg}
then reconsider u = u as Element of Bags n ;
A25: m . u <> 0. R by A24, POLYNOM1:def 4;

now :: thesis: not u <> bg

assume u <> bg ; :: thesis: contradiction
then not u in dom (bg .--> (p . bg)) by TARSKI:def 1;
then m . u = (0_ (n,R)) . u by A22, FUNCT_4:11;
hence contradiction by A25, POLYNOM1:22; :: thesis: verum

end;

hence u in {bg} by TARSKI:def 1; :: thesis: verum

end;

A27: for u being object st u in {bg} holds
u in Support m

proof

let u be object ; :: thesis: ( u in {bg} implies u in Support m )
bg in dom (bg .--> (p . bg)) by TARSKI:def 1;
then m . bg = (bg .--> (p . bg)) . bg by A22, FUNCT_4:13;
then A26: m . bg = p . bg by FUNCOP_1:72;
assume u in {bg} ; :: thesis: u in Support m
then u = bg by TARSKI:def 1;
hence u in Support m by A8, A26, POLYNOM1:def 4; :: thesis: verum

end;

then Support m = {bg} by A23, TARSKI:2;
then reconsider m = m as Polynomial of n,R by POLYNOM1:def 5;
reconsider m = m as Polynomial of n,R ;
A28: for u being object st u in Bags n holds
(p9 + m) . u = p . u

proof

let u be object ; :: thesis: ( u in Bags n implies (p9 + m) . u = p . u )
assume u in Bags n ; :: thesis: (p9 + m) . u = p . u
then reconsider u = u as bag of n ;

per cases ( u = bg or u <> bg ) ;

suppose A29: u = bg ; :: thesis: (p9 + m) . u = p . u

bg in dom (bg .--> (p . bg)) by TARSKI:def 1;
then m . bg = (bg .--> (p . bg)) . bg by A22, FUNCT_4:13;
then A30: m . bg = p . bg by FUNCOP_1:72;
u in dom (bg .--> (0. R)) by A29, TARSKI:def 1;
then A31: p9 . u = (bg .--> (0. R)) . bg by A9, A29, FUNCT_4:13;
(p9 + m) . u = (p9 . u) + (m . u) by POLYNOM1:15
.= (0. R) + (p . bg) by A29, A31, A30, FUNCOP_1:72
.= p . bg ;
hence (p9 + m) . u = p . u by A29; :: thesis: verum

end;

suppose A32: u <> bg ; :: thesis: (p9 + m) . u = p . u

then A33: not u in dom (bg .--> (0. R)) by TARSKI:def 1;
not u in dom (bg .--> (p . bg)) by A32, TARSKI:def 1;
then m . u = (0_ (n,R)) . u by A22, FUNCT_4:11;
then A34: m . u = 0. R by POLYNOM1:22;
(p9 + m) . u = (p9 . u) + (m . u) by POLYNOM1:15
.= p . u by A9, A33, A34, FUNCT_4:11 ;
hence (p9 + m) . u = p . u ; :: thesis: verum

end;

end;

end;

A35: dom (p9 + m) = Bags n by FUNCT_2:def 1;
then Ext_eval (p,x) = Ext_eval ((m + p9),x) by A12, A28, FUNCT_1:2
.= (Ext_eval (p9,x)) + (Ext_eval (m,x)) by A27, A23, TARSKI:2, A0, Lm7 ;
hence (Ext_eval (p,x)) * (Ext_eval (q,x)) = ((Ext_eval (p9,x)) * (Ext_eval (q,x))) + ((Ext_eval (m,x)) * (Ext_eval (q,x))) by VECTSP_1:def 7
.= (Ext_eval ((p9 *' q),x)) + ((Ext_eval (m,x)) * (Ext_eval (q,x))) by A3, A21
.= (Ext_eval ((p9 *' q),x)) + ((Ext_eval (q,x)) * (Ext_eval (m,x))) by GROUP_1:def 12
.= (Ext_eval ((p9 *' q),x)) + (Ext_eval ((m *' q),x)) by A27, A23, TARSKI:2, A0, Lm9
.= Ext_eval (((p9 *' q) + (m *' q)),x) by A0, evalpl
.= Ext_eval ((q *' (p9 + m)),x) by POLYNOM1:26
.= Ext_eval ((p *' q),x) by A35, A12, A28, FUNCT_1:2 ;
:: thesis: verum

end;

A36: S₁[ 0 ]

proof

let p be Polynomial of n,R; :: thesis: ( card (Support p) = 0 implies Ext_eval ((p *' q),x) = (Ext_eval (p,x)) * (Ext_eval (q,x)) )
assume card (Support p) = 0 ; :: thesis: Ext_eval ((p *' q),x) = (Ext_eval (p,x)) * (Ext_eval (q,x))
then Support p = {} ;
then A37: p = 0_ (n,R) by POLYNOM2:17;
hence Ext_eval ((p *' q),x) = Ext_eval (p,x) by POLYNOM1:28
.= (0. S) * (Ext_eval (q,x)) by A37, ev0
.= (Ext_eval (p,x)) * (Ext_eval (q,x)) by A37, ev0 ;
:: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A36, A2);
hence Ext_eval ((p *' q),x) = (Ext_eval (p,x)) * (Ext_eval (q,x)) by A1; :: thesis: verum