set f = drastic_norm ;
FF: for a, b being Element of [.0,1.] holds drastic_norm . (a,b) = drastic_norm . (b,a)
proof
let a, b be Element of [.0,1.]; :: thesis: drastic_norm . (a,b) = drastic_norm . (b,a)
per cases ( a = 1 or b = 1 or ( a <> 1 & b <> 1 ) ) ;
end;
end;
TT: for a being Element of [.0,1.] holds drastic_norm . (a,1) = a
proof
let a be Element of [.0,1.]; :: thesis: drastic_norm . (a,1) = a
1 in [.0,1.] by XXREAL_1:1;
hence drastic_norm . (a,1) = a by DrasticDef; :: thesis: verum
end;
D1: for a, b, c, d being Element of [.0,1.] st a <= c & b <= d holds
drastic_norm . (a,b) <= drastic_norm . (c,d)
proof
let a, b, c, d be Element of [.0,1.]; :: thesis: ( a <= c & b <= d implies drastic_norm . (a,b) <= drastic_norm . (c,d) )
B2: drastic_norm . (c,d) >= 0 by XXREAL_1:1;
assume S1: ( a <= c & b <= d ) ; :: thesis: drastic_norm . (a,b) <= drastic_norm . (c,d)
per cases ( a = 1 or b = 1 or ( b <> 1 & a <> 1 ) ) ;
end;
end;
H1: 0 in [.0,1.] by XXREAL_1:1;
BU: for a being Element of [.0,1.] holds drastic_norm . (a,0) = 0
proof
let a be Element of [.0,1.]; :: thesis: drastic_norm . (a,0) = 0
H2: 0 <= a by XXREAL_1:1;
per cases ( max (a,0) = 1 or max (a,0) <> 1 ) ;
suppose max (a,0) = 1 ; :: thesis: drastic_norm . (a,0) = 0
then drastic_norm . (a,0) = min (a,0) by
.= 0 by ;
hence drastic_norm . (a,0) = 0 ; :: thesis: verum
end;
suppose max (a,0) <> 1 ; :: thesis: drastic_norm . (a,0) = 0
hence drastic_norm . (a,0) = 0 by ; :: thesis: verum
end;
end;
end;
for a, b, c being Element of [.0,1.] holds drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . ((drastic_norm . (a,b)),c)
proof
let a, b, c be Element of [.0,1.]; :: thesis: drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . ((drastic_norm . (a,b)),c)
Z4: min (a,b) in [.0,1.] by MinIn01;
EE: min (b,c) in [.0,1.] by MinIn01;
per cases ( ( max (a,b) = 1 & max (b,c) = 1 ) or ( max (a,b) = 1 & max (b,c) <> 1 ) or ( max (a,b) <> 1 & max (b,c) = 1 ) or ( max (a,b) <> 1 & max (b,c) <> 1 ) ) ;
suppose Z1: ( max (a,b) = 1 & max (b,c) = 1 ) ; :: thesis: drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . ((drastic_norm . (a,b)),c)
then K1: ( a = 1 or b = 1 ) by XXREAL_0:16;
max (a,c) in [.0,1.] by MaxIn01;
then U2: max (a,c) <= 1 by XXREAL_1:1;
Z2: drastic_norm . (b,c) = min (b,c) by ;
UU: max (a,(min (b,c))) = min ((max (a,b)),(max (a,c))) by XXREAL_0:39
.= max (a,c) by ;
per cases ( max (a,c) = 1 or max (a,c) <> 1 ) ;
suppose HU: max (a,c) = 1 ; :: thesis: drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . ((drastic_norm . (a,b)),c)
U2: max ((min (a,b)),c) = min ((max (a,c)),(max (b,c))) by XXREAL_0:39
.= 1 by Z1, HU ;
drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . (a,(min (b,c))) by
.= min (a,(min (b,c))) by
.= min ((min (a,b)),c) by XXREAL_0:33
.= drastic_norm . ((min (a,b)),c) by
.= drastic_norm . ((drastic_norm . (a,b)),c) by ;
hence drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . ((drastic_norm . (a,b)),c) ; :: thesis: verum
end;
suppose HU: max (a,c) <> 1 ; :: thesis: drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . ((drastic_norm . (a,b)),c)
then a <= b by ;
then K3: min (a,b) = a by XXREAL_0:def 9;
U1: drastic_norm . (a,b) = min (a,b) by ;
drastic_norm . (a,(drastic_norm . (b,c))) = 0 by
.= drastic_norm . ((drastic_norm . (a,b)),c) by ;
hence drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . ((drastic_norm . (a,b)),c) ; :: thesis: verum
end;
end;
end;
suppose Z1: ( max (a,b) = 1 & max (b,c) <> 1 ) ; :: thesis: drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . ((drastic_norm . (a,b)),c)
then z1: ( a = 1 or b = 1 ) by XXREAL_0:16;
max (b,c) in [.0,1.] by MaxIn01;
then W1: max (b,c) <= 1 by XXREAL_1:1;
za: b <> 1
proof
assume b = 1 ; :: thesis: contradiction
then max (b,c) >= 1 by XXREAL_0:25;
hence contradiction by Z1, XXREAL_0:1, W1; :: thesis: verum
end;
c <= 1 by XXREAL_1:1;
then z3: max (a,c) = 1 by ;
qq: max ((min (a,b)),c) = min ((max (a,c)),(max (b,c))) by XXREAL_0:39
.= max (b,c) by ;
drastic_norm . (b,c) = 0 by ;
then drastic_norm . (a,(drastic_norm . (b,c))) = 0 by BU
.= drastic_norm . ((min (a,b)),c) by
.= drastic_norm . ((drastic_norm . (a,b)),c) by ;
hence drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . ((drastic_norm . (a,b)),c) ; :: thesis: verum
end;
suppose Z1: ( max (a,b) <> 1 & max (b,c) = 1 ) ; :: thesis: drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . ((drastic_norm . (a,b)),c)
then z1: ( c = 1 or b = 1 ) by XXREAL_0:16;
max (a,b) in [.0,1.] by MaxIn01;
then w1: max (a,b) <= 1 by XXREAL_1:1;
zz: b <> 1
proof
assume b = 1 ; :: thesis: contradiction
then max (a,b) >= 1 by XXREAL_0:25;
hence contradiction by Z1, w1, XXREAL_0:1; :: thesis: verum
end;
Z2: drastic_norm . (b,c) = min (b,c) by ;
Y1: drastic_norm . (a,b) = 0 by ;
b <= c by ;
then drastic_norm . (b,c) = b by ;
then drastic_norm . (a,(drastic_norm . (b,c))) = 0 by
.= drastic_norm . (c,0) by BU
.= drastic_norm . ((drastic_norm . (a,b)),c) by Y1, FF ;
hence drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . ((drastic_norm . (a,b)),c) ; :: thesis: verum
end;
suppose Z1: ( max (a,b) <> 1 & max (b,c) <> 1 ) ; :: thesis: drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . ((drastic_norm . (a,b)),c)
then Z2: drastic_norm . (b,c) = 0 by Drastic2Def;
Z3: drastic_norm . (a,b) = 0 by ;
drastic_norm . (a,(drastic_norm . (b,c))) = 0 by BU, Z2
.= drastic_norm . (c,0) by BU
.= drastic_norm . ((drastic_norm . (a,b)),c) by Z3, FF ;
hence drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . ((drastic_norm . (a,b)),c) ; :: thesis: verum
end;
end;
end;
hence ( drastic_norm is commutative & drastic_norm is associative & drastic_norm is with-1-identity & drastic_norm is monotonic ) by ; :: thesis: verum