let p be Element of the carrier of (Polynom-Ring F_Rat); :: thesis: the carrier of F_Rat /\ the carrier of ((Polynom-Ring F_Rat) / ({p} -Ideal)) = {}
set F = F_Rat ;
set FX = Polynom-Ring F_Rat;
set I = {p} -Ideal ;
set K = (Polynom-Ring F_Rat) / ({p} -Ideal);
set x = the Element of the carrier of F_Rat /\ the carrier of ((Polynom-Ring F_Rat) / ({p} -Ideal));
now :: thesis: not the carrier of F_Rat /\ the carrier of ((Polynom-Ring F_Rat) / ({p} -Ideal)) <> {}
assume AS: the carrier of F_Rat /\ the carrier of ((Polynom-Ring F_Rat) / ({p} -Ideal)) <> {} ; :: thesis: contradiction
reconsider x = the Element of the carrier of F_Rat /\ the carrier of ((Polynom-Ring F_Rat) / ({p} -Ideal)) as Element of F_Rat by AS, XBOOLE_0:def 4;
reconsider q = x as Element of ((Polynom-Ring F_Rat) / ({p} -Ideal)) by AS, XBOOLE_0:def 4;
consider a being Element of (Polynom-Ring F_Rat) such that
A1: q = Class ((EqRel ((Polynom-Ring F_Rat),({p} -Ideal))),a) by RING_1:11;
reconsider pa = a as Polynomial of F_Rat by POLYNOM3:def 10;
a - a = 0. (Polynom-Ring F_Rat) by RLVECT_1:15;
then A2: a in q by A1, RING_1:5, IDEAL_1:3;
XZ: x in (RAT+ \/ [:{0},RAT+:]) \ {[0,0]} by NUMBERS:def 3, RAT_1:def 2;
XX: not x in RAT+
proof
assume x in RAT+ ; :: thesis: contradiction
per cases then ( x in omega or x in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } \ { [k,1] where k is Element of omega : verum } ) by XBOOLE_0:def 3, ARYTM_3:def 7;
suppose x in omega ; :: thesis: contradiction
then reconsider n = x as Element of omega ;
n = { m where m is Nat : m < n } by AXIOMS:4;
then consider m being Nat such that
B1: ( a = m & m < n ) by A2;
dom pa = NAT by FUNCT_2:def 1;
hence contradiction by B1; :: thesis: verum
end;
suppose x in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } \ { [k,1] where k is Element of omega : verum } ; :: thesis: contradiction
then x in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } ;
then consider i, j being Element of omega such that
A4: ( x = [i,j] & i,j are_coprime & j <> {} ) ;
A5: dom pa = NAT by FUNCT_2:def 1;
pa in {{i},{i,j}} by A2, A4, TARSKI:def 5;
per cases then ( pa = {i} or pa = {i,j} ) by TARSKI:def 2;
suppose pa = {i,j} ; :: thesis: contradiction
per cases then ( [i,(pa . i)] = i or [i,(pa . i)] = j ) by A5;
suppose [i,(pa . i)] = i ; :: thesis: contradiction
hence contradiction ; :: thesis: verum
end;
suppose [i,(pa . i)] = j ; :: thesis: contradiction
hence contradiction ; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
not x in [:{0},RAT+:]
proof
assume x in [:{0},RAT+:] ; :: thesis: contradiction
then consider y, z being object such that
A4: ( y in {0} & z in RAT+ & x = [y,z] ) by ZFMISC_1:def 2;
reconsider y = y as Element of NAT by A4, TARSKI:def 1;
A5: dom pa = NAT by FUNCT_2:def 1;
pa in {{y},{y,z}} by A2, A4, TARSKI:def 5;
per cases then ( pa = {y} or pa = {y,z} ) by TARSKI:def 2;
suppose pa = {y,z} ; :: thesis: contradiction
per cases then ( [0,(pa . 0)] = y or [0,(pa . 0)] = z ) by A5;
suppose [0,(pa . 0)] = y ; :: thesis: contradiction
hence contradiction ; :: thesis: verum
end;
suppose A7: [0,(pa . 0)] = z ; :: thesis: contradiction
per cases ( z in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } \ { [k,1] where k is Element of omega : verum } or z in omega ) by A4, ARYTM_3:def 7, XBOOLE_0:def 3;
suppose A9: z in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } \ { [k,1] where k is Element of omega : verum } ; :: thesis: contradiction
then z in { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } ;
then consider i, j being Element of omega such that
A8: ( z = [i,j] & i,j are_coprime & j <> {} ) ;
i = 0 by A7, A8, XTUPLE_0:1;
then j = 1 by A8, ARYTM_3:3;
then z in { [k,1] where k is Element of omega : verum } by A8;
hence contradiction by A9, XBOOLE_0:def 5; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
hence contradiction by XZ, XX, XBOOLE_0:def 3; :: thesis: verum
end;
hence the carrier of F_Rat /\ the carrier of ((Polynom-Ring F_Rat) / ({p} -Ideal)) = {} ; :: thesis: verum