let p be Element of the carrier of (Polynom-Ring F_Rat); 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 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)) <> {}
;
contradictionreconsider 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+
;
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 { [i,j] where i, j is Element of omega : ( i,j are_coprime & j <> {} ) } \ { [k,1] where k is Element of omega : verum }
;
contradictionthen
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;
end; end;
end;
not
x in [:{0},RAT+:]
proof
assume
x in [:{0},RAT+:]
;
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}
;
contradictionhence
contradiction
by A5;
verum end; suppose
pa = {y,z}
;
contradictionper cases then
( [0,(pa . 0)] = y or [0,(pa . 0)] = z )
by A5;
suppose
[0,(pa . 0)] = y
;
contradictionhence
contradiction
;
verum end; suppose A7:
[0,(pa . 0)] = z
;
contradictionper 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 }
;
contradictionthen
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;
verum end; end; end; end; end; end;
end; hence
contradiction
by XZ, XX, XBOOLE_0:def 3;
verum end;
hence
the carrier of F_Rat /\ the carrier of ((Polynom-Ring F_Rat) / ({p} -Ideal)) = {}
; verum