Nuprl Lemma : geo-cong-angle_functionality
∀e:EuclideanPlane. ∀a1,a2,b1,b2,c1,c2,d1,d2,f1,f2,g1,g2:Point.
  (a1 ≡ a2 
⇒ b1 ≡ b2 
⇒ c1 ≡ c2 
⇒ d1 ≡ d2 
⇒ f1 ≡ f2 
⇒ g1 ≡ g2 
⇒ (a1b1c1 ≅a d1f1g1 
⇐⇒ a2b2c2 ≅a d2f2g2))
Proof
Definitions occuring in Statement : 
geo-cong-angle: abc ≅a xyz
, 
euclidean-plane: EuclideanPlane
, 
geo-eq: a ≡ b
, 
geo-point: Point
, 
all: ∀x:A. B[x]
, 
iff: P 
⇐⇒ Q
, 
implies: P 
⇒ Q
Definitions unfolded in proof : 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
iff: P 
⇐⇒ Q
, 
and: P ∧ Q
, 
geo-cong-angle: abc ≅a xyz
, 
member: t ∈ T
, 
uall: ∀[x:A]. B[x]
, 
basic-geometry: BasicGeometry
, 
prop: ℙ
, 
rev_implies: P 
⇐ Q
, 
subtype_rel: A ⊆r B
, 
guard: {T}
, 
uimplies: b supposing a
, 
exists: ∃x:A. B[x]
Lemmas referenced : 
geo-cong-angle_wf, 
geo-eq_wf, 
euclidean-plane-structure-subtype, 
euclidean-plane-subtype, 
subtype_rel_transitivity, 
euclidean-plane_wf, 
euclidean-plane-structure_wf, 
geo-primitives_wf, 
geo-point_wf, 
geo-between_wf, 
geo-congruent_wf, 
geo-sep_functionality, 
geo-eq_weakening, 
geo-between_functionality, 
geo-congruent_functionality
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
lambdaFormation_alt, 
independent_pairFormation, 
sqequalHypSubstitution, 
universeIsType, 
cut, 
introduction, 
extract_by_obid, 
isectElimination, 
thin, 
sqequalRule, 
hypothesisEquality, 
hypothesis, 
applyEquality, 
instantiate, 
independent_isectElimination, 
because_Cache, 
inhabitedIsType, 
productIsType, 
productElimination, 
promote_hyp, 
dependent_functionElimination, 
independent_functionElimination, 
dependent_pairFormation_alt
Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a1,a2,b1,b2,c1,c2,d1,d2,f1,f2,g1,g2:Point.
    (a1  \mequiv{}  a2
    {}\mRightarrow{}  b1  \mequiv{}  b2
    {}\mRightarrow{}  c1  \mequiv{}  c2
    {}\mRightarrow{}  d1  \mequiv{}  d2
    {}\mRightarrow{}  f1  \mequiv{}  f2
    {}\mRightarrow{}  g1  \mequiv{}  g2
    {}\mRightarrow{}  (a1b1c1  \mcong{}\msuba{}  d1f1g1  \mLeftarrow{}{}\mRightarrow{}  a2b2c2  \mcong{}\msuba{}  d2f2g2))
Date html generated:
2019_10_16-PM-01_27_30
Last ObjectModification:
2018_11_07-PM-00_58_08
Theory : euclidean!plane!geometry
Home
Index