Proofgold Asset

Known df_mgm2__df_cmgm2__df_sgrp2__df_csgrp2__df_rng0__df_rnghomo__df_rngisom__df_rngc__df_rngcALTV__df_ringc__df_ringcALTV__df_dmatalt__df_scmatalt__df_linc__df_lco__df_lininds__df_lindeps__df_fdiv : ∀ x0 : ο . (wceq cmgm2 (cab (λ x1 . wbr (cfv (cv x1) cplusg) (cfv (cv x1) cbs) ccllaw)) ⟶ wceq ccmgm2 (crab (λ x1 . wbr (cfv (cv x1) cplusg) (cfv (cv x1) cbs) ccomlaw) (λ x1 . cmgm2)) ⟶ wceq csgrp2 (crab (λ x1 . wbr (cfv (cv x1) cplusg) (cfv (cv x1) cbs) casslaw) (λ x1 . cmgm2)) ⟶ wceq ccsgrp2 (crab (λ x1 . wbr (cfv (cv x1) cplusg) (cfv (cv x1) cbs) ccomlaw) (λ x1 . csgrp2)) ⟶ wceq crng (crab (λ x1 . wa (wcel (cfv (cv x1) cmgp) csgrp) (wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wral (λ x5 . wral (λ x6 . wral (λ x7 . wa (wceq (co (cv x5) (co (cv x6) (cv x7) (cv x3)) (cv x4)) (co (co (cv x5) (cv x6) (cv x4)) (co (cv x5) (cv x7) (cv x4)) (cv x3))) (wceq (co (co (cv x5) (cv x6) (cv x3)) (cv x7) (cv x4)) (co (co (cv x5) (cv x7) (cv x4)) (co (cv x6) (cv x7) (cv x4)) (cv x3)))) (λ x7 . cv x2)) (λ x6 . cv x2)) (λ x5 . cv x2)) (cfv (cv x1) cmulr)) (cfv (cv x1) cplusg)) (cfv (cv x1) cbs))) (λ x1 . cabl)) ⟶ wceq crngh (cmpt2 (λ x1 x2 . crng) (λ x1 x2 . crng) (λ x1 x2 . csb (cfv (cv x1) cbs) (λ x3 . csb (cfv (cv x2) cbs) (λ x4 . crab (λ x5 . wral (λ x6 . wral (λ x7 . wa (wceq (cfv (co (cv x6) (cv x7) (cfv (cv x1) cplusg)) (cv x5)) (co (cfv (cv x6) (cv x5)) (cfv (cv x7) (cv x5)) (cfv (cv x2) cplusg))) (wceq (cfv (co (cv x6) (cv x7) (cfv (cv x1) cmulr)) (cv x5)) (co (cfv (cv x6) (cv x5)) (cfv (cv x7) (cv x5)) (cfv (cv x2) cmulr)))) (λ x7 . cv x3)) (λ x6 . cv x3)) (λ x5 . co (cv x4) (cv x3) cmap))))) ⟶ wceq crngs (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . crab (λ x3 . wcel (ccnv (cv x3)) (co (cv x2) (cv x1) crngh)) (λ x3 . co (cv x1) (cv x2) crngh))) ⟶ wceq crngc (cmpt (λ x1 . cvv) (λ x1 . co (cfv (cv x1) cestrc) (cres crngh (cxp (cin (cv x1) crng) (cin (cv x1) crng))) cresc)) ⟶ wceq crngcALTV (cmpt (λ x1 . cvv) (λ x1 . csb (cin (cv x1) crng) (λ x2 . ctp (cop (cfv cnx cbs) (cv x2)) (cop (cfv cnx chom) (cmpt2 (λ x3 x4 . cv x2) (λ x3 x4 . cv x2) (λ x3 x4 . co (cv x3) (cv x4) crngh))) (cop (cfv cnx cco) (cmpt2 (λ x3 x4 . cxp (cv x2) (cv x2)) (λ x3 x4 . cv x2) (λ x3 x4 . cmpt2 (λ x5 x6 . co (cfv (cv x3) c2nd) (cv x4) crngh) (λ x5 x6 . co (cfv (cv x3) c1st) (cfv (cv x3) c2nd) crngh) (λ x5 x6 . ccom (cv x5) (cv x6)))))))) ⟶ wceq cringc (cmpt (λ x1 . cvv) (λ x1 . co (cfv (cv x1) cestrc) (cres crh (cxp (cin (cv x1) crg) (cin (cv x1) crg))) cresc)) ⟶ wceq cringcALTV (cmpt (λ x1 . cvv) (λ x1 . csb (cin (cv x1) crg) (λ x2 . ctp (cop (cfv cnx cbs) (cv x2)) (cop (cfv cnx chom) (cmpt2 (λ x3 x4 . cv x2) (λ x3 x4 . cv x2) (λ x3 x4 . co (cv x3) (cv x4) crh))) (cop (cfv cnx cco) (cmpt2 (λ x3 x4 . cxp (cv x2) (cv x2)) (λ x3 x4 . cv x2) (λ x3 x4 . cmpt2 (λ x5 x6 . co (cfv (cv x3) c2nd) (cv x4) crh) (λ x5 x6 . co (cfv (cv x3) c1st) (cfv (cv x3) c2nd) crh) (λ x5 x6 . ccom (cv x5) (cv x6)))))))) ⟶ wceq cdmatalt (cmpt2 (λ x1 x2 . cfn) (λ x1 x2 . cvv) (λ x1 x2 . csb (co (cv x1) (cv x2) cmat) (λ x3 . co (cv x3) (crab (λ x4 . wral (λ x5 . wral (λ x6 . wne (cv x5) (cv x6) ⟶ wceq (co (cv x5) (cv x6) (cv x4)) (cfv (cv x2) c0g)) (λ x6 . cv x1)) (λ x5 . cv x1)) (λ x4 . cfv (cv x3) cbs)) cress))) ⟶ wceq cscmatalt (cmpt2 (λ x1 x2 . cfn) (λ x1 x2 . cvv) (λ x1 x2 . csb (co (cv x1) (cv x2) cmat) (λ x3 . co (cv x3) (crab (λ x4 . wrex (λ x5 . wral (λ x6 . wral (λ x7 . wceq (co (cv x6) (cv x7) (cv x4)) (cif (wceq (cv x6) (cv x7)) (cv x5) (cfv (cv x2) c0g))) (λ x7 . cv x1)) (λ x6 . cv x1)) (λ x5 . cfv (cv x2) cbs)) (λ x4 . cfv (cv x3) cbs)) cress))) ⟶ wceq clinc (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . co (cfv (cfv (cv x1) csca) cbs) (cv x3) cmap) (λ x2 x3 . cpw (cfv (cv x1) cbs)) (λ x2 x3 . co (cv x1) (cmpt (λ x4 . cv x3) (λ x4 . co (cfv (cv x4) (cv x2)) (cv x4) (cfv (cv x1) cvsca))) cgsu))) ⟶ wceq clinco (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cpw (cfv (cv x1) cbs)) (λ x1 x2 . crab (λ x3 . wrex (λ x4 . wa (wbr (cv x4) (cfv (cfv (cv x1) csca) c0g) cfsupp) (wceq (cv x3) (co (cv x4) (cv x2) (cfv (cv x1) clinc)))) (λ x4 . co (cfv (cfv (cv x1) csca) cbs) (cv x2) cmap)) (λ x3 . cfv (cv x1) cbs))) ⟶ wceq clininds (copab (λ x1 x2 . wa (wcel (cv x1) (cpw (cfv (cv x2) cbs))) (wral (λ x3 . wa (wbr (cv x3) (cfv (cfv (cv x2) csca) c0g) cfsupp) (wceq (co (cv x3) (cv x1) (cfv (cv x2) clinc)) (cfv (cv x2) c0g)) ⟶ wral (λ x4 . wceq (cfv (cv x4) (cv x3)) (cfv (cfv (cv x2) csca) c0g)) (λ x4 . cv x1)) (λ x3 . co (cfv (cfv (cv x2) csca) cbs) (cv x1) cmap)))) ⟶ wceq clindeps (copab (λ x1 x2 . wn (wbr (cv x1) (cv x2) clininds))) ⟶ wceq cfdiv (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cres (co (cv x1) (cv x2) (cof cdiv)) (co (cv x2) cc0 csupp))) ⟶ x0) ⟶ x0
Theorem df_mgm2 : wceq cmgm2 (cab (λ x0 . wbr (cfv (cv x0) cplusg) (cfv (cv x0) cbs) ccllaw)) (proof)
Theorem df_cmgm2 : wceq ccmgm2 (crab (λ x0 . wbr (cfv (cv x0) cplusg) (cfv (cv x0) cbs) ccomlaw) (λ x0 . cmgm2)) (proof)
Theorem df_sgrp2 : wceq csgrp2 (crab (λ x0 . wbr (cfv (cv x0) cplusg) (cfv (cv x0) cbs) casslaw) (λ x0 . cmgm2)) (proof)
Theorem df_csgrp2 : wceq ccsgrp2 (crab (λ x0 . wbr (cfv (cv x0) cplusg) (cfv (cv x0) cbs) ccomlaw) (λ x0 . csgrp2)) (proof)
Theorem df_rng0 : wceq crng (crab (λ x0 . wa (wcel (cfv (cv x0) cmgp) csgrp) (wsbc (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wral (λ x4 . wral (λ x5 . wral (λ x6 . wa (wceq (co (cv x4) (co (cv x5) (cv x6) (cv x2)) (cv x3)) (co (co (cv x4) (cv x5) (cv x3)) (co (cv x4) (cv x6) (cv x3)) (cv x2))) (wceq (co (co (cv x4) (cv x5) (cv x2)) (cv x6) (cv x3)) (co (co (cv x4) (cv x6) (cv x3)) (co (cv x5) (cv x6) (cv x3)) (cv x2)))) (λ x6 . cv x1)) (λ x5 . cv x1)) (λ x4 . cv x1)) (cfv (cv x0) cmulr)) (cfv (cv x0) cplusg)) (cfv (cv x0) cbs))) (λ x0 . cabl)) (proof)
Theorem df_rnghomo : wceq crngh (cmpt2 (λ x0 x1 . crng) (λ x0 x1 . crng) (λ x0 x1 . csb (cfv (cv x0) cbs) (λ x2 . csb (cfv (cv x1) cbs) (λ x3 . crab (λ x4 . wral (λ x5 . wral (λ x6 . wa (wceq (cfv (co (cv x5) (cv x6) (cfv (cv x0) cplusg)) (cv x4)) (co (cfv (cv x5) (cv x4)) (cfv (cv x6) (cv x4)) (cfv (cv x1) cplusg))) (wceq (cfv (co (cv x5) (cv x6) (cfv (cv x0) cmulr)) (cv x4)) (co (cfv (cv x5) (cv x4)) (cfv (cv x6) (cv x4)) (cfv (cv x1) cmulr)))) (λ x6 . cv x2)) (λ x5 . cv x2)) (λ x4 . co (cv x3) (cv x2) cmap))))) (proof)
Theorem df_rngisom : wceq crngs (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . crab (λ x2 . wcel (ccnv (cv x2)) (co (cv x1) (cv x0) crngh)) (λ x2 . co (cv x0) (cv x1) crngh))) (proof)
Theorem df_rngc : wceq crngc (cmpt (λ x0 . cvv) (λ x0 . co (cfv (cv x0) cestrc) (cres crngh (cxp (cin (cv x0) crng) (cin (cv x0) crng))) cresc)) (proof)
Theorem df_rngcALTV : wceq crngcALTV (cmpt (λ x0 . cvv) (λ x0 . csb (cin (cv x0) crng) (λ x1 . ctp (cop (cfv cnx cbs) (cv x1)) (cop (cfv cnx chom) (cmpt2 (λ x2 x3 . cv x1) (λ x2 x3 . cv x1) (λ x2 x3 . co (cv x2) (cv x3) crngh))) (cop (cfv cnx cco) (cmpt2 (λ x2 x3 . cxp (cv x1) (cv x1)) (λ x2 x3 . cv x1) (λ x2 x3 . cmpt2 (λ x4 x5 . co (cfv (cv x2) c2nd) (cv x3) crngh) (λ x4 x5 . co (cfv (cv x2) c1st) (cfv (cv x2) c2nd) crngh) (λ x4 x5 . ccom (cv x4) (cv x5)))))))) (proof)
Theorem df_ringc : wceq cringc (cmpt (λ x0 . cvv) (λ x0 . co (cfv (cv x0) cestrc) (cres crh (cxp (cin (cv x0) crg) (cin (cv x0) crg))) cresc)) (proof)
Theorem df_ringcALTV : wceq cringcALTV (cmpt (λ x0 . cvv) (λ x0 . csb (cin (cv x0) crg) (λ x1 . ctp (cop (cfv cnx cbs) (cv x1)) (cop (cfv cnx chom) (cmpt2 (λ x2 x3 . cv x1) (λ x2 x3 . cv x1) (λ x2 x3 . co (cv x2) (cv x3) crh))) (cop (cfv cnx cco) (cmpt2 (λ x2 x3 . cxp (cv x1) (cv x1)) (λ x2 x3 . cv x1) (λ x2 x3 . cmpt2 (λ x4 x5 . co (cfv (cv x2) c2nd) (cv x3) crh) (λ x4 x5 . co (cfv (cv x2) c1st) (cfv (cv x2) c2nd) crh) (λ x4 x5 . ccom (cv x4) (cv x5)))))))) (proof)
Theorem df_dmatalt : wceq cdmatalt (cmpt2 (λ x0 x1 . cfn) (λ x0 x1 . cvv) (λ x0 x1 . csb (co (cv x0) (cv x1) cmat) (λ x2 . co (cv x2) (crab (λ x3 . wral (λ x4 . wral (λ x5 . wne (cv x4) (cv x5) ⟶ wceq (co (cv x4) (cv x5) (cv x3)) (cfv (cv x1) c0g)) (λ x5 . cv x0)) (λ x4 . cv x0)) (λ x3 . cfv (cv x2) cbs)) cress))) (proof)
Theorem df_scmatalt : wceq cscmatalt (cmpt2 (λ x0 x1 . cfn) (λ x0 x1 . cvv) (λ x0 x1 . csb (co (cv x0) (cv x1) cmat) (λ x2 . co (cv x2) (crab (λ x3 . wrex (λ x4 . wral (λ x5 . wral (λ x6 . wceq (co (cv x5) (cv x6) (cv x3)) (cif (wceq (cv x5) (cv x6)) (cv x4) (cfv (cv x1) c0g))) (λ x6 . cv x0)) (λ x5 . cv x0)) (λ x4 . cfv (cv x1) cbs)) (λ x3 . cfv (cv x2) cbs)) cress))) (proof)
Theorem df_linc : wceq clinc (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . co (cfv (cfv (cv x0) csca) cbs) (cv x2) cmap) (λ x1 x2 . cpw (cfv (cv x0) cbs)) (λ x1 x2 . co (cv x0) (cmpt (λ x3 . cv x2) (λ x3 . co (cfv (cv x3) (cv x1)) (cv x3) (cfv (cv x0) cvsca))) cgsu))) (proof)
Theorem df_lco : wceq clinco (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cpw (cfv (cv x0) cbs)) (λ x0 x1 . crab (λ x2 . wrex (λ x3 . wa (wbr (cv x3) (cfv (cfv (cv x0) csca) c0g) cfsupp) (wceq (cv x2) (co (cv x3) (cv x1) (cfv (cv x0) clinc)))) (λ x3 . co (cfv (cfv (cv x0) csca) cbs) (cv x1) cmap)) (λ x2 . cfv (cv x0) cbs))) (proof)
Theorem df_lininds : wceq clininds (copab (λ x0 x1 . wa (wcel (cv x0) (cpw (cfv (cv x1) cbs))) (wral (λ x2 . wa (wbr (cv x2) (cfv (cfv (cv x1) csca) c0g) cfsupp) (wceq (co (cv x2) (cv x0) (cfv (cv x1) clinc)) (cfv (cv x1) c0g)) ⟶ wral (λ x3 . wceq (cfv (cv x3) (cv x2)) (cfv (cfv (cv x1) csca) c0g)) (λ x3 . cv x0)) (λ x2 . co (cfv (cfv (cv x1) csca) cbs) (cv x0) cmap)))) (proof)
Theorem df_lindeps : wceq clindeps (copab (λ x0 x1 . wn (wbr (cv x0) (cv x1) clininds))) (proof)
Theorem df_fdiv : wceq cfdiv (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cres (co (cv x0) (cv x1) (cof cdiv)) (co (cv x1) cc0 csupp))) (proof)