Theory MMI_Complex_ZF

(* 
    This file is a part of MMIsar - a translation of Metamath's set.mm to Isabelle 2005 (ZF logic).

    Copyright (C) 2006  Slawomir Kolodynski

    This program is free software; Redistribution and use in source and binary forms, 
    with or without modification, are permitted provided that the following conditions are met:

   1. Redistributions of source code must retain the above copyright notice, 
   this list of conditions and the following disclaimer.
   2. Redistributions in binary form must reproduce the above copyright notice, 
   this list of conditions and the following disclaimer in the documentation and/or 
   other materials provided with the distribution.
   3. The name of the author may not be used to endorse or promote products 
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES,
INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT,
INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR
BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,
STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE
USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

*)

section ‹Complex numbers in Metamatah - introduction›

theory MMI_Complex_ZF imports MMI_logic_and_sets

begin 

text‹This theory contains theorems (with proofs) about complex numbers
  imported from the Metamath's set.mm database. 
  The original Metamath proofs were mostly written by Norman Megill, 
  see the Metamath Proof Explorer pages for full atribution.
  This theory contains about 200 theorems from "recnt" to "div11t".
›

  lemma (in MMIsar0) MMI_recnt: 
   shows "A ∈ ℝ ⟶ A ∈ ℂ"
proof -
   have S1: "ℝ ⊆ ℂ" by (rule MMI_axresscn)
   from S1 show "A ∈ ℝ ⟶ A ∈ ℂ" by (rule MMI_sseli)
qed

lemma (in MMIsar0) MMI_recn: assumes A1: "A ∈ ℝ"   
   shows "A ∈ ℂ"
proof -
   have S1: "ℝ ⊆ ℂ" by (rule MMI_axresscn)
   from A1 have S2: "A ∈ ℝ".
   from S1 S2 show "A ∈ ℂ" by (rule MMI_sselii)
qed

lemma (in MMIsar0) MMI_recnd: assumes A1: "φ ⟶ A ∈ ℝ"   
   shows "φ ⟶ A ∈ ℂ"
proof -
   from A1 have S1: "φ ⟶ A ∈ ℝ".
   have S2: "A ∈ ℝ ⟶ A ∈ ℂ" by (rule MMI_recnt)
   from S1 S2 show "φ ⟶ A ∈ ℂ" by (rule MMI_syl)
qed

lemma (in MMIsar0) MMI_elimne0: 
   shows "if ( A ≠ 𝟬 , A , 𝟭 ) ≠ 𝟬"
proof -
   have S1: "A = if ( A ≠ 𝟬 , A , 𝟭 ) ⟶ 
     ( A ≠ 𝟬 ⟷ if ( A ≠ 𝟬 , A , 𝟭 ) ≠ 𝟬 )" by (rule MMI_neeq1)
   have S2: "𝟭 = if ( A ≠ 𝟬 , A , 𝟭 ) ⟶ 
     ( 𝟭 ≠ 𝟬 ⟷ if ( A ≠ 𝟬 , A , 𝟭 ) ≠ 𝟬 )" by (rule MMI_neeq1)
   have S3: "𝟭 ≠ 𝟬" by (rule MMI_ax1ne0)
   from S1 S2 S3 show "if ( A ≠ 𝟬 , A , 𝟭 ) ≠ 𝟬" by (rule MMI_elimhyp)
qed

lemma (in MMIsar0) MMI_addex: 
   shows "\<caddset> isASet"
proof -
   have S1: "ℂ isASet" by (rule MMI_axcnex)
   have S2: "ℂ isASet" by (rule MMI_axcnex)
   from S1 S2 have S3: "( ℂ × ℂ ) isASet" by (rule MMI_xpex)
   have S4: "\<caddset> : ( ℂ × ℂ ) → ℂ" by (rule MMI_axaddopr)
   have S5: "( ℂ × ℂ ) isASet ⟶ 
     ( \<caddset> : ( ℂ × ℂ ) → ℂ ⟶ \<caddset> isASet )" by (rule MMI_fex)
   from S3 S4 S5 show "\<caddset> isASet" by (rule MMI_mp2)
qed

lemma (in MMIsar0) MMI_mulex: 
   shows "\<cmulset> isASet"
proof -
   have S1: "ℂ isASet" by (rule MMI_axcnex)
   have S2: "ℂ isASet" by (rule MMI_axcnex)
   from S1 S2 have S3: "( ℂ × ℂ ) isASet" by (rule MMI_xpex)
   have S4: "\<cmulset> : ( ℂ × ℂ ) → ℂ" by (rule MMI_axmulopr)
   have S5: "( ℂ × ℂ ) isASet ⟶ 
     ( \<cmulset> : ( ℂ × ℂ ) → ℂ ⟶ \<cmulset> isASet )" by (rule MMI_fex)
   from S3 S4 S5 show "\<cmulset> isASet" by (rule MMI_mp2)
qed

lemma (in MMIsar0) MMI_adddirt: 
   shows "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ 
  ( ( A \<ca> B ) ⋅ C ) = ( ( A ⋅ C ) \<ca> ( B ⋅ C ) )"
proof -
   have S1: "( C ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℂ ) ⟶ 
     ( C ⋅ ( A \<ca> B ) ) = ( ( C ⋅ A ) \<ca> ( C ⋅ B ) )" 
     by (rule MMI_axdistr)
   from S1 have S2: "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ 
     ( C ⋅ ( A \<ca> B ) ) = ( ( C ⋅ A ) \<ca> ( C ⋅ B ) )" by (rule MMI_3coml)
   have S3: "( ( A \<ca> B ) ∈ ℂ ∧ C ∈ ℂ ) ⟶ 
     ( ( A \<ca> B ) ⋅ C ) = ( C ⋅ ( A \<ca> B ) )" by (rule MMI_axmulcom)
   have S4: "( A ∈ ℂ ∧ B ∈ ℂ ) ⟶ ( A \<ca> B ) ∈ ℂ" by (rule MMI_axaddcl)
   from S3 S4 have S5: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ C ∈ ℂ ) ⟶ 
     ( ( A \<ca> B ) ⋅ C ) = ( C ⋅ ( A \<ca> B ) )" by (rule MMI_sylan)
   from S5 have S6: "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ 
     ( ( A \<ca> B ) ⋅ C ) = ( C ⋅ ( A \<ca> B ) )" by (rule MMI_3impa)
   have S7: "( A ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( A ⋅ C ) = ( C ⋅ A )" 
     by (rule MMI_axmulcom)
   from S7 have S8: "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( A ⋅ C ) = ( C ⋅ A )" 
     by (rule MMI_3adant2)
   have S9: "( B ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( B ⋅ C ) = ( C ⋅ B )" 
     by (rule MMI_axmulcom)
   from S9 have S10: "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( B ⋅ C ) = ( C ⋅ B )" 
     by (rule MMI_3adant1)
   from S8 S10 have S11: "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ 
     ( ( A ⋅ C ) \<ca> ( B ⋅ C ) ) = ( ( C ⋅ A ) \<ca> ( C ⋅ B ) )" 
     by (rule MMI_opreq12d)
   from S2 S6 S11 show "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ 
     ( ( A \<ca> B ) ⋅ C ) = ( ( A ⋅ C ) \<ca> ( B ⋅ C ) )" 
     by (rule MMI_3eqtr4d)
qed

lemma (in MMIsar0) MMI_addcl: assumes A1: "A ∈ ℂ" and
    A2: "B ∈ ℂ"   
   shows "( A \<ca> B ) ∈ ℂ"
proof -
   from A1 have S1: "A ∈ ℂ".
   from A2 have S2: "B ∈ ℂ".
   have S3: "( A ∈ ℂ ∧ B ∈ ℂ ) ⟶ ( A \<ca> B ) ∈ ℂ" by (rule MMI_axaddcl)
   from S1 S2 S3 show "( A \<ca> B ) ∈ ℂ" by (rule MMI_mp2an)
qed

lemma (in MMIsar0) MMI_mulcl: assumes A1: "A ∈ ℂ" and
    A2: "B ∈ ℂ"   
   shows "( A ⋅ B ) ∈ ℂ"
proof -
   from A1 have S1: "A ∈ ℂ".
   from A2 have S2: "B ∈ ℂ".
   have S3: "( A ∈ ℂ ∧ B ∈ ℂ ) ⟶ ( A ⋅ B ) ∈ ℂ" by (rule MMI_axmulcl)
   from S1 S2 S3 show "( A ⋅ B ) ∈ ℂ" by (rule MMI_mp2an)
qed

lemma (in MMIsar0) MMI_addcom: assumes A1: "A ∈ ℂ" and
    A2: "B ∈ ℂ"   
   shows "( A \<ca> B ) = ( B \<ca> A )"
proof -
   from A1 have S1: "A ∈ ℂ".
   from A2 have S2: "B ∈ ℂ".
   have S3: "( A ∈ ℂ ∧ B ∈ ℂ ) ⟶ ( A \<ca> B ) = ( B \<ca> A )" 
     by (rule MMI_axaddcom)
   from S1 S2 S3 show "( A \<ca> B ) = ( B \<ca> A )" by (rule MMI_mp2an)
qed

lemma (in MMIsar0) MMI_mulcom: assumes A1: "A ∈ ℂ" and
    A2: "B ∈ ℂ"   
   shows "( A ⋅ B ) = ( B ⋅ A )"
proof -
   from A1 have S1: "A ∈ ℂ".
   from A2 have S2: "B ∈ ℂ".
   have S3: "( A ∈ ℂ ∧ B ∈ ℂ ) ⟶ ( A ⋅ B ) = ( B ⋅ A )" 
     by (rule MMI_axmulcom)
   from S1 S2 S3 show "( A ⋅ B ) = ( B ⋅ A )" by (rule MMI_mp2an)
qed

lemma (in MMIsar0) MMI_addass: assumes A1: "A ∈ ℂ" and
    A2: "B ∈ ℂ" and
    A3: "C ∈ ℂ"   
   shows "( ( A \<ca> B ) \<ca> C ) = ( A \<ca> ( B \<ca> C ) )"
proof -
   from A1 have S1: "A ∈ ℂ".
   from A2 have S2: "B ∈ ℂ".
   from A3 have S3: "C ∈ ℂ".
   have S4: "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( ( A \<ca> B ) \<ca> C ) = 
     ( A \<ca> ( B \<ca> C ) )" by (rule MMI_axaddass)
   from S1 S2 S3 S4 show "( ( A \<ca> B ) \<ca> C ) = 
     ( A \<ca> ( B \<ca> C ) )" by (rule MMI_mp3an)
qed

lemma (in MMIsar0) MMI_mulass: assumes A1: "A ∈ ℂ" and
    A2: "B ∈ ℂ" and
    A3: "C ∈ ℂ"   
   shows "( ( A ⋅ B ) ⋅ C ) = ( A ⋅ ( B ⋅ C ) )"
proof -
   from A1 have S1: "A ∈ ℂ".
   from A2 have S2: "B ∈ ℂ".
   from A3 have S3: "C ∈ ℂ".
   have S4: "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( ( A ⋅ B ) ⋅ C ) = 
     ( A ⋅ ( B ⋅ C ) )" by (rule MMI_axmulass)
   from S1 S2 S3 S4 show "( ( A ⋅ B ) ⋅ C ) = ( A ⋅ ( B ⋅ C ) )" 
     by (rule MMI_mp3an)
qed

lemma (in MMIsar0) MMI_adddi: assumes A1: "A ∈ ℂ" and
    A2: "B ∈ ℂ" and
    A3: "C ∈ ℂ"   
   shows "( A ⋅ ( B \<ca> C ) ) = ( ( A ⋅ B ) \<ca> ( A ⋅ C ) )"
proof -
   from A1 have S1: "A ∈ ℂ".
   from A2 have S2: "B ∈ ℂ".
   from A3 have S3: "C ∈ ℂ".
   have S4: "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( A ⋅ ( B \<ca> C ) ) = 
     ( ( A ⋅ B ) \<ca> ( A ⋅ C ) )" by (rule MMI_axdistr)
   from S1 S2 S3 S4 show "( A ⋅ ( B \<ca> C ) ) = 
     ( ( A ⋅ B ) \<ca> ( A ⋅ C ) )" by (rule MMI_mp3an)
qed

lemma (in MMIsar0) MMI_adddir: assumes A1: "A ∈ ℂ" and
    A2: "B ∈ ℂ" and
    A3: "C ∈ ℂ"   
   shows "( ( A \<ca> B ) ⋅ C ) = ( ( A ⋅ C ) \<ca> ( B ⋅ C ) )"
proof -
   from A1 have S1: "A ∈ ℂ".
   from A2 have S2: "B ∈ ℂ".
   from A3 have S3: "C ∈ ℂ".
   have S4: "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( ( A \<ca> B ) ⋅ C ) = 
     ( ( A ⋅ C ) \<ca> ( B ⋅ C ) )" by (rule MMI_adddirt)
   from S1 S2 S3 S4 show "( ( A \<ca> B ) ⋅ C ) = 
     ( ( A ⋅ C ) \<ca> ( B ⋅ C ) )" by (rule MMI_mp3an)
qed

lemma (in MMIsar0) MMI_1cn: 
   shows "𝟭 ∈ ℂ"
proof -
   have S1: "𝟭 ∈ ℝ" by (rule MMI_ax1re)
   from S1 show "𝟭 ∈ ℂ" by (rule MMI_recn)
qed

lemma (in MMIsar0) MMI_0cn: 
   shows "𝟬 ∈ ℂ"
proof -
   have S1: "( ( 𝗂 ⋅ 𝗂 ) \<ca> 𝟭 ) = 𝟬" by (rule MMI_axi2m1)
   have S2: "𝗂 ∈ ℂ" by (rule MMI_axicn)
   have S3: "𝗂 ∈ ℂ" by (rule MMI_axicn)
   from S2 S3 have S4: "( 𝗂 ⋅ 𝗂 ) ∈ ℂ" by (rule MMI_mulcl)
   have S5: "𝟭 ∈ ℂ" by (rule MMI_1cn)
   from S4 S5 have S6: "( ( 𝗂 ⋅ 𝗂 ) \<ca> 𝟭 ) ∈ ℂ" by (rule MMI_addcl)
   from S1 S6 show "𝟬 ∈ ℂ" by (rule MMI_eqeltrr)
qed

lemma (in MMIsar0) MMI_addid1: assumes A1: "A ∈ ℂ"   
   shows "( A \<ca> 𝟬 ) = A"
proof -
   from A1 have S1: "A ∈ ℂ".
   have S2: "A ∈ ℂ ⟶ ( A \<ca> 𝟬 ) = A" by (rule MMI_ax0id)
   from S1 S2 show "( A \<ca> 𝟬 ) = A" by (rule MMI_ax_mp)
qed

lemma (in MMIsar0) MMI_addid2: assumes A1: "A ∈ ℂ"   
   shows "( 𝟬 \<ca> A ) = A"
proof -
   have S1: "𝟬 ∈ ℂ" by (rule MMI_0cn)
   from A1 have S2: "A ∈ ℂ".
   from S1 S2 have S3: "( 𝟬 \<ca> A ) = ( A \<ca> 𝟬 )" by (rule MMI_addcom)
   from A1 have S4: "A ∈ ℂ".
   from S4 have S5: "( A \<ca> 𝟬 ) = A" by (rule MMI_addid1)
   from S3 S5 show "( 𝟬 \<ca> A ) = A" by (rule MMI_eqtr)
qed

(*-----------------------------------------------------------------*)


lemma (in MMIsar0) MMI_mulid1: assumes A1: "A ∈ ℂ"   
   shows "( A ⋅ 𝟭 ) = A"
proof -
   from A1 have S1: "A ∈ ℂ".
   have S2: "A ∈ ℂ ⟶ ( A ⋅ 𝟭 ) = A" by (rule MMI_ax1id)
   from S1 S2 show "( A ⋅ 𝟭 ) = A" by (rule MMI_ax_mp)
qed

lemma (in MMIsar0) MMI_mulid2: assumes A1: "A ∈ ℂ"   
   shows "( 𝟭 ⋅ A ) = A"
proof -
   have S1: "𝟭 ∈ ℂ" by (rule MMI_1cn)
   from A1 have S2: "A ∈ ℂ".
   from S1 S2 have S3: "( 𝟭 ⋅ A ) = ( A ⋅ 𝟭 )" by (rule MMI_mulcom)
   from A1 have S4: "A ∈ ℂ".
   from S4 have S5: "( A ⋅ 𝟭 ) = A" by (rule MMI_mulid1)
   from S3 S5 show "( 𝟭 ⋅ A ) = A" by (rule MMI_eqtr)
qed

lemma (in MMIsar0) MMI_negex: assumes A1: "A ∈ ℂ"   
   shows "∃ x ∈ ℂ . ( A \<ca> x ) = 𝟬"
proof -
   from A1 have S1: "A ∈ ℂ".
   have S2: "A ∈ ℂ ⟶ ( ∃ x ∈ ℂ . ( A \<ca> x ) = 𝟬 )" by (rule MMI_axnegex)
   from S1 S2 show "∃ x ∈ ℂ . ( A \<ca> x ) = 𝟬" by (rule MMI_ax_mp)
qed

lemma (in MMIsar0) MMI_recex: assumes A1: "A ∈ ℂ" and
    A2: "A ≠ 𝟬"   
   shows "∃ x ∈ ℂ . ( A ⋅ x ) = 𝟭"
proof -
   from A1 have S1: "A ∈ ℂ".
   from A2 have S2: "A ≠ 𝟬".
   have S3: "( A ∈ ℂ ∧ A ≠ 𝟬 ) ⟶ ( ∃ x ∈ ℂ . ( A ⋅ x ) = 𝟭 )" 
     by (rule MMI_axrecex)
   from S1 S2 S3 show "∃ x ∈ ℂ . ( A ⋅ x ) = 𝟭" by (rule MMI_mp2an)
qed

lemma (in MMIsar0) MMI_readdcl: assumes A1: "A ∈ ℝ" and
    A2: "B ∈ ℝ"   
   shows "( A \<ca> B ) ∈ ℝ"
proof -
   from A1 have S1: "A ∈ ℝ".
   from A2 have S2: "B ∈ ℝ".
   have S3: "( A ∈ ℝ ∧ B ∈ ℝ ) ⟶ ( A \<ca> B ) ∈ ℝ" by (rule MMI_axaddrcl)
   from S1 S2 S3 show "( A \<ca> B ) ∈ ℝ" by (rule MMI_mp2an)
qed

lemma (in MMIsar0) MMI_remulcl: assumes A1: "A ∈ ℝ" and
    A2: "B ∈ ℝ"   
   shows "( A ⋅ B ) ∈ ℝ"
proof -
   from A1 have S1: "A ∈ ℝ".
   from A2 have S2: "B ∈ ℝ".
   have S3: "( A ∈ ℝ ∧ B ∈ ℝ ) ⟶ ( A ⋅ B ) ∈ ℝ" by (rule MMI_axmulrcl)
   from S1 S2 S3 show "( A ⋅ B ) ∈ ℝ" by (rule MMI_mp2an)
qed

lemma (in MMIsar0) MMI_addcan: assumes A1: "A ∈ ℂ" and
    A2: "B ∈ ℂ" and
    A3: "C ∈ ℂ"   
   shows "( A \<ca> B ) = ( A \<ca> C ) ⟷ B = C"
proof -
   from A1 have S1: "A ∈ ℂ".
   from S1 have S2: "∃ x ∈ ℂ . ( A \<ca> x ) = 𝟬" by (rule MMI_negex)
   from A1 have S3: "A ∈ ℂ".
   from A2 have S4: "B ∈ ℂ".
   { fix x
     have S5: "( x ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℂ ) ⟶ ( ( x \<ca> A ) \<ca> B ) = 
       ( x \<ca> ( A \<ca> B ) )" by (rule MMI_axaddass)
     from S4 S5 have S6: "( x ∈ ℂ ∧ A ∈ ℂ ) ⟶ ( ( x \<ca> A ) \<ca> B ) = 
       ( x \<ca> ( A \<ca> B ) )" by (rule MMI_mp3an3)
     from A3 have S7: "C ∈ ℂ".
     have S8: "( x ∈ ℂ ∧ A ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( ( x \<ca> A ) \<ca> C ) = 
       ( x \<ca> ( A \<ca> C ) )" by (rule MMI_axaddass)
     from S7 S8 have S9: "( x ∈ ℂ ∧ A ∈ ℂ ) ⟶ ( ( x \<ca> A ) \<ca> C ) = 
       ( x \<ca> ( A \<ca> C ) )" by (rule MMI_mp3an3)
     from S6 S9 have S10: "( x ∈ ℂ ∧ A ∈ ℂ ) ⟶ 
       ( ( ( x \<ca> A ) \<ca> B ) = ( ( x \<ca> A ) \<ca> C ) ⟷ 
       ( x \<ca> ( A \<ca> B ) ) = ( x \<ca> ( A \<ca> C ) ) )" 
       by (rule MMI_eqeq12d)
     from S3 S10 have S11: "x ∈ ℂ ⟶ ( ( ( x \<ca> A ) \<ca> B ) = 
       ( ( x \<ca> A ) \<ca> C ) ⟷ ( x \<ca> ( A \<ca> B ) ) = 
       ( x \<ca> ( A \<ca> C ) ) )" by (rule MMI_mpan2)
     have S12: "( A \<ca> B ) = ( A \<ca> C ) ⟶ ( x \<ca> ( A \<ca> B ) ) = 
       ( x \<ca> ( A \<ca> C ) )" by (rule MMI_opreq2)
     from S11 S12 have S13: "x ∈ ℂ ⟶ ( ( A \<ca> B ) = ( A \<ca> C ) ⟶ 
       ( ( x \<ca> A ) \<ca> B ) = ( ( x \<ca> A ) \<ca> C ) )" 
       by (rule MMI_syl5bir)
     from S13 have S14: "( x ∈ ℂ ∧ ( A \<ca> x ) = 𝟬 ) ⟶ ( ( A \<ca> B ) = 
       ( A \<ca> C ) ⟶ ( ( x \<ca> A ) \<ca> B ) = 
       ( ( x \<ca> A ) \<ca> C ) )" by (rule MMI_adantr)
     from A1 have S15: "A ∈ ℂ".
     have S16: "( A ∈ ℂ ∧ x ∈ ℂ ) ⟶ ( A \<ca> x ) = ( x \<ca> A )" 
       by (rule MMI_axaddcom)
     from S15 S16 have S17: "x ∈ ℂ ⟶ ( A \<ca> x ) = ( x \<ca> A )" 
       by (rule MMI_mpan)
     from S17 have S18: "x ∈ ℂ ⟶ ( ( A \<ca> x ) = 𝟬 ⟷ 
       ( x \<ca> A ) = 𝟬 )" by (rule MMI_eqeq1d)
     have S19: "( x \<ca> A ) = 𝟬 ⟶ ( ( x \<ca> A ) \<ca> B ) = 
       ( 𝟬 \<ca> B )" by (rule MMI_opreq1)
     from A2 have S20: "B ∈ ℂ".
     from S20 have S21: "( 𝟬 \<ca> B ) = B" by (rule MMI_addid2)
     from S19 S21 have S22: "( x \<ca> A ) = 𝟬 ⟶ 
       ( ( x \<ca> A ) \<ca> B ) = B" by (rule MMI_syl6eq)
     have S23: "( x \<ca> A ) = 𝟬 ⟶ ( ( x \<ca> A ) \<ca> C ) = 
       ( 𝟬 \<ca> C )" by (rule MMI_opreq1)
     from A3 have S24: "C ∈ ℂ".
     from S24 have S25: "( 𝟬 \<ca> C ) = C" by (rule MMI_addid2)
     from S23 S25 have S26: "( x \<ca> A ) = 𝟬 ⟶ 
       ( ( x \<ca> A ) \<ca> C ) = C" by (rule MMI_syl6eq)
     from S22 S26 have S27: "( x \<ca> A ) = 𝟬 ⟶ 
       ( ( ( x \<ca> A ) \<ca> B ) = ( ( x \<ca> A ) \<ca> C ) ⟷ B = C )" 
       by (rule MMI_eqeq12d)
     from S18 S27 have S28: "x ∈ ℂ ⟶ ( ( A \<ca> x ) = 𝟬 ⟶ 
       ( ( ( x \<ca> A ) \<ca> B ) = ( ( x \<ca> A ) \<ca> C ) ⟷ B = C ) )" 
       by (rule MMI_syl6bi)
     from S28 have S29: "( x ∈ ℂ ∧ ( A \<ca> x ) = 𝟬 ) ⟶ 
       ( ( ( x \<ca> A ) \<ca> B ) = ( ( x \<ca> A ) \<ca> C ) ⟷ B = C )" 
       by (rule MMI_imp)
     from S14 S29 have S30: "( x ∈ ℂ ∧ ( A \<ca> x ) = 𝟬 ) ⟶ 
       ( ( A \<ca> B ) = ( A \<ca> C ) ⟶ B = C )" by (rule MMI_sylibd)
     from S30 have "x ∈ ℂ ⟶ ( ( A \<ca> x ) = 𝟬 ⟶ 
       ( ( A \<ca> B ) = ( A \<ca> C ) ⟶ B = C ) )" by (rule MMI_ex)
   } then have S31: "∀ x. (x ∈ ℂ ⟶ ( ( A \<ca> x ) = 𝟬 ⟶ 
       ( ( A \<ca> B ) = ( A \<ca> C ) ⟶ B = C ) ))" by auto
   from S31 have S32: "( ∃ x ∈ ℂ . ( A \<ca> x ) = 𝟬 ) ⟶ 
     ( ( A \<ca> B ) = ( A \<ca> C ) ⟶ B = C )" by (rule MMI_r19_23aiv)
   from S2 S32 have S33: "( A \<ca> B ) = ( A \<ca> C ) ⟶ B = C" 
     by (rule MMI_ax_mp)
   have S34: "B = C ⟶ ( A \<ca> B ) = ( A \<ca> C )" by (rule MMI_opreq2)
   from S33 S34 show "( A \<ca> B ) = ( A \<ca> C ) ⟷ B = C" 
     by (rule MMI_impbi)
qed

lemma (in MMIsar0) MMI_addcan2: assumes A1: "A ∈ ℂ" and
    A2: "B ∈ ℂ" and
    A3: "C ∈ ℂ"   
   shows "( A \<ca> C ) = ( B \<ca> C ) ⟷ A = B"
proof -
   from A1 have S1: "A ∈ ℂ".
   from A3 have S2: "C ∈ ℂ".
   from S1 S2 have S3: "( A \<ca> C ) = ( C \<ca> A )" by (rule MMI_addcom)
   from A2 have S4: "B ∈ ℂ".
   from A3 have S5: "C ∈ ℂ".
   from S4 S5 have S6: "( B \<ca> C ) = ( C \<ca> B )" by (rule MMI_addcom)
   from S3 S6 have S7: "( A \<ca> C ) = ( B \<ca> C ) ⟷ 
     ( C \<ca> A ) = ( C \<ca> B )" by (rule MMI_eqeq12i)
   from A3 have S8: "C ∈ ℂ".
   from A1 have S9: "A ∈ ℂ".
   from A2 have S10: "B ∈ ℂ".
   from S8 S9 S10 have S11: "( C \<ca> A ) = ( C \<ca> B ) ⟷ A = B" 
     by (rule MMI_addcan)
   from S7 S11 show "( A \<ca> C ) = ( B \<ca> C ) ⟷ A = B" by (rule MMI_bitr)
qed

lemma (in MMIsar0) MMI_addcant: 
   shows "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ 
  ( ( A \<ca> B ) = ( A \<ca> C ) ⟷ B = C )"
proof -
   have S1: "A = if ( A ∈ ℂ , A , 𝟬 ) ⟶ ( A \<ca> B ) = ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> B )" by (rule MMI_opreq1)
   have S2: "A = if ( A ∈ ℂ , A , 𝟬 ) ⟶ 
     ( A \<ca> C ) = ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> C )" by (rule MMI_opreq1)
   from S1 S2 have S3: "A = if ( A ∈ ℂ , A , 𝟬 ) ⟶ 
     ( ( A \<ca> B ) = ( A \<ca> C ) ⟷ 
     ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> B ) = ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> C ) )" 
     by (rule MMI_eqeq12d)
   from S3 have S4: "A = if ( A ∈ ℂ , A , 𝟬 ) ⟶ 
     ( ( ( A \<ca> B ) = ( A \<ca> C ) ⟷ B = C ) ⟷ 
     ( ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> B ) = ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> C ) 
     ⟷ B = C ) )" by (rule MMI_bibi1d)
   have S5: "B = if ( B ∈ ℂ , B , 𝟬 ) ⟶ 
     ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> B ) = 
     ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> if ( B ∈ ℂ , B , 𝟬 ) )" by (rule MMI_opreq2)
   from S5 have S6: "B = if ( B ∈ ℂ , B , 𝟬 ) ⟶ 
     ( ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> B ) = ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> C ) 
     ⟷ ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> if ( B ∈ ℂ , B , 𝟬 ) ) = 
     ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> C ) )" by (rule MMI_eqeq1d)
   have S7: "B = if ( B ∈ ℂ , B , 𝟬 ) ⟶ ( B = C ⟷ 
     if ( B ∈ ℂ , B , 𝟬 ) = C )" by (rule MMI_eqeq1)
   from S6 S7 have S8: "B = if ( B ∈ ℂ , B , 𝟬 ) ⟶ 
     ( ( ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> B ) = 
     ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> C ) ⟷ B = C ) ⟷ 
     ( ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> if ( B ∈ ℂ , B , 𝟬 ) ) = 
     ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> C ) ⟷ if ( B ∈ ℂ , B , 𝟬 ) = C ) )" 
     by (rule MMI_bibi12d)
   have S9: "C = if ( C ∈ ℂ , C , 𝟬 ) ⟶ ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> C ) = 
     ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> if ( C ∈ ℂ , C , 𝟬 ) )" 
     by (rule MMI_opreq2)
   from S9 have S10: "C = if ( C ∈ ℂ , C , 𝟬 ) ⟶ 
     ( ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> if ( B ∈ ℂ , B , 𝟬 ) ) = 
     ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> C ) ⟷ 
     ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> if ( B ∈ ℂ , B , 𝟬 ) ) = 
     ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> if ( C ∈ ℂ , C , 𝟬 ) ) )" 
     by (rule MMI_eqeq2d)
   have S11: "C = if ( C ∈ ℂ , C , 𝟬 ) ⟶ ( if ( B ∈ ℂ , B , 𝟬 ) = C ⟷ 
     if ( B ∈ ℂ , B , 𝟬 ) = if ( C ∈ ℂ , C , 𝟬 ) )" by (rule MMI_eqeq2)
   from S10 S11 have S12: "C = if ( C ∈ ℂ , C , 𝟬 ) ⟶ 
     ( ( ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> if ( B ∈ ℂ , B , 𝟬 ) ) = 
     ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> C ) ⟷ if ( B ∈ ℂ , B , 𝟬 ) = C ) ⟷ 
     ( ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> if ( B ∈ ℂ , B , 𝟬 ) ) = 
     ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> if ( C ∈ ℂ , C , 𝟬 ) ) ⟷ 
     if ( B ∈ ℂ , B , 𝟬 ) = if ( C ∈ ℂ , C , 𝟬 ) ) )" by (rule MMI_bibi12d)
   have S13: "𝟬 ∈ ℂ" by (rule MMI_0cn)
   from S13 have S14: "if ( A ∈ ℂ , A , 𝟬 ) ∈ ℂ" by (rule MMI_elimel)
   have S15: "𝟬 ∈ ℂ" by (rule MMI_0cn)
   from S15 have S16: "if ( B ∈ ℂ , B , 𝟬 ) ∈ ℂ" by (rule MMI_elimel)
   have S17: "𝟬 ∈ ℂ" by (rule MMI_0cn)
   from S17 have S18: "if ( C ∈ ℂ , C , 𝟬 ) ∈ ℂ" by (rule MMI_elimel)
   from S14 S16 S18 have S19: 
     "( if ( A ∈ ℂ , A , 𝟬 ) \<ca> if ( B ∈ ℂ , B , 𝟬 ) ) = 
     ( if ( A ∈ ℂ , A , 𝟬 ) \<ca> if ( C ∈ ℂ , C , 𝟬 ) ) ⟷ 
     if ( B ∈ ℂ , B , 𝟬 ) = if ( C ∈ ℂ , C , 𝟬 )" by (rule MMI_addcan)
   from S4 S8 S12 S19 show "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ 
     ( ( A \<ca> B ) = ( A \<ca> C ) ⟷ B = C )" by (rule MMI_dedth3h)
qed

lemma (in MMIsar0) MMI_addcan2t: 
   shows "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( ( A \<ca> C ) = ( B \<ca> C ) ⟷ 
  A = B )"
proof -
   have S1: "( C ∈ ℂ ∧ A ∈ ℂ ) ⟶ ( C \<ca> A ) = ( A \<ca> C )" 
     by (rule MMI_axaddcom)
   from S1 have S2: "( C ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℂ ) ⟶ ( C \<ca> A ) = 
     ( A \<ca> C )" by (rule MMI_3adant3)
   have S3: "( C ∈ ℂ ∧ B ∈ ℂ ) ⟶ ( C \<ca> B ) = ( B \<ca> C )" 
     by (rule MMI_axaddcom)
   from S3 have S4: "( C ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℂ ) ⟶ ( C \<ca> B ) = 
     ( B \<ca> C )" by (rule MMI_3adant2)
   from S2 S4 have S5: "( C ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℂ ) ⟶ 
     ( ( C \<ca> A ) = ( C \<ca> B ) ⟷ ( A \<ca> C ) = ( B \<ca> C ) )" 
     by (rule MMI_eqeq12d)
   have S6: "( C ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℂ ) ⟶ ( ( C \<ca> A ) = 
     ( C \<ca> B ) ⟷ A = B )" by (rule MMI_addcant)
   from S5 S6 have S7: "( C ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℂ ) ⟶ ( ( A \<ca> C ) = 
     ( B \<ca> C ) ⟷ A = B )" by (rule MMI_bitr3d)
   from S7 show "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( ( A \<ca> C ) = 
     ( B \<ca> C ) ⟷ A = B )" by (rule MMI_3coml)
qed

(************************ 20-30********************************)

lemma (in MMIsar0) MMI_add12t: 
   shows "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( A \<ca> ( B \<ca> C ) ) = 
  ( B \<ca> ( A \<ca> C ) )"
proof -
   have S1: "( A ∈ ℂ ∧ B ∈ ℂ ) ⟶ ( A \<ca> B ) = ( B \<ca> A )" 
     by (rule MMI_axaddcom)
   from S1 have S2: "( A ∈ ℂ ∧ B ∈ ℂ ) ⟶ ( ( A \<ca> B ) \<ca> C ) = 
     ( ( B \<ca> A ) \<ca> C )" by (rule MMI_opreq1d)
   from S2 have S3: "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ 
     ( ( A \<ca> B ) \<ca> C ) = ( ( B \<ca> A ) \<ca> C )" 
     by (rule MMI_3adant3)
   have S4: "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( ( A \<ca> B ) \<ca> C ) = 
     ( A \<ca> ( B \<ca> C ) )" by (rule MMI_axaddass)
   have S5: "( B ∈ ℂ ∧ A ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( ( B \<ca> A ) \<ca> C ) = 
     ( B \<ca> ( A \<ca> C ) )" by (rule MMI_axaddass)
   from S5 have S6: "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ 
     ( ( B \<ca> A ) \<ca> C ) = ( B \<ca> ( A \<ca> C ) )" by (rule MMI_3com12)
   from S3 S4 S6 show "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ 
     ( A \<ca> ( B \<ca> C ) ) = ( B \<ca> ( A \<ca> C ) )" 
     by (rule MMI_3eqtr3d)
qed

lemma (in MMIsar0) MMI_add23t: 
   shows "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( ( A \<ca> B ) \<ca> C ) = 
  ( ( A \<ca> C ) \<ca> B )"
proof -
   have S1: "( B ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( B \<ca> C ) = ( C \<ca> B )" 
     by (rule MMI_axaddcom)
   from S1 have S2: "( B ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( A \<ca> ( B \<ca> C ) ) = 
     ( A \<ca> ( C \<ca> B ) )" by (rule MMI_opreq2d)
   from S2 have S3: "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ 
     ( A \<ca> ( B \<ca> C ) ) = ( A \<ca> ( C \<ca> B ) )" 
     by (rule MMI_3adant1)
   have S4: "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( ( A \<ca> B ) \<ca> C ) = 
     ( A \<ca> ( B \<ca> C ) )" by (rule MMI_axaddass)
   have S5: "( A ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ ) ⟶ ( ( A \<ca> C ) \<ca> B ) = 
     ( A \<ca> ( C \<ca> B ) )" by (rule MMI_axaddass)
   from S5 have S6: "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ 
     ( ( A \<ca> C ) \<ca> B ) = ( A \<ca> ( C \<ca> B ) )" by (rule MMI_3com23)
   from S3 S4 S6 show "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ 
     ( ( A \<ca> B ) \<ca> C ) = ( ( A \<ca> C ) \<ca> B )" 
     by (rule MMI_3eqtr4d)
qed

lemma (in MMIsar0) MMI_add4t: 
   shows "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
  ( ( A \<ca> B ) \<ca> ( C \<ca> D ) ) = ( ( A \<ca> C ) \<ca> ( B \<ca> D ) )"
proof -
   have S1: "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ 
     ( ( A \<ca> B ) \<ca> C ) = ( ( A \<ca> C ) \<ca> B )" by (rule MMI_add23t)
   from S1 have S2: "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ 
     ( ( ( A \<ca> B ) \<ca> C ) \<ca> D ) = 
     ( ( ( A \<ca> C ) \<ca> B ) \<ca> D )" by (rule MMI_opreq1d)
   from S2 have S3: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ C ∈ ℂ ) ⟶ 
     ( ( ( A \<ca> B ) \<ca> C ) \<ca> D ) = 
     ( ( ( A \<ca> C ) \<ca> B ) \<ca> D )" by (rule MMI_3expa)
   from S3 have S4: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
     ( ( ( A \<ca> B ) \<ca> C ) \<ca> D ) = 
     ( ( ( A \<ca> C ) \<ca> B ) \<ca> D )" by (rule MMI_adantrr)
   have S5: "( ( A \<ca> B ) ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ) ⟶ 
     ( ( ( A \<ca> B ) \<ca> C ) \<ca> D ) = 
     ( ( A \<ca> B ) \<ca> ( C \<ca> D ) )" by (rule MMI_axaddass)
   from S5 have S6: "( ( A \<ca> B ) ∈ ℂ ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
     ( ( ( A \<ca> B ) \<ca> C ) \<ca> D ) = 
     ( ( A \<ca> B ) \<ca> ( C \<ca> D ) )" by (rule MMI_3expb)
   have S7: "( A ∈ ℂ ∧ B ∈ ℂ ) ⟶ ( A \<ca> B ) ∈ ℂ" by (rule MMI_axaddcl)
   from S6 S7 have S8: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
     ( ( ( A \<ca> B ) \<ca> C ) \<ca> D ) = 
     ( ( A \<ca> B ) \<ca> ( C \<ca> D ) )" by (rule MMI_sylan)
   have S9: "( ( A \<ca> C ) ∈ ℂ ∧ B ∈ ℂ ∧ D ∈ ℂ ) ⟶ 
     ( ( ( A \<ca> C ) \<ca> B ) \<ca> D ) = 
     ( ( A \<ca> C ) \<ca> ( B \<ca> D ) )" by (rule MMI_axaddass)
   from S9 have S10: "( ( A \<ca> C ) ∈ ℂ ∧ ( B ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
     ( ( ( A \<ca> C ) \<ca> B ) \<ca> D ) = 
     ( ( A \<ca> C ) \<ca> ( B \<ca> D ) )" by (rule MMI_3expb)
   have S11: "( A ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( A \<ca> C ) ∈ ℂ" by (rule MMI_axaddcl)
   from S10 S11 have S12: "( ( A ∈ ℂ ∧ C ∈ ℂ ) ∧ ( B ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
     ( ( ( A \<ca> C ) \<ca> B ) \<ca> D ) = 
     ( ( A \<ca> C ) \<ca> ( B \<ca> D ) )" by (rule MMI_sylan)
   from S12 have S13: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
     ( ( ( A \<ca> C ) \<ca> B ) \<ca> D ) = 
     ( ( A \<ca> C ) \<ca> ( B \<ca> D ) )" by (rule MMI_an4s)
   from S4 S8 S13 show "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
     ( ( A \<ca> B ) \<ca> ( C \<ca> D ) ) = 
     ( ( A \<ca> C ) \<ca> ( B \<ca> D ) )" by (rule MMI_3eqtr3d)
qed

lemma (in MMIsar0) MMI_add42t: 
   shows "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
  ( ( A \<ca> B ) \<ca> ( C \<ca> D ) ) = ( ( A \<ca> C ) \<ca> ( D \<ca> B ) )"
proof -
   have S1: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
     ( ( A \<ca> B ) \<ca> ( C \<ca> D ) ) = 
     ( ( A \<ca> C ) \<ca> ( B \<ca> D ) )" by (rule MMI_add4t)
   have S2: "( B ∈ ℂ ∧ D ∈ ℂ ) ⟶ ( B \<ca> D ) = 
     ( D \<ca> B )" by (rule MMI_axaddcom)
   from S2 have S3: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
     ( B \<ca> D ) = ( D \<ca> B )" by (rule MMI_ad2ant2l)
   from S3 have S4: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
     ( ( A \<ca> C ) \<ca> ( B \<ca> D ) ) = 
     ( ( A \<ca> C ) \<ca> ( D \<ca> B ) )" by (rule MMI_opreq2d)
   from S1 S4 show "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
     ( ( A \<ca> B ) \<ca> ( C \<ca> D ) ) = 
     ( ( A \<ca> C ) \<ca> ( D \<ca> B ) )" by (rule MMI_eqtrd)
qed

lemma (in MMIsar0) MMI_add12: assumes A1: "A ∈ ℂ" and
    A2: "B ∈ ℂ" and
    A3: "C ∈ ℂ"   
   shows "( A \<ca> ( B \<ca> C ) ) = ( B \<ca> ( A \<ca> C ) )"
proof -
   from A1 have S1: "A ∈ ℂ".
   from A2 have S2: "B ∈ ℂ".
   from A3 have S3: "C ∈ ℂ".
   have S4: "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( A \<ca> ( B \<ca> C ) ) = 
     ( B \<ca> ( A \<ca> C ) )" by (rule MMI_add12t)
   from S1 S2 S3 S4 show "( A \<ca> ( B \<ca> C ) ) = 
     ( B \<ca> ( A \<ca> C ) )" by (rule MMI_mp3an)
qed

lemma (in MMIsar0) MMI_add23: assumes A1: "A ∈ ℂ" and
    A2: "B ∈ ℂ" and
    A3: "C ∈ ℂ"   
   shows "( ( A \<ca> B ) \<ca> C ) = ( ( A \<ca> C ) \<ca> B )"
proof -
   from A1 have S1: "A ∈ ℂ".
   from A2 have S2: "B ∈ ℂ".
   from A3 have S3: "C ∈ ℂ".
   have S4: "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ 
     ( ( A \<ca> B ) \<ca> C ) = ( ( A \<ca> C ) \<ca> B )" by (rule MMI_add23t)
   from S1 S2 S3 S4 show "( ( A \<ca> B ) \<ca> C ) = 
     ( ( A \<ca> C ) \<ca> B )" by (rule MMI_mp3an)
qed

lemma (in MMIsar0) MMI_add4: assumes A1: "A ∈ ℂ" and
    A2: "B ∈ ℂ" and
    A3: "C ∈ ℂ" and
    A4: "D ∈ ℂ"   
   shows "( ( A \<ca> B ) \<ca> ( C \<ca> D ) ) = 
  ( ( A \<ca> C ) \<ca> ( B \<ca> D ) )"
proof -
   from A1 have S1: "A ∈ ℂ".
   from A2 have S2: "B ∈ ℂ".
   from S1 S2 have S3: "A ∈ ℂ ∧ B ∈ ℂ" by (rule MMI_pm3_2i)
   from A3 have S4: "C ∈ ℂ".
   from A4 have S5: "D ∈ ℂ".
   from S4 S5 have S6: "C ∈ ℂ ∧ D ∈ ℂ" by (rule MMI_pm3_2i)
   have S7: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
     ( ( A \<ca> B ) \<ca> ( C \<ca> D ) ) = 
     ( ( A \<ca> C ) \<ca> ( B \<ca> D ) )" by (rule MMI_add4t)
   from S3 S6 S7 show "( ( A \<ca> B ) \<ca> ( C \<ca> D ) ) = 
     ( ( A \<ca> C ) \<ca> ( B \<ca> D ) )" by (rule MMI_mp2an)
qed

lemma (in MMIsar0) MMI_add42: assumes A1: "A ∈ ℂ" and
    A2: "B ∈ ℂ" and
    A3: "C ∈ ℂ" and
    A4: "D ∈ ℂ"   
   shows "( ( A \<ca> B ) \<ca> ( C \<ca> D ) ) = 
  ( ( A \<ca> C ) \<ca> ( D \<ca> B ) )"
proof -
   from A1 have S1: "A ∈ ℂ".
   from A2 have S2: "B ∈ ℂ".
   from A3 have S3: "C ∈ ℂ".
   from A4 have S4: "D ∈ ℂ".
   from S1 S2 S3 S4 have S5: "( ( A \<ca> B ) \<ca> ( C \<ca> D ) ) = 
     ( ( A \<ca> C ) \<ca> ( B \<ca> D ) )" by (rule MMI_add4)
   from A2 have S6: "B ∈ ℂ".
   from A4 have S7: "D ∈ ℂ".
   from S6 S7 have S8: "( B \<ca> D ) = ( D \<ca> B )" by (rule MMI_addcom)
   from S8 have S9: "( ( A \<ca> C ) \<ca> ( B \<ca> D ) ) = 
     ( ( A \<ca> C ) \<ca> ( D \<ca> B ) )" by (rule MMI_opreq2i)
   from S5 S9 show "( ( A \<ca> B ) \<ca> ( C \<ca> D ) ) = 
     ( ( A \<ca> C ) \<ca> ( D \<ca> B ) )" by (rule MMI_eqtr)
qed

lemma (in MMIsar0) MMI_addid2t: 
   shows "A ∈ ℂ ⟶ ( 𝟬 \<ca> A ) = A"
proof -
   have S1: "𝟬 ∈ ℂ" by (rule MMI_0cn)
   have S2: "( 𝟬 ∈ ℂ ∧ A ∈ ℂ ) ⟶ ( 𝟬 \<ca> A ) = ( A \<ca> 𝟬 )" 
     by (rule MMI_axaddcom)
   from S1 S2 have S3: "A ∈ ℂ ⟶ ( 𝟬 \<ca> A ) = ( A \<ca> 𝟬 )" 
     by (rule MMI_mpan)
   have S4: "A ∈ ℂ ⟶ ( A \<ca> 𝟬 ) = A" by (rule MMI_ax0id)
   from S3 S4 show "A ∈ ℂ ⟶ ( 𝟬 \<ca> A ) = A" by (rule MMI_eqtrd)
qed

lemma (in MMIsar0) MMI_peano2cn: 
   shows "A ∈ ℂ ⟶ ( A \<ca> 𝟭 ) ∈ ℂ"
proof -
   have S1: "𝟭 ∈ ℂ" by (rule MMI_1cn)
   have S2: "( A ∈ ℂ ∧ 𝟭 ∈ ℂ ) ⟶ ( A \<ca> 𝟭 ) ∈ ℂ" by (rule MMI_axaddcl)
   from S1 S2 show "A ∈ ℂ ⟶ ( A \<ca> 𝟭 ) ∈ ℂ" by (rule MMI_mpan2)
qed

(*** 31-34 ********************************************************)

lemma (in MMIsar0) MMI_peano2re: 
   shows "A ∈ ℝ ⟶ ( A \<ca> 𝟭 ) ∈ ℝ"
proof -
   have S1: "𝟭 ∈ ℝ" by (rule MMI_ax1re)
   have S2: "( A ∈ ℝ ∧ 𝟭 ∈ ℝ ) ⟶ ( A \<ca> 𝟭 ) ∈ ℝ" by (rule MMI_axaddrcl)
   from S1 S2 show "A ∈ ℝ ⟶ ( A \<ca> 𝟭 ) ∈ ℝ" by (rule MMI_mpan2)
qed

lemma (in MMIsar0) MMI_negeu: assumes A1: "A ∈ ℂ" and
    A2: "B ∈ ℂ"   
   shows "∃! x . x ∈ ℂ ∧ ( A \<ca> x ) = B"
proof -
   { fix x y
     have S1: "x = y ⟶ ( A \<ca> x ) = ( A \<ca> y )" by (rule MMI_opreq2)
     from S1 have "x = y ⟶ ( ( A \<ca> x ) = B ⟷ ( A \<ca> y ) = B )" 
       by (rule MMI_eqeq1d)
   } then have S2: "∀x y. x = y ⟶ ( ( A \<ca> x ) = B ⟷ 
       ( A \<ca> y ) = B )" by simp
   from S2 have S3: "( ∃! x . x ∈ ℂ ∧ ( A \<ca> x ) = B ) ⟷ 
     ( ( ∃ x ∈ ℂ . ( A \<ca> x ) = B ) ∧ 
     ( ∀ x ∈ ℂ . ∀ y ∈ ℂ . ( ( ( A \<ca> x ) = B ∧ ( A \<ca> y ) = B ) ⟶ 
     x = y ) ) )" by (rule MMI_reu4)
   from A1 have S4: "A ∈ ℂ".
   from S4 have S5: "∃ y ∈ ℂ . ( A \<ca> y ) = 𝟬" by (rule MMI_negex)
   from A2 have S6: "B ∈ ℂ".
   { fix y
     have S7: "( y ∈ ℂ ∧ B ∈ ℂ ) ⟶ ( y \<ca> B ) ∈ ℂ" by (rule MMI_axaddcl)
     from S6 S7 have S8: "y ∈ ℂ ⟶ ( y \<ca> B ) ∈ ℂ" by (rule MMI_mpan2)
     have S9: "( y \<ca> B ) ∈ ℂ ⟷ ( ∃ x ∈ ℂ . x = ( y \<ca> B ) )" 
       by (rule MMI_risset)
     from S8 S9 have S10: "y ∈ ℂ ⟶ ( ∃ x ∈ ℂ . x = ( y \<ca> B ) )" 
       by (rule MMI_sylib)
     { fix x
       have S11: "x = ( y \<ca> B ) ⟶ ( A \<ca> x ) = 
	 ( A \<ca> ( y \<ca> B ) )" by (rule MMI_opreq2)
       from A1 have S12: "A ∈ ℂ".
       from A2 have S13: "B ∈ ℂ".
       have S14: "( A ∈ ℂ ∧ y ∈ ℂ ∧ B ∈ ℂ ) ⟶ 
	 ( ( A \<ca> y ) \<ca> B ) = ( A \<ca> ( y \<ca> B ) )" 
	 by (rule MMI_axaddass)
       from S12 S13 S14 have S15: "y ∈ ℂ ⟶ ( ( A \<ca> y ) \<ca> B ) = 
	 ( A \<ca> ( y \<ca> B ) )" by (rule MMI_mp3an13)
       from S15 have S16: "y ∈ ℂ ⟶ ( A \<ca> ( y \<ca> B ) ) = 
	 ( ( A \<ca> y ) \<ca> B )" by (rule MMI_eqcomd)
       from S11 S16 have S17: "( y ∈ ℂ ∧ x = ( y \<ca> B ) ) 
	 ⟶ ( A \<ca> x ) = ( ( A \<ca> y ) \<ca> B )" by (rule MMI_sylan9eqr)
       have S18: "( A \<ca> y ) = 𝟬 ⟶ 
	 ( ( A \<ca> y ) \<ca> B ) = ( 𝟬 \<ca> B )" by (rule MMI_opreq1)
       from A2 have S19: "B ∈ ℂ".
       from S19 have S20: "( 𝟬 \<ca> B ) = B" by (rule MMI_addid2)
       from S18 S20 have S21: "( A \<ca> y ) = 𝟬 ⟶ 
	 ( ( A \<ca> y ) \<ca> B ) = B" by (rule MMI_syl6eq)
       from S17 S21 have S22: "( ( A \<ca> y ) = 𝟬 ∧ ( y ∈ ℂ ∧ x = 
	 ( y \<ca> B ) ) ) ⟶ ( A \<ca> x ) = B" by (rule MMI_sylan9eqr)
       from S22 have S23: "( A \<ca> y ) = 𝟬 ⟶ 
	 ( y ∈ ℂ ⟶ ( x = ( y \<ca> B ) ⟶ ( A \<ca> x ) = B ) )" 
	 by (rule MMI_exp32)
       from S23 have S24: "( y ∈ ℂ ∧ ( A \<ca> y ) = 𝟬 ) ⟶ 
	 ( x = ( y \<ca> B ) ⟶ ( A \<ca> x ) = B )" by (rule MMI_impcom)
       from S24 have "( y ∈ ℂ ∧ ( A \<ca> y ) = 𝟬 ) ⟶ 
	 ( x ∈ ℂ ⟶ ( x = ( y \<ca> B ) ⟶ ( A \<ca> x ) = B ) )" 
	 by (rule MMI_a1d)
     } then have S25: "∀ x. ( y ∈ ℂ ∧ ( A \<ca> y ) = 𝟬 ) ⟶ 
	 ( x ∈ ℂ ⟶ ( x = ( y \<ca> B ) ⟶ ( A \<ca> x ) = B ) )" by auto
     from S25 have S26: "( y ∈ ℂ ∧ ( A \<ca> y ) = 𝟬 ) ⟶ 
       ( ∀ x ∈ ℂ . ( x = ( y \<ca> B ) ⟶ ( A \<ca> x ) = B ) )" 
       by (rule MMI_r19_21aiv)
     from S26 have S27: "y ∈ ℂ ⟶ ( ( A \<ca> y ) = 𝟬 ⟶ 
       ( ∀ x ∈ ℂ . ( x = ( y \<ca> B ) ⟶ ( A \<ca> x ) = B ) ) )" 
       by (rule MMI_ex)
     have S28: "( ∀ x ∈ ℂ . ( x = ( y \<ca> B ) ⟶ ( A \<ca> x ) = B ) ) 
       ⟶ ( ( ∃ x ∈ ℂ . x = ( y \<ca> B ) ) ⟶ 
       ( ∃ x ∈ ℂ . ( A \<ca> x ) = B ) )" by (rule MMI_r19_22)
     from S27 S28 have S29: "y ∈ ℂ ⟶ ( ( A \<ca> y ) = 𝟬 ⟶ 
       ( ( ∃ x ∈ ℂ . x = ( y \<ca> B ) ) ⟶ 
       ( ∃ x ∈ ℂ . ( A \<ca> x ) = B ) ) )" by (rule MMI_syl6)
     from S10 S29 have "y ∈ ℂ ⟶ ( ( A \<ca> y ) = 𝟬 ⟶ 
       ( ∃ x ∈ ℂ . ( A \<ca> x ) = B ) )" by (rule MMI_mpid)
   } then have S30: "∀ y. y ∈ ℂ ⟶ ( ( A \<ca> y ) = 𝟬 ⟶ 
       ( ∃ x ∈ ℂ . ( A \<ca> x ) = B ) )" by simp
   from S30 have S31: "( ∃ y ∈ ℂ . ( A \<ca> y ) = 𝟬 ) ⟶ 
     ( ∃ x ∈ ℂ . ( A \<ca> x ) = B )" by (rule MMI_r19_23aiv)
   from S5 S31 have S32: "∃ x ∈ ℂ . ( A \<ca> x ) = B" by (rule MMI_ax_mp)
   from A1 have S33: "A ∈ ℂ".
   { fix x y
     have S34: "( A ∈ ℂ ∧ x ∈ ℂ ∧ y ∈ ℂ ) ⟶ 
       ( ( A \<ca> x ) = ( A \<ca> y ) ⟷ x = y )" by (rule MMI_addcant)
     have S35: "( ( A \<ca> x ) = B ∧ ( A \<ca> y ) = B ) ⟶ 
       ( A \<ca> x ) = ( A \<ca> y )" by (rule MMI_eqtr3t)
     from S34 S35 have S36: "( A ∈ ℂ ∧ x ∈ ℂ ∧ y ∈ ℂ ) ⟶ 
       ( ( ( A \<ca> x ) = B ∧ ( A \<ca> y ) = B ) ⟶ x = y )" 
       by (rule MMI_syl5bi)
     from S33 S36 have "( x ∈ ℂ ∧ y ∈ ℂ ) ⟶ 
       ( ( ( A \<ca> x ) = B ∧ ( A \<ca> y ) = B ) ⟶ x = y )" 
       by (rule MMI_mp3an1)
   } then have S37: "∀x y . ( x ∈ ℂ ∧ y ∈ ℂ ) ⟶ 
       ( ( ( A \<ca> x ) = B ∧ ( A \<ca> y ) = B ) ⟶ x = y )" by auto
   from S37 have S38: "∀ x ∈ ℂ . ∀ y ∈ ℂ . ( ( ( A \<ca> x ) = B ∧ 
     ( A \<ca> y ) = B ) ⟶ x = y )" by (rule MMI_rgen2)
   from S3 S32 S38 show "∃! x . x ∈ ℂ ∧ ( A \<ca> x ) = B" 
     by (rule MMI_mpbir2an)
qed

(** this is proven by definition rather than importing the Metamath proof **)

lemma (in MMIsar0) MMI_subval: assumes "A ∈ ℂ"  "B ∈ ℂ"
  shows "A \<cs> B =  ⋃ { x ∈ ℂ . B \<ca> x = A }"
  using sub_def by simp

(** this is a definition in Metamath *)

lemma (in MMIsar0) MMI_df_neg: shows "(\<cn> A) = 𝟬 \<cs> A"
  using cneg_def by simp

(************** 35-37 ****************************************)
 
lemma (in MMIsar0) MMI_negeq: 
   shows "A = B ⟶ (\<cn>A) = (\<cn> B)"
proof -
   have S1: "A = B ⟶ ( 𝟬 \<cs> A ) = ( 𝟬 \<cs> B )" by (rule MMI_opreq2)
   have S2: "(\<cn>A) = ( 𝟬 \<cs> A )" by (rule MMI_df_neg)
   have S3: "(\<cn>B) = ( 𝟬 \<cs> B )" by (rule MMI_df_neg)
   from S1 S2 S3 show "A = B ⟶ (\<cn>A) = (\<cn>B)" by (rule MMI_3eqtr4g)
qed

lemma (in MMIsar0) MMI_negeqi: assumes A1: "A = B"   
   shows "(\<cn>  A) = (\<cn>B)"
proof -
   from A1 have S1: "A = B".
   have S2: "A = B ⟶ (\<cn>A) = (\<cn>B)" by (rule MMI_negeq)
   from S1 S2 show "(\<cn>A) = (\<cn>B)" by (rule MMI_ax_mp)
qed

lemma (in MMIsar0) MMI_negeqd: assumes A1: "φ ⟶ A = B"   
   shows "φ ⟶ (\<cn>A) = (\<cn>B)"
proof -
   from A1 have S1: "φ ⟶ A = B".
   have S2: "A = B ⟶ (\<cn>A) = (\<cn>B)" by (rule MMI_negeq)
   from S1 S2 show "φ ⟶ (\<cn>A) = (\<cn>B)" by (rule MMI_syl)
qed

(**********************auto************************************)

lemma (in MMIsar0) MMI_hbneg: assumes A1: "y ∈ A ⟶ ( ∀ x . y ∈ A )"   
   shows "y ∈ ((\<cn>  A)) ⟶ ( ∀ x . (y ∈ ((\<cn>  A)) ) )"
  using assms by auto

lemma (in MMIsar0) MMI_minusex: 
   shows "((\<cn>  A)) isASet" by auto

(********38-43************************************************)

lemma (in MMIsar0) MMI_subcl: assumes A1: "A ∈ ℂ" and
    A2: "B ∈ ℂ"   
   shows "( A \<cs> B ) ∈ ℂ"
proof -
   from A1 have S1: "A ∈ ℂ".
   from A2 have S2: "B ∈ ℂ".
   from S1 S2 have S3: "( A \<cs> B ) = ⋃ { x ∈ ℂ . ( B \<ca> x ) = A }" 
     by (rule MMI_subval)
   from A2 have S4: "B ∈ ℂ".
   from A1 have S5: "A ∈ ℂ".
   from S4 S5 have S6: "∃! x . x ∈ ℂ ∧ ( B \<ca> x ) = A" by (rule MMI_negeu)
   have S7: "( ∃! x . x ∈ ℂ ∧ ( B \<ca> x ) = A ) ⟶ 
     ⋃ { x ∈ ℂ . ( B \<ca> x ) = A } ∈ ℂ" by (rule MMI_reucl)
   from S6 S7 have S8: "⋃ { x ∈ ℂ . ( B \<ca> x ) = A } ∈ ℂ" 
     by (rule MMI_ax_mp)
   from S3 S8 show "( A \<cs> B ) ∈ ℂ" by simp
qed

lemma (in MMIsar0) MMI_subclt: 
   shows "( A ∈ ℂ ∧ B ∈ ℂ ) ⟶ ( A \<cs> B ) ∈ ℂ"
proof -
   have S1: "A = if ( A ∈ ℂ , A , 𝟬 ) ⟶ ( A \<cs> B ) = 
     ( if ( A ∈ ℂ , A , 𝟬 ) \<cs> B )" by (rule MMI_opreq1)
   from S1 have S2: "A = if ( A ∈ ℂ , A , 𝟬 ) ⟶ ( ( A \<cs> B ) ∈ ℂ ⟷ 
     ( if ( A ∈ ℂ , A , 𝟬 ) \<cs> B ) ∈ ℂ )" by (rule MMI_eleq1d)
   have S3: "B = if ( B ∈ ℂ , B , 𝟬 ) ⟶ ( if ( A ∈ ℂ , A , 𝟬 ) \<cs> B ) = 
     ( if ( A ∈ ℂ , A , 𝟬 ) \<cs> if ( B ∈ ℂ , B , 𝟬 ) )" by (rule MMI_opreq2)
   from S3 have S4: "B = if ( B ∈ ℂ , B , 𝟬 ) ⟶ 
     ( ( if ( A ∈ ℂ , A , 𝟬 ) \<cs> B ) ∈ ℂ ⟷ 
     ( if ( A ∈ ℂ , A , 𝟬 ) \<cs> if ( B ∈ ℂ , B , 𝟬 ) ) ∈ ℂ )" 
     by (rule MMI_eleq1d)
   have S5: "𝟬 ∈ ℂ" by (rule MMI_0cn)
   from S5 have S6: "if ( A ∈ ℂ , A , 𝟬 ) ∈ ℂ" by (rule MMI_elimel)
   have S7: "𝟬 ∈ ℂ" by (rule MMI_0cn)
   from S7 have S8: "if ( B ∈ ℂ , B , 𝟬 ) ∈ ℂ" by (rule MMI_elimel)
   from S6 S8 have S9: 
     "( if ( A ∈ ℂ , A , 𝟬 ) \<cs> if ( B ∈ ℂ , B , 𝟬 ) ) ∈ ℂ" 
     by (rule MMI_subcl)
   from S2 S4 S9 show "( A ∈ ℂ ∧ B ∈ ℂ ) ⟶ ( A \<cs> B ) ∈ ℂ" 
     by (rule MMI_dedth2h)
qed

lemma (in MMIsar0) MMI_negclt: 
   shows "A ∈ ℂ ⟶ ( (\<cn>  A) ) ∈ ℂ"
proof -
   have S1: "𝟬 ∈ ℂ" by (rule MMI_0cn)
   have S2: "( 𝟬 ∈ ℂ ∧ A ∈ ℂ ) ⟶ ( 𝟬 \<cs> A ) ∈ ℂ" by (rule MMI_subclt)
   from S1 S2 have S3: "A ∈ ℂ ⟶ ( 𝟬 \<cs> A ) ∈ ℂ" by (rule MMI_mpan)
   have S4: "( (\<cn>  A) ) = ( 𝟬 \<cs> A )" by (rule MMI_df_neg)
   from S3 S4 show "A ∈ ℂ ⟶ ( (\<cn>  A) ) ∈ ℂ" by (rule MMI_syl5eqel)
qed

lemma (in MMIsar0) MMI_negcl: assumes A1: "A ∈ ℂ"   
   shows "( (\<cn>  A) ) ∈ ℂ"
proof -
   from A1 have S1: "A ∈ ℂ".
   have S2: "A ∈ ℂ ⟶ ( (\<cn>  A) ) ∈ ℂ" by (rule MMI_negclt)
   from S1 S2 show "( (\<cn>  A) ) ∈ ℂ" by (rule MMI_ax_mp)
qed

lemma (in MMIsar0) MMI_subadd: assumes A1: "A ∈ ℂ" and
    A2: "B ∈ ℂ" and
    A3: "C ∈ ℂ"   
   shows "( A \<cs> B ) = C ⟷ ( B \<ca> C ) = A"
proof -
   from A3 have S1: "C ∈ ℂ".
   { fix x
     have S2: "x = C ⟶ ( ( A \<cs> B ) = x ⟷ ( A \<cs> B ) = C )" 
       by (rule MMI_eqeq2)
     have S3: "x = C ⟶ ( B \<ca> x ) = ( B \<ca> C )" by (rule MMI_opreq2)
     from S3 have S4: "x = C ⟶ ( ( B \<ca> x ) = A ⟷ ( B \<ca> C ) = A )" 
       by (rule MMI_eqeq1d)
     from S2 S4 have "x = C ⟶ ( ( ( A \<cs> B ) = x ⟷ 
       ( B \<ca> x ) = A ) ⟷ ( ( A \<cs> B ) = C ⟷ ( B \<ca> C ) = A ) )" 
       by (rule MMI_bibi12d)
   } then have S5: "∀x. x = C ⟶ ( ( ( A \<cs> B ) = x ⟷ 
       ( B \<ca> x ) = A ) ⟷ ( ( A \<cs> B ) = C ⟷ 
       ( B \<ca> C ) = A ) )" by simp
   from A2 have S6: "B ∈ ℂ".
   from A1 have S7: "A ∈ ℂ".
   from S6 S7 have S8: "∃! x . x ∈ ℂ ∧ ( B \<ca> x ) = A" by (rule MMI_negeu)
   { fix x 
     have S9: "( x ∈ ℂ ∧ ( ∃! x . x ∈ ℂ ∧ ( B \<ca> x ) = A ) ⟶ 
       ( ( B \<ca> x ) = A ) ⟷ ⋃ { x ∈ ℂ . ( B \<ca> x ) = A } = x )" 
       by (rule MMI_reuuni1)
     from S8 S9 have "x ∈ ℂ ⟶ ( ( B \<ca> x ) = A ⟷ 
       ⋃ { x ∈ ℂ . ( B \<ca> x ) = A } = x )" by (rule MMI_mpan2)
   } then have S10: "∀ x. x ∈ ℂ ⟶ ( ( B \<ca> x ) = A ⟷ 
       ⋃ { x ∈ ℂ . ( B \<ca> x ) = A } = x )" by blast
   from A1 have S11: "A ∈ ℂ".
   from A2 have S12: "B ∈ ℂ".
   from S11 S12 have S13: "( A \<cs> B ) = ⋃ { x ∈ ℂ . ( B \<ca> x ) = A }" 
     by (rule MMI_subval)
   from S13 have S14: "∀x. ( A \<cs> B ) = x ⟷ 
     ⋃ { x ∈ ℂ . ( B \<ca> x ) = A } = x" by simp  (* (rule MMI_eqeq1i)*)
   from S10 S14 have S15: "∀x. x ∈ ℂ ⟶ ( ( A \<cs> B ) = x ⟷ 
     ( B \<ca> x ) = A )" by (rule MMI_syl6rbbr)
   from S5 S15 have S16: "C ∈ ℂ ⟶ ( ( A \<cs> B ) = C ⟷ 
     ( B \<ca> C ) = A )" by (rule MMI_vtoclga)
   from S1 S16 show "( A \<cs> B ) = C ⟷ ( B \<ca> C ) = A" 
     by (rule MMI_ax_mp)
qed

(*******************44-53*********************************************)


lemma (in MMIsar0) MMI_subsub23: assumes A1: "A ∈ ℂ" and
    A2: "B ∈ ℂ" and
    A3: "C ∈ ℂ"   
   shows "( A \<cs> B ) = C ⟷ ( A \<cs> C ) = B"
proof -
   from A2 have S1: "B ∈ ℂ".
   from A3 have S2: "C ∈ ℂ".
   from S1 S2 have S3: "( B \<ca> C ) = ( C \<ca> B )" by (rule MMI_addcom)
   from S3 have S4: "( B \<ca> C ) = A ⟷ ( C \<ca> B ) = A" 
     by (rule MMI_eqeq1i)
   from A1 have S5: "A ∈ ℂ".
   from A2 have S6: "B ∈ ℂ".
   from A3 have S7: "C ∈ ℂ".
   from S5 S6 S7 have S8: "( A \<cs> B ) = C ⟷ ( B \<ca> C ) = A" 
     by (rule MMI_subadd)
   from A1 have S9: "A ∈ ℂ".
   from A3 have S10: "C ∈ ℂ".
   from A2 have S11: "B ∈ ℂ".
   from S9 S10 S11 have S12: "( A \<cs> C ) = B ⟷ ( C \<ca> B ) = A" 
     by (rule MMI_subadd)
   from S4 S8 S12 show "( A \<cs> B ) = C ⟷ ( A \<cs> C ) = B" 
     by (rule MMI_3bitr4)
qed

lemma (in MMIsar0) MMI_subaddt: 
   shows "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( ( A \<cs> B ) = C ⟷ 
  ( B \<ca> C ) = A )"
proof -
   have S1: "A = if ( A ∈ ℂ , A , 𝟬 ) ⟶ ( A \<cs> B ) = 
     ( if ( A ∈ ℂ , A , 𝟬 ) \<cs> B )" by (rule MMI_opreq1)
   from S1 have S2: "A = if ( A ∈ ℂ , A , 𝟬 ) ⟶ ( ( A \<cs> B ) = C ⟷ 
     ( if ( A ∈ ℂ , A , 𝟬 ) \<cs> B ) = C )" by (rule MMI_eqeq1d)
   have S3: "A = if ( A ∈ ℂ , A , 𝟬 ) ⟶ ( ( B \<ca> C ) = A ⟷ 
     ( B \<ca> C ) = if ( A ∈ ℂ , A , 𝟬 ) )" by (rule MMI_eqeq2)
   from S2 S3 have S4: "A = if ( A ∈ ℂ , A , 𝟬 ) ⟶ 
     ( ( ( A \<cs> B ) = C ⟷ ( B \<ca> C ) = A ) ⟷ 
     ( ( if ( A ∈ ℂ , A , 𝟬 ) \<cs> B )