Nuprl Lemma : rng_times_when_l

[r:Rng]. ∀[u,v:|r|]. ∀[b:𝔹].  ((u (when b. v)) (when b. (u v)) ∈ |r|)


Proof




Definitions occuring in Statement :  rng_when: rng_when rng: Rng rng_times: * rng_car: |r| bool: 𝔹 uall: [x:A]. B[x] infix_ap: y equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T rng_when: rng_when mon_when: when b. p bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  bfalse: ff add_grp_of_rng: r↓+gp grp_id: e pi2: snd(t) pi1: fst(t) rng: Rng squash: T prop: and: P ∧ Q true: True subtype_rel: A ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q rev_implies:  Q implies:  Q
Lemmas referenced :  bool_wf rng_car_wf rng_wf infix_ap_wf rng_times_wf equal_wf squash_wf true_wf rng_times_zero rng_zero_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution unionElimination thin equalityElimination sqequalRule hypothesis extract_by_obid isect_memberEquality isectElimination hypothesisEquality axiomEquality because_Cache setElimination rename applyEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry universeEquality productElimination natural_numberEquality imageMemberEquality baseClosed independent_isectElimination independent_functionElimination

Latex:
\mforall{}[r:Rng].  \mforall{}[u,v:|r|].  \mforall{}[b:\mBbbB{}].    ((u  *  (when  b.  v))  =  (when  b.  (u  *  v)))



Date html generated: 2017_10_01-AM-08_19_44
Last ObjectModification: 2017_02_28-PM-02_04_06

Theory : rings_1


Home Index