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

Theorem tgifscgr 27759
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 482 . . 3 ((πœ‘ ∧ (β™―β€˜π‘ƒ) = 1) β†’ 𝐺 ∈ TarskiG)
6 tgbtwncgr.b . . . 4 (πœ‘ β†’ 𝐡 ∈ 𝑃)
76adantr 482 . . 3 ((πœ‘ ∧ (β™―β€˜π‘ƒ) = 1) β†’ 𝐡 ∈ 𝑃)
8 tgbtwncgr.d . . . 4 (πœ‘ β†’ 𝐷 ∈ 𝑃)
98adantr 482 . . 3 ((πœ‘ ∧ (β™―β€˜π‘ƒ) = 1) β†’ 𝐷 ∈ 𝑃)
10 tgifscgr.f . . . 4 (πœ‘ β†’ 𝐹 ∈ 𝑃)
1110adantr 482 . . 3 ((πœ‘ ∧ (β™―β€˜π‘ƒ) = 1) β†’ 𝐹 ∈ 𝑃)
12 simpr 486 . . 3 ((πœ‘ ∧ (β™―β€˜π‘ƒ) = 1) β†’ (β™―β€˜π‘ƒ) = 1)
13 tgifscgr.h . . . 4 (πœ‘ β†’ 𝐻 ∈ 𝑃)
1413adantr 482 . . 3 ((πœ‘ ∧ (β™―β€˜π‘ƒ) = 1) β†’ 𝐻 ∈ 𝑃)
151, 2, 3, 5, 7, 9, 11, 12, 14tgldim0cgr 27756 . 2 ((πœ‘ ∧ (β™―β€˜π‘ƒ) = 1) β†’ (𝐡 βˆ’ 𝐷) = (𝐹 βˆ’ 𝐻))
16 tgifscgr.6 . . . . 5 (πœ‘ β†’ (𝐢 βˆ’ 𝐷) = (𝐾 βˆ’ 𝐻))
1716ad2antrr 725 . . . 4 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ (𝐢 βˆ’ 𝐷) = (𝐾 βˆ’ 𝐻))
184ad2antrr 725 . . . . . 6 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐺 ∈ TarskiG)
19 tgbtwncgr.c . . . . . . 7 (πœ‘ β†’ 𝐢 ∈ 𝑃)
2019ad2antrr 725 . . . . . 6 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐢 ∈ 𝑃)
216ad2antrr 725 . . . . . 6 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐡 ∈ 𝑃)
22 tgifscgr.1 . . . . . . . 8 (πœ‘ β†’ 𝐡 ∈ (𝐴𝐼𝐢))
2322ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐡 ∈ (𝐴𝐼𝐢))
24 simpr 486 . . . . . . . 8 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐴 = 𝐢)
2524oveq1d 7424 . . . . . . 7 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ (𝐴𝐼𝐢) = (𝐢𝐼𝐢))
2623, 25eleqtrd 2836 . . . . . 6 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐡 ∈ (𝐢𝐼𝐢))
271, 2, 3, 18, 20, 21, 26axtgbtwnid 27717 . . . . 5 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐢 = 𝐡)
2827oveq1d 7424 . . . 4 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ (𝐢 βˆ’ 𝐷) = (𝐡 βˆ’ 𝐷))
29 tgifscgr.g . . . . . . 7 (πœ‘ β†’ 𝐾 ∈ 𝑃)
3029ad2antrr 725 . . . . . 6 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐾 ∈ 𝑃)
3110ad2antrr 725 . . . . . 6 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐹 ∈ 𝑃)
32 tgifscgr.2 . . . . . . . 8 (πœ‘ β†’ 𝐹 ∈ (𝐸𝐼𝐾))
3332ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐹 ∈ (𝐸𝐼𝐾))
34 tgifscgr.e . . . . . . . . . 10 (πœ‘ β†’ 𝐸 ∈ 𝑃)
3534ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐸 ∈ 𝑃)
36 tgbtwncgr.a . . . . . . . . . 10 (πœ‘ β†’ 𝐴 ∈ 𝑃)
3736ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐴 ∈ 𝑃)
3824oveq2d 7425 . . . . . . . . . 10 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ (𝐴 βˆ’ 𝐴) = (𝐴 βˆ’ 𝐢))
39 tgifscgr.3 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴 βˆ’ 𝐢) = (𝐸 βˆ’ 𝐾))
4039ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ (𝐴 βˆ’ 𝐢) = (𝐸 βˆ’ 𝐾))
4138, 40eqtr2d 2774 . . . . . . . . 9 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ (𝐸 βˆ’ 𝐾) = (𝐴 βˆ’ 𝐴))
421, 2, 3, 18, 35, 30, 37, 41axtgcgrid 27714 . . . . . . . 8 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐸 = 𝐾)
4342oveq1d 7424 . . . . . . 7 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ (𝐸𝐼𝐾) = (𝐾𝐼𝐾))
4433, 43eleqtrd 2836 . . . . . 6 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐹 ∈ (𝐾𝐼𝐾))
451, 2, 3, 18, 30, 31, 44axtgbtwnid 27717 . . . . 5 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ 𝐾 = 𝐹)
4645oveq1d 7424 . . . 4 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ (𝐾 βˆ’ 𝐻) = (𝐹 βˆ’ 𝐻))
4717, 28, 463eqtr3d 2781 . . 3 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 = 𝐢) β†’ (𝐡 βˆ’ 𝐷) = (𝐹 βˆ’ 𝐻))
484ad2antrr 725 . . . . . . . 8 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) β†’ 𝐺 ∈ TarskiG)
4948ad2antrr 725 . . . . . . 7 (((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) β†’ 𝐺 ∈ TarskiG)
5049ad2antrr 725 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐺 ∈ TarskiG)
51 simp-4r 783 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝑒 ∈ 𝑃)
5219ad2antrr 725 . . . . . . . 8 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) β†’ 𝐢 ∈ 𝑃)
5352ad2antrr 725 . . . . . . 7 (((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) β†’ 𝐢 ∈ 𝑃)
5453ad2antrr 725 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐢 ∈ 𝑃)
556ad6antr 735 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐡 ∈ 𝑃)
56 simplr 768 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝑓 ∈ 𝑃)
5729ad4antr 731 . . . . . . 7 (((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) β†’ 𝐾 ∈ 𝑃)
5857ad2antrr 725 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐾 ∈ 𝑃)
5910ad6antr 735 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐹 ∈ 𝑃)
608ad6antr 735 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐷 ∈ 𝑃)
6113ad6antr 735 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐻 ∈ 𝑃)
62 simpllr 775 . . . . . . . 8 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒))
6362simprd 497 . . . . . . 7 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐢 β‰  𝑒)
6463necomd 2997 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝑒 β‰  𝐢)
6536ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) β†’ 𝐴 ∈ 𝑃)
6665ad4antr 731 . . . . . . . 8 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐴 ∈ 𝑃)
6722ad6antr 735 . . . . . . . 8 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐡 ∈ (𝐴𝐼𝐢))
6862simpld 496 . . . . . . . 8 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐢 ∈ (𝐴𝐼𝑒))
691, 2, 3, 50, 66, 55, 54, 51, 67, 68tgbtwnexch3 27745 . . . . . . 7 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐢 ∈ (𝐡𝐼𝑒))
701, 2, 3, 50, 55, 54, 51, 69tgbtwncom 27739 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐢 ∈ (𝑒𝐼𝐡))
7134ad6antr 735 . . . . . . . 8 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐸 ∈ 𝑃)
7232ad6antr 735 . . . . . . . 8 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐹 ∈ (𝐸𝐼𝐾))
73 simprl 770 . . . . . . . 8 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐾 ∈ (𝐸𝐼𝑓))
741, 2, 3, 50, 71, 59, 58, 56, 72, 73tgbtwnexch3 27745 . . . . . . 7 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐾 ∈ (𝐹𝐼𝑓))
751, 2, 3, 50, 59, 58, 56, 74tgbtwncom 27739 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐾 ∈ (𝑓𝐼𝐹))
76 simprr 772 . . . . . . . 8 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))
7776eqcomd 2739 . . . . . . 7 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ (𝐢 βˆ’ 𝑒) = (𝐾 βˆ’ 𝑓))
781, 2, 3, 50, 54, 51, 58, 56, 77tgcgrcomlr 27731 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ (𝑒 βˆ’ 𝐢) = (𝑓 βˆ’ 𝐾))
79 tgifscgr.4 . . . . . . . 8 (πœ‘ β†’ (𝐡 βˆ’ 𝐢) = (𝐹 βˆ’ 𝐾))
8079ad6antr 735 . . . . . . 7 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ (𝐡 βˆ’ 𝐢) = (𝐹 βˆ’ 𝐾))
811, 2, 3, 50, 55, 54, 59, 58, 80tgcgrcomlr 27731 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ (𝐢 βˆ’ 𝐡) = (𝐾 βˆ’ 𝐹))
82 simp-5r 785 . . . . . . 7 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ 𝐴 β‰  𝐢)
8339ad6antr 735 . . . . . . 7 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ (𝐴 βˆ’ 𝐢) = (𝐸 βˆ’ 𝐾))
84 tgifscgr.5 . . . . . . . 8 (πœ‘ β†’ (𝐴 βˆ’ 𝐷) = (𝐸 βˆ’ 𝐻))
8584ad6antr 735 . . . . . . 7 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ (𝐴 βˆ’ 𝐷) = (𝐸 βˆ’ 𝐻))
8616ad6antr 735 . . . . . . 7 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ (𝐢 βˆ’ 𝐷) = (𝐾 βˆ’ 𝐻))
871, 2, 3, 50, 66, 54, 51, 71, 58, 56, 60, 61, 82, 68, 73, 83, 77, 85, 86axtg5seg 27716 . . . . . 6 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ (𝑒 βˆ’ 𝐷) = (𝑓 βˆ’ 𝐻))
881, 2, 3, 50, 51, 54, 55, 56, 58, 59, 60, 61, 64, 70, 75, 78, 81, 87, 86axtg5seg 27716 . . . . 5 (((((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒))) β†’ (𝐡 βˆ’ 𝐷) = (𝐹 βˆ’ 𝐻))
8934ad4antr 731 . . . . . 6 (((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) β†’ 𝐸 ∈ 𝑃)
90 simplr 768 . . . . . 6 (((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) β†’ 𝑒 ∈ 𝑃)
911, 2, 3, 49, 89, 57, 53, 90axtgsegcon 27715 . . . . 5 (((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) β†’ βˆƒπ‘“ ∈ 𝑃 (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 βˆ’ 𝑓) = (𝐢 βˆ’ 𝑒)))
9288, 91r19.29a 3163 . . . 4 (((((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) ∧ 𝑒 ∈ 𝑃) ∧ (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒)) β†’ (𝐡 βˆ’ 𝐷) = (𝐹 βˆ’ 𝐻))
93 simplr 768 . . . . 5 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) β†’ 2 ≀ (β™―β€˜π‘ƒ))
941, 2, 3, 48, 65, 52, 93tgbtwndiff 27757 . . . 4 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) β†’ βˆƒπ‘’ ∈ 𝑃 (𝐢 ∈ (𝐴𝐼𝑒) ∧ 𝐢 β‰  𝑒))
9592, 94r19.29a 3163 . . 3 (((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) ∧ 𝐴 β‰  𝐢) β†’ (𝐡 βˆ’ 𝐷) = (𝐹 βˆ’ 𝐻))
9647, 95pm2.61dane 3030 . 2 ((πœ‘ ∧ 2 ≀ (β™―β€˜π‘ƒ)) β†’ (𝐡 βˆ’ 𝐷) = (𝐹 βˆ’ 𝐻))
971, 36tgldimor 27753 . 2 (πœ‘ β†’ ((β™―β€˜π‘ƒ) = 1 ∨ 2 ≀ (β™―β€˜π‘ƒ)))
9815, 96, 97mpjaodan 958 1 (πœ‘ β†’ (𝐡 βˆ’ 𝐷) = (𝐹 βˆ’ 𝐻))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107   β‰  wne 2941   class class class wbr 5149  β€˜cfv 6544  (class class class)co 7409  1c1 11111   ≀ cle 11249  2c2 12267  β™―chash 14290  Basecbs 17144  distcds 17206  TarskiGcstrkg 27678  Itvcitv 27684
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-oadd 8470  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-dju 9896  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-2 12275  df-n0 12473  df-xnn0 12545  df-z 12559  df-uz 12823  df-fz 13485  df-hash 14291  df-trkgc 27699  df-trkgb 27700  df-trkgcb 27701  df-trkg 27704
This theorem is referenced by:  tgcgrsub  27760  tgbtwnxfr  27781  tgfscgr  27819  tgbtwnconn1lem3  27825  miriso  27921  krippenlem  27941  midexlem  27943  colperpexlem1  27981  opphllem  27986
  Copyright terms: Public domain W3C validator