:: by Pawe{\l} Sadowski, Andrzej Trybulec and Konrad Raczkowski

::

:: Received December 18, 1989

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

definition

let X be non empty set ;

let S be SigmaField of X;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff x is Probability of S )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff x is Probability of S ) ) & ( for x being set holds

( x in b_{2} iff x is Probability of S ) ) holds

b_{1} = b_{2}

end;
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 for x being set holds

( x in it iff x is Probability of S );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def1 defines Probabilities QMAX_1:def 1 :

for X being non empty set

for S being SigmaField of X

for b_{3} being set holds

( b_{3} = Probabilities S iff for x being set holds

( x in b_{3} iff x is Probability of S ) );

for X being non empty set

for S being SigmaField of X

for b

( b

( x in b

registration
end;

definition

attr c_{1} is strict ;

struct QM_Str -> ;

aggr QM_Str(# Observables, FStates, Quantum_Probability #) -> QM_Str ;

sel Observables c_{1} -> non empty set ;

sel FStates c_{1} -> non empty set ;

sel Quantum_Probability c_{1} -> Function of [: the Observables of c_{1}, the FStates of c_{1}:],(Probabilities Borel_Sets);

end;
struct QM_Str -> ;

aggr QM_Str(# Observables, FStates, Quantum_Probability #) -> QM_Str ;

sel Observables c

sel FStates c

sel Quantum_Probability c

definition
end;

definition

let Q be QM_Str ;

let A1 be Element of Obs Q;

let s be Element of Sts Q;

the Quantum_Probability of Q . [A1,s] is Probability of Borel_Sets

end;
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];

the Quantum_Probability of Q . [A1,s] is Probability of Borel_Sets

proof 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];

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 end;

Lm3: P . REAL = 1

proof end;

Lm4: for A, B being Event of Borel_Sets st A misses B holds

P . (A \/ B) = (P . A) + (P . B)

proof 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 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)) ) )

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)) ) )

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))

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

end;
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

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
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;
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

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

thus
for s1, s2 being Element of Sts QM_Str(# {0},{0},Y #)
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;
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

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;
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

definition

let IT be QM_Str ;

end;
attr IT 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)) ) );

( ( 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)) ) );

:: 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)) ) ) );

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
end;

definition

attr c_{1} is strict ;

struct OrthoRelStr -> RelStr , ComplStr ;

aggr OrthoRelStr(# carrier, InternalRel, Compl #) -> OrthoRelStr ;

end;
struct OrthoRelStr -> RelStr , ComplStr ;

aggr OrthoRelStr(# carrier, InternalRel, Compl #) -> OrthoRelStr ;

definition

let X1 be set ;

let Inv be Function of X1,X1;

end;
let Inv be Function of X1,X1;

pred Inv is_an_involution means :: QMAX_1:def 6

for x1 being Element of X1 holds Inv . (Inv . x1) = x1;

for x1 being Element of X1 holds Inv . (Inv . x1) = x1;

:: 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 );

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 ;

end;
pred W 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 ) );

( 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 ) );

:: 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 ) ) );

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 ) ) );

:: deftheorem defines Prop QMAX_1:def 8 :

for Q being Quantum_Mechanics holds Prop Q = [:(Obs Q),Borel_Sets:];

for Q being Quantum_Mechanics holds Prop Q = [:(Obs Q),Borel_Sets:];

registration
end;

definition

let Q be Quantum_Mechanics;

let p be Element of Prop Q;

:: original: `1

redefine func p `1 -> Element of Obs Q;

coherence

p `1 is Element of Obs Q by MCART_1:10;

:: original: `2

redefine func p `2 -> Event of Borel_Sets ;

coherence

p `2 is Event of Borel_Sets by MCART_1:10;

end;
let p be Element of Prop Q;

:: original: `1

redefine func p `1 -> Element of Obs Q;

coherence

p `1 is Element of Obs Q by MCART_1:10;

:: original: `2

redefine func p `2 -> Event of Borel_Sets ;

coherence

p `2 is Event of Borel_Sets by MCART_1:10;

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)

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 end;

definition

let Q be Quantum_Mechanics;

let p be Element of Prop Q;

coherence

[(p `1),((p `2) `)] is Element of Prop Q

for b_{1}, b_{2} being Element of Prop Q st b_{1} = [(b_{2} `1),((b_{2} `2) `)] holds

b_{2} = [(b_{1} `1),((b_{1} `2) `)]

end;
let p be Element of Prop Q;

coherence

[(p `1),((p `2) `)] is Element of Prop Q

proof end;

involutiveness for b

b

proof 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) `)];

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;

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;
let p, q be Element of Prop Q;

pred p |- 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 s being Element of Sts Q holds (Meas ((p `1),s)) . (p `2) <= (Meas ((q `1),s)) . (q `2);

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) ;

:: 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) );

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;

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;
let p, q be Element of Prop Q;

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 ) ;

:: 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 ) );

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) )

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 end;

theorem :: QMAX_1:6

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

for p, q, r being Element of Prop Q st p <==> q & q <==> r holds

p <==> r

proof end;

definition

let Q be Quantum_Mechanics;

ex b_{1} being Equivalence_Relation of (Prop Q) st

for p, q being Element of Prop Q holds

( [p,q] in b_{1} iff p <==> q )

for b_{1}, b_{2} being Equivalence_Relation of (Prop Q) st ( for p, q being Element of Prop Q holds

( [p,q] in b_{1} iff p <==> q ) ) & ( for p, q being Element of Prop Q holds

( [p,q] in b_{2} iff p <==> q ) ) holds

b_{1} = b_{2}

end;
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 for p, q being Element of Prop Q holds

( [p,q] in it iff p <==> q );

ex b

for p, q being Element of Prop Q holds

( [p,q] in b

proof end;

uniqueness for b

( [p,q] in b

( [p,q] in b

b

proof end;

:: deftheorem Def12 defines PropRel QMAX_1:def 12 :

for Q being Quantum_Mechanics

for b_{2} being Equivalence_Relation of (Prop Q) holds

( b_{2} = PropRel Q iff for p, q being Element of Prop Q holds

( [p,q] in b_{2} iff p <==> q ) );

for Q being Quantum_Mechanics

for b

( b

( [p,q] in b

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

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 end;

definition

let Q be Quantum_Mechanics;

ex b_{1} being Relation of (Class (PropRel Q)) st

for B, C being Subset of (Prop Q) holds

( [B,C] in b_{1} 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_{1}, b_{2} being Relation of (Class (PropRel Q)) st ( for B, C being Subset of (Prop Q) holds

( [B,C] in b_{1} 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 b_{2} 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

b_{1} = b_{2}

end;
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 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 ) ) );

ex b

for B, C being Subset of (Prop Q) holds

( [B,C] in b

p |- q ) ) )

proof end;

uniqueness for b

( [B,C] in b

p |- q ) ) ) ) & ( for B, C being Subset of (Prop Q) holds

( [B,C] in b

p |- q ) ) ) ) holds

b

proof end;

:: deftheorem Def13 defines OrdRel QMAX_1:def 13 :

for Q being Quantum_Mechanics

for b_{2} being Relation of (Class (PropRel Q)) holds

( b_{2} = OrdRel Q iff for B, C being Subset of (Prop Q) holds

( [B,C] in b_{2} 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 Q being Quantum_Mechanics

for b

( b

( [B,C] in b

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 )

for p, q being Element of Prop Q holds

( p |- q iff [(Class ((PropRel Q),p)),(Class ((PropRel Q),q))] in OrdRel Q )

proof 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

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 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

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 end;

definition

let Q be Quantum_Mechanics;

ex b_{1} being Function of (Class (PropRel Q)),(Class (PropRel Q)) st

for p being Element of Prop Q holds b_{1} . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p))

for b_{1}, b_{2} being Function of (Class (PropRel Q)),(Class (PropRel Q)) st ( for p being Element of Prop Q holds b_{1} . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p)) ) & ( for p being Element of Prop Q holds b_{2} . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p)) ) holds

b_{1} = b_{2}

end;
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 for p being Element of Prop Q holds it . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p));

ex b

for p being Element of Prop Q holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def14 defines InvRel QMAX_1:def 14 :

for Q being Quantum_Mechanics

for b_{2} being Function of (Class (PropRel Q)),(Class (PropRel Q)) holds

( b_{2} = InvRel Q iff for p being Element of Prop Q holds b_{2} . (Class ((PropRel Q),p)) = Class ((PropRel Q),('not' p)) );

for Q being Quantum_Mechanics

for b

( b

theorem :: QMAX_1:14

for Q being Quantum_Mechanics holds OrthoRelStr(# (Class (PropRel Q)),(OrdRel Q),(InvRel Q) #) is_a_Quantum_Logic

proof end;