qmax_1.miz



    begin

    reserve X1,x,y,z for set,

n,m for Nat,

X for non empty set;

    reserve A,B for Event of Borel_Sets ,

D for Subset of REAL ;

    definition

      let X;

      let S be SigmaField of X;

      :: QMAX_1:def1

      func Probabilities (S) -> set means

      : Def1: for x be object holds x in it iff x is Probability of S;

      existence

      proof

        defpred P[ object] means $1 is Probability of S;

        consider X be set such that

         A1: for x be object holds x in X iff x in ( Funcs (S, REAL )) & P[x] from XBOOLE_0:sch 1;

        take X;

        let x be object;

        x is Probability of S implies x in ( Funcs (S, REAL )) by FUNCT_2: 8;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let A1,A2 be set;

        assume that

         A2: for x be object holds x in A1 iff x is Probability of S and

         A3: for x be object holds x in A2 iff x is Probability of S;

        now

          let y be object;

          y in A1 iff y is Probability of S by A2;

          hence y in A1 iff y in A2 by A3;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    registration

      let X;

      let S be SigmaField of X;

      cluster ( Probabilities S) -> non empty;

      coherence

      proof

        set x = the Probability of S;

        x in ( Probabilities S) by Def1;

        hence thesis;

      end;

    end

    definition

      struct QM_Str (# the Observables, FStates -> non empty set,

the Quantum_Probability -> Function of [: the Observables, the FStates:], ( Probabilities Borel_Sets ) #)

       attr strict strict;

    end

    reserve Q for QM_Str;

    definition

      let Q;

      :: QMAX_1:def2

      func Obs Q -> set equals the Observables of Q;

      coherence ;

      :: QMAX_1:def3

      func Sts Q -> set equals the FStates of Q;

      coherence ;

    end

    registration

      let Q;

      cluster ( Obs Q) -> non empty;

      coherence ;

      cluster ( Sts Q) -> non empty;

      coherence ;

    end

    reserve A1 for Element of ( Obs Q);

    reserve s for Element of ( Sts Q);

    reserve E for Event of Borel_Sets ;

    reserve ASeq for SetSequence of Borel_Sets ;

    definition

      let Q, A1, s;

      :: QMAX_1:def4

      func Meas (A1,s) -> Probability of Borel_Sets equals (the Quantum_Probability of Q . [A1, s]);

      coherence

      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 thesis by Def1;

      end;

    end

    set X = { 0 };

    consider P be Function of Borel_Sets , REAL such that

     Lm1: for D 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 holds 0 <= (P . A)

    proof

      let A;

      now

        per cases ;

          suppose 0 in A;

          then (P . A) = 1 by Lm1;

          hence thesis;

        end;

          suppose not 0 in A;

          hence thesis by Lm1;

        end;

      end;

      hence thesis;

    end;

    

     Lm3: (P . REAL ) = 1

    proof

      

       A1: 0 in REAL by XREAL_0:def 1;

      ( [#] REAL ) in Borel_Sets by PROB_1: 5;

      hence thesis by Lm1, A1;

    end;

    

     Lm4: for A, B st A misses B holds (P . (A \/ B)) = ((P . A) + (P . B))

    proof

      let A, B such that

       A1: A misses B;

      now

        per cases by A1, XBOOLE_0: 3;

          suppose

           A2: 0 in A & not 0 in B;

          then

           A3: 0 in (A \/ B) by XBOOLE_0:def 3;

          (P . A) = 1 & (P . B) = 0 by A2, Lm1;

          hence thesis by A3, Lm1;

        end;

          suppose

           A4: not 0 in A & 0 in B;

          then

           A5: 0 in (A \/ B) by XBOOLE_0:def 3;

          (P . A) = 0 & (P . B) = 1 by A4, Lm1;

          hence thesis by A5, Lm1;

        end;

          suppose

           A6: not 0 in A & not 0 in B;

          then

           A7: not 0 in (A \/ B) by XBOOLE_0:def 3;

          (P . A) = 0 & (P . B) = 0 by A6, Lm1;

          hence thesis by A7, Lm1;

        end;

      end;

      hence thesis;

    end;

    for ASeq st ASeq is non-ascending holds (P * ASeq) is convergent & ( lim (P * ASeq)) = (P . ( Intersection ASeq))

    proof

      let ASeq;

       A1:

      now

        let n;

        

         A2: n in NAT by ORDINAL1:def 12;

        ( dom (P * ASeq)) = NAT by FUNCT_2:def 1;

        hence ((P * ASeq) . n) = (P . (ASeq . n)) by A2, FUNCT_1: 12;

      end;

      assume

       A3: ASeq is non-ascending;

      now

        per cases ;

          suppose

           A4: for n holds 0 in (ASeq . n);

          ( rng ASeq) c= Borel_Sets by RELAT_1:def 19;

          then

           A5: ( Intersection ASeq) in Borel_Sets by PROB_1:def 6;

          

           A6: 0 in ( Intersection ASeq) by A4, PROB_1: 13;

           A7:

          now

            let n;

            

             A8: ( rng ASeq) c= Borel_Sets & (ASeq . n) in ( rng ASeq) by NAT_1: 51, RELAT_1:def 19;

            

             A9: (ASeq . n) in Borel_Sets by A8;

             0 in (ASeq . n) by A4;

            then (P . (ASeq . n)) = 1 by Lm1, A9;

            hence ((P * ASeq) . n) = 1 by A1;

          end;

          

           A10: ex m st for n st m <= n holds ((P * ASeq) . n) = 1

          proof

            take 0 ;

            thus thesis by A7;

          end;

          then ( lim (P * ASeq)) = 1 by PROB_1: 1;

          hence thesis by A10, A6, A5, Lm1, PROB_1: 1;

        end;

          suppose

           A11: not (for n holds 0 in (ASeq . n));

          ( rng ASeq) c= Borel_Sets by RELAT_1:def 19;

          then

           A12: ( Intersection ASeq) in Borel_Sets by PROB_1:def 6;

          

           A13: not 0 in ( Intersection ASeq) by A11, PROB_1: 13;

          

           A14: ex m st for n st m <= n holds ((P * ASeq) . n) = 0

          proof

            consider m such that

             A15: not 0 in (ASeq . m) by A11;

            take m;

            for n st m <= n holds ((P * ASeq) . n) = 0

            proof

              let n;

              assume m <= n;

              then (ASeq . n) c= (ASeq . m) by A3, PROB_1:def 4;

              then

               A16: not 0 in (ASeq . n) by A15;

              ( rng ASeq) c= Borel_Sets & (ASeq . n) in ( rng ASeq) by NAT_1: 51, RELAT_1:def 19;

              then (ASeq . n) in Borel_Sets ;

              then (P . (ASeq . n)) = 0 by A16, Lm1;

              hence thesis by A1;

            end;

            hence thesis;

          end;

          then ( lim (P * ASeq)) = 0 by PROB_1: 1;

          hence thesis by A14, A13, A12, Lm1, PROB_1: 1;

        end;

      end;

      hence thesis;

    end;

    then

    reconsider P as Probability of Borel_Sets by Lm2, Lm3, Lm4, PROB_1:def 8;

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

    ( dom f) = { [ 0 , 0 ]} by RELAT_1: 9;

    then

     Lm5: ( dom f) = [:X, X:] by ZFMISC_1: 29;

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

    then ( rng f) c= ( Probabilities Borel_Sets ) by ZFMISC_1: 31;

    then

    reconsider Y = f as Function of [:X, X:], ( Probabilities Borel_Sets ) by Lm5, FUNCT_2:def 1, RELSET_1: 4;

     Lm6:

    now

      thus for A1,A2 be Element of ( Obs QM_Str (# X, X, Y #)) st for s be Element of ( Sts QM_Str (# X, X, Y #)) holds ( Meas (A1,s)) = ( Meas (A2,s)) holds A1 = A2

      proof

        let A1,A2 be Element of ( Obs QM_Str (# X, X, Y #));

        A1 = 0 by TARSKI:def 1;

        hence thesis by TARSKI:def 1;

      end;

      thus for s1,s2 be Element of ( Sts QM_Str (# X, X, Y #)) st for A be Element of ( Obs QM_Str (# X, X, Y #)) holds ( Meas (A,s1)) = ( Meas (A,s2)) holds s1 = s2

      proof

        let s1,s2 be Element of ( Sts QM_Str (# X, X, Y #));

        s1 = 0 by TARSKI:def 1;

        hence thesis by TARSKI:def 1;

      end;

      thus for s1,s2 be Element of ( Sts QM_Str (# X, X, Y #)), t be Real st 0 <= t & t <= 1 holds ex s be Element of ( Sts QM_Str (# X, X, Y #)) st for A be Element of ( Obs QM_Str (# X, X, Y #)), E 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 (# X, X, Y #));

        let t be Real;

        assume 0 <= t & t <= 1;

        take s2;

        let A be Element of ( Obs QM_Str (# X, X, Y #)), E;

        s1 = 0 & s2 = 0 by TARSKI:def 1;

        hence thesis;

      end;

    end;

    definition

      let IT be QM_Str;

      :: QMAX_1:def5

      attr IT is Quantum_Mechanics-like means

      : Def5: (for A1,A2 be Element of ( Obs IT) st for s be Element of ( Sts IT) holds ( Meas (A1,s)) = ( Meas (A2,s)) holds A1 = A2) & (for s1,s2 be Element of ( Sts IT) st for A be Element of ( Obs IT) holds ( Meas (A,s1)) = ( Meas (A,s2)) holds s1 = s2) & for s1,s2 be Element of ( Sts IT), t be Real st 0 <= t & t <= 1 holds ex s be Element of ( Sts IT) st for A be Element of ( Obs IT), E holds (( Meas (A,s)) . E) = ((t * (( Meas (A,s1)) . E)) + ((1 - t) * (( Meas (A,s2)) . E)));

    end

    registration

      cluster strict Quantum_Mechanics-like for QM_Str;

      existence by Def5, Lm6;

    end

    definition

      mode Quantum_Mechanics is Quantum_Mechanics-like QM_Str;

    end

    reserve Q for Quantum_Mechanics;

    reserve s for Element of ( Sts Q);

    definition

      struct ( RelStr, ComplStr) OrthoRelStr (# the carrier -> set,

the InternalRel -> Relation of the carrier,

the Compl -> Function of the carrier, the carrier #)

       attr strict strict;

    end

    reserve x1 for Element of X1;

    reserve Inv for Function of X1, X1;

    definition

      let X1, Inv;

      :: QMAX_1:def6

      pred Inv is_an_involution means (Inv . (Inv . x1)) = x1;

    end

    definition

      let W be OrthoRelStr;

      :: QMAX_1:def7

      pred W is_a_Quantum_Logic means the InternalRel of W partially_orders the carrier of W & the Compl of W is_an_involution & for x,y be 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

    definition

      let Q;

      :: QMAX_1:def8

      func Prop Q -> set equals [:( Obs Q), Borel_Sets :];

      coherence ;

    end

    registration

      let Q;

      cluster ( Prop Q) -> non empty;

      coherence ;

    end

    reserve p,q,r,p1,q1 for Element of ( Prop Q);

    definition

      let Q, p;

      :: original: `1

      redefine

      func p `1 -> Element of ( Obs Q) ;

      coherence by MCART_1: 10;

      :: original: `2

      redefine

      func p `2 -> Event of Borel_Sets ;

      coherence by MCART_1: 10;

    end

    theorem :: QMAX_1:1

    

     Th1: for E st E = ((p `2 ) ` ) holds (( Meas ((p `1 ),s)) . (p `2 )) = (1 - (( Meas ((p `1 ),s)) . E))

    proof

      let E such that

       A1: E = ((p `2 ) ` );

      ( [#] Borel_Sets ) = REAL & ( REAL \ E) = (E ` ) by PROB_1:def 7;

      hence thesis by A1, PROB_1: 32;

    end;

    definition

      let Q, p;

      :: QMAX_1:def9

      func 'not' p -> Element of ( Prop Q) equals [(p `1 ), ((p `2 ) ` )];

      coherence

      proof

        reconsider x = ((p `2 ) ` ) as Event of Borel_Sets by PROB_1: 20;

        x in Borel_Sets ;

        hence thesis by ZFMISC_1: 87;

      end;

      involutiveness by MCART_1: 21;

    end

    definition

      let Q, p, q;

      :: QMAX_1:def10

      pred p |- q means for s holds (( Meas ((p `1 ),s)) . (p `2 )) <= (( Meas ((q `1 ),s)) . (q `2 ));

      reflexivity ;

    end

    definition

      let Q, p, q;

      :: QMAX_1:def11

      pred p <==> q means p |- q & q |- p;

      reflexivity ;

      symmetry ;

    end

    theorem :: QMAX_1:2

    

     Th2: p <==> q iff for s holds (( Meas ((p `1 ),s)) . (p `2 )) = (( Meas ((q `1 ),s)) . (q `2 ))

    proof

      thus p <==> q implies for s holds (( Meas ((p `1 ),s)) . (p `2 )) = (( Meas ((q `1 ),s)) . (q `2 ))

      proof

        assume

         A1: p <==> q;

        let s;

        q |- p by A1;

        then

         A2: (( Meas ((q `1 ),s)) . (q `2 )) <= (( Meas ((p `1 ),s)) . (p `2 ));

        p |- q by A1;

        then (( Meas ((p `1 ),s)) . (p `2 )) <= (( Meas ((q `1 ),s)) . (q `2 ));

        hence thesis by A2, XXREAL_0: 1;

      end;

      assume

       A3: for s holds (( Meas ((p `1 ),s)) . (p `2 )) = (( Meas ((q `1 ),s)) . (q `2 ));

      thus p |- q by A3;

      let s;

      thus thesis by A3;

    end;

    theorem :: QMAX_1:3

    p |- p;

    theorem :: QMAX_1:4

    

     Th4: p |- q & q |- r implies p |- r

    proof

      assume

       A1: p |- q & q |- r;

      let s;

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

      hence thesis by XXREAL_0: 2;

    end;

    theorem :: QMAX_1:5

    p <==> p;

    theorem :: QMAX_1:6

    p <==> q implies q <==> p;

    theorem :: QMAX_1:7

    

     Th7: p <==> q & q <==> r implies p <==> r by Th4;

    ::$Canceled

    theorem :: QMAX_1:9

    

     Th8: p |- q implies ( 'not' q) |- ( 'not' p)

    proof

      assume

       A1: p |- q;

      let s;

      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), p2 = (( Meas ((q `1 ),s)) . E1);

      

       A2: ( - (1 - p1)) = (p1 - 1) & ( - (1 - p2)) = (p2 - 1);

      

       A4: (( Meas ((q `1 ),s)) . (q `2 )) = (1 - p2) & (( Meas ((p `1 ),s)) . (p `2 )) = (1 - p1) by Th1;

      (( Meas ((p `1 ),s)) . (p `2 )) <= (( Meas ((q `1 ),s)) . (q `2 )) by A1;

      then (p2 - 1) <= (p1 - 1) by A4, A2, XREAL_1: 24;

      hence thesis by XREAL_1: 9;

    end;

    definition

      let Q;

      :: QMAX_1:def12

      func PropRel Q -> Equivalence_Relation of ( Prop Q) means

      : Def12: [p, q] in it iff p <==> q;

      existence

      proof

        defpred P[ object, object] means ex p, q st p = $1 & q = $2 & p <==> q;

        

         A1: for x,y be object st P[x, y] holds P[y, x];

        

         A2: for x,y,z be object st P[x, y] & P[y, z] holds P[x, z] by Th7;

        

         A3: for x be object st x in ( Prop Q) holds P[x, x];

        consider R be Equivalence_Relation of ( Prop Q) such that

         A4: for x,y be object holds [x, y] in R iff x in ( Prop Q) & y in ( Prop Q) & P[x, y] from EQREL_1:sch 1( A3, A1, A2);

        take R;

         [p, q] in R iff p <==> q

        proof

          thus [p, q] in R implies p <==> q

          proof

            assume [p, q] in R;

            then ex p1, q1 st p1 = p & q1 = q & p1 <==> q1 by A4;

            hence thesis;

          end;

          assume p <==> q;

          hence thesis by A4;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let R1,R2 be Equivalence_Relation of ( Prop Q);

        assume that

         A5: for p, q holds [p, q] in R1 iff p <==> q and

         A6: for p, q holds [p, q] in R2 iff p <==> q;

        

         A7: for p, q holds [p, q] in R1 iff [p, q] in R2 by A5, A6;

        for x,y be object holds [x, y] in R1 iff [x, y] in R2

        proof

          let x,y be object;

          thus [x, y] in R1 implies [x, y] in R2

          proof

            assume

             A8: [x, y] in R1;

            then x is Element of ( Prop Q) & y is Element of ( Prop Q) by ZFMISC_1: 87;

            hence thesis by A7, A8;

          end;

          assume

           A9: [x, y] in R2;

          then x is Element of ( Prop Q) & y is Element of ( Prop Q) by ZFMISC_1: 87;

          hence thesis by A7, A9;

        end;

        hence thesis by RELAT_1:def 2;

      end;

    end

    reserve B,C for Subset of ( Prop Q);

    theorem :: QMAX_1:10

    

     Th9: for B, C st B in ( Class ( PropRel Q)) & C in ( Class ( PropRel Q)) holds for a,b,c,d be Element of ( Prop Q) holds a in B & b in B & c in C & d in C & a |- c implies b |- d

    proof

      let B, C such that

       A1: B in ( Class ( PropRel Q)) and

       A2: C in ( Class ( PropRel Q));

      let a,b,c,d be Element of ( Prop Q);

      assume that

       A3: a in B & b in B and

       A4: c in C & d in C;

      assume

       A5: a |- c;

      let s;

      ex y be object 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 be object 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 thesis by A5, A6;

    end;

    definition

      let Q;

      :: QMAX_1:def13

      func OrdRel Q -> Relation of ( Class ( PropRel Q)) means

      : Def13: [B, C] in it iff B in ( Class ( PropRel Q)) & C in ( Class ( PropRel Q)) & for p, q st p in B & q in C holds p |- q;

      existence

      proof

        defpred P[ object, object] means ex B, C st $1 = B & $2 = C & for p, q st p in B & q in C holds p |- q;

        consider R be Relation of ( Class ( PropRel Q)), ( Class ( PropRel Q)) such that

         A1: for x,y be object holds [x, y] in R iff x in ( Class ( PropRel Q)) & y in ( Class ( PropRel Q)) & P[x, y] from RELSET_1:sch 1;

         [B, C] in R iff B in ( Class ( PropRel Q)) & C in ( Class ( PropRel Q)) & for p, q st p in B & q in C holds p |- q

        proof

          thus [B, C] in R implies B in ( Class ( PropRel Q)) & C in ( Class ( PropRel Q)) & for p, q st p in B & q in C holds p |- q

          proof

            assume

             A2: [B, C] in R;

            then ex B9,C9 be Subset of ( Prop Q) st B = B9 & C = C9 & for p, q st p in B9 & q in C9 holds p |- q by A1;

            hence thesis by A1, A2;

          end;

          assume B in ( Class ( PropRel Q)) & C in ( Class ( PropRel Q)) & for p, q st p in B & q in C holds p |- q;

          hence thesis by A1;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let R1,R2 be Relation of ( Class ( PropRel Q));

        assume that

         A3: for B, C holds [B, C] in R1 iff B in ( Class ( PropRel Q)) & C in ( Class ( PropRel Q)) & for p, q st p in B & q in C holds p |- q and

         A4: for B, C holds [B, C] in R2 iff B in ( Class ( PropRel Q)) & C in ( Class ( PropRel Q)) & for p, q st p in B & q in C holds p |- q;

         A5:

        now

          let B, C;

           [B, C] in R1 iff B in ( Class ( PropRel Q)) & C in ( Class ( PropRel Q)) & for p, 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;

        end;

        for x,y be object holds [x, y] in R1 iff [x, y] in R2

        proof

          let x,y be object;

          thus [x, y] in R1 implies [x, y] in R2

          proof

            assume

             A6: [x, y] in R1;

            then x in ( Class ( PropRel Q)) & y in ( Class ( PropRel Q)) by ZFMISC_1: 87;

            hence thesis by A5, A6;

          end;

          assume

           A7: [x, y] in R2;

          then x in ( Class ( PropRel Q)) & y in ( Class ( PropRel Q)) by ZFMISC_1: 87;

          hence thesis by A5, A7;

        end;

        hence thesis by RELAT_1:def 2;

      end;

    end

    theorem :: QMAX_1:11

    

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

    proof

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

      proof

        assume p |- q;

        then for p1, q1 holds p1 in ( Class (( PropRel Q),p)) & q1 in ( Class (( PropRel Q),q)) implies p1 |- q1 by A1, A2, A3, Th9;

        hence thesis by A3, Def13;

      end;

      thus thesis by A1, A2, Def13;

    end;

    theorem :: QMAX_1:12

    

     Th11: for B, C st B in ( Class ( PropRel Q)) & C in ( Class ( PropRel Q)) holds for p1, q1 holds p1 in B & q1 in B & ( 'not' p1) in C implies ( 'not' q1) in C

    proof

      let B, C such that

       A1: B in ( Class ( PropRel Q)) and

       A2: C in ( Class ( PropRel Q));

      consider y be object such that

       A3: y in ( Prop Q) and

       A4: C = ( Class (( PropRel Q),y)) by A2, EQREL_1:def 3;

      let p1, q1;

      assume that

       A5: p1 in B & q1 in B and

       A6: ( 'not' p1) in C;

      ex x be object 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

        reconsider E1 = ((q1 `2 ) ` ), E = ((p1 `2 ) ` ) as Event of Borel_Sets by PROB_1: 20;

        let s;

        set r1 = (( Meas ((p1 `1 ),s)) . E), r2 = (( Meas ((q1 `1 ),s)) . E1);

        (1 - r1) = (( Meas ((p1 `1 ),s)) . (p1 `2 )) by Th1

        .= (( Meas ((q1 `1 ),s)) . (q1 `2 )) by A7, Th2

        .= (1 - r2) by Th1;

        hence (( Meas ((( 'not' p1) `1 ),s)) . (( 'not' p1) `2 )) = (( Meas ((( 'not' q1) `1 ),s)) . (( 'not' q1) `2 ));

      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 thesis by A4, EQREL_1: 19;

    end;

    theorem :: QMAX_1:13

    for B, C st B in ( Class ( PropRel Q)) & C in ( Class ( PropRel Q)) holds for p, q holds ( 'not' p) in C & ( 'not' q) in C & p in B implies q in B

    proof

      let B, C such that

       A1: B in ( Class ( PropRel Q)) & C in ( Class ( PropRel Q));

      let p, q;

      ( 'not' ( 'not' p)) = p & ( 'not' ( 'not' q)) = q;

      hence thesis by A1, Th11;

    end;

    definition

      let Q;

      :: QMAX_1:def14

      func InvRel Q -> Function of ( Class ( PropRel Q)), ( Class ( PropRel Q)) means

      : Def14: (it . ( Class (( PropRel Q),p))) = ( Class (( PropRel Q),( 'not' p)));

      existence

      proof

        defpred P[ object, object] means for p st $1 = ( Class (( PropRel Q),p)) holds $2 = ( Class (( PropRel Q),( 'not' p)));

        

         A1: for x be object st x in ( Class ( PropRel Q)) holds ex y be object st y in ( Class ( PropRel Q)) & P[x, y]

        proof

          let x be object;

          assume

           A2: x in ( Class ( PropRel Q));

          then

          consider q such that

           A3: x = ( Class (( PropRel Q),q)) by EQREL_1: 36;

          reconsider y = ( Class (( PropRel Q),( 'not' q))) as set;

          take y;

          thus

           A4: y in ( Class ( PropRel Q)) by EQREL_1:def 3;

          let p;

          assume

           A5: x = ( Class (( PropRel Q),p));

          then

          reconsider 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, Th11;

          hence thesis by EQREL_1: 23;

        end;

        consider F be Function of ( Class ( PropRel Q)), ( Class ( PropRel Q)) such that

         A8: for x be object st x in ( Class ( PropRel Q)) holds P[x, (F . x)] from FUNCT_2:sch 1( A1);

        take F;

        let p;

        ( Class (( PropRel Q),p)) in ( Class ( PropRel Q)) by EQREL_1:def 3;

        hence thesis by A8;

      end;

      uniqueness

      proof

        let F1,F2 be Function of ( Class ( PropRel Q)), ( Class ( PropRel Q));

        assume that

         A9: for p holds (F1 . ( Class (( PropRel Q),p))) = ( Class (( PropRel Q),( 'not' p))) and

         A10: for p holds (F2 . ( Class (( PropRel Q),p))) = ( Class (( PropRel Q),( 'not' p)));

        now

          let x be object;

          assume x in ( Class ( PropRel Q));

          then

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

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: QMAX_1:14

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

    proof

      let Q;

      

       A1: ( OrdRel Q) is_transitive_in ( Class ( PropRel Q))

      proof

        let x,y,z be object;

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

        consider p such that

         A6: x = ( Class (( PropRel Q),p)) by A2, EQREL_1: 36;

        consider r such that

         A7: z = ( Class (( PropRel Q),r)) by A4, EQREL_1: 36;

        consider q such that

         A8: y = ( Class (( PropRel Q),q)) by A3, EQREL_1: 36;

        p |- q & q |- r implies p |- r by Th4;

        hence thesis by A5, A6, A8, A7, Th10;

      end;

      

       A9: ( OrdRel Q) is_antisymmetric_in ( Class ( PropRel Q))

      proof

        let x,y be object;

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

        consider p such that

         A13: x = ( Class (( PropRel Q),p)) by A10, EQREL_1: 36;

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

        thus thesis by A12, A13, A14, A15, Th10, EQREL_1: 35;

      end;

      

       A16: for x,y be 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));

        consider p such that

         A17: x = ( Class (( PropRel Q),p)) by EQREL_1: 36;

        consider q such that

         A18: y = ( Class (( PropRel Q),q)) by EQREL_1: 36;

        

         A19: p |- q implies ( 'not' q) |- ( 'not' p) by Th8;

        (( 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 thesis by A17, A18, A19, Th10;

      end;

      

       A20: ( InvRel Q) is_an_involution

      proof

        let x be Element of ( Class ( PropRel Q));

        consider p 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 thesis by A21;

      end;

      ( OrdRel Q) is_reflexive_in ( Class ( PropRel Q))

      proof

        let x be object;

        assume x in ( Class ( PropRel Q));

        then ex p st x = ( Class (( PropRel Q),p)) by EQREL_1: 36;

        hence thesis by Th10;

      end;

      then ( OrdRel Q) partially_orders ( Class ( PropRel Q)) by A1, A9, ORDERS_1:def 8;

      hence thesis by A20, A16;

    end;