### 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