:: QMAX_1 semantic presentation

definition
let c1 be non empty set ;
let c2 be SigmaField of c1;
func Probabilities c2 -> set means :Def1: :: QMAX_1:def 1
for b1 being set holds
( b1 in a3 iff b1 is Probability of a2 );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff b2 is Probability of c2 )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff b3 is Probability of c2 ) ) & ( for b3 being set holds
( b3 in b2 iff b3 is Probability of c2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Probabilities QMAX_1:def 1 :
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being set holds
( b3 = Probabilities b2 iff for b4 being set holds
( b4 in b3 iff b4 is Probability of b2 ) );

registration
let c1 be non empty set ;
let c2 be SigmaField of c1;
cluster Probabilities a2 -> non empty ;
coherence
not Probabilities c2 is empty
proof end;
end;

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

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

:: deftheorem Def2 defines Obs QMAX_1:def 2 :
for b1 being QM_Str holds Obs b1 = the Observables of b1;

:: deftheorem Def3 defines Sts QMAX_1:def 3 :
for b1 being QM_Str holds Sts b1 = the States of b1;

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

definition
let c1 be QM_Str ;
let c2 be Element of Obs c1;
let c3 be Element of Sts c1;
func Meas c2,c3 -> Probability of Borel_Sets equals :: QMAX_1:def 4
the Quantum_Probability of a1 . [a2,a3];
coherence
the Quantum_Probability of c1 . [c2,c3] is Probability of Borel_Sets
proof end;
end;

:: deftheorem Def4 defines Meas QMAX_1:def 4 :
for b1 being QM_Str
for b2 being Element of Obs b1
for b3 being Element of Sts b1 holds Meas b2,b3 = the Quantum_Probability of b1 . [b2,b3];

reconsider c1 = {0} as non empty set ;

consider c2 being Function of Borel_Sets , REAL such that
Lemma2: for b1 being Subset of REAL st b1 in Borel_Sets holds
( ( 0 in b1 implies c2 . b1 = 1 ) & ( not 0 in b1 implies c2 . b1 = 0 ) ) by PROB_1:60;

Lemma3: for b1 being Event of Borel_Sets holds
( ( 0 in b1 implies c2 . b1 = 1 ) & ( not 0 in b1 implies c2 . b1 = 0 ) )
proof end;

Lemma4: for b1 being Event of Borel_Sets holds 0 <= c2 . b1
proof end;

Lemma5: c2 . REAL = 1
proof end;

Lemma6: for b1, b2 being Event of Borel_Sets st b1 misses b2 holds
c2 . (b1 \/ b2) = (c2 . b1) + (c2 . b2)
proof end;

for b1 being SetSequence of Borel_Sets st b1 is non-increasing holds
( c2 * b1 is convergent & lim (c2 * b1) = c2 . (Intersection b1) )
proof end;

then reconsider c3 = c2 as Probability of Borel_Sets by Lemma4, Lemma5, Lemma6, PROB_1:def 13;

reconsider c4 = {[[0,0],c3]} as Function by GRFUNC_1:15;

Lemma7: ( dom c4 = {[0,0]} & rng c4 = {c3} )
by RELAT_1:23;

then Lemma8: dom c4 = [:c1,c1:]
by ZFMISC_1:35;

c3 in Probabilities Borel_Sets
by Def1;

then rng c4 c= Probabilities Borel_Sets
by Lemma7, ZFMISC_1:37;

then reconsider c5 = c4 as Function of [:c1,c1:], Probabilities Borel_Sets by Lemma8, FUNCT_2:def 1, RELSET_1:11;

E9: now
thus for b1, b2 being Element of Obs QM_Str(# c1,c1,c5 #) st ( for b3 being Element of Sts QM_Str(# c1,c1,c5 #) holds Meas b1,b3 = Meas b2,b3 ) holds
b1 = b2
proof
let c6, c7 be Element of Obs QM_Str(# c1,c1,c5 #);
( c6 = 0 & c7 = 0 ) by TARSKI:def 1;
hence ( ( for b1 being Element of Sts QM_Str(# c1,c1,c5 #) holds Meas c6,b1 = Meas c7,b1 ) implies c6 = c7 ) ;
end;
thus for b1, b2 being Element of Sts QM_Str(# c1,c1,c5 #) st ( for b3 being Element of Obs QM_Str(# c1,c1,c5 #) holds Meas b3,b1 = Meas b3,b2 ) holds
b1 = b2
proof
let c6, c7 be Element of Sts QM_Str(# c1,c1,c5 #);
( c6 = 0 & c7 = 0 ) by TARSKI:def 1;
hence ( ( for b1 being Element of Obs QM_Str(# c1,c1,c5 #) holds Meas b1,c6 = Meas b1,c7 ) implies c6 = c7 ) ;
end;
thus for b1, b2 being Element of Sts QM_Str(# c1,c1,c5 #)
for b3 being Real st 0 <= b3 & b3 <= 1 holds
ex b4 being Element of Sts QM_Str(# c1,c1,c5 #) st
for b5 being Element of Obs QM_Str(# c1,c1,c5 #)
for b6 being Event of Borel_Sets holds (Meas b5,b4) . b6 = (b3 * ((Meas b5,b1) . b6)) + ((1 - b3) * ((Meas b5,b2) . b6))
proof
let c6, c7 be Element of Sts QM_Str(# c1,c1,c5 #);
E10: ( c6 = 0 & c7 = 0 ) by TARSKI:def 1;
let c8 be Real;
assume ( 0 <= c8 & c8 <= 1 ) ;
take c7 ;
let c9 be Element of Obs QM_Str(# c1,c1,c5 #);
let c10 be Event of Borel_Sets ;
thus (Meas c9,c7) . c10 = (c8 + (1 - c8)) * ((Meas c9,c7) . c10)
.= (c8 * ((Meas c9,c6) . c10)) + ((1 - c8) * ((Meas c9,c7) . c10)) by E10, XCMPLX_1:8 ;
end;
end;

definition
let c6 be QM_Str ;
attr a1 is Quantum_Mechanics-like means :Def5: :: QMAX_1:def 5
( ( for b1, b2 being Element of Obs a1 st ( for b3 being Element of Sts a1 holds Meas b1,b3 = Meas b2,b3 ) holds
b1 = b2 ) & ( for b1, b2 being Element of Sts a1 st ( for b3 being Element of Obs a1 holds Meas b3,b1 = Meas b3,b2 ) holds
b1 = b2 ) & ( for b1, b2 being Element of Sts a1
for b3 being Real st 0 <= b3 & b3 <= 1 holds
ex b4 being Element of Sts a1 st
for b5 being Element of Obs a1
for b6 being Event of Borel_Sets holds (Meas b5,b4) . b6 = (b3 * ((Meas b5,b1) . b6)) + ((1 - b3) * ((Meas b5,b2) . b6)) ) );
end;

:: deftheorem Def5 defines Quantum_Mechanics-like QMAX_1:def 5 :
for b1 being QM_Str holds
( b1 is Quantum_Mechanics-like iff ( ( for b2, b3 being Element of Obs b1 st ( for b4 being Element of Sts b1 holds Meas b2,b4 = Meas b3,b4 ) holds
b2 = b3 ) & ( for b2, b3 being Element of Sts b1 st ( for b4 being Element of Obs b1 holds Meas b4,b2 = Meas b4,b3 ) holds
b2 = b3 ) & ( for b2, b3 being Element of Sts b1
for b4 being Real st 0 <= b4 & b4 <= 1 holds
ex b5 being Element of Sts b1 st
for b6 being Element of Obs b1
for b7 being Event of Borel_Sets holds (Meas b6,b5) . b7 = (b4 * ((Meas b6,b2) . b7)) + ((1 - b4) * ((Meas b6,b3) . b7)) ) ) );

registration
cluster strict Quantum_Mechanics-like QM_Str ;
existence
ex b1 being QM_Str st
( b1 is strict & b1 is Quantum_Mechanics-like )
proof end;
end;

definition
mode Quantum_Mechanics is Quantum_Mechanics-like QM_Str ;
end;

definition
let c6 be set ;
attr a2 is strict;
struct POI_Str of c1 -> ;
aggr POI_Str(# Ordering, Involution #) -> POI_Str of a1;
sel Ordering c2 -> Relation of a1;
sel Involution c2 -> Function of a1,a1;
end;

definition
let c6 be set ;
let c7 be Function of c6,c6;
pred c2 is_an_involution_in c1 means :: QMAX_1:def 6
for b1 being Element of a1 holds a2 . (a2 . b1) = b1;
end;

:: deftheorem Def6 defines is_an_involution_in QMAX_1:def 6 :
for b1 being set
for b2 being Function of b1,b1 holds
( b2 is_an_involution_in b1 iff for b3 being Element of b1 holds b2 . (b2 . b3) = b3 );

definition
let c6 be set ;
let c7 be POI_Str of c6;
pred c2 is_a_Quantuum_Logic_on c1 means :Def7: :: QMAX_1:def 7
ex b1 being Relation of a1ex b2 being Function of a1,a1 st
( a2 = POI_Str(# b1,b2 #) & b1 partially_orders a1 & b2 is_an_involution_in a1 & ( for b3, b4 being Element of a1 st [b3,b4] in b1 holds
[(b2 . b4),(b2 . b3)] in b1 ) );
end;

:: deftheorem Def7 defines is_a_Quantuum_Logic_on QMAX_1:def 7 :
for b1 being set
for b2 being POI_Str of b1 holds
( b2 is_a_Quantuum_Logic_on b1 iff ex b3 being Relation of b1ex b4 being Function of b1,b1 st
( b2 = POI_Str(# b3,b4 #) & b3 partially_orders b1 & b4 is_an_involution_in b1 & ( for b5, b6 being Element of b1 st [b5,b6] in b3 holds
[(b4 . b6),(b4 . b5)] in b3 ) ) );

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

:: deftheorem Def8 defines Prop QMAX_1:def 8 :
for b1 being Quantum_Mechanics holds Prop b1 = [:(Obs b1),Borel_Sets :];

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

definition
let c6 be Quantum_Mechanics;
let c7 be Element of Prop c6;
redefine func `1 as c2 `1 -> Element of Obs a1;
coherence
c7 `1 is Element of Obs c6 by MCART_1:10;
redefine func `2 as c2 `2 -> Event of Borel_Sets ;
coherence
c7 `2 is Event of Borel_Sets
proof end;
end;

theorem Th1: :: QMAX_1:1
canceled;

theorem Th2: :: QMAX_1:2
canceled;

theorem Th3: :: QMAX_1:3
canceled;

theorem Th4: :: QMAX_1:4
canceled;

theorem Th5: :: QMAX_1:5
canceled;

theorem Th6: :: QMAX_1:6
canceled;

theorem Th7: :: QMAX_1:7
canceled;

theorem Th8: :: QMAX_1:8
canceled;

theorem Th9: :: QMAX_1:9
canceled;

theorem Th10: :: QMAX_1:10
canceled;

theorem Th11: :: QMAX_1:11
canceled;

theorem Th12: :: QMAX_1:12
canceled;

theorem Th13: :: QMAX_1:13
canceled;

theorem Th14: :: QMAX_1:14
for b1 being Quantum_Mechanics
for b2 being Element of Prop b1 holds b2 = [(b2 `1 ),(b2 `2 )] by MCART_1:23;

theorem Th15: :: QMAX_1:15
canceled;

theorem Th16: :: QMAX_1:16
for b1 being Quantum_Mechanics
for b2 being Element of Sts b1
for b3 being Element of Prop b1
for b4 being Event of Borel_Sets st b4 = (b3 `2 ) ` holds
(Meas (b3 `1 ),b2) . (b3 `2 ) = 1 - ((Meas (b3 `1 ),b2) . b4)
proof end;

definition
let c6 be Quantum_Mechanics;
let c7 be Element of Prop c6;
func 'not' c2 -> Element of Prop a1 equals :: QMAX_1:def 9
[(a2 `1 ),((a2 `2 ) ` )];
coherence
[(c7 `1 ),((c7 `2 ) ` )] is Element of Prop c6
proof end;
end;

:: deftheorem Def9 defines 'not' QMAX_1:def 9 :
for b1 being Quantum_Mechanics
for b2 being Element of Prop b1 holds 'not' b2 = [(b2 `1 ),((b2 `2 ) ` )];

definition
let c6 be Quantum_Mechanics;
let c7, c8 be Element of Prop c6;
pred c2 |- c3 means :Def10: :: QMAX_1:def 10
for b1 being Element of Sts a1 holds (Meas (a2 `1 ),b1) . (a2 `2 ) <= (Meas (a3 `1 ),b1) . (a3 `2 );
end;

:: deftheorem Def10 defines |- QMAX_1:def 10 :
for b1 being Quantum_Mechanics
for b2, b3 being Element of Prop b1 holds
( b2 |- b3 iff for b4 being Element of Sts b1 holds (Meas (b2 `1 ),b4) . (b2 `2 ) <= (Meas (b3 `1 ),b4) . (b3 `2 ) );

definition
let c6 be Quantum_Mechanics;
let c7, c8 be Element of Prop c6;
pred c2 <==> c3 means :Def11: :: QMAX_1:def 11
( a2 |- a3 & a3 |- a2 );
end;

:: deftheorem Def11 defines <==> QMAX_1:def 11 :
for b1 being Quantum_Mechanics
for b2, b3 being Element of Prop b1 holds
( b2 <==> b3 iff ( b2 |- b3 & b3 |- b2 ) );

theorem Th17: :: QMAX_1:17
canceled;

theorem Th18: :: QMAX_1:18
canceled;

theorem Th19: :: QMAX_1:19
canceled;

theorem Th20: :: QMAX_1:20
for b1 being Quantum_Mechanics
for b2, b3 being Element of Prop b1 holds
( b2 <==> b3 iff for b4 being Element of Sts b1 holds (Meas (b2 `1 ),b4) . (b2 `2 ) = (Meas (b3 `1 ),b4) . (b3 `2 ) )
proof end;

theorem Th21: :: QMAX_1:21
for b1 being Quantum_Mechanics
for b2 being Element of Prop b1 holds b2 |- b2
proof end;

theorem Th22: :: QMAX_1:22
for b1 being Quantum_Mechanics
for b2, b3, b4 being Element of Prop b1 st b2 |- b3 & b3 |- b4 holds
b2 |- b4
proof end;

theorem Th23: :: QMAX_1:23
for b1 being Quantum_Mechanics
for b2 being Element of Prop b1 holds b2 <==> b2
proof end;

theorem Th24: :: QMAX_1:24
for b1 being Quantum_Mechanics
for b2, b3 being Element of Prop b1 st b2 <==> b3 holds
b3 <==> b2
proof end;

theorem Th25: :: QMAX_1:25
for b1 being Quantum_Mechanics
for b2, b3, b4 being Element of Prop b1 st b2 <==> b3 & b3 <==> b4 holds
b2 <==> b4
proof end;

theorem Th26: :: QMAX_1:26
for b1 being Quantum_Mechanics
for b2 being Element of Prop b1 holds
( ('not' b2) `1 = b2 `1 & ('not' b2) `2 = (b2 `2 ) ` ) by MCART_1:7;

theorem Th27: :: QMAX_1:27
for b1 being Quantum_Mechanics
for b2 being Element of Prop b1 holds 'not' ('not' b2) = b2
proof end;

theorem Th28: :: QMAX_1:28
for b1 being Quantum_Mechanics
for b2, b3 being Element of Prop b1 st b2 |- b3 holds
'not' b3 |- 'not' b2
proof end;

definition
let c6 be Quantum_Mechanics;
func PropRel c1 -> Equivalence_Relation of Prop a1 means :Def12: :: QMAX_1:def 12
for b1, b2 being Element of Prop a1 holds
( [b1,b2] in a2 iff b1 <==> b2 );
existence
ex b1 being Equivalence_Relation of Prop c6 st
for b2, b3 being Element of Prop c6 holds
( [b2,b3] in b1 iff b2 <==> b3 )
proof end;
uniqueness
for b1, b2 being Equivalence_Relation of Prop c6 st ( for b3, b4 being Element of Prop c6 holds
( [b3,b4] in b1 iff b3 <==> b4 ) ) & ( for b3, b4 being Element of Prop c6 holds
( [b3,b4] in b2 iff b3 <==> b4 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines PropRel QMAX_1:def 12 :
for b1 being Quantum_Mechanics
for b2 being Equivalence_Relation of Prop b1 holds
( b2 = PropRel b1 iff for b3, b4 being Element of Prop b1 holds
( [b3,b4] in b2 iff b3 <==> b4 ) );

theorem Th29: :: QMAX_1:29
canceled;

theorem Th30: :: QMAX_1:30
for b1 being Quantum_Mechanics
for b2, b3 being Subset of (Prop b1) st b2 in Class (PropRel b1) & b3 in Class (PropRel b1) holds
for b4, b5, b6, b7 being Element of Prop b1 st b4 in b2 & b5 in b2 & b6 in b3 & b7 in b3 & b4 |- b6 holds
b5 |- b7
proof end;

definition
let c6 be Quantum_Mechanics;
func OrdRel c1 -> Relation of Class (PropRel a1) means :Def13: :: QMAX_1:def 13
for b1, b2 being Subset of (Prop a1) holds
( [b1,b2] in a2 iff ( b1 in Class (PropRel a1) & b2 in Class (PropRel a1) & ( for b3, b4 being Element of Prop a1 st b3 in b1 & b4 in b2 holds
b3 |- b4 ) ) );
existence
ex b1 being Relation of Class (PropRel c6) st
for b2, b3 being Subset of (Prop c6) holds
( [b2,b3] in b1 iff ( b2 in Class (PropRel c6) & b3 in Class (PropRel c6) & ( for b4, b5 being Element of Prop c6 st b4 in b2 & b5 in b3 holds
b4 |- b5 ) ) )
proof end;
uniqueness
for b1, b2 being Relation of Class (PropRel c6) st ( for b3, b4 being Subset of (Prop c6) holds
( [b3,b4] in b1 iff ( b3 in Class (PropRel c6) & b4 in Class (PropRel c6) & ( for b5, b6 being Element of Prop c6 st b5 in b3 & b6 in b4 holds
b5 |- b6 ) ) ) ) & ( for b3, b4 being Subset of (Prop c6) holds
( [b3,b4] in b2 iff ( b3 in Class (PropRel c6) & b4 in Class (PropRel c6) & ( for b5, b6 being Element of Prop c6 st b5 in b3 & b6 in b4 holds
b5 |- b6 ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines OrdRel QMAX_1:def 13 :
for b1 being Quantum_Mechanics
for b2 being Relation of Class (PropRel b1) holds
( b2 = OrdRel b1 iff for b3, b4 being Subset of (Prop b1) holds
( [b3,b4] in b2 iff ( b3 in Class (PropRel b1) & b4 in Class (PropRel b1) & ( for b5, b6 being Element of Prop b1 st b5 in b3 & b6 in b4 holds
b5 |- b6 ) ) ) );

theorem Th31: :: QMAX_1:31
canceled;

theorem Th32: :: QMAX_1:32
for b1 being Quantum_Mechanics
for b2, b3 being Element of Prop b1 holds
( b2 |- b3 iff [(Class (PropRel b1),b2),(Class (PropRel b1),b3)] in OrdRel b1 )
proof end;

theorem Th33: :: QMAX_1:33
for b1 being Quantum_Mechanics
for b2, b3 being Subset of (Prop b1) st b2 in Class (PropRel b1) & b3 in Class (PropRel b1) holds
for b4, b5 being Element of Prop b1 st b4 in b2 & b5 in b2 & 'not' b4 in b3 holds
'not' b5 in b3
proof end;

theorem Th34: :: QMAX_1:34
for b1 being Quantum_Mechanics
for b2, b3 being Subset of (Prop b1) st b2 in Class (PropRel b1) & b3 in Class (PropRel b1) holds
for b4, b5 being Element of Prop b1 st 'not' b4 in b3 & 'not' b5 in b3 & b4 in b2 holds
b5 in b2
proof end;

definition
let c6 be Quantum_Mechanics;
func InvRel c1 -> Function of Class (PropRel a1), Class (PropRel a1) means :Def14: :: QMAX_1:def 14
for b1 being Element of Prop a1 holds a2 . (Class (PropRel a1),b1) = Class (PropRel a1),('not' b1);
existence
ex b1 being Function of Class (PropRel c6), Class (PropRel c6) st
for b2 being Element of Prop c6 holds b1 . (Class (PropRel c6),b2) = Class (PropRel c6),('not' b2)
proof end;
uniqueness
for b1, b2 being Function of Class (PropRel c6), Class (PropRel c6) st ( for b3 being Element of Prop c6 holds b1 . (Class (PropRel c6),b3) = Class (PropRel c6),('not' b3) ) & ( for b3 being Element of Prop c6 holds b2 . (Class (PropRel c6),b3) = Class (PropRel c6),('not' b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines InvRel QMAX_1:def 14 :
for b1 being Quantum_Mechanics
for b2 being Function of Class (PropRel b1), Class (PropRel b1) holds
( b2 = InvRel b1 iff for b3 being Element of Prop b1 holds b2 . (Class (PropRel b1),b3) = Class (PropRel b1),('not' b3) );

theorem Th35: :: QMAX_1:35
canceled;

theorem Th36: :: QMAX_1:36
for b1 being Quantum_Mechanics holds POI_Str(# (OrdRel b1),(InvRel b1) #) is_a_Quantuum_Logic_on Class (PropRel b1)
proof end;