Proofgold Address

Known df_pj__df_hil__df_obs__df_dsmm__df_frlm__df_uvc__df_lindf__df_linds__df_mamu__df_mat__df_dmat__df_scmat__df_mvmul__df_marrep__df_marepv__df_subma__df_mdet__df_madu : ∀ x0 : ο . (wceq cpj (cmpt (λ x1 . cvv) (λ x1 . cin (cmpt (λ x2 . cfv (cv x1) clss) (λ x2 . co (cv x2) (cfv (cv x2) (cfv (cv x1) cocv)) (cfv (cv x1) cpj1))) (cxp cvv (co (cfv (cv x1) cbs) (cfv (cv x1) cbs) cmap)))) ⟶ wceq chs (crab (λ x1 . wceq (cdm (cfv (cv x1) cpj)) (cfv (cv x1) ccss)) (λ x1 . cphl)) ⟶ wceq cobs (cmpt (λ x1 . cphl) (λ x1 . crab (λ x2 . wa (wral (λ x3 . wral (λ x4 . wceq (co (cv x3) (cv x4) (cfv (cv x1) cip)) (cif (wceq (cv x3) (cv x4)) (cfv (cfv (cv x1) csca) cur) (cfv (cfv (cv x1) csca) c0g))) (λ x4 . cv x2)) (λ x3 . cv x2)) (wceq (cfv (cv x2) (cfv (cv x1) cocv)) (csn (cfv (cv x1) c0g)))) (λ x2 . cpw (cfv (cv x1) cbs)))) ⟶ wceq cdsmm (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . co (co (cv x1) (cv x2) cprds) (crab (λ x3 . wcel (crab (λ x4 . wne (cfv (cv x4) (cv x3)) (cfv (cfv (cv x4) (cv x2)) c0g)) (λ x4 . cdm (cv x2))) cfn) (λ x3 . cixp (λ x4 . cdm (cv x2)) (λ x4 . cfv (cfv (cv x4) (cv x2)) cbs))) cress)) ⟶ wceq cfrlm (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . co (cv x1) (cxp (cv x2) (csn (cfv (cv x1) crglmod))) cdsmm)) ⟶ wceq cuvc (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cv x2) (λ x3 . cmpt (λ x4 . cv x2) (λ x4 . cif (wceq (cv x4) (cv x3)) (cfv (cv x1) cur) (cfv (cv x1) c0g))))) ⟶ wceq clindf (copab (λ x1 x2 . wa (wf (cdm (cv x1)) (cfv (cv x2) cbs) (cv x1)) (wsbc (λ x3 . wral (λ x4 . wral (λ x5 . wn (wcel (co (cv x5) (cfv (cv x4) (cv x1)) (cfv (cv x2) cvsca)) (cfv (cima (cv x1) (cdif (cdm (cv x1)) (csn (cv x4)))) (cfv (cv x2) clspn)))) (λ x5 . cdif (cfv (cv x3) cbs) (csn (cfv (cv x3) c0g)))) (λ x4 . cdm (cv x1))) (cfv (cv x2) csca)))) ⟶ wceq clinds (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wbr (cres cid (cv x2)) (cv x1) clindf) (λ x2 . cpw (cfv (cv x1) cbs)))) ⟶ wceq cmmul (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . csb (cfv (cfv (cv x2) c1st) c1st) (λ x3 . csb (cfv (cfv (cv x2) c1st) c2nd) (λ x4 . csb (cfv (cv x2) c2nd) (λ x5 . cmpt2 (λ x6 x7 . co (cfv (cv x1) cbs) (cxp (cv x3) (cv x4)) cmap) (λ x6 x7 . co (cfv (cv x1) cbs) (cxp (cv x4) (cv x5)) cmap) (λ x6 x7 . cmpt2 (λ x8 x9 . cv x3) (λ x8 x9 . cv x5) (λ x8 x9 . co (cv x1) (cmpt (λ x10 . cv x4) (λ x10 . co (co (cv x8) (cv x10) (cv x6)) (co (cv x10) (cv x9) (cv x7)) (cfv (cv x1) cmulr))) cgsu))))))) ⟶ wceq cmat (cmpt2 (λ x1 x2 . cfn) (λ x1 x2 . cvv) (λ x1 x2 . co (co (cv x2) (cxp (cv x1) (cv x1)) cfrlm) (cop (cfv cnx cmulr) (co (cv x2) (cotp (cv x1) (cv x1) (cv x1)) cmmul)) csts)) ⟶ wceq cdmat (cmpt2 (λ x1 x2 . cfn) (λ x1 x2 . cvv) (λ x1 x2 . crab (λ x3 . wral (λ x4 . wral (λ x5 . wne (cv x4) (cv x5) ⟶ wceq (co (cv x4) (cv x5) (cv x3)) (cfv (cv x2) c0g)) (λ x5 . cv x1)) (λ x4 . cv x1)) (λ x3 . cfv (co (cv x1) (cv x2) cmat) cbs))) ⟶ wceq cscmat (cmpt2 (λ x1 x2 . cfn) (λ x1 x2 . cvv) (λ x1 x2 . csb (co (cv x1) (cv x2) cmat) (λ x3 . crab (λ x4 . wrex (λ x5 . wceq (cv x4) (co (cv x5) (cfv (cv x3) cur) (cfv (cv x3) cvsca))) (λ x5 . cfv (cv x2) cbs)) (λ x4 . cfv (cv x3) cbs)))) ⟶ wceq cmvmul (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . csb (cfv (cv x2) c1st) (λ x3 . csb (cfv (cv x2) c2nd) (λ x4 . cmpt2 (λ x5 x6 . co (cfv (cv x1) cbs) (cxp (cv x3) (cv x4)) cmap) (λ x5 x6 . co (cfv (cv x1) cbs) (cv x4) cmap) (λ x5 x6 . cmpt (λ x7 . cv x3) (λ x7 . co (cv x1) (cmpt (λ x8 . cv x4) (λ x8 . co (co (cv x7) (cv x8) (cv x5)) (cfv (cv x8) (cv x6)) (cfv (cv x1) cmulr))) cgsu)))))) ⟶ wceq cmarrep (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt2 (λ x3 x4 . cfv (co (cv x1) (cv x2) cmat) cbs) (λ x3 x4 . cfv (cv x2) cbs) (λ x3 x4 . cmpt2 (λ x5 x6 . cv x1) (λ x5 x6 . cv x1) (λ x5 x6 . cmpt2 (λ x7 x8 . cv x1) (λ x7 x8 . cv x1) (λ x7 x8 . cif (wceq (cv x7) (cv x5)) (cif (wceq (cv x8) (cv x6)) (cv x4) (cfv (cv x2) c0g)) (co (cv x7) (cv x8) (cv x3))))))) ⟶ wceq cmatrepV (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt2 (λ x3 x4 . cfv (co (cv x1) (cv x2) cmat) cbs) (λ x3 x4 . co (cfv (cv x2) cbs) (cv x1) cmap) (λ x3 x4 . cmpt (λ x5 . cv x1) (λ x5 . cmpt2 (λ x6 x7 . cv x1) (λ x6 x7 . cv x1) (λ x6 x7 . cif (wceq (cv x7) (cv x5)) (cfv (cv x6) (cv x4)) (co (cv x6) (cv x7) (cv x3))))))) ⟶ wceq csubma (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cfv (co (cv x1) (cv x2) cmat) cbs) (λ x3 . cmpt2 (λ x4 x5 . cv x1) (λ x4 x5 . cv x1) (λ x4 x5 . cmpt2 (λ x6 x7 . cdif (cv x1) (csn (cv x4))) (λ x6 x7 . cdif (cv x1) (csn (cv x5))) (λ x6 x7 . co (cv x6) (cv x7) (cv x3)))))) ⟶ wceq cmdat (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cfv (co (cv x1) (cv x2) cmat) cbs) (λ x3 . co (cv x2) (cmpt (λ x4 . cfv (cfv (cv x1) csymg) cbs) (λ x4 . co (cfv (cv x4) (ccom (cfv (cv x2) czrh) (cfv (cv x1) cpsgn))) (co (cfv (cv x2) cmgp) (cmpt (λ x5 . cv x1) (λ x5 . co (cfv (cv x5) (cv x4)) (cv x5) (cv x3))) cgsu) (cfv (cv x2) cmulr))) cgsu))) ⟶ wceq cmadu (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . cfv (co (cv x1) (cv x2) cmat) cbs) (λ x3 . cmpt2 (λ x4 x5 . cv x1) (λ x4 x5 . cv x1) (λ x4 x5 . cfv (cmpt2 (λ x6 x7 . cv x1) (λ x6 x7 . cv x1) (λ x6 x7 . cif (wceq (cv x6) (cv x5)) (cif (wceq (cv x7) (cv x4)) (cfv (cv x2) cur) (cfv (cv x2) c0g)) (co (cv x6) (cv x7) (cv x3)))) (co (cv x1) (cv x2) cmdat))))) ⟶ x0) ⟶ x0
Theorem df_pj : wceq cpj (cmpt (λ x0 . cvv) (λ x0 . cin (cmpt (λ x1 . cfv (cv x0) clss) (λ x1 . co (cv x1) (cfv (cv x1) (cfv (cv x0) cocv)) (cfv (cv x0) cpj1))) (cxp cvv (co (cfv (cv x0) cbs) (cfv (cv x0) cbs) cmap)))) (proof)
Theorem df_hil : wceq chs (crab (λ x0 . wceq (cdm (cfv (cv x0) cpj)) (cfv (cv x0) ccss)) (λ x0 . cphl)) (proof)
Theorem df_obs : wceq cobs (cmpt (λ x0 . cphl) (λ x0 . crab (λ x1 . wa (wral (λ x2 . wral (λ x3 . wceq (co (cv x2) (cv x3) (cfv (cv x0) cip)) (cif (wceq (cv x2) (cv x3)) (cfv (cfv (cv x0) csca) cur) (cfv (cfv (cv x0) csca) c0g))) (λ x3 . cv x1)) (λ x2 . cv x1)) (wceq (cfv (cv x1) (cfv (cv x0) cocv)) (csn (cfv (cv x0) c0g)))) (λ x1 . cpw (cfv (cv x0) cbs)))) (proof)
Theorem df_dsmm : wceq cdsmm (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . co (co (cv x0) (cv x1) cprds) (crab (λ x2 . wcel (crab (λ x3 . wne (cfv (cv x3) (cv x2)) (cfv (cfv (cv x3) (cv x1)) c0g)) (λ x3 . cdm (cv x1))) cfn) (λ x2 . cixp (λ x3 . cdm (cv x1)) (λ x3 . cfv (cfv (cv x3) (cv x1)) cbs))) cress)) (proof)
Theorem df_frlm : wceq cfrlm (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . co (cv x0) (cxp (cv x1) (csn (cfv (cv x0) crglmod))) cdsmm)) (proof)
Theorem df_uvc : wceq cuvc (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cv x1) (λ x2 . cmpt (λ x3 . cv x1) (λ x3 . cif (wceq (cv x3) (cv x2)) (cfv (cv x0) cur) (cfv (cv x0) c0g))))) (proof)
Theorem df_lindf : wceq clindf (copab (λ x0 x1 . wa (wf (cdm (cv x0)) (cfv (cv x1) cbs) (cv x0)) (wsbc (λ x2 . wral (λ x3 . wral (λ x4 . wn (wcel (co (cv x4) (cfv (cv x3) (cv x0)) (cfv (cv x1) cvsca)) (cfv (cima (cv x0) (cdif (cdm (cv x0)) (csn (cv x3)))) (cfv (cv x1) clspn)))) (λ x4 . cdif (cfv (cv x2) cbs) (csn (cfv (cv x2) c0g)))) (λ x3 . cdm (cv x0))) (cfv (cv x1) csca)))) (proof)
Theorem df_linds : wceq clinds (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wbr (cres cid (cv x1)) (cv x0) clindf) (λ x1 . cpw (cfv (cv x0) cbs)))) (proof)
Theorem df_mamu : wceq cmmul (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . csb (cfv (cfv (cv x1) c1st) c1st) (λ x2 . csb (cfv (cfv (cv x1) c1st) c2nd) (λ x3 . csb (cfv (cv x1) c2nd) (λ x4 . cmpt2 (λ x5 x6 . co (cfv (cv x0) cbs) (cxp (cv x2) (cv x3)) cmap) (λ x5 x6 . co (cfv (cv x0) cbs) (cxp (cv x3) (cv x4)) cmap) (λ x5 x6 . cmpt2 (λ x7 x8 . cv x2) (λ x7 x8 . cv x4) (λ x7 x8 . co (cv x0) (cmpt (λ x9 . cv x3) (λ x9 . co (co (cv x7) (cv x9) (cv x5)) (co (cv x9) (cv x8) (cv x6)) (cfv (cv x0) cmulr))) cgsu))))))) (proof)
Theorem df_mat : wceq cmat (cmpt2 (λ x0 x1 . cfn) (λ x0 x1 . cvv) (λ x0 x1 . co (co (cv x1) (cxp (cv x0) (cv x0)) cfrlm) (cop (cfv cnx cmulr) (co (cv x1) (cotp (cv x0) (cv x0) (cv x0)) cmmul)) csts)) (proof)
Theorem df_dmat : wceq cdmat (cmpt2 (λ x0 x1 . cfn) (λ x0 x1 . cvv) (λ x0 x1 . crab (λ x2 . wral (λ x3 . wral (λ x4 . wne (cv x3) (cv x4) ⟶ wceq (co (cv x3) (cv x4) (cv x2)) (cfv (cv x1) c0g)) (λ x4 . cv x0)) (λ x3 . cv x0)) (λ x2 . cfv (co (cv x0) (cv x1) cmat) cbs))) (proof)
Theorem df_scmat : wceq cscmat (cmpt2 (λ x0 x1 . cfn) (λ x0 x1 . cvv) (λ x0 x1 . csb (co (cv x0) (cv x1) cmat) (λ x2 . crab (λ x3 . wrex (λ x4 . wceq (cv x3) (co (cv x4) (cfv (cv x2) cur) (cfv (cv x2) cvsca))) (λ x4 . cfv (cv x1) cbs)) (λ x3 . cfv (cv x2) cbs)))) (proof)
Theorem df_mvmul : wceq cmvmul (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . csb (cfv (cv x1) c1st) (λ x2 . csb (cfv (cv x1) c2nd) (λ x3 . cmpt2 (λ x4 x5 . co (cfv (cv x0) cbs) (cxp (cv x2) (cv x3)) cmap) (λ x4 x5 . co (cfv (cv x0) cbs) (cv x3) cmap) (λ x4 x5 . cmpt (λ x6 . cv x2) (λ x6 . co (cv x0) (cmpt (λ x7 . cv x3) (λ x7 . co (co (cv x6) (cv x7) (cv x4)) (cfv (cv x7) (cv x5)) (cfv (cv x0) cmulr))) cgsu)))))) (proof)
Theorem df_marrep : wceq cmarrep (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt2 (λ x2 x3 . cfv (co (cv x0) (cv x1) cmat) cbs) (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . cmpt2 (λ x4 x5 . cv x0) (λ x4 x5 . cv x0) (λ x4 x5 . cmpt2 (λ x6 x7 . cv x0) (λ x6 x7 . cv x0) (λ x6 x7 . cif (wceq (cv x6) (cv x4)) (cif (wceq (cv x7) (cv x5)) (cv x3) (cfv (cv x1) c0g)) (co (cv x6) (cv x7) (cv x2))))))) (proof)
Theorem df_marepv : wceq cmatrepV (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt2 (λ x2 x3 . cfv (co (cv x0) (cv x1) cmat) cbs) (λ x2 x3 . co (cfv (cv x1) cbs) (cv x0) cmap) (λ x2 x3 . cmpt (λ x4 . cv x0) (λ x4 . cmpt2 (λ x5 x6 . cv x0) (λ x5 x6 . cv x0) (λ x5 x6 . cif (wceq (cv x6) (cv x4)) (cfv (cv x5) (cv x3)) (co (cv x5) (cv x6) (cv x2))))))) (proof)
Theorem df_subma : wceq csubma (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cfv (co (cv x0) (cv x1) cmat) cbs) (λ x2 . cmpt2 (λ x3 x4 . cv x0) (λ x3 x4 . cv x0) (λ x3 x4 . cmpt2 (λ x5 x6 . cdif (cv x0) (csn (cv x3))) (λ x5 x6 . cdif (cv x0) (csn (cv x4))) (λ x5 x6 . co (cv x5) (cv x6) (cv x2)))))) (proof)
Theorem df_mdet : wceq cmdat (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cfv (co (cv x0) (cv x1) cmat) cbs) (λ x2 . co (cv x1) (cmpt (λ x3 . cfv (cfv (cv x0) csymg) cbs) (λ x3 . co (cfv (cv x3) (ccom (cfv (cv x1) czrh) (cfv (cv x0) cpsgn))) (co (cfv (cv x1) cmgp) (cmpt (λ x4 . cv x0) (λ x4 . co (cfv (cv x4) (cv x3)) (cv x4) (cv x2))) cgsu) (cfv (cv x1) cmulr))) cgsu))) (proof)
Theorem df_madu : wceq cmadu (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . cfv (co (cv x0) (cv x1) cmat) cbs) (λ x2 . cmpt2 (λ x3 x4 . cv x0) (λ x3 x4 . cv x0) (λ x3 x4 . cfv (cmpt2 (λ x5 x6 . cv x0) (λ x5 x6 . cv x0) (λ x5 x6 . cif (wceq (cv x5) (cv x4)) (cif (wceq (cv x6) (cv x3)) (cfv (cv x1) cur) (cfv (cv x1) c0g)) (co (cv x5) (cv x6) (cv x2)))) (co (cv x0) (cv x1) cmdat))))) (proof)