Nuprl Lemma : rng_when_swap

[r:Rng]. ∀[b,b':𝔹]. ∀[p:|r|].  ((when b. when b'. p) (when b'. when b. p) ∈ |r|)


Proof




Definitions occuring in Statement :  rng_when: rng_when rng: Rng rng_car: |r| bool: 𝔹 uall: [x:A]. B[x] equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B grp: Group{i} rng_when: rng_when add_grp_of_rng: r↓+gp grp_car: |g| pi1: fst(t) rng: Rng
Lemmas referenced :  mon_when_swap add_grp_of_rng_wf_a grp_wf rng_car_wf bool_wf rng_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis applyEquality lambdaEquality setElimination rename sqequalRule isect_memberEquality axiomEquality

Latex:
\mforall{}[r:Rng].  \mforall{}[b,b':\mBbbB{}].  \mforall{}[p:|r|].    ((when  b.  when  b'.  p)  =  (when  b'.  when  b.  p))



Date html generated: 2016_05_15-PM-00_29_16
Last ObjectModification: 2015_12_26-PM-11_58_13

Theory : rings_1


Home Index