Proofgold Address

Known df_rnghom__df_rngiso__df_ric__df_drng__df_field__df_subrg__df_rgspn__df_abv__df_staf__df_srng__df_lmod__df_scaf__df_lss__df_lsp__df_lmhm__df_lmim__df_lmic__df_lbs : ∀ x0 : ο . (wceq crh (cmpt2 (λ x1 x2 . crg) (λ x1 x2 . crg) (λ x1 x2 . csb (cfv (cv x1) cbs) (λ x3 . csb (cfv (cv x2) cbs) (λ x4 . crab (λ x5 . wa (wceq (cfv (cfv (cv x1) cur) (cv x5)) (cfv (cv x2) cur)) (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 crs (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . crab (λ x3 . wcel (ccnv (cv x3)) (co (cv x2) (cv x1) crh)) (λ x3 . co (cv x1) (cv x2) crh))) ⟶ wceq cric (cima (ccnv crs) (cdif cvv c1o)) ⟶ wceq cdr (crab (λ x1 . wceq (cfv (cv x1) cui) (cdif (cfv (cv x1) cbs) (csn (cfv (cv x1) c0g)))) (λ x1 . crg)) ⟶ wceq cfield (cin cdr ccrg) ⟶ wceq csubrg (cmpt (λ x1 . crg) (λ x1 . crab (λ x2 . wa (wcel (co (cv x1) (cv x2) cress) crg) (wcel (cfv (cv x1) cur) (cv x2))) (λ x2 . cpw (cfv (cv x1) cbs)))) ⟶ wceq crgspn (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cpw (cfv (cv x1) cbs)) (λ x2 . cint (crab (λ x3 . wss (cv x2) (cv x3)) (λ x3 . cfv (cv x1) csubrg))))) ⟶ wceq cabv (cmpt (λ x1 . crg) (λ x1 . crab (λ x2 . wral (λ x3 . wa (wb (wceq (cfv (cv x3) (cv x2)) cc0) (wceq (cv x3) (cfv (cv x1) c0g))) (wral (λ x4 . wa (wceq (cfv (co (cv x3) (cv x4) (cfv (cv x1) cmulr)) (cv x2)) (co (cfv (cv x3) (cv x2)) (cfv (cv x4) (cv x2)) cmul)) (wbr (cfv (co (cv x3) (cv x4) (cfv (cv x1) cplusg)) (cv x2)) (co (cfv (cv x3) (cv x2)) (cfv (cv x4) (cv x2)) caddc) cle)) (λ x4 . cfv (cv x1) cbs))) (λ x3 . cfv (cv x1) cbs)) (λ x2 . co (co cc0 cpnf cico) (cfv (cv x1) cbs) cmap))) ⟶ wceq cstf (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) cbs) (λ x2 . cfv (cv x2) (cfv (cv x1) cstv)))) ⟶ wceq csr (cab (λ x1 . wsbc (λ x2 . wa (wcel (cv x2) (co (cv x1) (cfv (cv x1) coppr) crh)) (wceq (cv x2) (ccnv (cv x2)))) (cfv (cv x1) cstf))) ⟶ wceq clmod (crab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wsbc (λ x5 . wsbc (λ x6 . wsbc (λ x7 . wsbc (λ x8 . wa (wcel (cv x4) crg) (wral (λ x9 . wral (λ x10 . wral (λ x11 . wral (λ x12 . wa (w3a (wcel (co (cv x10) (cv x12) (cv x5)) (cv x2)) (wceq (co (cv x10) (co (cv x12) (cv x11) (cv x3)) (cv x5)) (co (co (cv x10) (cv x12) (cv x5)) (co (cv x10) (cv x11) (cv x5)) (cv x3))) (wceq (co (co (cv x9) (cv x10) (cv x7)) (cv x12) (cv x5)) (co (co (cv x9) (cv x12) (cv x5)) (co (cv x10) (cv x12) (cv x5)) (cv x3)))) (wa (wceq (co (co (cv x9) (cv x10) (cv x8)) (cv x12) (cv x5)) (co (cv x9) (co (cv x10) (cv x12) (cv x5)) (cv x5))) (wceq (co (cfv (cv x4) cur) (cv x12) (cv x5)) (cv x12)))) (λ x12 . cv x2)) (λ x11 . cv x2)) (λ x10 . cv x6)) (λ x9 . cv x6))) (cfv (cv x4) cmulr)) (cfv (cv x4) cplusg)) (cfv (cv x4) cbs)) (cfv (cv x1) cvsca)) (cfv (cv x1) csca)) (cfv (cv x1) cplusg)) (cfv (cv x1) cbs)) (λ x1 . cgrp)) ⟶ wceq cscaf (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . cfv (cfv (cv x1) csca) cbs) (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . co (cv x2) (cv x3) (cfv (cv x1) cvsca)))) ⟶ wceq clss (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wral (λ x3 . wral (λ x4 . wral (λ x5 . wcel (co (co (cv x3) (cv x4) (cfv (cv x1) cvsca)) (cv x5) (cfv (cv x1) cplusg)) (cv x2)) (λ x5 . cv x2)) (λ x4 . cv x2)) (λ x3 . cfv (cfv (cv x1) csca) cbs)) (λ x2 . cdif (cpw (cfv (cv x1) cbs)) (csn c0)))) ⟶ wceq clspn (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cpw (cfv (cv x1) cbs)) (λ x2 . cint (crab (λ x3 . wss (cv x2) (cv x3)) (λ x3 . cfv (cv x1) clss))))) ⟶ wceq clmhm (cmpt2 (λ x1 x2 . clmod) (λ x1 x2 . clmod) (λ x1 x2 . crab (λ x3 . wsbc (λ x4 . wa (wceq (cfv (cv x2) csca) (cv x4)) (wral (λ x5 . wral (λ x6 . wceq (cfv (co (cv x5) (cv x6) (cfv (cv x1) cvsca)) (cv x3)) (co (cv x5) (cfv (cv x6) (cv x3)) (cfv (cv x2) cvsca))) (λ x6 . cfv (cv x1) cbs)) (λ x5 . cfv (cv x4) cbs))) (cfv (cv x1) csca)) (λ x3 . co (cv x1) (cv x2) cghm))) ⟶ wceq clmim (cmpt2 (λ x1 x2 . clmod) (λ x1 x2 . clmod) (λ x1 x2 . crab (λ x3 . wf1o (cfv (cv x1) cbs) (cfv (cv x2) cbs) (cv x3)) (λ x3 . co (cv x1) (cv x2) clmhm))) ⟶ wceq clmic (cima (ccnv clmim) (cdif cvv c1o)) ⟶ wceq clbs (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wa (wceq (cfv (cv x2) (cv x3)) (cfv (cv x1) cbs)) (wral (λ x5 . wral (λ x6 . wn (wcel (co (cv x6) (cv x5) (cfv (cv x1) cvsca)) (cfv (cdif (cv x2) (csn (cv x5))) (cv x3)))) (λ x6 . cdif (cfv (cv x4) cbs) (csn (cfv (cv x4) c0g)))) (λ x5 . cv x2))) (cfv (cv x1) csca)) (cfv (cv x1) clspn)) (λ x2 . cpw (cfv (cv x1) cbs)))) ⟶ x0) ⟶ x0
Theorem df_rnghom : wceq crh (cmpt2 (λ x0 x1 . crg) (λ x0 x1 . crg) (λ x0 x1 . csb (cfv (cv x0) cbs) (λ x2 . csb (cfv (cv x1) cbs) (λ x3 . crab (λ x4 . wa (wceq (cfv (cfv (cv x0) cur) (cv x4)) (cfv (cv x1) cur)) (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_rngiso : wceq crs (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . crab (λ x2 . wcel (ccnv (cv x2)) (co (cv x1) (cv x0) crh)) (λ x2 . co (cv x0) (cv x1) crh))) (proof)
Theorem df_ric : wceq cric (cima (ccnv crs) (cdif cvv c1o)) (proof)
Theorem df_drng : wceq cdr (crab (λ x0 . wceq (cfv (cv x0) cui) (cdif (cfv (cv x0) cbs) (csn (cfv (cv x0) c0g)))) (λ x0 . crg)) (proof)
Theorem df_field : wceq cfield (cin cdr ccrg) (proof)
Theorem df_subrg : wceq csubrg (cmpt (λ x0 . crg) (λ x0 . crab (λ x1 . wa (wcel (co (cv x0) (cv x1) cress) crg) (wcel (cfv (cv x0) cur) (cv x1))) (λ x1 . cpw (cfv (cv x0) cbs)))) (proof)
Theorem df_rgspn : wceq crgspn (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cpw (cfv (cv x0) cbs)) (λ x1 . cint (crab (λ x2 . wss (cv x1) (cv x2)) (λ x2 . cfv (cv x0) csubrg))))) (proof)
Theorem df_abv : wceq cabv (cmpt (λ x0 . crg) (λ x0 . crab (λ x1 . wral (λ x2 . wa (wb (wceq (cfv (cv x2) (cv x1)) cc0) (wceq (cv x2) (cfv (cv x0) c0g))) (wral (λ x3 . wa (wceq (cfv (co (cv x2) (cv x3) (cfv (cv x0) cmulr)) (cv x1)) (co (cfv (cv x2) (cv x1)) (cfv (cv x3) (cv x1)) cmul)) (wbr (cfv (co (cv x2) (cv x3) (cfv (cv x0) cplusg)) (cv x1)) (co (cfv (cv x2) (cv x1)) (cfv (cv x3) (cv x1)) caddc) cle)) (λ x3 . cfv (cv x0) cbs))) (λ x2 . cfv (cv x0) cbs)) (λ x1 . co (co cc0 cpnf cico) (cfv (cv x0) cbs) cmap))) (proof)
Theorem df_staf : wceq cstf (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) cbs) (λ x1 . cfv (cv x1) (cfv (cv x0) cstv)))) (proof)
Theorem df_srng : wceq csr (cab (λ x0 . wsbc (λ x1 . wa (wcel (cv x1) (co (cv x0) (cfv (cv x0) coppr) crh)) (wceq (cv x1) (ccnv (cv x1)))) (cfv (cv x0) cstf))) (proof)
Theorem df_lmod : wceq clmod (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wsbc (λ x5 . wsbc (λ x6 . wsbc (λ x7 . wa (wcel (cv x3) crg) (wral (λ x8 . wral (λ x9 . wral (λ x10 . wral (λ x11 . wa (w3a (wcel (co (cv x9) (cv x11) (cv x4)) (cv x1)) (wceq (co (cv x9) (co (cv x11) (cv x10) (cv x2)) (cv x4)) (co (co (cv x9) (cv x11) (cv x4)) (co (cv x9) (cv x10) (cv x4)) (cv x2))) (wceq (co (co (cv x8) (cv x9) (cv x6)) (cv x11) (cv x4)) (co (co (cv x8) (cv x11) (cv x4)) (co (cv x9) (cv x11) (cv x4)) (cv x2)))) (wa (wceq (co (co (cv x8) (cv x9) (cv x7)) (cv x11) (cv x4)) (co (cv x8) (co (cv x9) (cv x11) (cv x4)) (cv x4))) (wceq (co (cfv (cv x3) cur) (cv x11) (cv x4)) (cv x11)))) (λ x11 . cv x1)) (λ x10 . cv x1)) (λ x9 . cv x5)) (λ x8 . cv x5))) (cfv (cv x3) cmulr)) (cfv (cv x3) cplusg)) (cfv (cv x3) cbs)) (cfv (cv x0) cvsca)) (cfv (cv x0) csca)) (cfv (cv x0) cplusg)) (cfv (cv x0) cbs)) (λ x0 . cgrp)) (proof)
Theorem df_scaf : wceq cscaf (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cfv (cfv (cv x0) csca) cbs) (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . co (cv x1) (cv x2) (cfv (cv x0) cvsca)))) (proof)
Theorem df_lss : wceq clss (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wral (λ x2 . wral (λ x3 . wral (λ x4 . wcel (co (co (cv x2) (cv x3) (cfv (cv x0) cvsca)) (cv x4) (cfv (cv x0) cplusg)) (cv x1)) (λ x4 . cv x1)) (λ x3 . cv x1)) (λ x2 . cfv (cfv (cv x0) csca) cbs)) (λ x1 . cdif (cpw (cfv (cv x0) cbs)) (csn c0)))) (proof)
Theorem df_lsp : wceq clspn (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cpw (cfv (cv x0) cbs)) (λ x1 . cint (crab (λ x2 . wss (cv x1) (cv x2)) (λ x2 . cfv (cv x0) clss))))) (proof)
Theorem df_lmhm : wceq clmhm (cmpt2 (λ x0 x1 . clmod) (λ x0 x1 . clmod) (λ x0 x1 . crab (λ x2 . wsbc (λ x3 . wa (wceq (cfv (cv x1) csca) (cv x3)) (wral (λ x4 . wral (λ x5 . wceq (cfv (co (cv x4) (cv x5) (cfv (cv x0) cvsca)) (cv x2)) (co (cv x4) (cfv (cv x5) (cv x2)) (cfv (cv x1) cvsca))) (λ x5 . cfv (cv x0) cbs)) (λ x4 . cfv (cv x3) cbs))) (cfv (cv x0) csca)) (λ x2 . co (cv x0) (cv x1) cghm))) (proof)
Theorem df_lmim : wceq clmim (cmpt2 (λ x0 x1 . clmod) (λ x0 x1 . clmod) (λ x0 x1 . crab (λ x2 . wf1o (cfv (cv x0) cbs) (cfv (cv x1) cbs) (cv x2)) (λ x2 . co (cv x0) (cv x1) clmhm))) (proof)
Theorem df_lmic : wceq clmic (cima (ccnv clmim) (cdif cvv c1o)) (proof)
Theorem df_lbs : wceq clbs (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wa (wceq (cfv (cv x1) (cv x2)) (cfv (cv x0) cbs)) (wral (λ x4 . wral (λ x5 . wn (wcel (co (cv x5) (cv x4) (cfv (cv x0) cvsca)) (cfv (cdif (cv x1) (csn (cv x4))) (cv x2)))) (λ x5 . cdif (cfv (cv x3) cbs) (csn (cfv (cv x3) c0g)))) (λ x4 . cv x1))) (cfv (cv x0) csca)) (cfv (cv x0) clspn)) (λ x1 . cpw (cfv (cv x0) cbs)))) (proof)