MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tgasa1 Structured version   Visualization version   GIF version

Theorem tgasa1 28867
Description: Second congruence theorem: ASA. (Angle-Side-Angle): If two pairs of angles of two triangles are equal in measurement, and the included sides are equal in length, then the triangles are congruent. Theorem 11.50 of [Schwabhauser] p. 108. (Contributed by Thierry Arnoux, 15-Aug-2020.)
Hypotheses
Ref Expression
tgsas.p 𝑃 = (Base‘𝐺)
tgsas.m = (dist‘𝐺)
tgsas.i 𝐼 = (Itv‘𝐺)
tgsas.g (𝜑𝐺 ∈ TarskiG)
tgsas.a (𝜑𝐴𝑃)
tgsas.b (𝜑𝐵𝑃)
tgsas.c (𝜑𝐶𝑃)
tgsas.d (𝜑𝐷𝑃)
tgsas.e (𝜑𝐸𝑃)
tgsas.f (𝜑𝐹𝑃)
tgasa.l 𝐿 = (LineG‘𝐺)
tgasa.1 (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
tgasa.2 (𝜑 → (𝐴 𝐵) = (𝐷 𝐸))
tgasa.3 (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
tgasa.4 (𝜑 → ⟨“𝐶𝐴𝐵”⟩(cgrA‘𝐺)⟨“𝐹𝐷𝐸”⟩)
Assertion
Ref Expression
tgasa1 (𝜑 → (𝐵 𝐶) = (𝐸 𝐹))

Proof of Theorem tgasa1
Dummy variables 𝑎 𝑏 𝑓 𝑤 𝑡 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simprr 772 . . 3 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → (𝐸 𝑓) = (𝐵 𝐶))
2 tgsas.p . . . . 5 𝑃 = (Base‘𝐺)
3 tgsas.i . . . . 5 𝐼 = (Itv‘𝐺)
4 tgasa.l . . . . 5 𝐿 = (LineG‘𝐺)
5 tgsas.g . . . . . 6 (𝜑𝐺 ∈ TarskiG)
65ad2antrr 726 . . . . 5 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝐺 ∈ TarskiG)
7 tgsas.f . . . . . 6 (𝜑𝐹𝑃)
87ad2antrr 726 . . . . 5 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝐹𝑃)
9 tgsas.d . . . . . 6 (𝜑𝐷𝑃)
109ad2antrr 726 . . . . 5 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝐷𝑃)
11 tgsas.e . . . . . 6 (𝜑𝐸𝑃)
1211ad2antrr 726 . . . . 5 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝐸𝑃)
13 tgsas.m . . . . . . 7 = (dist‘𝐺)
14 tgsas.a . . . . . . 7 (𝜑𝐴𝑃)
15 tgsas.b . . . . . . 7 (𝜑𝐵𝑃)
16 tgsas.c . . . . . . 7 (𝜑𝐶𝑃)
17 tgasa.3 . . . . . . 7 (𝜑 → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
18 tgasa.1 . . . . . . 7 (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
192, 3, 13, 5, 14, 15, 16, 9, 11, 7, 17, 4, 18cgrancol 28838 . . . . . 6 (𝜑 → ¬ (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
2019ad2antrr 726 . . . . 5 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → ¬ (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
21 eqid 2736 . . . . . 6 (hlG‘𝐺) = (hlG‘𝐺)
22 simplr 768 . . . . . 6 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝑓𝑃)
2316ad2antrr 726 . . . . . . 7 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝐶𝑃)
2414ad2antrr 726 . . . . . . 7 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝐴𝑃)
2515ad2antrr 726 . . . . . . 7 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝐵𝑃)
2618ad2antrr 726 . . . . . . 7 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
275ad3antrrr 730 . . . . . . . . 9 ((((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 𝐺 ∈ TarskiG)
289ad3antrrr 730 . . . . . . . . 9 ((((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 𝐷𝑃)
2911ad3antrrr 730 . . . . . . . . 9 ((((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 𝐸𝑃)
307ad3antrrr 730 . . . . . . . . 9 ((((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 𝐹𝑃)
3114ad3antrrr 730 . . . . . . . . 9 ((((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 𝐴𝑃)
3215ad3antrrr 730 . . . . . . . . 9 ((((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 𝐵𝑃)
3316ad3antrrr 730 . . . . . . . . 9 ((((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 𝐶𝑃)
342, 3, 5, 21, 14, 15, 16, 9, 11, 7, 17cgracom 28831 . . . . . . . . . 10 (𝜑 → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
3534ad3antrrr 730 . . . . . . . . 9 ((((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → ⟨“𝐷𝐸𝐹”⟩(cgrA‘𝐺)⟨“𝐴𝐵𝐶”⟩)
36 simpr 484 . . . . . . . . . . 11 ((((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹))
372, 4, 3, 27, 28, 30, 29, 36colcom 28567 . . . . . . . . . 10 ((((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → (𝐸 ∈ (𝐹𝐿𝐷) ∨ 𝐹 = 𝐷))
382, 4, 3, 27, 30, 28, 29, 37colrot1 28568 . . . . . . . . 9 ((((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
392, 3, 13, 27, 28, 29, 30, 31, 32, 33, 35, 4, 38cgracol 28837 . . . . . . . 8 ((((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
4018ad3antrrr 730 . . . . . . . 8 ((((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
4139, 40pm2.65da 816 . . . . . . 7 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → ¬ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹))
42 eqid 2736 . . . . . . . . . 10 (cgrG‘𝐺) = (cgrG‘𝐺)
4317ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝐹”⟩)
44 simprl 770 . . . . . . . . . . . . 13 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝑓((hlG‘𝐺)‘𝐸)𝐹)
452, 3, 21, 6, 24, 25, 23, 10, 12, 8, 43, 22, 44cgrahl2 28826 . . . . . . . . . . . 12 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → ⟨“𝐴𝐵𝐶”⟩(cgrA‘𝐺)⟨“𝐷𝐸𝑓”⟩)
462, 3, 21, 5, 14, 15, 16, 9, 11, 7, 17cgrane1 28821 . . . . . . . . . . . . . 14 (𝜑𝐴𝐵)
472, 3, 21, 14, 14, 15, 5, 46hlid 28618 . . . . . . . . . . . . 13 (𝜑𝐴((hlG‘𝐺)‘𝐵)𝐴)
4847ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝐴((hlG‘𝐺)‘𝐵)𝐴)
492, 3, 21, 5, 14, 15, 16, 9, 11, 7, 17cgrane2 28822 . . . . . . . . . . . . . . 15 (𝜑𝐵𝐶)
5049necomd 2995 . . . . . . . . . . . . . 14 (𝜑𝐶𝐵)
512, 3, 21, 16, 14, 15, 5, 50hlid 28618 . . . . . . . . . . . . 13 (𝜑𝐶((hlG‘𝐺)‘𝐵)𝐶)
5251ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝐶((hlG‘𝐺)‘𝐵)𝐶)
53 tgasa.2 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 𝐵) = (𝐷 𝐸))
542, 13, 3, 5, 14, 15, 9, 11, 53tgcgrcomlr 28489 . . . . . . . . . . . . 13 (𝜑 → (𝐵 𝐴) = (𝐸 𝐷))
5554ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → (𝐵 𝐴) = (𝐸 𝐷))
561eqcomd 2742 . . . . . . . . . . . 12 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → (𝐵 𝐶) = (𝐸 𝑓))
572, 3, 21, 6, 24, 25, 23, 10, 12, 22, 45, 24, 13, 23, 48, 52, 55, 56cgracgr 28827 . . . . . . . . . . 11 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → (𝐴 𝐶) = (𝐷 𝑓))
582, 13, 3, 6, 24, 23, 10, 22, 57tgcgrcomlr 28489 . . . . . . . . . 10 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → (𝐶 𝐴) = (𝑓 𝐷))
5953ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → (𝐴 𝐵) = (𝐷 𝐸))
602, 13, 42, 6, 23, 24, 25, 22, 10, 12, 58, 59, 56trgcgr 28525 . . . . . . . . 9 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → ⟨“𝐶𝐴𝐵”⟩(cgrG‘𝐺)⟨“𝑓𝐷𝐸”⟩)
612, 3, 4, 5, 16, 14, 15, 18ncolne1 28634 . . . . . . . . . . . 12 (𝜑𝐶𝐴)
6261ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝐶𝐴)
632, 13, 3, 6, 23, 24, 22, 10, 58, 62tgcgrneq 28492 . . . . . . . . . 10 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝑓𝐷)
642, 3, 21, 22, 8, 10, 6, 63hlid 28618 . . . . . . . . 9 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝑓((hlG‘𝐺)‘𝐷)𝑓)
65 tgasa.4 . . . . . . . . . . . . 13 (𝜑 → ⟨“𝐶𝐴𝐵”⟩(cgrA‘𝐺)⟨“𝐹𝐷𝐸”⟩)
662, 3, 21, 5, 16, 14, 15, 7, 9, 11, 65cgrane4 28824 . . . . . . . . . . . 12 (𝜑𝐷𝐸)
6766necomd 2995 . . . . . . . . . . 11 (𝜑𝐸𝐷)
682, 3, 21, 11, 14, 9, 5, 67hlid 28618 . . . . . . . . . 10 (𝜑𝐸((hlG‘𝐺)‘𝐷)𝐸)
6968ad2antrr 726 . . . . . . . . 9 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝐸((hlG‘𝐺)‘𝐷)𝐸)
702, 3, 21, 6, 23, 24, 25, 22, 10, 12, 22, 12, 60, 64, 69iscgrad 28820 . . . . . . . 8 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → ⟨“𝐶𝐴𝐵”⟩(cgrA‘𝐺)⟨“𝑓𝐷𝐸”⟩)
7166ad2antrr 726 . . . . . . . . 9 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝐷𝐸)
722, 3, 6, 21, 22, 10, 12, 63, 71cgraswap 28829 . . . . . . . 8 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → ⟨“𝑓𝐷𝐸”⟩(cgrA‘𝐺)⟨“𝐸𝐷𝑓”⟩)
732, 3, 6, 21, 23, 24, 25, 22, 10, 12, 70, 12, 10, 22, 72cgratr 28832 . . . . . . 7 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → ⟨“𝐶𝐴𝐵”⟩(cgrA‘𝐺)⟨“𝐸𝐷𝑓”⟩)
742, 3, 21, 5, 16, 14, 15, 7, 9, 11, 65cgrane3 28823 . . . . . . . . . . 11 (𝜑𝐷𝐹)
7574necomd 2995 . . . . . . . . . 10 (𝜑𝐹𝐷)
762, 3, 5, 21, 7, 9, 11, 75, 66cgraswap 28829 . . . . . . . . 9 (𝜑 → ⟨“𝐹𝐷𝐸”⟩(cgrA‘𝐺)⟨“𝐸𝐷𝐹”⟩)
772, 3, 5, 21, 16, 14, 15, 7, 9, 11, 65, 11, 9, 7, 76cgratr 28832 . . . . . . . 8 (𝜑 → ⟨“𝐶𝐴𝐵”⟩(cgrA‘𝐺)⟨“𝐸𝐷𝐹”⟩)
7877ad2antrr 726 . . . . . . 7 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → ⟨“𝐶𝐴𝐵”⟩(cgrA‘𝐺)⟨“𝐸𝐷𝐹”⟩)
792, 3, 4, 5, 11, 9, 67tgelrnln 28639 . . . . . . . . 9 (𝜑 → (𝐸𝐿𝐷) ∈ ran 𝐿)
8079ad2antrr 726 . . . . . . . 8 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → (𝐸𝐿𝐷) ∈ ran 𝐿)
81 simpl 482 . . . . . . . . . . . 12 ((𝑎 = 𝑢𝑏 = 𝑣) → 𝑎 = 𝑢)
8281eleq1d 2825 . . . . . . . . . . 11 ((𝑎 = 𝑢𝑏 = 𝑣) → (𝑎 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ↔ 𝑢 ∈ (𝑃 ∖ (𝐸𝐿𝐷))))
83 simpr 484 . . . . . . . . . . . 12 ((𝑎 = 𝑢𝑏 = 𝑣) → 𝑏 = 𝑣)
8483eleq1d 2825 . . . . . . . . . . 11 ((𝑎 = 𝑢𝑏 = 𝑣) → (𝑏 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ↔ 𝑣 ∈ (𝑃 ∖ (𝐸𝐿𝐷))))
8582, 84anbi12d 632 . . . . . . . . . 10 ((𝑎 = 𝑢𝑏 = 𝑣) → ((𝑎 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ∧ 𝑏 ∈ (𝑃 ∖ (𝐸𝐿𝐷))) ↔ (𝑢 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐸𝐿𝐷)))))
86 simpr 484 . . . . . . . . . . . 12 (((𝑎 = 𝑢𝑏 = 𝑣) ∧ 𝑡 = 𝑤) → 𝑡 = 𝑤)
87 simpll 766 . . . . . . . . . . . . 13 (((𝑎 = 𝑢𝑏 = 𝑣) ∧ 𝑡 = 𝑤) → 𝑎 = 𝑢)
88 simplr 768 . . . . . . . . . . . . 13 (((𝑎 = 𝑢𝑏 = 𝑣) ∧ 𝑡 = 𝑤) → 𝑏 = 𝑣)
8987, 88oveq12d 7450 . . . . . . . . . . . 12 (((𝑎 = 𝑢𝑏 = 𝑣) ∧ 𝑡 = 𝑤) → (𝑎𝐼𝑏) = (𝑢𝐼𝑣))
9086, 89eleq12d 2834 . . . . . . . . . . 11 (((𝑎 = 𝑢𝑏 = 𝑣) ∧ 𝑡 = 𝑤) → (𝑡 ∈ (𝑎𝐼𝑏) ↔ 𝑤 ∈ (𝑢𝐼𝑣)))
9190cbvrexdva 3239 . . . . . . . . . 10 ((𝑎 = 𝑢𝑏 = 𝑣) → (∃𝑡 ∈ (𝐸𝐿𝐷)𝑡 ∈ (𝑎𝐼𝑏) ↔ ∃𝑤 ∈ (𝐸𝐿𝐷)𝑤 ∈ (𝑢𝐼𝑣)))
9285, 91anbi12d 632 . . . . . . . . 9 ((𝑎 = 𝑢𝑏 = 𝑣) → (((𝑎 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ∧ 𝑏 ∈ (𝑃 ∖ (𝐸𝐿𝐷))) ∧ ∃𝑡 ∈ (𝐸𝐿𝐷)𝑡 ∈ (𝑎𝐼𝑏)) ↔ ((𝑢 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐸𝐿𝐷))) ∧ ∃𝑤 ∈ (𝐸𝐿𝐷)𝑤 ∈ (𝑢𝐼𝑣))))
9392cbvopabv 5215 . . . . . . . 8 {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ∧ 𝑏 ∈ (𝑃 ∖ (𝐸𝐿𝐷))) ∧ ∃𝑡 ∈ (𝐸𝐿𝐷)𝑡 ∈ (𝑎𝐼𝑏))} = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐸𝐿𝐷))) ∧ ∃𝑤 ∈ (𝐸𝐿𝐷)𝑤 ∈ (𝑢𝐼𝑣))}
942, 3, 4, 5, 11, 9, 67tglinerflx1 28642 . . . . . . . . . 10 (𝜑𝐸 ∈ (𝐸𝐿𝐷))
9594ad2antrr 726 . . . . . . . . 9 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝐸 ∈ (𝐸𝐿𝐷))
962, 4, 3, 5, 9, 11, 7, 19ncolcom 28570 . . . . . . . . . . 11 (𝜑 → ¬ (𝐹 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
97 pm2.45 881 . . . . . . . . . . 11 (¬ (𝐹 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷) → ¬ 𝐹 ∈ (𝐸𝐿𝐷))
9896, 97syl 17 . . . . . . . . . 10 (𝜑 → ¬ 𝐹 ∈ (𝐸𝐿𝐷))
9998ad2antrr 726 . . . . . . . . 9 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → ¬ 𝐹 ∈ (𝐸𝐿𝐷))
1002, 3, 21, 22, 8, 12, 6, 44hlcomd 28613 . . . . . . . . 9 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝐹((hlG‘𝐺)‘𝐸)𝑓)
1012, 3, 4, 6, 80, 12, 93, 21, 95, 8, 22, 99, 100hphl 28780 . . . . . . . 8 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝐹((hpG‘𝐺)‘(𝐸𝐿𝐷))𝑓)
1022, 3, 4, 6, 80, 8, 93, 22, 101hpgcom 28776 . . . . . . 7 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝑓((hpG‘𝐺)‘(𝐸𝐿𝐷))𝐹)
1032, 3, 4, 5, 79, 7, 93, 98hpgid 28775 . . . . . . . 8 (𝜑𝐹((hpG‘𝐺)‘(𝐸𝐿𝐷))𝐹)
104103ad2antrr 726 . . . . . . 7 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝐹((hpG‘𝐺)‘(𝐸𝐿𝐷))𝐹)
1052, 3, 13, 6, 23, 24, 25, 12, 10, 8, 4, 26, 41, 22, 8, 21, 73, 78, 102, 104acopyeu 28843 . . . . . 6 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝑓((hlG‘𝐺)‘𝐷)𝐹)
1062, 3, 21, 22, 8, 10, 6, 4, 105hlln 28616 . . . . 5 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝑓 ∈ (𝐹𝐿𝐷))
1072, 3, 4, 5, 7, 9, 75tglinerflx1 28642 . . . . . 6 (𝜑𝐹 ∈ (𝐹𝐿𝐷))
108107ad2antrr 726 . . . . 5 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝐹 ∈ (𝐹𝐿𝐷))
1092, 3, 21, 5, 14, 15, 16, 9, 11, 7, 17cgrane4 28824 . . . . . . 7 (𝜑𝐸𝐹)
110109ad2antrr 726 . . . . . 6 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝐸𝐹)
1112, 3, 21, 22, 8, 12, 6, 4, 44hlln 28616 . . . . . 6 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝑓 ∈ (𝐹𝐿𝐸))
1122, 3, 4, 6, 12, 8, 22, 110, 111lncom 28631 . . . . 5 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝑓 ∈ (𝐸𝐿𝐹))
1132, 3, 4, 6, 12, 8, 110tglinerflx2 28643 . . . . 5 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝐹 ∈ (𝐸𝐿𝐹))
1142, 3, 4, 6, 8, 10, 12, 8, 20, 106, 108, 112, 113tglineinteq 28654 . . . 4 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → 𝑓 = 𝐹)
115114oveq2d 7448 . . 3 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → (𝐸 𝑓) = (𝐸 𝐹))
1161, 115eqtr3d 2778 . 2 (((𝜑𝑓𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶))) → (𝐵 𝐶) = (𝐸 𝐹))
117109necomd 2995 . . 3 (𝜑𝐹𝐸)
1182, 3, 21, 11, 15, 16, 5, 7, 13, 117, 49hlcgrex 28625 . 2 (𝜑 → ∃𝑓𝑃 (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 𝑓) = (𝐵 𝐶)))
119116, 118r19.29a 3161 1 (𝜑 → (𝐵 𝐶) = (𝐸 𝐹))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 847   = wceq 1539  wcel 2107  wne 2939  wrex 3069  cdif 3947   class class class wbr 5142  {copab 5204  ran crn 5685  cfv 6560  (class class class)co 7432  ⟨“cs3 14882  Basecbs 17248  distcds 17307  TarskiGcstrkg 28436  Itvcitv 28442  LineGclng 28443  cgrGccgrg 28519  hlGchlg 28609  hpGchpg 28766  cgrAccgra 28816
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-cnex 11212  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-1st 8015  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-1o 8507  df-oadd 8511  df-er 8746  df-map 8869  df-pm 8870  df-en 8987  df-dom 8988  df-sdom 8989  df-fin 8990  df-dju 9942  df-card 9980  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-nn 12268  df-2 12330  df-3 12331  df-n0 12529  df-xnn0 12602  df-z 12616  df-uz 12880  df-fz 13549  df-fzo 13696  df-hash 14371  df-word 14554  df-concat 14610  df-s1 14635  df-s2 14888  df-s3 14889  df-trkgc 28457  df-trkgb 28458  df-trkgcb 28459  df-trkgld 28461  df-trkg 28462  df-cgrg 28520  df-leg 28592  df-hlg 28610  df-mir 28662  df-rag 28703  df-perpg 28705  df-hpg 28767  df-mid 28783  df-lmi 28784  df-cgra 28817
This theorem is referenced by:  tgasa  28868
  Copyright terms: Public domain W3C validator