let R be non empty transitive asymmetric RelStr ; for a, b being bag of the carrier of R
for x being Element of R
for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p holds
( x is_maximal_in support b iff a . x > 0 )
let a, b be bag of the carrier of R; for x being Element of R
for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p holds
( x is_maximal_in support b iff a . x > 0 )
let x be Element of R; for p being partition of b -' a
for q being partition of b st q is ordered & q = <*a*> ^ p holds
( x is_maximal_in support b iff a . x > 0 )
let p be partition of b -' a; for q being partition of b st q is ordered & q = <*a*> ^ p holds
( x is_maximal_in support b iff a . x > 0 )
let q be partition of b; ( q is ordered & q = <*a*> ^ p implies ( x is_maximal_in support b iff a . x > 0 ) )
assume Z0:
q is ordered
; ( not q = <*a*> ^ p or ( x is_maximal_in support b iff a . x > 0 ) )
assume Z1:
q = <*a*> ^ p
; ( x is_maximal_in support b iff a . x > 0 )
rng p c= Bags the carrier of R
by RELAT_1:def 19;
then reconsider p = p as FinSequence of Bags the carrier of R by FINSEQ_1:def 4;
set I = the carrier of R;
hereby ( a . x > 0 implies x is_maximal_in support b )
assume
x is_maximal_in support b
;
a . x > 0 then A7:
(
x in support b & ( for
y being
Element of
R holds
( not
y in support b or not
x < y ) ) )
by WAYBEL_4:55;
then
x in support (Sum q)
by PART;
then consider d being
bag of the
carrier of
R such that A8:
(
d in rng q &
x in support d )
by Th27;
consider i being
object such that A9:
(
i in dom q &
d = q . i )
by A8, FUNCT_1:def 3;
reconsider i =
i as
Nat by A9;
1
<= i
by A9, FINSEQ_3:25;
per cases then
( i = 1 or i > 1 )
by XXREAL_0:1;
suppose
i > 1
;
a . x > 0 then
i >= 1
+ 1
by NAT_1:13;
then consider k being
Nat such that A10:
i = (1 + 1) + k
by NAT_1:10;
( 1
<= 1
+ k & 1
+ k <= (1 + k) + 1 &
(1 + k) + 1
= i &
i <= len q )
by A9, A10, NAT_1:11, FINSEQ_3:25;
then
( 1
<= 1
+ k & 1
+ k <= len q )
by XXREAL_0:2;
then A11:
1
+ k in dom q
by FINSEQ_3:25;
then A12:
(
q /. i = q . i &
q /. (1 + k) = q . (1 + k) )
by A9, PARTFUN1:def 6;
d . x <> 0
by A8, PRE_POLY:def 7;
then
(
d . x > 0 &
i = (1 + k) + 1 )
by A10;
then consider y being
Element of
R such that A13:
(
(q /. (1 + k)) . y > 0 &
x <= y )
by Z0, A9, A11, A12;
q . (1 + k) in rng q
by A11, FUNCT_1:def 3;
then
(
y in support (q /. (1 + k)) &
support (q /. (1 + k)) c= support (Sum q) &
support (Sum q) = support b )
by A13, A12, Th26, PART, BAGORDER:21, PRE_POLY:def 7;
hence
a . x > 0
by A7, A13, Lem2;
verum end;
end;
assume B0:
a . x > 0
; x is_maximal_in support b
then B1:
x in support a
by PRE_POLY:def 7;
( a in {a} & {a} = rng <*a*> & rng <*a*> c= rng q )
by Z1, TARSKI:def 1, FINSEQ_1:39, FINSEQ_1:29;
then B4:
( a divides Sum q & Sum q = b )
by Th26, PART;
then AA:
support a c= support b
by BAGORDER:21;
for y being Element of R holds
( not y in support b or not x < y )
proof
let y be
Element of
R;
( not y in support b or not x < y )
assume B3:
(
y in support b &
x <= y &
x <> y )
;
ORDERS_2:def 6 contradiction
per cases
( a . y > 0 or a . y = 0 )
;
suppose B5:
a . y = 0
;
contradictionconsider d being
bag of the
carrier of
R such that B6:
(
d in rng q &
y in support d )
by B4, B3, Th27;
B7:
d . y <> 0
by B6, PRE_POLY:def 7;
then
( not
d in {a} &
{a} = rng <*a*> &
rng q = (rng <*a*>) \/ (rng p) )
by Z1, B5, TARSKI:def 1, FINSEQ_1:31, FINSEQ_1:39;
then
(
d . y > 0 &
d in rng p )
by B6, B7, XBOOLE_0:def 3;
then consider z being
Element of
R such that B8:
(
a . z > 0 &
y <= z )
by Z0, Z1, Th36;
(
x <= z &
x ## z )
by Z0, Z1, B0, B3, B8, ORDERS_2:3, Th32;
hence
contradiction
;
verum end;
end;
hence
x is_maximal_in support b
by B1, AA, WAYBEL_4:55; verum