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

Theorem tgifscgr 25448
Description: Inner five segment congruence. Take two triangles, 𝐴𝐷𝐶 and 𝐸𝐻𝐾, with 𝐵 between 𝐴 and 𝐶 and 𝐹 between 𝐸 and 𝐾. If the other components of the triangles are congruent, then so are 𝐵𝐷 and 𝐹𝐻. Theorem 4.2 of [Schwabhauser] p. 34. (Contributed by Thierry Arnoux, 24-Mar-2019.)
Hypotheses
Ref Expression
tgbtwncgr.p 𝑃 = (Base‘𝐺)
tgbtwncgr.m = (dist‘𝐺)
tgbtwncgr.i 𝐼 = (Itv‘𝐺)
tgbtwncgr.g (𝜑𝐺 ∈ TarskiG)
tgbtwncgr.a (𝜑𝐴𝑃)
tgbtwncgr.b (𝜑𝐵𝑃)
tgbtwncgr.c (𝜑𝐶𝑃)
tgbtwncgr.d (𝜑𝐷𝑃)
tgifscgr.e (𝜑𝐸𝑃)
tgifscgr.f (𝜑𝐹𝑃)
tgifscgr.g (𝜑𝐾𝑃)
tgifscgr.h (𝜑𝐻𝑃)
tgifscgr.1 (𝜑𝐵 ∈ (𝐴𝐼𝐶))
tgifscgr.2 (𝜑𝐹 ∈ (𝐸𝐼𝐾))
tgifscgr.3 (𝜑 → (𝐴 𝐶) = (𝐸 𝐾))
tgifscgr.4 (𝜑 → (𝐵 𝐶) = (𝐹 𝐾))
tgifscgr.5 (𝜑 → (𝐴 𝐷) = (𝐸 𝐻))
tgifscgr.6 (𝜑 → (𝐶 𝐷) = (𝐾 𝐻))
Assertion
Ref Expression
tgifscgr (𝜑 → (𝐵 𝐷) = (𝐹 𝐻))

Proof of Theorem tgifscgr
Dummy variables 𝑒 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tgbtwncgr.p . . 3 𝑃 = (Base‘𝐺)
2 tgbtwncgr.m . . 3 = (dist‘𝐺)
3 tgbtwncgr.i . . 3 𝐼 = (Itv‘𝐺)
4 tgbtwncgr.g . . . 4 (𝜑𝐺 ∈ TarskiG)
54adantr 480 . . 3 ((𝜑 ∧ (#‘𝑃) = 1) → 𝐺 ∈ TarskiG)
6 tgbtwncgr.b . . . 4 (𝜑𝐵𝑃)
76adantr 480 . . 3 ((𝜑 ∧ (#‘𝑃) = 1) → 𝐵𝑃)
8 tgbtwncgr.d . . . 4 (𝜑𝐷𝑃)
98adantr 480 . . 3 ((𝜑 ∧ (#‘𝑃) = 1) → 𝐷𝑃)
10 tgifscgr.f . . . 4 (𝜑𝐹𝑃)
1110adantr 480 . . 3 ((𝜑 ∧ (#‘𝑃) = 1) → 𝐹𝑃)
12 simpr 476 . . 3 ((𝜑 ∧ (#‘𝑃) = 1) → (#‘𝑃) = 1)
13 tgifscgr.h . . . 4 (𝜑𝐻𝑃)
1413adantr 480 . . 3 ((𝜑 ∧ (#‘𝑃) = 1) → 𝐻𝑃)
151, 2, 3, 5, 7, 9, 11, 12, 14tgldim0cgr 25445 . 2 ((𝜑 ∧ (#‘𝑃) = 1) → (𝐵 𝐷) = (𝐹 𝐻))
16 tgifscgr.6 . . . . 5 (𝜑 → (𝐶 𝐷) = (𝐾 𝐻))
1716ad2antrr 762 . . . 4 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐶 𝐷) = (𝐾 𝐻))
184ad2antrr 762 . . . . . 6 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐺 ∈ TarskiG)
19 tgbtwncgr.c . . . . . . 7 (𝜑𝐶𝑃)
2019ad2antrr 762 . . . . . 6 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐶𝑃)
216ad2antrr 762 . . . . . 6 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐵𝑃)
22 tgifscgr.1 . . . . . . . 8 (𝜑𝐵 ∈ (𝐴𝐼𝐶))
2322ad2antrr 762 . . . . . . 7 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐵 ∈ (𝐴𝐼𝐶))
24 simpr 476 . . . . . . . 8 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐴 = 𝐶)
2524oveq1d 6705 . . . . . . 7 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐴𝐼𝐶) = (𝐶𝐼𝐶))
2623, 25eleqtrd 2732 . . . . . 6 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐵 ∈ (𝐶𝐼𝐶))
271, 2, 3, 18, 20, 21, 26axtgbtwnid 25410 . . . . 5 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐶 = 𝐵)
2827oveq1d 6705 . . . 4 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐶 𝐷) = (𝐵 𝐷))
29 tgifscgr.g . . . . . . 7 (𝜑𝐾𝑃)
3029ad2antrr 762 . . . . . 6 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐾𝑃)
3110ad2antrr 762 . . . . . 6 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐹𝑃)
32 tgifscgr.2 . . . . . . . 8 (𝜑𝐹 ∈ (𝐸𝐼𝐾))
3332ad2antrr 762 . . . . . . 7 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐹 ∈ (𝐸𝐼𝐾))
34 tgifscgr.e . . . . . . . . . 10 (𝜑𝐸𝑃)
3534ad2antrr 762 . . . . . . . . 9 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐸𝑃)
36 tgbtwncgr.a . . . . . . . . . 10 (𝜑𝐴𝑃)
3736ad2antrr 762 . . . . . . . . 9 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐴𝑃)
3824oveq2d 6706 . . . . . . . . . 10 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐴 𝐴) = (𝐴 𝐶))
39 tgifscgr.3 . . . . . . . . . . 11 (𝜑 → (𝐴 𝐶) = (𝐸 𝐾))
4039ad2antrr 762 . . . . . . . . . 10 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐴 𝐶) = (𝐸 𝐾))
4138, 40eqtr2d 2686 . . . . . . . . 9 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐸 𝐾) = (𝐴 𝐴))
421, 2, 3, 18, 35, 30, 37, 41axtgcgrid 25407 . . . . . . . 8 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐸 = 𝐾)
4342oveq1d 6705 . . . . . . 7 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐸𝐼𝐾) = (𝐾𝐼𝐾))
4433, 43eleqtrd 2732 . . . . . 6 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐹 ∈ (𝐾𝐼𝐾))
451, 2, 3, 18, 30, 31, 44axtgbtwnid 25410 . . . . 5 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐾 = 𝐹)
4645oveq1d 6705 . . . 4 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐾 𝐻) = (𝐹 𝐻))
4717, 28, 463eqtr3d 2693 . . 3 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐵 𝐷) = (𝐹 𝐻))
484ad2antrr 762 . . . . . . . 8 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) → 𝐺 ∈ TarskiG)
4948ad2antrr 762 . . . . . . 7 (((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) → 𝐺 ∈ TarskiG)
5049ad2antrr 762 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐺 ∈ TarskiG)
51 simp-4r 824 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝑒𝑃)
5219ad2antrr 762 . . . . . . . 8 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) → 𝐶𝑃)
5352ad2antrr 762 . . . . . . 7 (((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) → 𝐶𝑃)
5453ad2antrr 762 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐶𝑃)
556ad6antr 777 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐵𝑃)
56 simplr 807 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝑓𝑃)
5729ad4antr 769 . . . . . . 7 (((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) → 𝐾𝑃)
5857ad2antrr 762 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐾𝑃)
5910ad6antr 777 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐹𝑃)
608ad6antr 777 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐷𝑃)
6113ad6antr 777 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐻𝑃)
62 simpllr 815 . . . . . . . 8 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒))
6362simprd 478 . . . . . . 7 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐶𝑒)
6463necomd 2878 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝑒𝐶)
6536ad2antrr 762 . . . . . . . . 9 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) → 𝐴𝑃)
6665ad4antr 769 . . . . . . . 8 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐴𝑃)
6722ad6antr 777 . . . . . . . 8 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐵 ∈ (𝐴𝐼𝐶))
6862simpld 474 . . . . . . . 8 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐶 ∈ (𝐴𝐼𝑒))
691, 2, 3, 50, 66, 55, 54, 51, 67, 68tgbtwnexch3 25434 . . . . . . 7 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐶 ∈ (𝐵𝐼𝑒))
701, 2, 3, 50, 55, 54, 51, 69tgbtwncom 25428 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐶 ∈ (𝑒𝐼𝐵))
7134ad6antr 777 . . . . . . . 8 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐸𝑃)
7232ad6antr 777 . . . . . . . 8 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐹 ∈ (𝐸𝐼𝐾))
73 simprl 809 . . . . . . . 8 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐾 ∈ (𝐸𝐼𝑓))
741, 2, 3, 50, 71, 59, 58, 56, 72, 73tgbtwnexch3 25434 . . . . . . 7 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐾 ∈ (𝐹𝐼𝑓))
751, 2, 3, 50, 59, 58, 56, 74tgbtwncom 25428 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐾 ∈ (𝑓𝐼𝐹))
76 simprr 811 . . . . . . . 8 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → (𝐾 𝑓) = (𝐶 𝑒))
7776eqcomd 2657 . . . . . . 7 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → (𝐶 𝑒) = (𝐾 𝑓))
781, 2, 3, 50, 54, 51, 58, 56, 77tgcgrcomlr 25420 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → (𝑒 𝐶) = (𝑓 𝐾))
79 tgifscgr.4 . . . . . . . 8 (𝜑 → (𝐵 𝐶) = (𝐹 𝐾))
8079ad6antr 777 . . . . . . 7 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → (𝐵 𝐶) = (𝐹 𝐾))
811, 2, 3, 50, 55, 54, 59, 58, 80tgcgrcomlr 25420 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → (𝐶 𝐵) = (𝐾 𝐹))
82 simp-5r 826 . . . . . . 7 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐴𝐶)
8339ad6antr 777 . . . . . . 7 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → (𝐴 𝐶) = (𝐸 𝐾))
84 tgifscgr.5 . . . . . . . 8 (𝜑 → (𝐴 𝐷) = (𝐸 𝐻))
8584ad6antr 777 . . . . . . 7 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → (𝐴 𝐷) = (𝐸 𝐻))
8616ad6antr 777 . . . . . . 7 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → (𝐶 𝐷) = (𝐾 𝐻))
871, 2, 3, 50, 66, 54, 51, 71, 58, 56, 60, 61, 82, 68, 73, 83, 77, 85, 86axtg5seg 25409 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → (𝑒 𝐷) = (𝑓 𝐻))
881, 2, 3, 50, 51, 54, 55, 56, 58, 59, 60, 61, 64, 70, 75, 78, 81, 87, 86axtg5seg 25409 . . . . 5 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → (𝐵 𝐷) = (𝐹 𝐻))
8934ad4antr 769 . . . . . 6 (((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) → 𝐸𝑃)
90 simplr 807 . . . . . 6 (((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) → 𝑒𝑃)
911, 2, 3, 49, 89, 57, 53, 90axtgsegcon 25408 . . . . 5 (((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) → ∃𝑓𝑃 (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒)))
9288, 91r19.29a 3107 . . . 4 (((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) → (𝐵 𝐷) = (𝐹 𝐻))
93 simplr 807 . . . . 5 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) → 2 ≤ (#‘𝑃))
941, 2, 3, 48, 65, 52, 93tgbtwndiff 25446 . . . 4 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) → ∃𝑒𝑃 (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒))
9592, 94r19.29a 3107 . . 3 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) → (𝐵 𝐷) = (𝐹 𝐻))
9647, 95pm2.61dane 2910 . 2 ((𝜑 ∧ 2 ≤ (#‘𝑃)) → (𝐵 𝐷) = (𝐹 𝐻))
971, 36tgldimor 25442 . 2 (𝜑 → ((#‘𝑃) = 1 ∨ 2 ≤ (#‘𝑃)))
9815, 96, 97mpjaodan 844 1 (𝜑 → (𝐵 𝐷) = (𝐹 𝐻))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  wcel 2030  wne 2823   class class class wbr 4685  cfv 5926  (class class class)co 6690  1c1 9975  cle 10113  2c2 11108  #chash 13157  Basecbs 15904  distcds 15997  TarskiGcstrkg 25374  Itvcitv 25380
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-n0 11331  df-xnn0 11402  df-z 11416  df-uz 11726  df-fz 12365  df-hash 13158  df-trkgc 25392  df-trkgb 25393  df-trkgcb 25394  df-trkg 25397
This theorem is referenced by:  tgcgrsub  25449  tgbtwnxfr  25470  tgfscgr  25508  tgbtwnconn1lem3  25514  miriso  25610  krippenlem  25630  midexlem  25632  colperpexlem1  25667  opphllem  25672
  Copyright terms: Public domain W3C validator