### Nuprl Lemma : ring_p_wf

[T:Type]. ∀[pl:T ⟶ T ⟶ T]. ∀[zero:T]. ∀[neg:T ⟶ T]. ∀[tm:T ⟶ T ⟶ T]. ∀[one:T].  (IsRing(T;pl;zero;neg;tm;one) ∈ ℙ)

Proof

Definitions occuring in Statement :  ring_p: IsRing(T;plus;zero;neg;times;one) uall: [x:A]. B[x] prop: member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  ring_p: IsRing(T;plus;zero;neg;times;one) uall: [x:A]. B[x] member: t ∈ T
Lemmas referenced :  and_wf group_p_wf monoid_p_wf bilinear_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache functionEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[pl:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T].  \mforall{}[zero:T].  \mforall{}[neg:T  {}\mrightarrow{}  T].  \mforall{}[tm:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T].  \mforall{}[one:T].
(IsRing(T;pl;zero;neg;tm;one)  \mmember{}  \mBbbP{})

Date html generated: 2016_05_15-PM-00_20_21
Last ObjectModification: 2015_12_27-AM-00_02_58

Theory : rings_1

Home Index