Nuprl Lemma : geo-perp-symmetry

e:BasicGeometry. ∀a,b,c,d:Point.  (ab ⊥ cd  cd ⊥ ab)


Proof




Definitions occuring in Statement :  geo-perp: ab ⊥ cd basic-geometry: BasicGeometry geo-point: Point all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T uall: [x:A]. B[x] guard: {T} and: P ∧ Q cand: c∧ B prop: subtype_rel: A ⊆B uimplies: supposing a
Lemmas referenced :  geo-perp-all-symmetry geo-perp_wf geo-point_wf euclidean-plane-structure-subtype euclidean-plane-subtype basic-geometry-subtype subtype_rel_transitivity basic-geometry_wf euclidean-plane_wf euclidean-plane-structure_wf geo-primitives_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality isectElimination independent_functionElimination hypothesis productElimination universeIsType inhabitedIsType applyEquality instantiate independent_isectElimination sqequalRule

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,d:Point.    (ab  \mbot{}  cd  {}\mRightarrow{}  cd  \mbot{}  ab)



Date html generated: 2019_10_16-PM-01_29_15
Last ObjectModification: 2018_12_11-PM-06_11_25

Theory : euclidean!plane!geometry


Home Index