Nuprl Lemma : grp_op_polarity

[g:OGrp]. ∀[a,b:|g|].  (e ≤ (a b)) supposing ((e ≤ b) and (e ≤ a))


Proof




Definitions occuring in Statement :  ocgrp: OGrp grp_leq: a ≤ b grp_id: e grp_op: * grp_car: |g| uimplies: supposing a uall: [x:A]. B[x] infix_ap: y
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a grp_leq: a ≤ b infix_ap: y ocgrp: OGrp ocmon: OCMon abmonoid: AbMon mon: Mon implies:  Q prop: uiff: uiff(P;Q) and: P ∧ Q squash: T subtype_rel: A ⊆B guard: {T} true: True iff: ⇐⇒ Q
Lemmas referenced :  grp_leq_transitivity iff_weakening_equal imon_wf iabmonoid_wf abmonoid_wf abdmonoid_wf ocmon_wf subtype_rel_transitivity ocgrp_subtype_ocmon ocmon_subtype_abdmonoid abdmonoid_abmonoid abmonoid_subtype_iabmonoid iabmonoid_subtype_imon mon_ident grp_sig_wf true_wf squash_wf grp_leq_op_l ocgrp_wf grp_car_wf grp_leq_wf grp_op_wf grp_id_wf grp_le_wf assert_witness
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution lemma_by_obid isectElimination thin applyEquality setElimination rename hypothesisEquality hypothesis independent_functionElimination isect_memberEquality because_Cache equalityTransitivity equalitySymmetry productElimination independent_isectElimination lambdaEquality imageElimination instantiate natural_numberEquality imageMemberEquality baseClosed universeEquality

Latex:
\mforall{}[g:OGrp].  \mforall{}[a,b:|g|].    (e  \mleq{}  (a  *  b))  supposing  ((e  \mleq{}  b)  and  (e  \mleq{}  a))



Date html generated: 2016_05_15-PM-00_13_26
Last ObjectModification: 2016_01_15-PM-11_05_14

Theory : groups_1


Home Index