Nuprl Lemma : straight-angle-sum1_symm

e:EuclideanPlane. ∀a,b,c,x,y,z,i,j,k:Point.  (abc xyz ≅ ijk  x-y-z  out(b ac))


Proof




Definitions occuring in Statement :  hp-angle-sum: abc xyz ≅ def geo-out: out(p ab) euclidean-plane: EuclideanPlane geo-strict-between: a-b-c geo-point: Point all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q hp-angle-sum: abc xyz ≅ def exists: x:A. B[x] and: P ∧ Q geo-cong-angle: abc ≅a xyz cand: c∧ B member: t ∈ T uall: [x:A]. B[x] uimplies: supposing a basic-geometry-: BasicGeometry- subtype_rel: A ⊆B guard: {T} prop: basic-geometry: BasicGeometry geo-out: out(p ab) iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  geo-sep-sym angle-cong-preserves-straight-angle geo-between-symmetry geo-strict-between-implies-between geo-strict-between_wf euclidean-plane-structure-subtype euclidean-plane-subtype subtype_rel_transitivity euclidean-plane_wf euclidean-plane-structure_wf geo-primitives_wf hp-angle-sum_wf geo-point_wf angle-cong-preserves-zero-angle geo-out_transitivity geo-out_inversion geo-out-iff-between1 geo-strict-between-sep3 extended-out-preserves-between geo-between-inner-trans geo-between-exchange3 geo-between-exchange4
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt sqequalHypSubstitution productElimination thin cut introduction extract_by_obid dependent_functionElimination hypothesisEquality independent_functionElimination hypothesis independent_pairFormation because_Cache isectElimination independent_isectElimination sqequalRule universeIsType applyEquality instantiate inhabitedIsType

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y,z,i,j,k:Point.    (abc  +  xyz  \mcong{}  ijk  {}\mRightarrow{}  x-y-z  {}\mRightarrow{}  out(b  ac))



Date html generated: 2019_10_16-PM-02_04_50
Last ObjectModification: 2019_06_24-AM-10_15_40

Theory : euclidean!plane!geometry


Home Index