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