Nuprl Lemma : comm_shift

[A,B:Type]. ∀[opa:A ⟶ A ⟶ A]. ∀[opb:B ⟶ B ⟶ B]. ∀[f:A ⟶ B].
  (Comm(A;opa)) supposing (Comm(B;opb) and FunThru2op(A;B;opa;opb;f) and Inj(A;B;f))


Proof




Definitions occuring in Statement :  fun_thru_2op: FunThru2op(A;B;opa;opb;f) comm: Comm(T;op) inject: Inj(A;B;f) uimplies: supposing a uall: [x:A]. B[x] function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a comm: Comm(T;op) fun_thru_2op: FunThru2op(A;B;opa;opb;f) inject: Inj(A;B;f) prop: all: x:A. B[x] infix_ap: y implies:  Q squash: T true: True subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q
Lemmas referenced :  comm_wf fun_thru_2op_wf inject_wf equal_wf squash_wf true_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution hypothesis hypothesisEquality sqequalRule isect_memberEquality isectElimination thin axiomEquality because_Cache extract_by_obid cumulativity functionExtensionality applyEquality equalityTransitivity equalitySymmetry functionEquality universeEquality dependent_functionElimination independent_functionElimination lambdaEquality imageElimination natural_numberEquality imageMemberEquality baseClosed independent_isectElimination productElimination

Latex:
\mforall{}[A,B:Type].  \mforall{}[opa:A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].  \mforall{}[opb:B  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[f:A  {}\mrightarrow{}  B].
    (Comm(A;opa))  supposing  (Comm(B;opb)  and  FunThru2op(A;B;opa;opb;f)  and  Inj(A;B;f))



Date html generated: 2017_10_01-AM-08_13_03
Last ObjectModification: 2017_02_28-PM-01_57_21

Theory : gen_algebra_1


Home Index