Nuprl Lemma : Euclid-Prop4

e:EuclideanPlane. ∀a,b,c,A,B,C:Point.
  ((Triangle(a;b;c) ∧ Triangle(A;B;C))
   (ab ≅ AB ∧ ac ≅ AC ∧ bac ≅a BAC)
   (bc ≅ BC ∧ abc ≅a ABC ∧ bca ≅a BCA ∧ Cong3(abc,ABC)))


Proof




Definitions occuring in Statement :  geo-cong-tri: Cong3(abc,a'b'c') geo-cong-angle: abc ≅a xyz geo-tri: Triangle(a;b;c) euclidean-plane: EuclideanPlane geo-congruent: ab ≅ cd geo-point: Point all: x:A. B[x] implies:  Q and: P ∧ Q
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q and: P ∧ Q cand: c∧ B member: t ∈ T uall: [x:A]. B[x] subtype_rel: A ⊆B guard: {T} uimplies: supposing a prop: basic-geometry: BasicGeometry geo-tri: Triangle(a;b;c) geo-cong-angle: abc ≅a xyz exists: x:A. B[x] uiff: uiff(P;Q) geo-cong-tri: Cong3(abc,a'b'c')
Lemmas referenced :  geo-congruent_wf euclidean-plane-structure-subtype euclidean-plane-subtype subtype_rel_transitivity euclidean-plane_wf euclidean-plane-structure_wf geo-primitives_wf geo-cong-angle_wf geo-tri_wf geo-point_wf geo-sas geo-between_wf geo-between-trivial geo-congruent-iff-length geo-length-flip
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt sqequalHypSubstitution productElimination thin cut independent_pairFormation hypothesis sqequalRule productIsType universeIsType introduction extract_by_obid isectElimination hypothesisEquality applyEquality instantiate independent_isectElimination because_Cache dependent_functionElimination inhabitedIsType dependent_pairFormation_alt equalityTransitivity equalitySymmetry

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,A,B,C:Point.
    ((Triangle(a;b;c)  \mwedge{}  Triangle(A;B;C))
    {}\mRightarrow{}  (ab  \mcong{}  AB  \mwedge{}  ac  \mcong{}  AC  \mwedge{}  bac  \mcong{}\msuba{}  BAC)
    {}\mRightarrow{}  (bc  \mcong{}  BC  \mwedge{}  abc  \mcong{}\msuba{}  ABC  \mwedge{}  bca  \mcong{}\msuba{}  BCA  \mwedge{}  Cong3(abc,ABC)))



Date html generated: 2019_10_16-PM-01_42_14
Last ObjectModification: 2018_11_07-PM-01_00_52

Theory : euclidean!plane!geometry


Home Index