---

Step * of Lemma geo-congruent-functionality-lemma

No Annotations
∀g:EuclideanPlane
  ((∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc))
  ⇒ (∀a1,a2,b1,b2,c1,c2,d1,d2:Point.  (a1 ≡ a2 ⇒ b1 ≡ b2 ⇒ c1 ≡ c2 ⇒ d1 ≡ d2 ⇒ a1b1 ≅ c1d1 ⇒ a2b2 ≅ c2d2)))
BY
{ (Auto
   THEN (Assert a1b1 ≅ a2b2 BY
               ((Assert a1b1 ≅ a2b1 BY
                       (InstHyp [⌜a1⌝;⌜a2⌝;⌜b1⌝] (2)⋅ THEN Auto))
                THEN (Assert a2b1 ≅ b1a2 BY
                            (InstLemma `geo-congruent-full-symmetry` [⌜g⌝]⋅ THEN Auto))
                THEN (Assert b1a2 ≅ b2a2 BY
                            (InstHyp [⌜b1⌝;⌜b2⌝;⌜a2⌝] (2)⋅ THEN Auto))
                THEN (Assert b2a2 ≅ a2b2 BY
                            (InstLemma `geo-congruent-full-symmetry` [⌜g⌝]⋅ THEN Auto))
                THEN (FLemma `geo-congruent-transitivity` [-4;-3] THENA Auto)
                THEN RepeatFor 2 ((FLemma `geo-congruent-transitivity` [-1;-3] THENA Auto))
                THEN Auto))
   THEN (Assert c1d1 ≅ c2d2 BY
               ((Assert c1d1 ≅ c2d1 BY
                       (InstHyp [⌜c1⌝;⌜c2⌝;⌜d1⌝] (2)⋅ THEN Auto))
                THEN (Assert c2d1 ≅ d1c2 BY
                            (InstLemma `geo-congruent-full-symmetry` [⌜g⌝]⋅ THEN Auto))
                THEN (Assert d1c2 ≅ d2c2 BY
                            (InstHyp [⌜d1⌝;⌜d2⌝;⌜c2⌝] (2)⋅ THEN Auto))
                THEN (Assert d2c2 ≅ c2d2 BY
                            (InstLemma `geo-congruent-full-symmetry` [⌜g⌝]⋅ THEN Auto))
                THEN (FLemma `geo-congruent-transitivity` [-4;-3] THENA Auto)
                THEN RepeatFor 2 ((FLemma `geo-congruent-transitivity` [-1;-3] THENA Auto))
                THEN Auto))) }

1
1. g : EuclideanPlane
2. ∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc)
3. a1 : Point
4. a2 : Point
5. b1 : Point
6. b2 : Point
7. c1 : Point
8. c2 : Point
9. d1 : Point
10. d2 : Point
11. a1 ≡ a2
12. b1 ≡ b2
13. c1 ≡ c2
14. d1 ≡ d2
15. a1b1 ≅ c1d1
16. a1b1 ≅ a2b2
17. c1d1 ≅ c2d2
⊢ a2b2 ≅ c2d2

---

Latex:

---

Latex:
No  Annotations
\mforall{}g:EuclideanPlane
    ((\mforall{}a,b,c:Point.    (a  \mequiv{}  b  {}\mRightarrow{}  ac  \mcong{}  bc))
    {}\mRightarrow{}  (\mforall{}a1,a2,b1,b2,c1,c2,d1,d2:Point.
                (a1  \mequiv{}  a2  {}\mRightarrow{}  b1  \mequiv{}  b2  {}\mRightarrow{}  c1  \mequiv{}  c2  {}\mRightarrow{}  d1  \mequiv{}  d2  {}\mRightarrow{}  a1b1  \mcong{}  c1d1  {}\mRightarrow{}  a2b2  \mcong{}  c2d2)))


By

---

Latex:
(Auto
  THEN  (Assert  a1b1  \mcong{}  a2b2  BY
                          ((Assert  a1b1  \mcong{}  a2b1  BY
                                          (InstHyp  [\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}a2\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{}]  (2)\mcdot{}  THEN  Auto))
                            THEN  (Assert  a2b1  \mcong{}  b1a2  BY
                                                    (InstLemma  `geo-congruent-full-symmetry`  [\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THEN  Auto))
                            THEN  (Assert  b1a2  \mcong{}  b2a2  BY
                                                    (InstHyp  [\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}b2\mkleeneclose{};\mkleeneopen{}a2\mkleeneclose{}]  (2)\mcdot{}  THEN  Auto))
                            THEN  (Assert  b2a2  \mcong{}  a2b2  BY
                                                    (InstLemma  `geo-congruent-full-symmetry`  [\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THEN  Auto))
                            THEN  (FLemma  `geo-congruent-transitivity`  [-4;-3]  THENA  Auto)
                            THEN  RepeatFor  2  ((FLemma  `geo-congruent-transitivity`  [-1;-3]  THENA  Auto))
                            THEN  Auto))
  THEN  (Assert  c1d1  \mcong{}  c2d2  BY
                          ((Assert  c1d1  \mcong{}  c2d1  BY
                                          (InstHyp  [\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}c2\mkleeneclose{};\mkleeneopen{}d1\mkleeneclose{}]  (2)\mcdot{}  THEN  Auto))
                            THEN  (Assert  c2d1  \mcong{}  d1c2  BY
                                                    (InstLemma  `geo-congruent-full-symmetry`  [\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THEN  Auto))
                            THEN  (Assert  d1c2  \mcong{}  d2c2  BY
                                                    (InstHyp  [\mkleeneopen{}d1\mkleeneclose{};\mkleeneopen{}d2\mkleeneclose{};\mkleeneopen{}c2\mkleeneclose{}]  (2)\mcdot{}  THEN  Auto))
                            THEN  (Assert  d2c2  \mcong{}  c2d2  BY
                                                    (InstLemma  `geo-congruent-full-symmetry`  [\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THEN  Auto))
                            THEN  (FLemma  `geo-congruent-transitivity`  [-4;-3]  THENA  Auto)
                            THEN  RepeatFor  2  ((FLemma  `geo-congruent-transitivity`  [-1;-3]  THENA  Auto))
                            THEN  Auto)))

---

Home Index