let Q be Quantale; :: thesis: for D being Element of Q st D is dualizing holds
( Q is unital & the_unity_wrt the multF of Q = D -r> D & the_unity_wrt the multF of Q = D -l> D )
let D be Element of Q; :: thesis: ( D is dualizing implies ( Q is unital & the_unity_wrt the multF of Q = D -r> D & the_unity_wrt the multF of Q = D -l> D ) )
set I = D -l> D;
set J = D -r> D;
assume A1: for a being Element of Q holds
( (a -r> D) -l> D = a & (a -l> D) -r> D = a ) ; :: according to QUANTAL1:def 17 :: thesis: ( Q is unital & the_unity_wrt the multF of Q = D -r> D & the_unity_wrt the multF of Q = D -l> D )
A2: now :: thesis: for a being Element of Q holds
( a [*] (D -l> D) = a & (D -r> D) [*] a = a )
deffunc H5( set ) -> set = $1;
let a be Element of Q; :: thesis: ( a [*] (D -l> D) = a & (D -r> D) [*] a = a )
defpred S1[ Element of Q] means $1 [*] (a [*] (D -l> D)) [= D;
defpred S2[ Element of Q] means $1 [*] a [= D;
defpred S3[ Element of Q] means ((D -r> D) [*] a) [*] $1 [= D;
defpred S4[ Element of Q] means a [*] $1 [= D;
A3: for b being Element of Q holds
( S1[b] iff S2[b] )
proof
let b be Element of Q; :: thesis: ( S1[b] iff S2[b] )
( b [*] (a [*] (D -l> D)) = (b [*] a) [*] (D -l> D) & (D -l> D) -r> D = D ) by A1, GROUP_1:def 3;
hence ( S1[b] iff S2[b] ) by Th12; :: thesis: verum
end;
A4: { H5(b) where b is Element of Q : S1[b] } = { H5(c) where c is Element of Q : S2[c] } from FRAENKEL:sch 3(A3);
thus a [*] (D -l> D) = ((a [*] (D -l> D)) -r> D) -l> D by A1
.= (a -r> D) -l> D by A4
.= a by A1 ; :: thesis: (D -r> D) [*] a = a
A5: for b being Element of Q holds
( S3[b] iff S4[b] )
proof
let b be Element of Q; :: thesis: ( S3[b] iff S4[b] )
( (D -r> D) [*] (a [*] b) = ((D -r> D) [*] a) [*] b & (D -r> D) -l> D = D ) by A1, GROUP_1:def 3;
hence ( S3[b] iff S4[b] ) by Th11; :: thesis: verum
end;
A6: { H5(b) where b is Element of Q : S3[b] } = { H5(c) where c is Element of Q : S4[c] } from FRAENKEL:sch 3(A5);
thus (D -r> D) [*] a = (((D -r> D) [*] a) -l> D) -r> D by A1
.= (a -l> D) -r> D by A6
.= a by A1 ; :: thesis: verum
end;
A7: D -l> D is_a_right_unity_wrt H4(Q)
proof
let a be Element of Q; :: according to BINOP_1:def 17 :: thesis: H4(Q) . (a,(D -l> D)) = a
thus H4(Q) . (a,(D -l> D)) = a [*] (D -l> D)
.= a by A2 ; :: thesis: verum
end;
A8: D -l> D = (D -r> D) [*] (D -l> D) by A2;
D -l> D is_a_left_unity_wrt H4(Q)
proof
let a be Element of Q; :: according to BINOP_1:def 16 :: thesis: H4(Q) . ((D -l> D),a) = a
thus H4(Q) . ((D -l> D),a) = (D -r> D) [*] a by A2, A8
.= a by A2 ; :: thesis: verum
end;
then A9: D -l> D is_a_unity_wrt H4(Q) by A7;
hence H4(Q) is having_a_unity ; :: according to MONOID_0:def 10 :: thesis: ( the_unity_wrt the multF of Q = D -r> D & the_unity_wrt the multF of Q = D -l> D )
D -r> D = (D -r> D) [*] (D -l> D) by A2;
hence ( the_unity_wrt the multF of Q = D -r> D & the_unity_wrt the multF of Q = D -l> D ) by A8, A9, BINOP_1:def 8; :: thesis: verum