set f = nilmin_norm ;
FF: for a, b being Element of [.0,1.] holds nilmin_norm . (a,b) = nilmin_norm . (b,a)

proof

let a, b be Element of [.0,1.]; :: thesis: nilmin_norm . (a,b) = nilmin_norm . (b,a)

per cases ( a + b > 1 or a + b <= 1 ) ;

suppose A1: a + b > 1 ; :: thesis: nilmin_norm . (a,b) = nilmin_norm . (b,a)

hence nilmin_norm . (a,b) = min (a,b) by NilminDef
.= nilmin_norm . (b,a) by NilminDef, A1 ;
:: thesis: verum

end;

suppose a + b <= 1 ; :: thesis: nilmin_norm . (a,b) = nilmin_norm . (b,a)

then ( nilmin_norm . (a,b) = 0 & nilmin_norm . (b,a) = 0 ) by NilminDef;
hence nilmin_norm . (a,b) = nilmin_norm . (b,a) ; :: thesis: verum

end;

end;

end;

U1: 1 in [.0,1.] by XXREAL_1:1;
TT: for a being Element of [.0,1.] holds nilmin_norm . (a,1) = a

proof

let a be Element of [.0,1.]; :: thesis: nilmin_norm . (a,1) = a
U4: ( 0 <= a & a <= 1 ) by XXREAL_1:1;

per cases ( a + 1 > 1 or a + 1 <= 1 ) ;

suppose a + 1 > 1 ; :: thesis: nilmin_norm . (a,1) = a

then nilmin_norm . (a,1) = min (a,1) by NilminDef, U1
.= a by U4, XXREAL_0:def 9 ;
hence nilmin_norm . (a,1) = a ; :: thesis: verum

end;

suppose U2: a + 1 <= 1 ; :: thesis: nilmin_norm . (a,1) = a

then a <= 1 - 1 by XREAL_1:19;
then a = 0 by XXREAL_1:1;
hence nilmin_norm . (a,1) = a by NilminDef, U2, U1; :: thesis: verum

end;

end;

end;

D1: for a, b, c, d being Element of [.0,1.] st a <= c & b <= d holds
nilmin_norm . (a,b) <= nilmin_norm . (c,d)

proof

let a, b, c, d be Element of [.0,1.]; :: thesis: ( a <= c & b <= d implies nilmin_norm . (a,b) <= nilmin_norm . (c,d) )
assume S1: ( a <= c & b <= d ) ; :: thesis: nilmin_norm . (a,b) <= nilmin_norm . (c,d)

per cases ( a + b > 1 or a + b <= 1 ) ;

suppose S0: a + b > 1 ; :: thesis: nilmin_norm . (a,b) <= nilmin_norm . (c,d)

then Sa: nilmin_norm . (a,b) = min (a,b) by NilminDef;
a + b <= c + d by S1, XREAL_1:7;
then c + d > 1 by S0, XXREAL_0:2;
then nilmin_norm . (c,d) = min (c,d) by NilminDef;
hence nilmin_norm . (a,b) <= nilmin_norm . (c,d) by S1, Sa, XXREAL_0:18; :: thesis: verum

end;

suppose a + b <= 1 ; :: thesis: nilmin_norm . (a,b) <= nilmin_norm . (c,d)

then nilmin_norm . (a,b) = 0 by NilminDef;
hence nilmin_norm . (a,b) <= nilmin_norm . (c,d) by XXREAL_1:1; :: thesis: verum

end;

end;

end;

H1: 0 in [.0,1.] by XXREAL_1:1;
BU: for a being Element of [.0,1.] holds nilmin_norm . (a,0) = 0

proof

let a be Element of [.0,1.]; :: thesis: nilmin_norm . (a,0) = 0

per cases ( a + 0 > 1 or a + 0 <= 1 ) ;

suppose a + 0 > 1 ; :: thesis: nilmin_norm . (a,0) = 0

hence nilmin_norm . (a,0) = 0 by XXREAL_1:1; :: thesis: verum

end;

suppose a + 0 <= 1 ; :: thesis: nilmin_norm . (a,0) = 0

hence nilmin_norm . (a,0) = 0 by NilminDef, H1; :: thesis: verum

end;

end;

end;

for a, b, c being Element of [.0,1.] holds nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)

proof

let a, b, c be Element of [.0,1.]; :: thesis: nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)
EE: min (b,c) in [.0,1.] by MinIn01;
U3: min (a,b) in [.0,1.] by MinIn01;

per cases ( ( a + b > 1 & b + c > 1 ) or ( a + b > 1 & b + c <= 1 ) or ( a + b <= 1 & b + c > 1 ) or ( a + b <= 1 & b + c <= 1 ) ) ;

suppose Z1: ( a + b > 1 & b + c > 1 ) ; :: thesis: nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)

then Z2: nilmin_norm . (b,c) = min (b,c) by NilminDef;

per cases ( a + c > 1 or a + c <= 1 ) ;

suppose HU: a + c > 1 ; :: thesis: nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)

then W6: a + (min (b,c)) > 1 by Z1, XXREAL_0:15;
W7: c + (min (a,b)) > 1 by HU, Z1, XXREAL_0:15;
nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . (a,(min (b,c))) by Z1, NilminDef
.= min (a,(min (b,c))) by NilminDef, EE, W6
.= min ((min (a,b)),c) by XXREAL_0:33
.= nilmin_norm . ((min (a,b)),c) by NilminDef, U3, W7
.= nilmin_norm . ((nilmin_norm . (a,b)),c) by NilminDef, Z1 ;
hence nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c) ; :: thesis: verum

end;

suppose HU: a + c <= 1 ; :: thesis: nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)

a + (min (b,c)) <= a + c by XREAL_1:6, XXREAL_0:17;
then W1: a + (min (b,c)) <= 1 by HU, XXREAL_0:2;
c + (min (a,b)) <= a + c by XREAL_1:6, XXREAL_0:17;
then W2: c + (min (a,b)) <= 1 by HU, XXREAL_0:2;
U1: nilmin_norm . (a,b) = min (a,b) by NilminDef, Z1;
nilmin_norm . (a,(nilmin_norm . (b,c))) = 0 by W1, NilminDef, Z2
.= nilmin_norm . ((nilmin_norm . (a,b)),c) by U1, W2, NilminDef ;
hence nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c) ; :: thesis: verum

end;

end;

end;

suppose Z1: ( a + b > 1 & b + c <= 1 ) ; :: thesis: nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)

then Z2: nilmin_norm . (a,b) = min (a,b) by NilminDef;

per cases ( a + c <= 1 or a + c > 1 ) ;

suppose a + c <= 1 ; :: thesis: nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)

then G2: (min (a,b)) + c <= 1 by Z1, XXREAL_0:15;
nilmin_norm . (b,c) = 0 by NilminDef, Z1;
then nilmin_norm . (a,(nilmin_norm . (b,c))) = 0 by BU
.= nilmin_norm . ((nilmin_norm . (a,b)),c) by Z2, NilminDef, G2 ;
hence nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c) ; :: thesis: verum

end;

suppose hh: a + c > 1 ; :: thesis: nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)

g4: (min (a,b)) + c = min ((a + c),(b + c)) by FUZZY_2:42
.= b + c by XXREAL_0:def 9, hh, XXREAL_0:2, Z1 ;
nilmin_norm . (b,c) = 0 by NilminDef, Z1;
hence nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c) by Z2, g4, BU; :: thesis: verum

end;

end;

end;

suppose Z1: ( a + b <= 1 & b + c > 1 ) ; :: thesis: nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)

then Z2: nilmin_norm . (b,c) = min (b,c) by NilminDef;
ZZ: nilmin_norm . (a,b) = 0 by NilminDef, Z1;

per cases ( a + c <= 1 or a + c > 1 ) ;

suppose a + c <= 1 ; :: thesis: nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)

then G2: (min (b,c)) + a <= 1 by Z1, XXREAL_0:15;
nilmin_norm . ((nilmin_norm . (a,b)),c) = nilmin_norm . (0,c) by Z1, NilminDef
.= nilmin_norm . (c,0) by FF, H1
.= 0 by BU
.= nilmin_norm . (a,(nilmin_norm . (b,c))) by Z2, NilminDef, G2 ;
hence nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c) ; :: thesis: verum

end;

suppose g5: a + c > 1 ; :: thesis: nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)

g4: (min (c,b)) + a = min ((c + a),(b + a)) by FUZZY_2:42
.= a + b by XXREAL_0:def 9, g5, XXREAL_0:2, Z1 ;
nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . (a,(min (b,c))) by NilminDef, Z1
.= 0 by NilminDef, g4, Z1
.= nilmin_norm . (c,0) by BU
.= nilmin_norm . ((nilmin_norm . (a,b)),c) by ZZ, FF ;
hence nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c) ; :: thesis: verum

end;

end;

end;

suppose Z1: ( a + b <= 1 & b + c <= 1 ) ; :: thesis: nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c)

then Z2: nilmin_norm . (b,c) = 0 by NilminDef;
Z3: nilmin_norm . (a,b) = 0 by NilminDef, Z1;
nilmin_norm . (a,(nilmin_norm . (b,c))) = 0 by BU, Z2
.= nilmin_norm . (c,0) by BU
.= nilmin_norm . ((nilmin_norm . (a,b)),c) by Z3, FF ;
hence nilmin_norm . (a,(nilmin_norm . (b,c))) = nilmin_norm . ((nilmin_norm . (a,b)),c) ; :: thesis: verum

end;

end;

end;

hence ( nilmin_norm is commutative & nilmin_norm is associative & nilmin_norm is with-1-identity & nilmin_norm is monotonic ) by FF, TT, D1, BINOP_1:def 3, BINOP_1:def 2; :: thesis: verum