:: QMAX_1 semantic presentation

begin


definition
let X be non empty set ;
let S be SigmaField of X;
func Probabilities S ->  set  means :Def1: :: QMAX_1:def 1
 for x being set holds
( x in it iff x is Probability of S );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff x is Probability of S )
proof
defpred S1[ set ] means $1 is Probability of S;
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in Funcs (S,REAL) & S1[x] ) ) from XBOOLE_0:sch_1();
take  X ; ::_thesis: for x being set holds
( x in X iff x is Probability of S )
let x be set ; ::_thesis: ( x in X iff x is Probability of S )
 ( x is Probability of S implies x in Funcs (S,REAL) ) by FUNCT_2:8;
hence  ( x in X iff x is Probability of S ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is Probability of S ) ) & ( for x being set holds
( x in b2 iff x is Probability of S ) ) holds
b1 = b2
proof
let A1, A2 be set ; ::_thesis: ( ( for x being set holds
( x in A1 iff x is Probability of S ) ) & ( for x being set holds
( x in A2 iff x is Probability of S ) ) implies A1 = A2 )
assume that
A2: for x being set holds
( x in A1 iff x is Probability of S ) and
A3: for x being set holds
( x in A2 iff x is Probability of S ) ; ::_thesis: A1 = A2
now__::_thesis:_for_y_being_set_holds_
(_y_in_A1_iff_y_in_A2_)
let y be set ; ::_thesis: ( y in A1 iff y in A2 )
 ( y in A1 iff y is Probability of S ) by A2;
hence  ( y in A1 iff y in A2 ) by A3; ::_thesis: verum
end;
hence  A1 = A2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Probabilities QMAX_1:def_1_:_
 for X being non empty set
for S being SigmaField of X
for b3 being set holds
( b3 = Probabilities S iff for x being set holds
( x in b3 iff x is Probability of S ) );

registration
let X be non empty set ;
let S be SigmaField of X;
cluster Probabilities S ->  non empty ;
coherence
 not Probabilities S is empty
proof
set x = the Probability of S;
 the Probability of S in Probabilities S by Def1;
hence  not Probabilities S is empty ; ::_thesis: verum
end;
end;

definition
attrc1 is strict ;
struct QM_Str  -> ;
aggrQM_Str(# Observables, FStates, Quantum_Probability #) ->  QM_Str ;
sel Observables c1 ->  non empty set ;
sel FStates c1 ->  non empty set ;
sel Quantum_Probability c1 ->  Function of [: the Observables of c1, the FStates of c1:],(Probabilities Borel_Sets);
end;

definition
let Q be QM_Str ;
func Obs Q ->  set  equals :: QMAX_1:def 2
 the Observables of Q;
coherence
 the Observables of Q is set ;
func Sts Q ->  set  equals :: QMAX_1:def 3
 the FStates of Q;
coherence
 the FStates of Q is set ;
end;

:: deftheorem  defines Obs QMAX_1:def_2_:_
 for Q being QM_Str holds Obs Q = the Observables of Q;

:: deftheorem  defines Sts QMAX_1:def_3_:_
 for Q being QM_Str holds Sts Q = the FStates of Q;

registration
let Q be QM_Str ;
cluster Obs Q ->  non empty ;
coherence
 not Obs Q is empty ;
cluster Sts Q ->  non empty ;
coherence
 not Sts Q is empty ;
end;


definition
let Q be QM_Str ;
let A1 be Element of Obs Q;
let s be Element of Sts Q;
func Meas (A1,s) ->  Probability of Borel_Sets  equals :: QMAX_1:def 4
 the Quantum_Probability of Q . [A1,s];
coherence
 the Quantum_Probability of Q . [A1,s] is Probability of Borel_Sets
proof
reconsider A1s = [A1,s] as Element of [: the Observables of Q, the FStates of Q:] ;
 the Quantum_Probability of Q . A1s is Element of Probabilities Borel_Sets ;
hence  the Quantum_Probability of Q . [A1,s] is Probability of Borel_Sets by Def1; ::_thesis: verum
end;
end;

:: deftheorem  defines Meas QMAX_1:def_4_:_
 for Q being QM_Str
for A1 being Element of Obs Q
for s being Element of Sts Q holds Meas (A1,s) = the Quantum_Probability of Q . [A1,s];

set X = {0};

consider P being Function of Borel_Sets,REAL such that
Lm1:  for D being Subset of REAL st D in Borel_Sets holds
( ( 0 in D implies P . D = 1 ) & ( not 0 in D implies P . D = 0 ) ) by PROB_1:28;

Lm2:  for A being Event of Borel_Sets holds 0 <= P . A
proof
let A be Event of Borel_Sets ; ::_thesis: 0 <= P . A
now__::_thesis:_0_<=_P_._A
percases ( 0 in A or not 0 in A ) ;
suppose 0 in A ; ::_thesis: 0 <= P . A
then  P . A = 1 by Lm1;
hence  0 <= P . A ; ::_thesis: verum
end;
suppose not 0 in A ; ::_thesis: 0 <= P . A
hence  0 <= P . A by Lm1; ::_thesis: verum
end;
end;
end;
hence  0 <= P . A ; ::_thesis: verum
end;

Lm3:  P . REAL = 1
proof
 [#] REAL in Borel_Sets by PROB_1:5;
hence  P . REAL = 1 by Lm1; ::_thesis: verum
end;

Lm4:  for A, B being Event of Borel_Sets st A misses B holds
P . (A \/ B) = (P . A) + (P . B)
proof
let A, B be Event of Borel_Sets ; ::_thesis: ( A misses B implies P . (A \/ B) = (P . A) + (P . B) )
assume A1: A misses B ; ::_thesis: P . (A \/ B) = (P . A) + (P . B)
now__::_thesis:_P_._(A_\/_B)_=_(P_._A)_+_(P_._B)
percases ( ( 0 in A & not 0 in B ) or ( not 0 in A & 0 in B ) or ( not 0 in A & not 0 in B ) ) by A1, XBOOLE_0:3;
supposeA2: ( 0 in A & not 0 in B ) ; ::_thesis: P . (A \/ B) = (P . A) + (P . B)
then A3: 0 in A \/ B by XBOOLE_0:def_3;
 ( P . A = 1 & P . B = 0 ) by A2, Lm1;
hence  P . (A \/ B) = (P . A) + (P . B) by A3, Lm1; ::_thesis: verum
end;
supposeA4: ( not 0 in A & 0 in B ) ; ::_thesis: P . (A \/ B) = (P . A) + (P . B)
then A5: 0 in A \/ B by XBOOLE_0:def_3;
 ( P . A = 0 & P . B = 1 ) by A4, Lm1;
hence  P . (A \/ B) = (P . A) + (P . B) by A5, Lm1; ::_thesis: verum
end;
supposeA6: ( not 0 in A & not 0 in B ) ; ::_thesis: P . (A \/ B) = (P . A) + (P . B)
then A7: not 0 in A \/ B by XBOOLE_0:def_3;
 ( P . A = 0 & P . B = 0 ) by A6, Lm1;
hence  P . (A \/ B) = (P . A) + (P . B) by A7, Lm1; ::_thesis: verum
end;
end;
end;
hence  P . (A \/ B) = (P . A) + (P . B) ; ::_thesis: verum
end;

 for ASeq being SetSequence of Borel_Sets st ASeq is non-ascending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )
proof
let ASeq be SetSequence of Borel_Sets ; ::_thesis: ( ASeq is non-ascending implies ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) )
A1: now__::_thesis:_for_n_being_Element_of_NAT_holds_(P_*_ASeq)_._n_=_P_._(ASeq_._n)
let n be Element of NAT ; ::_thesis: (P * ASeq) . n = P . (ASeq . n)
 dom (P * ASeq) = NAT by FUNCT_2:def_1;
hence  (P * ASeq) . n = P . (ASeq . n) by FUNCT_1:12; ::_thesis: verum
end;
assume A2: ASeq is non-ascending ; ::_thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )
now__::_thesis:_(_P_*_ASeq_is_convergent_&_lim_(P_*_ASeq)_=_P_._(Intersection_ASeq)_)
percases ( for n being Element of NAT holds 0 in ASeq . n or ex n being Element of NAT st not 0 in ASeq . n ) ;
supposeA3: for n being Element of NAT holds 0 in ASeq . n ; ::_thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )
reconsider r = 1 as Real ;
 rng ASeq c= Borel_Sets by RELAT_1:def_19;
then A4: Intersection ASeq in Borel_Sets by PROB_1:def_6;
A5: 0 in Intersection ASeq by A3, PROB_1:13;
A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_(P_*_ASeq)_._n_=_1
let n be Element of NAT ; ::_thesis: (P * ASeq) . n = 1
A7: ( rng ASeq c= Borel_Sets & ASeq . n in rng ASeq ) by NAT_1:51, RELAT_1:def_19;
 0 in ASeq . n by A3;
then  P . (ASeq . n) = 1 by A7, Lm1;
hence  (P * ASeq) . n = 1 by A1; ::_thesis: verum
end;
A8: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
(P * ASeq) . n = r
proof
take  0 ; ::_thesis: for n being Element of NAT st 0 <= n holds
(P * ASeq) . n = r
thus  for n being Element of NAT st 0 <= n holds
(P * ASeq) . n = r by A6; ::_thesis: verum
end;
then  lim (P * ASeq) = 1 by PROB_1:1;
hence  ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) by A8, A5, A4, Lm1, PROB_1:1; ::_thesis: verum
end;
supposeA9: not for n being Element of NAT holds 0 in ASeq . n ; ::_thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )
 rng ASeq c= Borel_Sets by RELAT_1:def_19;
then A10: Intersection ASeq in Borel_Sets by PROB_1:def_6;
A11: not 0 in Intersection ASeq by A9, PROB_1:13;
A12: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
(P * ASeq) . n = 0
proof
consider m being Element of NAT  such that
A13: not 0 in ASeq . m by A9;
take  m ; ::_thesis: for n being Element of NAT st m <= n holds
(P * ASeq) . n = 0
 for n being Element of NAT st m <= n holds
(P * ASeq) . n = 0
proof
let n be Element of NAT ; ::_thesis: ( m <= n implies (P * ASeq) . n = 0 )
assume  m <= n ; ::_thesis: (P * ASeq) . n = 0
then  ASeq . n c= ASeq . m by A2, PROB_1:def_4;
then A14: not 0 in ASeq . n by A13;
 ( rng ASeq c= Borel_Sets & ASeq . n in rng ASeq ) by NAT_1:51, RELAT_1:def_19;
then  P . (ASeq . n) = 0 by A14, Lm1;
hence  (P * ASeq) . n = 0 by A1; ::_thesis: verum
end;
hence  for n being Element of NAT st m <= n holds
(P * ASeq) . n = 0 ; ::_thesis: verum
end;
then  lim (P * ASeq) = 0 by PROB_1:1;
hence  ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) by A12, A11, A10, Lm1, PROB_1:1; ::_thesis: verum
end;
end;
end;
hence  ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) ; ::_thesis: verum
end;

then reconsider P = P as Probability of Borel_Sets by Lm2, Lm3, Lm4, PROB_1:def_8;

set f = {[[0,0],P]};

 dom {[[0,0],P]} = {[0,0]}
by RELAT_1:9;

then Lm5:  dom {[[0,0],P]} = [:{0},{0}:]
by ZFMISC_1:29;

 ( rng {[[0,0],P]} = {P} & P in Probabilities Borel_Sets )
by Def1, RELAT_1:9;

then  rng {[[0,0],P]} c= Probabilities Borel_Sets
by ZFMISC_1:31;

then reconsider Y = {[[0,0],P]} as Function of [:{0},{0}:],(Probabilities Borel_Sets) by Lm5, FUNCT_2:def_1, RELSET_1:4;

Lm6: now__::_thesis:_(_(_for_A1,_A2_being_Element_of_Obs_QM_Str(#_{0},{0},Y_#)_st_(_for_s_being_Element_of_Sts_QM_Str(#_{0},{0},Y_#)_holds_Meas_(A1,s)_=_Meas_(A2,s)_)_holds_
A1_=_A2_)_&_(_for_s1,_s2_being_Element_of_Sts_QM_Str(#_{0},{0},Y_#)_st_(_for_A_being_Element_of_Obs_QM_Str(#_{0},{0},Y_#)_holds_Meas_(A,s1)_=_Meas_(A,s2)_)_holds_
s1_=_s2_)_&_(_for_s1,_s2_being_Element_of_Sts_QM_Str(#_{0},{0},Y_#)
for_t_being_Real_st_0_<=_t_&_t_<=_1_holds_
ex_s_being_Element_of_Sts_QM_Str(#_{0},{0},Y_#)_st_
for_A_being_Element_of_Obs_QM_Str(#_{0},{0},Y_#)
for_E_being_Event_of_Borel_Sets_holds_(Meas_(A,s))_._E_=_(t_*_((Meas_(A,s1))_._E))_+_((1_-_t)_*_((Meas_(A,s2))_._E))_)_)
thus  for A1, A2 being Element of Obs QM_Str(# {0},{0},Y #) st ( for s being Element of Sts QM_Str(# {0},{0},Y #) holds Meas (A1,s) = Meas (A2,s) ) holds
A1 = A2 ::_thesis: ( ( for s1, s2 being Element of Sts QM_Str(# {0},{0},Y #) st ( for A being Element of Obs QM_Str(# {0},{0},Y #) holds Meas (A,s1) = Meas (A,s2) ) holds
s1 = s2 ) & ( for s1, s2 being Element of Sts QM_Str(# {0},{0},Y #)
for t being Real st 0 <= t & t <= 1 holds
ex s being Element of Sts QM_Str(# {0},{0},Y #) st
for A being Element of Obs QM_Str(# {0},{0},Y #)
for E being Event of Borel_Sets holds (Meas (A,s)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E)) ) )
proof
let A1, A2 be Element of Obs QM_Str(# {0},{0},Y #); ::_thesis: ( ( for s being Element of Sts QM_Str(# {0},{0},Y #) holds Meas (A1,s) = Meas (A2,s) ) implies A1 = A2 )
 A1 = 0 by TARSKI:def_1;
hence  ( ( for s being Element of Sts QM_Str(# {0},{0},Y #) holds Meas (A1,s) = Meas (A2,s) ) implies A1 = A2 ) by TARSKI:def_1; ::_thesis: verum
end;
thus  for s1, s2 being Element of Sts QM_Str(# {0},{0},Y #) st ( for A being Element of Obs QM_Str(# {0},{0},Y #) holds Meas (A,s1) = Meas (A,s2) ) holds
s1 = s2 ::_thesis: for s1, s2 being Element of Sts QM_Str(# {0},{0},Y #)
for t being Real st 0 <= t & t <= 1 holds
ex s being Element of Sts QM_Str(# {0},{0},Y #) st
for A being Element of Obs QM_Str(# {0},{0},Y #)
for E being Event of Borel_Sets holds (Meas (A,s)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E))
proof
let s1, s2 be Element of Sts QM_Str(# {0},{0},Y #); ::_thesis: ( ( for A being Element of Obs QM_Str(# {0},{0},Y #) holds Meas (A,s1) = Meas (A,s2) ) implies s1 = s2 )
 s1 = 0 by TARSKI:def_1;
hence  ( ( for A being Element of Obs QM_Str(# {0},{0},Y #) holds Meas (A,s1) = Meas (A,s2) ) implies s1 = s2 ) by TARSKI:def_1; ::_thesis: verum
end;
thus  for s1, s2 being Element of Sts QM_Str(# {0},{0},Y #)
for t being Real st 0 <= t & t <= 1 holds
ex s being Element of Sts QM_Str(# {0},{0},Y #) st
for A being Element of Obs QM_Str(# {0},{0},Y #)
for E being Event of Borel_Sets holds (Meas (A,s)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E)) ::_thesis: verum
proof
let s1, s2 be Element of Sts QM_Str(# {0},{0},Y #); ::_thesis: for t being Real st 0 <= t & t <= 1 holds
ex s being Element of Sts QM_Str(# {0},{0},Y #) st
for A being Element of Obs QM_Str(# {0},{0},Y #)
for E being Event of Borel_Sets holds (Meas (A,s)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E))
let t be Real; ::_thesis: ( 0 <= t & t <= 1 implies ex s being Element of Sts QM_Str(# {0},{0},Y #) st
for A being Element of Obs QM_Str(# {0},{0},Y #)
for E being Event of Borel_Sets holds (Meas (A,s)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E)) )
assume  ( 0 <= t & t <= 1 ) ; ::_thesis: ex s being Element of Sts QM_Str(# {0},{0},Y #) st
for A being Element of Obs QM_Str(# {0},{0},Y #)
for E being Event of Borel_Sets holds (Meas (A,s)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E))
take  s2 ; ::_thesis: for A being Element of Obs QM_Str(# {0},{0},Y #)
for E being Event of Borel_Sets holds (Meas (A,s2)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E))
let A be Element of Obs QM_Str(# {0},{0},Y #); ::_thesis: for E being Event of Borel_Sets holds (Meas (A,s2)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E))
let E be Event of Borel_Sets ; ::_thesis: (Meas (A,s2)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E))
 ( s1 = 0 & s2 = 0 ) by TARSKI:def_1;
hence  (Meas (A,s2)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E)) ; ::_thesis: verum
end;
end;

definition
let IT be QM_Str ;
attrIT is Quantum_Mechanics-like  means :Def5: :: QMAX_1:def 5
( ( for A1, A2 being Element of Obs IT st ( for s being Element of Sts IT holds Meas (A1,s) = Meas (A2,s) ) holds
A1 = A2 ) & ( for s1, s2 being Element of Sts IT st ( for A being Element of Obs IT holds Meas (A,s1) = Meas (A,s2) ) holds
s1 = s2 ) & ( for s1, s2 being Element of Sts IT
for t being Real st 0 <= t & t <= 1 holds
ex s being Element of Sts IT st
for A being Element of Obs IT
for E being Event of Borel_Sets holds (Meas (A,s)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E)) ) );
end;

:: deftheorem Def5 defines Quantum_Mechanics-like QMAX_1:def_5_:_
 for IT being QM_Str holds
( IT is Quantum_Mechanics-like iff ( ( for A1, A2 being Element of Obs IT st ( for s being Element of Sts IT holds Meas (A1,s) = Meas (A2,s) ) holds
A1 = A2 ) & ( for s1, s2 being Element of Sts IT st ( for A being Element of Obs IT holds Meas (A,s1) = Meas (A,s2) ) holds
s1 = s2 ) & ( for s1, s2 being Element of Sts IT
for t being Real st 0 <= t & t <= 1 holds
ex s being Element of Sts IT st
for A being Element of Obs IT
for E being Event of Borel_Sets holds (Meas (A,s)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E)) ) ) );

registration
cluster strict Quantum_Mechanics-like for QM_Str ;
existence
 ex b1 being QM_Str st
( b1 is strict & b1 is Quantum_Mechanics-like )
proof
 QM_Str(# {0},{0},Y #) is Quantum_Mechanics-like by Def5, Lm6;
hence  ex b1 being QM_Str st
( b1 is strict & b1 is Quantum_Mechanics-like ) ; ::_thesis: verum
end;
end;

definition
mode Quantum_Mechanics is Quantum_Mechanics-like QM_Str ;
end;


definition
attrc1 is strict ;
struct OrthoRelStr  ->  RelStr , ComplStr ;
aggrOrthoRelStr(# carrier, InternalRel, Compl #) ->  OrthoRelStr ;
end;


definition
let X1 be set ;
let Inv be Function of X1,X1;
predInv is_an_involution  means :: QMAX_1:def 6
 for x1 being Element of X1 holds Inv . (Inv . x1) = x1;
end;

:: deftheorem  defines is_an_involution QMAX_1:def_6_:_
 for X1 being set
for Inv being Function of X1,X1 holds
( Inv is_an_involution iff for x1 being Element of X1 holds Inv . (Inv . x1) = x1 );

definition
let W be OrthoRelStr ;
predW is_a_Quantum_Logic  means :Def7: :: QMAX_1:def 7
( the InternalRel of W partially_orders the carrier of W & the Compl of W is_an_involution & ( for x, y being Element of W st [x,y] in the InternalRel of W holds
[( the Compl of W . y),( the Compl of W . x)] in the InternalRel of W ) );
end;

:: deftheorem Def7 defines is_a_Quantum_Logic QMAX_1:def_7_:_
 for W being OrthoRelStr holds
( W is_a_Quantum_Logic iff ( the InternalRel of W partially_orders the carrier of W & the Compl of W is_an_involution & ( for x, y being Element of W st [x,y] in the InternalRel of W holds
[( the Compl of W . y),( the Compl of W . x)] in the InternalRel of W ) ) );

definition
let Q be Quantum_Mechanics;
func Prop Q ->  set  equals :: QMAX_1:def 8
[:(Obs Q),Borel_Sets:];
coherence
 [:(Obs Q),Borel_Sets:] is set ;
end;

:: deftheorem  defines Prop QMAX_1:def_8_:_
 for Q being Quantum_Mechanics holds Prop Q = [:(Obs Q),Borel_Sets:];

registration
let Q be Quantum_Mechanics;
cluster Prop Q ->  non empty ;
coherence
 not Prop Q is empty ;
end;


definition
let Q be Quantum_Mechanics;
let p be Element of Prop Q;
:: original: `1
redefine funcp `1  ->  Element of Obs Q;
coherence
 p `1 is Element of Obs Q by MCART_1:10;
:: original: `2
redefine funcp `2  ->  Event of Borel_Sets ;
coherence
 p `2 is Event of Borel_Sets by MCART_1:10;
end;

theorem Th1: :: QMAX_1:1
for Q being Quantum_Mechanics
for s being Element of Sts Q
for p being Element of Prop Q
for E being Event of Borel_Sets st E = (p `2) ` holds
(Meas ((p `1),s)) . (p `2) = 1 - ((Meas ((p `1),s)) . E)
proof
let Q be Quantum_Mechanics; ::_thesis: for s being Element of Sts Q
for p being Element of Prop Q
for E being Event of Borel_Sets st E = (p `2) ` holds
(Meas ((p `1),s)) . (p `2) = 1 - ((Meas ((p `1),s)) . E)
let s be Element of Sts Q; ::_thesis: for p being Element of Prop Q
for E being Event of Borel_Sets st E = (p `2) ` holds
(Meas ((p `1),s)) . (p `2) = 1 - ((Meas ((p `1),s)) . E)
let p be Element of Prop Q; ::_thesis: for E being Event of Borel_Sets st E = (p `2) ` holds
(Meas ((p `1),s)) . (p `2) = 1 - ((Meas ((p `1),s)) . E)
let E be Event of Borel_Sets ; ::_thesis: ( E = (p `2) ` implies (Meas ((p `1),s)) . (p `2) = 1 - ((Meas ((p `1),s)) . E) )
assume A1: E = (p `2) ` ; ::_thesis: (Meas ((p `1),s)) . (p `2) = 1 - ((Meas ((p `1),s)) . E)
 ( [#] Borel_Sets = REAL & REAL \ E = E ` ) by PROB_1:def_7;
hence  (Meas ((p `1),s)) . (p `2) = 1 - ((Meas ((p `1),s)) . E) by A1, PROB_1:32; ::_thesis: verum
end;

definition
let Q be Quantum_Mechanics;
let p be Element of Prop Q;
func 'not' p ->  Element of Prop Q equals :: QMAX_1:def 9
[(p `1),((p `2) `)];
coherence
 [(p `1),((p `2) `)] is Element of Prop Q
proof
reconsider x = (p `2) ` as Event of Borel_Sets by PROB_1:20;
 x in Borel_Sets ;
hence  [(p `1),((p `2) `)] is Element of Prop Q by ZFMISC_1:87; ::_thesis: verum
end;
involutiveness
 for b1, b2 being Element of Prop Q st b1 = [(b2 `1),((b2 `2) `)] holds
b2 = [(b1 `1),((b1 `2) `)]
proof
let r, p be Element of Prop Q; ::_thesis: ( r = [(p `1),((p `2) `)] implies p = [(r `1),((r `2) `)] )
assume A1: r = [(p `1),((p `2) `)] ; ::_thesis: p = [(r `1),((r `2) `)]
thus p = [(p `1),(((p `2) `) `)] by MCART_1:21
.= [(r `1),(((p `2) `) `)] by A1, MCART_1:7
.= [(r `1),((r `2) `)] by A1, MCART_1:7 ; ::_thesis: verum
end;
end;

:: deftheorem  defines 'not' QMAX_1:def_9_:_
 for Q being Quantum_Mechanics
for p being Element of Prop Q holds 'not' p = [(p `1),((p `2) `)];

definition
let Q be Quantum_Mechanics;
let p, q be Element of Prop Q;
predp |- q means :Def10: :: QMAX_1:def 10
 for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) <= (Meas ((q `1),s)) . (q `2);
reflexivity
 for p being Element of Prop Q
for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) <= (Meas ((p `1),s)) . (p `2) ;
end;

:: deftheorem Def10 defines |- QMAX_1:def_10_:_
 for Q being Quantum_Mechanics
for p, q being Element of Prop Q holds
( p |- q iff for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) <= (Meas ((q `1),s)) . (q `2) );

definition
let Q be Quantum_Mechanics;
let p, q be Element of Prop Q;
predp <==> q means :Def11: :: QMAX_1:def 11
( p |- q & q |- p );
reflexivity
 for p being Element of Prop Q holds
( p |- p & p |- p ) ;
symmetry
 for p, q being Element of Prop Q st p |- q & q |- p holds
( q |- p & p |- q ) ;
end;

:: deftheorem Def11 defines <==> QMAX_1:def_11_:_
 for Q being Quantum_Mechanics
for p, q being Element of Prop Q holds
( p <==> q iff ( p |- q & q |- p ) );

theorem Th2: :: QMAX_1:2
for Q being Quantum_Mechanics
for p, q being Element of Prop Q holds
( p <==> q iff for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2) )
proof
let Q be Quantum_Mechanics; ::_thesis: for p, q being Element of Prop Q holds
( p <==> q iff for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2) )
let p, q be Element of Prop Q; ::_thesis: ( p <==> q iff for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2) )
thus  ( p <==> q implies for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2) ) ::_thesis: ( ( for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2) ) implies p <==> q )
proof
assume A1: p <==> q ; ::_thesis: for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2)
let s be Element of Sts Q; ::_thesis: (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2)
 q |- p by A1, Def11;
then A2: (Meas ((q `1),s)) . (q `2) <= (Meas ((p `1),s)) . (p `2) by Def10;
 p |- q by A1, Def11;
then  (Meas ((p `1),s)) . (p `2) <= (Meas ((q `1),s)) . (q `2) by Def10;
hence  (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2) by A2, XXREAL_0:1; ::_thesis: verum
end;
assume A3: for s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) = (Meas ((q `1),s)) . (q `2) ; ::_thesis: p <==> q
thus  p |- q :: according to QMAX_1:def_11 ::_thesis: q |- p
proof
let s be Element of Sts Q; :: according to QMAX_1:def_10 ::_thesis: (Meas ((p `1),s)) . (p `2) <= (Meas ((q `1),s)) . (q `2)
thus  (Meas ((p `1),s)) . (p `2) <= (Meas ((q `1),s)) . (q `2) by A3; ::_thesis: verum
end;
let s be Element of Sts Q; :: according to QMAX_1:def_10 ::_thesis: (Meas ((q `1),s)) . (q `2) <= (Meas ((p `1),s)) . (p `2)
thus  (Meas ((q `1),s)) . (q `2) <= (Meas ((p `1),s)) . (p `2) by A3; ::_thesis: verum
end;

theorem :: QMAX_1:3
for Q being Quantum_Mechanics
for p being Element of Prop Q holds p |- p ;

theorem Th4: :: QMAX_1:4
for Q being Quantum_Mechanics
for p, q, r being Element of Prop Q st p |- q & q |- r holds
p |- r
proof
let Q be Quantum_Mechanics; ::_thesis: for p, q, r being Element of Prop Q st p |- q & q |- r holds
p |- r
let p, q, r be Element of Prop Q; ::_thesis: ( p |- q & q |- r implies p |- r )
assume A1: ( p |- q & q |- r ) ; ::_thesis: p |- r
let s be Element of Sts Q; :: according to QMAX_1:def_10 ::_thesis: (Meas ((p `1),s)) . (p `2) <= (Meas ((r `1),s)) . (r `2)
 ( (Meas ((p `1),s)) . (p `2) <= (Meas ((q `1),s)) . (q `2) & (Meas ((q `1),s)) . (q `2) <= (Meas ((r `1),s)) . (r `2) ) by A1, Def10;
hence  (Meas ((p `1),s)) . (p `2) <= (Meas ((r `1),s)) . (r `2) by XXREAL_0:2; ::_thesis: verum
end;

theorem :: QMAX_1:5
for Q being Quantum_Mechanics
for p being Element of Prop Q holds p <==> p ;

theorem :: QMAX_1:6
for Q being Quantum_Mechanics
for p, q being Element of Prop Q st p <==> q holds
q <==> p ;

theorem Th7: :: QMAX_1:7
for Q being Quantum_Mechanics
for p, q, r being Element of Prop Q st p <==> q & q <==> r holds
p <==> r
proof
let Q be Quantum_Mechanics; ::_thesis: for p, q, r being Element of Prop Q st p <==> q & q <==> r holds
p <==> r
let p, q, r be Element of Prop Q; ::_thesis: ( p <==> q & q <==> r implies p <==> r )
assume  ( p |- q & q |- p & q |- r & r |- q ) ; :: according to QMAX_1:def_11 ::_thesis: p <==> r
hence  ( p |- r & r |- p ) by Th4; :: according to QMAX_1:def_11 ::_thesis: verum
end;

theorem :: QMAX_1:8
canceled;

theorem Th9: :: QMAX_1:9
for Q being Quantum_Mechanics
for p, q being Element of Prop Q st p |- q holds
'not' q |- 'not' p
proof
let Q be Quantum_Mechanics; ::_thesis: for p, q being Element of Prop Q st p |- q holds
'not' q |- 'not' p
let p, q be Element of Prop Q; ::_thesis: ( p |- q implies 'not' q |- 'not' p )
assume A1: p |- q ; ::_thesis: 'not' q |- 'not' p
let s be Element of Sts Q; :: according to QMAX_1:def_10 ::_thesis: (Meas ((('not' q) `1),s)) . (('not' q) `2) <= (Meas ((('not' p) `1),s)) . (('not' p) `2)
reconsider E1 = (q `2) ` as Event of Borel_Sets by PROB_1:20;
reconsider E = (p `2) ` as Event of Borel_Sets by PROB_1:20;
set p1 = (Meas ((p `1),s)) . E;
set p2 = (Meas ((q `1),s)) . E1;
A2: ( - (1 - ((Meas ((p `1),s)) . E)) = ((Meas ((p `1),s)) . E) - 1 & - (1 - ((Meas ((q `1),s)) . E1)) = ((Meas ((q `1),s)) . E1) - 1 ) ;
A3: ( ('not' p) `1 = p `1 & ('not' p) `2 = (p `2) ` ) by MCART_1:7;
A4: ( (Meas ((q `1),s)) . (q `2) = 1 - ((Meas ((q `1),s)) . E1) & (Meas ((p `1),s)) . (p `2) = 1 - ((Meas ((p `1),s)) . E) ) by Th1;
A5: ( ('not' q) `1 = q `1 & ('not' q) `2 = (q `2) ` ) by MCART_1:7;
 (Meas ((p `1),s)) . (p `2) <= (Meas ((q `1),s)) . (q `2) by A1, Def10;
then  ((Meas ((q `1),s)) . E1) - 1 <= ((Meas ((p `1),s)) . E) - 1 by A4, A2, XREAL_1:24;
hence  (Meas ((('not' q) `1),s)) . (('not' q) `2) <= (Meas ((('not' p) `1),s)) . (('not' p) `2) by A5, A3, XREAL_1:9; ::_thesis: verum
end;

definition
let Q be Quantum_Mechanics;
func PropRel Q ->  Equivalence_Relation of (Prop Q) means :Def12: :: QMAX_1:def 12
 for p, q being Element of Prop Q holds
( [p,q] in it iff p <==> q );
existence
 ex b1 being Equivalence_Relation of (Prop Q) st
for p, q being Element of Prop Q holds
( [p,q] in b1 iff p <==> q )
proof
defpred S1[ set , set ] means  ex p, q being Element of Prop Q st
( p = $1 & q = $2 & p <==> q );
A1: for x, y being set st S1[x,y] holds
S1[y,x] ;
A2: for x, y, z being set st S1[x,y] & S1[y,z] holds
S1[x,z] by Th7;
A3: for x being set st x in Prop Q holds
S1[x,x] ;
consider R being Equivalence_Relation of (Prop Q) such that
A4: for x, y being set holds
( [x,y] in R iff ( x in Prop Q & y in Prop Q & S1[x,y] ) ) from EQREL_1:sch_1(A3, A1, A2);
take  R ; ::_thesis: for p, q being Element of Prop Q holds
( [p,q] in R iff p <==> q )
 for p, q being Element of Prop Q holds
( [p,q] in R iff p <==> q )
proof
let p, q be Element of Prop Q; ::_thesis: ( [p,q] in R iff p <==> q )
thus  ( [p,q] in R implies p <==> q ) ::_thesis: ( p <==> q implies [p,q] in R )
proof
assume  [p,q] in R ; ::_thesis: p <==> q
then  ex p1, q1 being Element of Prop Q st
( p1 = p & q1 = q & p1 <==> q1 ) by A4;
hence  p <==> q ; ::_thesis: verum
end;
assume  p <==> q ; ::_thesis: [p,q] in R
hence  [p,q] in R by A4; ::_thesis: verum
end;
hence  for p, q being Element of Prop Q holds
( [p,q] in R iff p <==> q ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Equivalence_Relation of (Prop Q) st ( for p, q being Element of Prop Q holds
( [p,q] in b1 iff p <==> q ) ) & ( for p, q being Element of Prop Q holds
( [p,q] in b2 iff p <==> q ) ) holds
b1 = b2
proof
let R1, R2 be Equivalence_Relation of (Prop Q); ::_thesis: ( ( for p, q being Element of Prop Q holds
( [p,q] in R1 iff p <==> q ) ) & ( for p, q being Element of Prop Q holds
( [p,q] in R2 iff p <==> q ) ) implies R1 = R2 )
assume that
A5: for p, q being Element of Prop Q holds
( [p,q] in R1 iff p <==> q ) and
A6: for p, q being Element of Prop Q holds
( [p,q] in R2 iff p <==> q ) ; ::_thesis: R1 = R2
A7: now__::_thesis:_for_p,_q_being_Element_of_Prop_Q_holds_
(_[p,q]_in_R1_iff_[p,q]_in_R2_)
let p, q be Element of Prop Q; ::_thesis: ( [p,q] in R1 iff [p,q] in R2 )
 ( [p,q] in R1 iff p <==> q ) by A5;
hence  ( [p,q] in R1 iff [p,q] in R2 ) by A6; ::_thesis: verum
end;
 for x, y being set holds
( [x,y] in R1 iff [x,y] in R2 )
proof
let x, y be set ; ::_thesis: ( [x,y] in R1 iff [x,y] in R2 )
thus  ( [x,y] in R1 implies [x,y] in R2 ) ::_thesis: ( [x,y] in R2 implies [x,y] in R1 )
proof
assume A8: [x,y] in R1 ; ::_thesis: [x,y] in R2
then  ( x is Element of Prop Q & y is Element of Prop Q ) by ZFMISC_1:87;
hence  [x,y] in R2 by A7, A8; ::_thesis: verum
end;
assume A9: [x,y] in R2 ; ::_thesis: [x,y] in R1
then  ( x is Element of Prop Q & y is Element of Prop Q ) by ZFMISC_1:87;
hence  [x,y] in R1 by A7, A9; ::_thesis: verum
end;
hence  R1 = R2 by RELAT_1:def_2; ::_thesis: verum
end;
end;

:: deftheorem Def12 defines PropRel QMAX_1:def_12_:_
 for Q being Quantum_Mechanics
for b2 being Equivalence_Relation of (Prop Q) holds
( b2 = PropRel Q iff for p, q being Element of Prop Q holds
( [p,q] in b2 iff p <==> q ) );


theorem Th10: :: QMAX_1:10
for Q being Quantum_Mechanics
for B, C being Subset of (Prop Q) st B in Class (PropRel Q) & C in Class (PropRel Q) holds
for a, b, c, d being Element of Prop Q st a in B & b in B & c in C & d in C & a |- c holds
b |- d
proof
let Q be Quantum_Mechanics; ::_thesis: for B, C being Subset of (Prop Q) st B in Class (PropRel Q) & C in Class (PropRel Q) holds
for a, b, c, d being Element of Prop Q st a in B & b in B & c in C & d in C & a |- c holds
b |- d
let B, C be Subset of (Prop Q); ::_thesis: ( B in Class (PropRel Q) & C in Class (PropRel Q) implies for a, b, c, d being Element of Prop Q st a in B & b in B & c in C & d in C & a |- c holds
b |- d )
assume that
A1: B in Class (PropRel Q) and
A2: C in Class (PropRel Q) ; ::_thesis: for a, b, c, d being Element of Prop Q st a in B & b in B & c in C & d in C & a |- c holds
b |- d
let a, b, c, d be Element of Prop Q; ::_thesis: ( a in B & b in B & c in C & d in C & a |- c implies b |- d )
assume that
A3: ( a in B & b in B ) and
A4: ( c in C & d in C ) ; ::_thesis: ( not a |- c or b |- d )
assume A5: a |- c ; ::_thesis: b |- d
let s be Element of Sts Q; :: according to QMAX_1:def_10 ::_thesis: (Meas ((b `1),s)) . (b `2) <= (Meas ((d `1),s)) . (d `2)
 ex y being set st
( y in Prop Q & C = Class ((PropRel Q),y) ) by A2, EQREL_1:def_3;
then  [c,d] in PropRel Q by A4, EQREL_1:22;
then  c <==> d by Def12;
then A6: (Meas ((c `1),s)) . (c `2) = (Meas ((d `1),s)) . (d `2) by Th2;
 ex x being set st
( x in Prop Q & B = Class ((PropRel Q),x) ) by A1, EQREL_1:def_3;
then  [a,b] in PropRel Q by A3, EQREL_1:22;
then  a <==> b by Def12;
then  (Meas ((a `1),s)) . (a `2) = (Meas ((b `1),s)) . (b `2) by Th2;
hence  (Meas ((b `1),s)) . (b `2) <= (Meas ((d `1),s)) . (d `2) by A5, A6, Def10; ::_thesis: verum
end;

definition
let Q be Quantum_Mechanics;
func OrdRel Q ->  Relation of (Class (PropRel Q)) means :Def13: :: QMAX_1:def 13
 for B, C being Subset of (Prop Q) holds
( [B,C] in it iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) );
existence
 ex b1 being Relation of (Class (PropRel Q)) st
for B, C being Subset of (Prop Q) holds
( [B,C] in b1 iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) )
proof
defpred S1[ set , set ] means  ex B, C being Subset of (Prop Q) st
( $1 = B & $2 = C & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) );
consider R being Relation of (Class (PropRel Q)),(Class (PropRel Q)) such that
A1: for x, y being set holds
( [x,y] in R iff ( x in Class (PropRel Q) & y in Class (PropRel Q) & S1[x,y] ) ) from RELSET_1:sch_1();
 for B, C being Subset of (Prop Q) holds
( [B,C] in R iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) )
proof
let B, C be Subset of (Prop Q); ::_thesis: ( [B,C] in R iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) )
thus  ( [B,C] in R implies ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) ::_thesis: ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) implies [B,C] in R )
proof
assume A2: [B,C] in R ; ::_thesis: ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) )
then  ex B9, C9 being Subset of (Prop Q) st
( B = B9 & C = C9 & ( for p, q being Element of Prop Q st p in B9 & q in C9 holds
p |- q ) ) by A1;
hence  ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) by A1, A2; ::_thesis: verum
end;
assume  ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ; ::_thesis: [B,C] in R
hence  [B,C] in R by A1; ::_thesis: verum
end;
hence  ex b1 being Relation of (Class (PropRel Q)) st
for B, C being Subset of (Prop Q) holds
( [B,C] in b1 iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation of (Class (PropRel Q)) st ( for B, C being Subset of (Prop Q) holds
( [B,C] in b1 iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) ) & ( for B, C being Subset of (Prop Q) holds
( [B,C] in b2 iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) ) holds
b1 = b2
proof
let R1, R2 be Relation of (Class (PropRel Q)); ::_thesis: ( ( for B, C being Subset of (Prop Q) holds
( [B,C] in R1 iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) ) & ( for B, C being Subset of (Prop Q) holds
( [B,C] in R2 iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) ) implies R1 = R2 )
assume that
A3: for B, C being Subset of (Prop Q) holds
( [B,C] in R1 iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) and
A4: for B, C being Subset of (Prop Q) holds
( [B,C] in R2 iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) ; ::_thesis: R1 = R2
A5: now__::_thesis:_for_B,_C_being_Subset_of_(Prop_Q)_holds_
(_[B,C]_in_R1_iff_[B,C]_in_R2_)
let B, C be Subset of (Prop Q); ::_thesis: ( [B,C] in R1 iff [B,C] in R2 )
 ( [B,C] in R1 iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) by A3;
hence  ( [B,C] in R1 iff [B,C] in R2 ) by A4; ::_thesis: verum
end;
 for x, y being set holds
( [x,y] in R1 iff [x,y] in R2 )
proof
let x, y be set ; ::_thesis: ( [x,y] in R1 iff [x,y] in R2 )
thus  ( [x,y] in R1 implies [x,y] in R2 ) ::_thesis: ( [x,y] in R2 implies [x,y] in R1 )
proof
assume A6: [x,y] in R1 ; ::_thesis: [x,y] in R2
then  ( x in Class (PropRel Q) & y in Class (PropRel Q) ) by ZFMISC_1:87;
hence  [x,y] in R2 by A5, A6; ::_thesis: verum
end;
assume A7: [x,y] in R2 ; ::_thesis: [x,y] in R1
then  ( x in Class (PropRel Q) & y in Class (PropRel Q) ) by ZFMISC_1:87;
hence  [x,y] in R1 by A5, A7; ::_thesis: verum
end;
hence  R1 = R2 by RELAT_1:def_2; ::_thesis: verum
end;
end;

:: deftheorem Def13 defines OrdRel QMAX_1:def_13_:_
 for Q being Quantum_Mechanics
for b2 being Relation of (Class (PropRel Q)) holds
( b2 = OrdRel Q iff for B, C being Subset of (Prop Q) holds
( [B,C] in b2 iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) );

theorem Th11: :: QMAX_1:11
for Q being Quantum_Mechanics
for p, q being Element of Prop Q holds
( p |- q iff [(Class ((PropRel Q),p)),(Class ((PropRel Q),q))] in OrdRel Q )
proof
let Q be Quantum_Mechanics; ::_thesis: for p, q being Element of Prop Q holds
( p |- q iff [(Class ((PropRel Q),p)),(Class ((PropRel Q),q))] in OrdRel Q )
let p, q be Element of Prop Q; ::_thesis: ( p |- q iff [(Class ((PropRel Q),p)),(Class ((PropRel Q),q))] in OrdRel Q )
 [p,p] in PropRel Q by Def12;
then A1: p in Class ((PropRel Q),p) by EQREL_1:19;
 [q,q] in PropRel Q by Def12;
then A2: q in Class ((PropRel Q),q) by EQREL_1:19;
A3: ( Class ((PropRel Q),p) in Class (PropRel Q) & Class ((PropRel Q),q) in Class (PropRel Q) ) by EQREL_1:def_3;
thus  ( p |- q implies [(Class ((PropRel Q),p)),(Class ((PropRel Q),q))] in OrdRel Q ) ::_thesis: ( [(Class ((PropRel Q),p)),(Class ((PropRel Q),q))] in OrdRel Q implies p |- q )
proof
assume  p |- q ; ::_thesis: [(Class ((PropRel Q),p)),(Class ((PropRel Q),q))] in OrdRel Q
then  for p1, q1 being Element of Prop Q st p1 in Class ((PropRel Q),p) & q1 in Class ((PropRel Q),q) holds
p1 |- q1 by A1, A2, A3, Th10;
hence  [(Class ((PropRel Q),p)),(Class ((PropRel Q),q))] in OrdRel Q by A3, Def13; ::_thesis: verum
end;
thus  ( [(Class ((PropRel Q),p)),(Class ((PropRel Q),q))] in OrdRel Q implies p |- q ) by A1, A2, Def13; ::_thesis: verum
end;

theorem Th12: :: QMAX_1:12
for Q being Quantum_Mechanics
for B, C being Subset of (Prop Q) st B in Class (PropRel Q) & C in Class (PropRel Q) holds
for p1, q1 being Element of Prop Q st p1 in B & q1 in B & 'not' p1 in C holds
'not' q1 in C
proof
let Q be Quantum_Mechanics; ::_thesis: for B, C being Subset of (Prop Q) st B in Class (PropRel Q) & C in Class (PropRel Q) holds
for p1, q1 being Element of Prop Q st p1 in B & q1 in B & 'not' p1 in C holds
'not' q1 in C
let B, C be Subset of (Prop Q); ::_thesis: ( B in Class (PropRel Q) & C in Class (PropRel Q) implies for p1, q1 being Element of Prop Q st p1 in B & q1 in B & 'not' p1 in C holds
'not' q1 in C )
assume that
A1: B in Class (PropRel Q) and
A2: C in Class (PropRel Q) ; ::_thesis: for p1, q1 being Element of Prop Q st p1 in B & q1 in B & 'not' p1 in C holds
'not' q1 in C
consider y being set  such that
A3: y in Prop Q and
A4: C = Class ((PropRel Q),y) by A2, EQREL_1:def_3;
let p1, q1 be Element of Prop Q; ::_thesis: ( p1 in B & q1 in B & 'not' p1 in C implies 'not' q1 in C )
assume that
A5: ( p1 in B & q1 in B ) and
A6: 'not' p1 in C ; ::_thesis: 'not' q1 in C
 ex x being set st
( x in Prop Q & B = Class ((PropRel Q),x) ) by A1, EQREL_1:def_3;
then  [p1,q1] in PropRel Q by A5, EQREL_1:22;
then A7: p1 <==> q1 by Def12;
now__::_thesis:_for_s_being_Element_of_Sts_Q_holds_(Meas_((('not'_p1)_`1),s))_._(('not'_p1)_`2)_=_(Meas_((('not'_q1)_`1),s))_._(('not'_q1)_`2)
reconsider E1 = (q1 `2) ` , E = (p1 `2) ` as Event of Borel_Sets by PROB_1:20;
let s be Element of Sts Q; ::_thesis: (Meas ((('not' p1) `1),s)) . (('not' p1) `2) = (Meas ((('not' q1) `1),s)) . (('not' q1) `2)
set r1 = (Meas ((p1 `1),s)) . E;
set r2 = (Meas ((q1 `1),s)) . E1;
A8: ( ('not' p1) `1 = p1 `1 & ('not' p1) `2 = (p1 `2) ` ) by MCART_1:7;
A9: ('not' q1) `1 = q1 `1 by MCART_1:7;
1 - ((Meas ((p1 `1),s)) . E) = (Meas ((p1 `1),s)) . (p1 `2) by Th1
.= (Meas ((q1 `1),s)) . (q1 `2) by A7, Th2
.= 1 - ((Meas ((q1 `1),s)) . E1) by Th1 ;
hence  (Meas ((('not' p1) `1),s)) . (('not' p1) `2) = (Meas ((('not' q1) `1),s)) . (('not' q1) `2) by A8, A9, MCART_1:7; ::_thesis: verum
end;
then A10: 'not' p1 <==> 'not' q1 by Th2;
reconsider q = y as Element of Prop Q by A3;
 [('not' p1),q] in PropRel Q by A4, A6, EQREL_1:19;
then  'not' p1 <==> q by Def12;
then  q <==> 'not' q1 by A10, Th7;
then  [('not' q1),q] in PropRel Q by Def12;
hence  'not' q1 in C by A4, EQREL_1:19; ::_thesis: verum
end;

theorem :: QMAX_1:13
for Q being Quantum_Mechanics
for B, C being Subset of (Prop Q) st B in Class (PropRel Q) & C in Class (PropRel Q) holds
for p, q being Element of Prop Q st 'not' p in C & 'not' q in C & p in B holds
q in B
proof
let Q be Quantum_Mechanics; ::_thesis: for B, C being Subset of (Prop Q) st B in Class (PropRel Q) & C in Class (PropRel Q) holds
for p, q being Element of Prop Q st 'not' p in C & 'not' q in C & p in B holds
q in B
let B, C be Subset of (Prop Q); ::_thesis: ( B in Class (PropRel Q) & C in Class (PropRel Q) implies for p, q being Element of Prop Q st 'not' p in C & 'not' q in C & p in B holds
q in B )
assume A1: ( B in Class (PropRel Q) & C in Class (PropRel Q) ) ; ::_thesis: for p, q being Element of Prop Q st 'not' p in C & 'not' q in C & p in B holds
q in B
let p, q be Element of Prop Q; ::_thesis: ( 'not' p in C & 'not' q in C & p in B implies q in B )
 ( 'not' ('not' p) = p & 'not' ('not' q) = q ) ;
hence  ( 'not' p in C & 'not' q in C & p in B implies q in B ) by A1, Th12; ::_thesis: verum
end;

definition
let Q be Quantum_Mechanics;
func InvRel Q ->  Function of (Class (PropRel Q)),(Class (PropRel Q)) means :Def14: :: QMAX_1:def 14
 for p being Element of Prop Q holds it . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p));
existence
 ex b1 being Function of (Class (PropRel Q)),(Class (PropRel Q)) st
for p being Element of Prop Q holds b1 . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p))
proof
defpred S1[ set , set ] means  for p being Element of Prop Q st $1 = Class ((PropRel Q),p) holds
$2 = Class ((PropRel Q),('not' p));
A1: for x being set st x in Class (PropRel Q) holds
ex y being set st
( y in Class (PropRel Q) & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in Class (PropRel Q) implies ex y being set st
( y in Class (PropRel Q) & S1[x,y] ) )
assume A2: x in Class (PropRel Q) ; ::_thesis: ex y being set st
( y in Class (PropRel Q) & S1[x,y] )
then consider q being Element of Prop Q such that
A3: x = Class ((PropRel Q),q) by EQREL_1:36;
reconsider y = Class ((PropRel Q),('not' q)) as set ;
take  y ; ::_thesis: ( y in Class (PropRel Q) & S1[x,y] )
thus A4: y in Class (PropRel Q) by EQREL_1:def_3; ::_thesis: S1[x,y]
let p be Element of Prop Q; ::_thesis: ( x = Class ((PropRel Q),p) implies y = Class ((PropRel Q),('not' p)) )
assume A5: x = Class ((PropRel Q),p) ; ::_thesis: y = Class ((PropRel Q),('not' p))
then reconsider x = x as Subset of (Prop Q) ;
A6: q in x by A3, EQREL_1:20;
reconsider y9 = y as Subset of (Prop Q) ;
A7: 'not' q in y9 by EQREL_1:20;
 p in x by A5, EQREL_1:20;
then  'not' p in y9 by A2, A4, A6, A7, Th12;
hence  y = Class ((PropRel Q),('not' p)) by EQREL_1:23; ::_thesis: verum
end;
consider F being Function of (Class (PropRel Q)),(Class (PropRel Q)) such that
A8: for x being set st x in Class (PropRel Q) holds
S1[x,F . x] from FUNCT_2:sch_1(A1);
take  F ; ::_thesis: for p being Element of Prop Q holds F . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p))
let p be Element of Prop Q; ::_thesis: F . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p))
 Class ((PropRel Q),p) in Class (PropRel Q) by EQREL_1:def_3;
hence  F . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p)) by A8; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (Class (PropRel Q)),(Class (PropRel Q)) st ( for p being Element of Prop Q holds b1 . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p)) ) & ( for p being Element of Prop Q holds b2 . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p)) ) holds
b1 = b2
proof
let F1, F2 be Function of (Class (PropRel Q)),(Class (PropRel Q)); ::_thesis: ( ( for p being Element of Prop Q holds F1 . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p)) ) & ( for p being Element of Prop Q holds F2 . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p)) ) implies F1 = F2 )
assume that
A9: for p being Element of Prop Q holds F1 . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p)) and
A10: for p being Element of Prop Q holds F2 . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p)) ; ::_thesis: F1 = F2
now__::_thesis:_for_x_being_set_st_x_in_Class_(PropRel_Q)_holds_
F1_._x_=_F2_._x
let x be set ; ::_thesis: ( x in Class (PropRel Q) implies F1 . x = F2 . x )
assume  x in Class (PropRel Q) ; ::_thesis: F1 . x = F2 . x
then consider p being Element of Prop Q such that
A11: x = Class ((PropRel Q),p) by EQREL_1:36;
 F1 . x = Class ((PropRel Q),('not' p)) by A9, A11;
hence  F1 . x = F2 . x by A10, A11; ::_thesis: verum
end;
hence  F1 = F2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def14 defines InvRel QMAX_1:def_14_:_
 for Q being Quantum_Mechanics
for b2 being Function of (Class (PropRel Q)),(Class (PropRel Q)) holds
( b2 = InvRel Q iff for p being Element of Prop Q holds b2 . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p)) );

theorem :: QMAX_1:14
for Q being Quantum_Mechanics holds OrthoRelStr(# (Class (PropRel Q)),(OrdRel Q),(InvRel Q) #) is_a_Quantum_Logic
proof
let Q be Quantum_Mechanics; ::_thesis: OrthoRelStr(# (Class (PropRel Q)),(OrdRel Q),(InvRel Q) #) is_a_Quantum_Logic
A1: OrdRel Q is_transitive_in Class (PropRel Q)
proof
let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds
( not x in Class (PropRel Q) or not b1 in Class (PropRel Q) or not b2 in Class (PropRel Q) or not [x,b1] in OrdRel Q or not [b1,b2] in OrdRel Q or [x,b2] in OrdRel Q )
let y, z be set ; ::_thesis: ( not x in Class (PropRel Q) or not y in Class (PropRel Q) or not z in Class (PropRel Q) or not [x,y] in OrdRel Q or not [y,z] in OrdRel Q or [x,z] in OrdRel Q )
assume that
A2: x in Class (PropRel Q) and
A3: y in Class (PropRel Q) and
A4: z in Class (PropRel Q) and
A5: ( [x,y] in OrdRel Q & [y,z] in OrdRel Q ) ; ::_thesis: [x,z] in OrdRel Q
consider p being Element of Prop Q such that
A6: x = Class ((PropRel Q),p) by A2, EQREL_1:36;
consider r being Element of Prop Q such that
A7: z = Class ((PropRel Q),r) by A4, EQREL_1:36;
consider q being Element of Prop Q such that
A8: y = Class ((PropRel Q),q) by A3, EQREL_1:36;
 ( p |- q & q |- r implies p |- r ) by Th4;
hence  [x,z] in OrdRel Q by A5, A6, A8, A7, Th11; ::_thesis: verum
end;
A9: OrdRel Q is_antisymmetric_in Class (PropRel Q)
proof
let x be set ; :: according to RELAT_2:def_4 ::_thesis: for b1 being set holds
( not x in Class (PropRel Q) or not b1 in Class (PropRel Q) or not [x,b1] in OrdRel Q or not [b1,x] in OrdRel Q or x = b1 )
let y be set ; ::_thesis: ( not x in Class (PropRel Q) or not y in Class (PropRel Q) or not [x,y] in OrdRel Q or not [y,x] in OrdRel Q or x = y )
assume that
A10: x in Class (PropRel Q) and
A11: y in Class (PropRel Q) and
A12: ( [x,y] in OrdRel Q & [y,x] in OrdRel Q ) ; ::_thesis: x = y
consider p being Element of Prop Q such that
A13: x = Class ((PropRel Q),p) by A10, EQREL_1:36;
consider q being Element of Prop Q such that
A14: y = Class ((PropRel Q),q) by A11, EQREL_1:36;
A15: ( p <==> q implies [p,q] in PropRel Q ) by Def12;
 ( p |- q & q |- p implies p <==> q ) by Def11;
hence  x = y by A12, A13, A14, A15, Th11, EQREL_1:35; ::_thesis: verum
end;
A16: for x, y being Element of Class (PropRel Q) st [x,y] in OrdRel Q holds
[((InvRel Q) . y),((InvRel Q) . x)] in OrdRel Q
proof
let x, y be Element of Class (PropRel Q); ::_thesis: ( [x,y] in OrdRel Q implies [((InvRel Q) . y),((InvRel Q) . x)] in OrdRel Q )
consider p being Element of Prop Q such that
A17: x = Class ((PropRel Q),p) by EQREL_1:36;
consider q being Element of Prop Q such that
A18: y = Class ((PropRel Q),q) by EQREL_1:36;
A19: ( p |- q implies 'not' q |- 'not' p ) by Th9;
 ( (InvRel Q) . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p)) & (InvRel Q) . (Class ((PropRel Q),q)) = Class ((PropRel Q),('not' q)) ) by Def14;
hence  ( [x,y] in OrdRel Q implies [((InvRel Q) . y),((InvRel Q) . x)] in OrdRel Q ) by A17, A18, A19, Th11; ::_thesis: verum
end;
A20: InvRel Q is_an_involution
proof
let x be Element of Class (PropRel Q); :: according to QMAX_1:def_6 ::_thesis: (InvRel Q) . ((InvRel Q) . x) = x
consider p being Element of Prop Q such that
A21: x = Class ((PropRel Q),p) by EQREL_1:36;
(InvRel Q) . ((InvRel Q) . x) = (InvRel Q) . (Class ((PropRel Q),('not' p))) by A21, Def14
.= Class ((PropRel Q),('not' ('not' p))) by Def14 ;
hence  (InvRel Q) . ((InvRel Q) . x) = x by A21; ::_thesis: verum
end;
 OrdRel Q is_reflexive_in Class (PropRel Q)
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in Class (PropRel Q) or [x,x] in OrdRel Q )
assume  x in Class (PropRel Q) ; ::_thesis: [x,x] in OrdRel Q
then  ex p being Element of Prop Q st x = Class ((PropRel Q),p) by EQREL_1:36;
hence  [x,x] in OrdRel Q by Th11; ::_thesis: verum
end;
then  OrdRel Q partially_orders Class (PropRel Q) by A1, A9, ORDERS_1:def_7;
hence  OrthoRelStr(# (Class (PropRel Q)),(OrdRel Q),(InvRel Q) #) is_a_Quantum_Logic by A20, A16, Def7; ::_thesis: verum
end;