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

Theorem tgifscgr 28026
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 483 . . 3 ((πœ‘ ∧ (β™―β€˜π‘ƒ) = 1) β†’ (β™―β€˜π‘ƒ) = 1)
13 tgifscgr.h . . . 4 (πœ‘ β†’ 𝐻 ∈ 𝑃)
1413adantr 479 . . 3 ((πœ‘ ∧ (β™―β€˜π‘ƒ) = 1) β†’ 𝐻 ∈ 𝑃)
151, 2, 3, 5, 7, 9, 11, 12, 14tgldim0cgr 28023 . 2 ((πœ‘ ∧ (β™―β€˜π‘ƒ) = 1) β†’ (𝐡 βˆ’ 𝐷) = (𝐹 βˆ’ 𝐻))
16 tgifscgr.6 . . . . 5 (πœ‘ β†’ (𝐢 βˆ’ 𝐷) = (𝐾 βˆ’ 𝐻))
1716ad2antrr 722 . . . 4 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ (𝐢 βˆ’ 𝐷) = (𝐾 βˆ’ 𝐻))
184ad2antrr 722 . . . . . 6 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐺 ∈ TarskiG)
19 tgbtwncgr.c . . . . . . 7 (πœ‘ β†’ 𝐢 ∈ 𝑃)
2019ad2antrr 722 . . . . . 6 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐢 ∈ 𝑃)
216ad2antrr 722 . . . . . 6 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐡 ∈ 𝑃)
22 tgifscgr.1 . . . . . . . 8 (πœ‘ β†’ 𝐡 ∈ (𝐴𝐼𝐢))
2322ad2antrr 722 . . . . . . 7 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐡 ∈ (𝐴𝐼𝐢))
24 simpr 483 . . . . . . . 8 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐴 = 𝐢)
2524oveq1d 7426 . . . . . . 7 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ (𝐴𝐼𝐢) = (𝐢𝐼𝐢))
2623, 25eleqtrd 2833 . . . . . 6 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐡 ∈ (𝐢𝐼𝐢))
271, 2, 3, 18, 20, 21, 26axtgbtwnid 27984 . . . . 5 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐢 = 𝐡)
2827oveq1d 7426 . . . 4 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ (𝐢 βˆ’ 𝐷) = (𝐡 βˆ’ 𝐷))
29 tgifscgr.g . . . . . . 7 (πœ‘ β†’ 𝐾 ∈ 𝑃)
3029ad2antrr 722 . . . . . 6 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐾 ∈ 𝑃)
3110ad2antrr 722 . . . . . 6 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐹 ∈ 𝑃)
32 tgifscgr.2 . . . . . . . 8 (πœ‘ β†’ 𝐹 ∈ (𝐸𝐼𝐾))
3332ad2antrr 722 . . . . . . 7 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐹 ∈ (𝐸𝐼𝐾))
34 tgifscgr.e . . . . . . . . . 10 (πœ‘ β†’ 𝐸 ∈ 𝑃)
3534ad2antrr 722 . . . . . . . . 9 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐸 ∈ 𝑃)
36 tgbtwncgr.a . . . . . . . . . 10 (πœ‘ β†’ 𝐴 ∈ 𝑃)
3736ad2antrr 722 . . . . . . . . 9 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐴 ∈ 𝑃)
3824oveq2d 7427 . . . . . . . . . 10 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ (𝐴 βˆ’ 𝐴) = (𝐴 βˆ’ 𝐢))
39 tgifscgr.3 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴 βˆ’ 𝐢) = (𝐸 βˆ’ 𝐾))
4039ad2antrr 722 . . . . . . . . . 10 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ (𝐴 βˆ’ 𝐢) = (𝐸 βˆ’ 𝐾))
4138, 40eqtr2d 2771 . . . . . . . . 9 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ (𝐸 βˆ’ 𝐾) = (𝐴 βˆ’ 𝐴))
421, 2, 3, 18, 35, 30, 37, 41axtgcgrid 27981 . . . . . . . 8 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐸 = 𝐾)
4342oveq1d 7426 . . . . . . 7 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ (𝐸𝐼𝐾) = (𝐾𝐼𝐾))
4433, 43eleqtrd 2833 . . . . . 6 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐹 ∈ (𝐾𝐼𝐾))
451, 2, 3, 18, 30, 31, 44axtgbtwnid 27984 . . . . 5 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐾 = 𝐹)
4645oveq1d 7426 . . . 4 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ (𝐾 βˆ’ 𝐻) = (𝐹 βˆ’ 𝐻))
4717, 28, 463eqtr3d 2778 . . 3 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ (𝐡 βˆ’ 𝐷) = (𝐹 βˆ’ 𝐻))
484ad2antrr 722 . . . . . . . 8 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) β†’ 𝐺 ∈ TarskiG)
4948ad2antrr 722 . . . . . . 7 (((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) β†’ 𝐺 ∈ TarskiG)
5049ad2antrr 722 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐺 ∈ TarskiG)
51 simp-4r 780 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝑒 ∈ 𝑃)
5219ad2antrr 722 . . . . . . . 8 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) β†’ 𝐢 ∈ 𝑃)
5352ad2antrr 722 . . . . . . 7 (((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) β†’ 𝐢 ∈ 𝑃)
5453ad2antrr 722 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐢 ∈ 𝑃)
556ad6antr 732 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐡 ∈ 𝑃)
56 simplr 765 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝑓 ∈ 𝑃)
5729ad4antr 728 . . . . . . 7 (((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) β†’ 𝐾 ∈ 𝑃)
5857ad2antrr 722 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐾 ∈ 𝑃)
5910ad6antr 732 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐹 ∈ 𝑃)
608ad6antr 732 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐷 ∈ 𝑃)
6113ad6antr 732 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐻 ∈ 𝑃)
62 simpllr 772 . . . . . . . 8 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒))
6362simprd 494 . . . . . . 7 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐢 β‰  𝑒)
6463necomd 2994 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝑒 β‰  𝐢)
6536ad2antrr 722 . . . . . . . . 9 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) β†’ 𝐴 ∈ 𝑃)
6665ad4antr 728 . . . . . . . 8 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐴 ∈ 𝑃)
6722ad6antr 732 . . . . . . . 8 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐡 ∈ (𝐴𝐼𝐢))
6862simpld 493 . . . . . . . 8 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐢 ∈ (𝐴𝐼𝑒))
691, 2, 3, 50, 66, 55, 54, 51, 67, 68tgbtwnexch3 28012 . . . . . . 7 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐢 ∈ (𝐡𝐼𝑒))
701, 2, 3, 50, 55, 54, 51, 69tgbtwncom 28006 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐢 ∈ (𝑒𝐼𝐡))
7134ad6antr 732 . . . . . . . 8 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐸 ∈ 𝑃)
7232ad6antr 732 . . . . . . . 8 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐹 ∈ (𝐸𝐼𝐾))
73 simprl 767 . . . . . . . 8 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐾 ∈ (𝐸𝐼𝑓))
741, 2, 3, 50, 71, 59, 58, 56, 72, 73tgbtwnexch3 28012 . . . . . . 7 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐾 ∈ (𝐹𝐼𝑓))
751, 2, 3, 50, 59, 58, 56, 74tgbtwncom 28006 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐾 ∈ (𝑓𝐼𝐹))
76 simprr 769 . . . . . . . 8 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))
7776eqcomd 2736 . . . . . . 7 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ (𝐢 βˆ’ 𝑒) = (𝐾 βˆ’ 𝑓))
781, 2, 3, 50, 54, 51, 58, 56, 77tgcgrcomlr 27998 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ (𝑒 βˆ’ 𝐢) = (𝑓 βˆ’ 𝐾))
79 tgifscgr.4 . . . . . . . 8 (πœ‘ β†’ (𝐡 βˆ’ 𝐢) = (𝐹 βˆ’ 𝐾))
8079ad6antr 732 . . . . . . 7 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ (𝐡 βˆ’ 𝐢) = (𝐹 βˆ’ 𝐾))
811, 2, 3, 50, 55, 54, 59, 58, 80tgcgrcomlr 27998 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ (𝐢 βˆ’ 𝐡) = (𝐾 βˆ’ 𝐹))
82 simp-5r 782 . . . . . . 7 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐴 β‰  𝐢)
8339ad6antr 732 . . . . . . 7 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ (𝐴 βˆ’ 𝐢) = (𝐸 βˆ’ 𝐾))
84 tgifscgr.5 . . . . . . . 8 (πœ‘ β†’ (𝐴 βˆ’ 𝐷) = (𝐸 βˆ’ 𝐻))
8584ad6antr 732 . . . . . . 7 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ (𝐴 βˆ’ 𝐷) = (𝐸 βˆ’ 𝐻))
8616ad6antr 732 . . . . . . 7 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ (𝐢 βˆ’ 𝐷) = (𝐾 βˆ’ 𝐻))
871, 2, 3, 50, 66, 54, 51, 71, 58, 56, 60, 61, 82, 68, 73, 83, 77, 85, 86axtg5seg 27983 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ (𝑒 βˆ’ 𝐷) = (𝑓 βˆ’ 𝐻))
881, 2, 3, 50, 51, 54, 55, 56, 58, 59, 60, 61, 64, 70, 75, 78, 81, 87, 86axtg5seg 27983 . . . . 5 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ (𝐡 βˆ’ 𝐷) = (𝐹 βˆ’ 𝐻))
8934ad4antr 728 . . . . . 6 (((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) β†’ 𝐸 ∈ 𝑃)
90 simplr 765 . . . . . 6 (((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) β†’ 𝑒 ∈ 𝑃)
911, 2, 3, 49, 89, 57, 53, 90axtgsegcon 27982 . . . . 5 (((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) β†’ βˆƒπ‘“ ∈ 𝑃 (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒)))
9288, 91r19.29a 3160 . . . 4 (((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) β†’ (𝐡 βˆ’ 𝐷) = (𝐹 βˆ’ 𝐻))
93 simplr 765 . . . . 5 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) β†’ 2 ≀ (β™―β€˜π‘ƒ))
941, 2, 3, 48, 65, 52, 93tgbtwndiff 28024 . . . 4 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) β†’ βˆƒπ‘’ ∈ 𝑃 (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒))
9592, 94r19.29a 3160 . . 3 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) β†’ (𝐡 βˆ’ 𝐷) = (𝐹 βˆ’ 𝐻))
9647, 95pm2.61dane 3027 . 2 ((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) β†’ (𝐡 βˆ’ 𝐷) = (𝐹 βˆ’ 𝐻))
971, 36tgldimor 28020 . 2 (πœ‘ β†’ ((β™―β€˜π‘ƒ) = 1 ∨ 2 ≀ (β™―β€˜π‘ƒ)))
9815, 96, 97mpjaodan 955 1 (πœ‘ β†’ (𝐡 βˆ’ 𝐷) = (𝐹 βˆ’ 𝐻))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 394   = wceq 1539   ∈ wcel 2104   β‰  wne 2938   class class class wbr 5147  β€˜cfv 6542  (class class class)co 7411  1c1 11113   ≀ cle 11253  2c2 12271  β™―chash 14294  Basecbs 17148  distcds 17210  TarskiGcstrkg 27945  Itvcitv 27951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-oadd 8472  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-dju 9898  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-2 12279  df-n0 12477  df-xnn0 12549  df-z 12563  df-uz 12827  df-fz 13489  df-hash 14295  df-trkgc 27966  df-trkgb 27967  df-trkgcb 27968  df-trkg 27971
This theorem is referenced by:  tgcgrsub  28027  tgbtwnxfr  28048  tgfscgr  28086  tgbtwnconn1lem3  28092  miriso  28188  krippenlem  28208  midexlem  28210  colperpexlem1  28248  opphllem  28253
  Copyright terms: Public domain W3C validator