Nuprl Lemma : grp_op_r

[g:GrpSig]. ∀[a,b,c:|g|].  (a c) (b c) ∈ |g| supposing b ∈ |g|


Proof




Definitions occuring in Statement :  grp_op: * grp_car: |g| grp_sig: GrpSig uimplies: supposing a uall: [x:A]. B[x] infix_ap: y equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a prop: infix_ap: y
Lemmas referenced :  equal_wf grp_car_wf grp_sig_wf infix_ap_wf grp_op_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule isect_memberEquality axiomEquality because_Cache equalityTransitivity equalitySymmetry hyp_replacement Error :applyLambdaEquality,  applyEquality

Latex:
\mforall{}[g:GrpSig].  \mforall{}[a,b,c:|g|].    (a  *  c)  =  (b  *  c)  supposing  a  =  b



Date html generated: 2016_10_21-AM-11_25_18
Last ObjectModification: 2016_07_12-PM-01_05_50

Theory : groups_1


Home Index