Nuprl Lemma : module_hom_p_wf

a:RngSig. ∀m,n:algebra_sig{i:l}(|a|). ∀f:m.car ⟶ n.car.  (module_hom_p(a; m; n; f) ∈ ℙ)


Proof




Definitions occuring in Statement :  module_hom_p: module_hom_p(a; m; n; f) alg_car: a.car algebra_sig: algebra_sig{i:l}(A) prop: all: x:A. B[x] member: t ∈ T function: x:A ⟶ B[x] rng_car: |r| rng_sig: RngSig
Definitions unfolded in proof :  module_hom_p: module_hom_p(a; m; n; f) all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  and_wf fun_thru_2op_wf alg_car_wf rng_car_wf alg_plus_wf all_wf fun_thru_1op_wf alg_act_wf algebra_sig_wf rng_sig_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin dependent_functionElimination hypothesisEquality hypothesis lambdaEquality applyEquality functionEquality

Latex:
\mforall{}a:RngSig.  \mforall{}m,n:algebra\_sig\{i:l\}(|a|).  \mforall{}f:m.car  {}\mrightarrow{}  n.car.    (module\_hom\_p(a;  m;  n;  f)  \mmember{}  \mBbbP{})



Date html generated: 2016_05_16-AM-07_27_05
Last ObjectModification: 2015_12_28-PM-05_07_41

Theory : algebras_1


Home Index