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

Theorem tgifscgr 25104
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 479 . . 3 ((𝜑 ∧ (#‘𝑃) = 1) → 𝐺 ∈ TarskiG)
6 tgbtwncgr.b . . . 4 (𝜑𝐵𝑃)
76adantr 479 . . 3 ((𝜑 ∧ (#‘𝑃) = 1) → 𝐵𝑃)
8 tgbtwncgr.d . . . 4 (𝜑𝐷𝑃)
98adantr 479 . . 3 ((𝜑 ∧ (#‘𝑃) = 1) → 𝐷𝑃)
10 tgifscgr.f . . . 4 (𝜑𝐹𝑃)
1110adantr 479 . . 3 ((𝜑 ∧ (#‘𝑃) = 1) → 𝐹𝑃)
12 simpr 475 . . 3 ((𝜑 ∧ (#‘𝑃) = 1) → (#‘𝑃) = 1)
13 tgifscgr.h . . . 4 (𝜑𝐻𝑃)
1413adantr 479 . . 3 ((𝜑 ∧ (#‘𝑃) = 1) → 𝐻𝑃)
151, 2, 3, 5, 7, 9, 11, 12, 14tgldim0cgr 25100 . 2 ((𝜑 ∧ (#‘𝑃) = 1) → (𝐵 𝐷) = (𝐹 𝐻))
16 tgifscgr.6 . . . . 5 (𝜑 → (𝐶 𝐷) = (𝐾 𝐻))
1716ad2antrr 757 . . . 4 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐶 𝐷) = (𝐾 𝐻))
184ad2antrr 757 . . . . . 6 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐺 ∈ TarskiG)
19 tgbtwncgr.c . . . . . . 7 (𝜑𝐶𝑃)
2019ad2antrr 757 . . . . . 6 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐶𝑃)
216ad2antrr 757 . . . . . 6 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐵𝑃)
22 tgifscgr.1 . . . . . . . 8 (𝜑𝐵 ∈ (𝐴𝐼𝐶))
2322ad2antrr 757 . . . . . . 7 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐵 ∈ (𝐴𝐼𝐶))
24 simpr 475 . . . . . . . 8 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐴 = 𝐶)
2524oveq1d 6440 . . . . . . 7 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐴𝐼𝐶) = (𝐶𝐼𝐶))
2623, 25eleqtrd 2594 . . . . . 6 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐵 ∈ (𝐶𝐼𝐶))
271, 2, 3, 18, 20, 21, 26axtgbtwnid 25065 . . . . 5 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐶 = 𝐵)
2827oveq1d 6440 . . . 4 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐶 𝐷) = (𝐵 𝐷))
29 tgifscgr.g . . . . . . 7 (𝜑𝐾𝑃)
3029ad2antrr 757 . . . . . 6 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐾𝑃)
3110ad2antrr 757 . . . . . 6 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐹𝑃)
32 tgifscgr.2 . . . . . . . 8 (𝜑𝐹 ∈ (𝐸𝐼𝐾))
3332ad2antrr 757 . . . . . . 7 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐹 ∈ (𝐸𝐼𝐾))
34 tgifscgr.e . . . . . . . . . 10 (𝜑𝐸𝑃)
3534ad2antrr 757 . . . . . . . . 9 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐸𝑃)
36 tgbtwncgr.a . . . . . . . . . 10 (𝜑𝐴𝑃)
3736ad2antrr 757 . . . . . . . . 9 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐴𝑃)
3824oveq2d 6441 . . . . . . . . . 10 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐴 𝐴) = (𝐴 𝐶))
39 tgifscgr.3 . . . . . . . . . . 11 (𝜑 → (𝐴 𝐶) = (𝐸 𝐾))
4039ad2antrr 757 . . . . . . . . . 10 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐴 𝐶) = (𝐸 𝐾))
4138, 40eqtr2d 2549 . . . . . . . . 9 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐸 𝐾) = (𝐴 𝐴))
421, 2, 3, 18, 35, 30, 37, 41axtgcgrid 25062 . . . . . . . 8 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐸 = 𝐾)
4342oveq1d 6440 . . . . . . 7 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐸𝐼𝐾) = (𝐾𝐼𝐾))
4433, 43eleqtrd 2594 . . . . . 6 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐹 ∈ (𝐾𝐼𝐾))
451, 2, 3, 18, 30, 31, 44axtgbtwnid 25065 . . . . 5 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐾 = 𝐹)
4645oveq1d 6440 . . . 4 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐾 𝐻) = (𝐹 𝐻))
4717, 28, 463eqtr3d 2556 . . 3 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐵 𝐷) = (𝐹 𝐻))
484ad2antrr 757 . . . . . . . 8 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) → 𝐺 ∈ TarskiG)
4948ad2antrr 757 . . . . . . 7 (((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) → 𝐺 ∈ TarskiG)
5049ad2antrr 757 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐺 ∈ TarskiG)
51 simp-4r 802 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝑒𝑃)
5219ad2antrr 757 . . . . . . . 8 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) → 𝐶𝑃)
5352ad2antrr 757 . . . . . . 7 (((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) → 𝐶𝑃)
5453ad2antrr 757 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐶𝑃)
556ad6antr 767 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐵𝑃)
56 simplr 787 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝑓𝑃)
5729ad4antr 763 . . . . . . 7 (((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) → 𝐾𝑃)
5857ad2antrr 757 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐾𝑃)
5910ad6antr 767 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐹𝑃)
608ad6antr 767 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐷𝑃)
6113ad6antr 767 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐻𝑃)
62 simpllr 794 . . . . . . . 8 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒))
6362simprd 477 . . . . . . 7 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐶𝑒)
6463necomd 2741 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝑒𝐶)
6536ad2antrr 757 . . . . . . . . 9 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) → 𝐴𝑃)
6665ad4antr 763 . . . . . . . 8 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐴𝑃)
6722ad6antr 767 . . . . . . . 8 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐵 ∈ (𝐴𝐼𝐶))
6862simpld 473 . . . . . . . 8 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐶 ∈ (𝐴𝐼𝑒))
691, 2, 3, 50, 66, 55, 54, 51, 67, 68tgbtwnexch3 25089 . . . . . . 7 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐶 ∈ (𝐵𝐼𝑒))
701, 2, 3, 50, 55, 54, 51, 69tgbtwncom 25083 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐶 ∈ (𝑒𝐼𝐵))
7134ad6antr 767 . . . . . . . 8 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐸𝑃)
7232ad6antr 767 . . . . . . . 8 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐹 ∈ (𝐸𝐼𝐾))
73 simprl 789 . . . . . . . 8 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐾 ∈ (𝐸𝐼𝑓))
741, 2, 3, 50, 71, 59, 58, 56, 72, 73tgbtwnexch3 25089 . . . . . . 7 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐾 ∈ (𝐹𝐼𝑓))
751, 2, 3, 50, 59, 58, 56, 74tgbtwncom 25083 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐾 ∈ (𝑓𝐼𝐹))
76 simprr 791 . . . . . . . 8 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → (𝐾 𝑓) = (𝐶 𝑒))
7776eqcomd 2520 . . . . . . 7 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → (𝐶 𝑒) = (𝐾 𝑓))
781, 2, 3, 50, 54, 51, 58, 56, 77tgcgrcomlr 25075 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → (𝑒 𝐶) = (𝑓 𝐾))
79 tgifscgr.4 . . . . . . . 8 (𝜑 → (𝐵 𝐶) = (𝐹 𝐾))
8079ad6antr 767 . . . . . . 7 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → (𝐵 𝐶) = (𝐹 𝐾))
811, 2, 3, 50, 55, 54, 59, 58, 80tgcgrcomlr 25075 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → (𝐶 𝐵) = (𝐾 𝐹))
82 simp-5r 804 . . . . . . 7 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → 𝐴𝐶)
8339ad6antr 767 . . . . . . 7 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → (𝐴 𝐶) = (𝐸 𝐾))
84 tgifscgr.5 . . . . . . . 8 (𝜑 → (𝐴 𝐷) = (𝐸 𝐻))
8584ad6antr 767 . . . . . . 7 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → (𝐴 𝐷) = (𝐸 𝐻))
8616ad6antr 767 . . . . . . 7 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → (𝐶 𝐷) = (𝐾 𝐻))
871, 2, 3, 50, 66, 54, 51, 71, 58, 56, 60, 61, 82, 68, 73, 83, 77, 85, 86axtg5seg 25064 . . . . . 6 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → (𝑒 𝐷) = (𝑓 𝐻))
881, 2, 3, 50, 51, 54, 55, 56, 58, 59, 60, 61, 64, 70, 75, 78, 81, 87, 86axtg5seg 25064 . . . . 5 (((((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) ∧ 𝑓𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒))) → (𝐵 𝐷) = (𝐹 𝐻))
8934ad4antr 763 . . . . . 6 (((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) → 𝐸𝑃)
90 simplr 787 . . . . . 6 (((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) → 𝑒𝑃)
911, 2, 3, 49, 89, 57, 53, 90axtgsegcon 25063 . . . . 5 (((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) → ∃𝑓𝑃 (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 𝑓) = (𝐶 𝑒)))
9288, 91r19.29a 2964 . . . 4 (((((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) ∧ 𝑒𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒)) → (𝐵 𝐷) = (𝐹 𝐻))
93 simplr 787 . . . . 5 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) → 2 ≤ (#‘𝑃))
941, 2, 3, 48, 65, 52, 93tgbtwndiff 25101 . . . 4 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) → ∃𝑒𝑃 (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶𝑒))
9592, 94r19.29a 2964 . . 3 (((𝜑 ∧ 2 ≤ (#‘𝑃)) ∧ 𝐴𝐶) → (𝐵 𝐷) = (𝐹 𝐻))
9647, 95pm2.61dane 2773 . 2 ((𝜑 ∧ 2 ≤ (#‘𝑃)) → (𝐵 𝐷) = (𝐹 𝐻))
971, 36tgldimor 25097 . 2 (𝜑 → ((#‘𝑃) = 1 ∨ 2 ≤ (#‘𝑃)))
9815, 96, 97mpjaodan 822 1 (𝜑 → (𝐵 𝐷) = (𝐹 𝐻))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1938  wne 2684   class class class wbr 4481  cfv 5689  (class class class)co 6425  1c1 9690  cle 9828  2c2 10823  #chash 12843  Basecbs 15583  distcds 15665  TarskiGcstrkg 25029  Itvcitv 25035
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-rep 4597  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6721  ax-cnex 9745  ax-resscn 9746  ax-1cn 9747  ax-icn 9748  ax-addcl 9749  ax-addrcl 9750  ax-mulcl 9751  ax-mulrcl 9752  ax-mulcom 9753  ax-addass 9754  ax-mulass 9755  ax-distr 9756  ax-i2m1 9757  ax-1ne0 9758  ax-1rid 9759  ax-rnegex 9760  ax-rrecex 9761  ax-cnre 9762  ax-pre-lttri 9763  ax-pre-lttrn 9764  ax-pre-ltadd 9765  ax-pre-mulgt0 9766
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-ral 2805  df-rex 2806  df-reu 2807  df-rmo 2808  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-int 4309  df-iun 4355  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-pred 5487  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-riota 6387  df-ov 6428  df-oprab 6429  df-mpt2 6430  df-om 6832  df-1st 6932  df-2nd 6933  df-wrecs 7167  df-recs 7229  df-rdg 7267  df-1o 7321  df-oadd 7325  df-er 7503  df-en 7716  df-dom 7717  df-sdom 7718  df-fin 7719  df-card 8522  df-cda 8747  df-pnf 9829  df-mnf 9830  df-xr 9831  df-ltxr 9832  df-le 9833  df-sub 10017  df-neg 10018  df-nn 10774  df-2 10832  df-n0 11046  df-z 11117  df-uz 11424  df-fz 12062  df-hash 12844  df-trkgc 25047  df-trkgb 25048  df-trkgcb 25049  df-trkg 25052
This theorem is referenced by:  tgcgrsub  25105  tgbtwnxfr  25126  tgfscgr  25164  tgbtwnconn1lem3  25170  miriso  25266  krippenlem  25286  midexlem  25288  colperpexlem1  25323  opphllem  25328
  Copyright terms: Public domain W3C validator